Product integrability for heat subordination

The heat subordination representation of the Newtonian kernel and of its first spatial derivative integrates a Gaussian family over positive times. The two lemmas here supply the product integrability on (0, ∞) × ℝ³ that licenses the Fubini exchange, for data that is smooth with compact support.

theorem CKN.heat_kernel_mul_compact_integrable {g : Foundation.Parabolic.Vec3 → ℝ} {y : Foundation.Parabolic.Vec3} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) : MeasureTheory.Integrable (fun (p : ℝ × Foundation.Parabolic.Vec3) => Foundation.Heat.heatKernel (p.2 - y) p.1 * g p.2) ((MeasureTheory.volume.restrict (Set.Ioi 0)).prod MeasureTheory.volume)

A compactly supported bounded factor preserves integrability of the heat kernel on the positive-time half-space.

theorem CKN.heat_derivative_mul_compact_integrable {g : Foundation.Parabolic.Vec3 → ℝ} {y : Foundation.Parabolic.Vec3} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (i : Fin 3) : MeasureTheory.Integrable (fun (p : ℝ × Foundation.Parabolic.Vec3) => Foundation.Heat.heatKernelSpaceDerivative (p.2 - y) p.1 i * g p.2) ((MeasureTheory.volume.restrict (Set.Ioi 0)).prod MeasureTheory.volume)

The spatial derivative of the heat kernel has the same compact-support product integrability, with the sharp large-time majorant used by the heat subordination formula.