Weak continuity and initial trace of the heat orbit

The Gaussian kernel is even, so the pairing of the heat orbit of an L² datum with an integrable test field equals the pairing of the datum with the heat orbit of the test field. For a smooth compactly supported test field the latter heat orbit is continuous in time, converges to the test field as time decreases to zero, and has a cubic spatial tail uniformly in time, so dominated convergence gives the weak continuity and the initial trace of the heat orbit required in prop:pv-local-solution.

theorem ESS.integral_heatConv_mul_eq {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) {t : ℝ} (ht : 0 < t) : ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Heat.heatConv t f x * g x = ∫ (y : CKN.Foundation.Parabolic.Vec3), f y * CKN.Foundation.Heat.heatConv t g y

The Gaussian convolution is symmetric: pairing the heat orbit of an L² datum with an integrable function equals pairing the datum with the heat orbit of that function.

theorem ESS.integral_mul_heatConv_continuous_tendsto {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) : ContinuousOn (fun (t : ℝ) => ∫ (y : CKN.Foundation.Parabolic.Vec3), f y * CKN.Foundation.Heat.heatConv t g y) (Set.Ioi 0) ∧ Filter.Tendsto (fun (t : ℝ) => ∫ (y : CKN.Foundation.Parabolic.Vec3), f y * CKN.Foundation.Heat.heatConv t g y) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (y : CKN.Foundation.Parabolic.Vec3), f y * g y))

The pairing of the datum with the heat orbit of a smooth compactly supported test function is continuous in positive time and converges to the pairing with the test function as time decreases to zero.

theorem ESS.heatOrbit_weak_continuity_initial {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (ha : CKN.IsInJ a) (τ : ℝ) {ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ContinuousOn (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, heatOrbit a (x, t) i * ψ x i) (Set.Ioc 0 τ) ∧ Filter.Tendsto (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, heatOrbit a (x, t) i * ψ x i) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, a x i * ψ x i))

(h7) The heat orbit of a datum in J is weakly continuous on (0, τ] and attains the datum weakly as time decreases to zero.