Localized Equation Duhamel Kernels

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.Core.Step3.duhamel_kernel_test_integrable_of_compact_support {k F : Foundation.Parabolic.ParabolicPoint → ℝ} {ζ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hk : MeasureTheory.LocallyIntegrable k MeasureTheory.volume) (hkm : Measurable k) (hζ : ContDiff ℝ (↑⊤) ζ) (hζc : HasCompactSupport ζ) (hF : MeasureTheory.Integrable F MeasureTheory.volume) (hFc : HasCompactSupport F) : MeasureTheory.Integrable (fun (q : Foundation.Parabolic.ParabolicPoint × Foundation.Parabolic.ParabolicPoint) => k (HeatPotential.pointSub q.1 q.2) * ζ q.1 * F q.2) (MeasureTheory.volume.prod MeasureTheory.volume)