Time continuity of the forced heat response against a test field

For a tensor G ∈ L^{5/2} supported in ℝ³ × (0, τ) and a smooth compactly supported test field ψ, the pairing t ↦ ∫ Z(x, t) · ψ(x) dx of the forced heat response Z = forcedHeat G is defined for every t ∈ [0, τ], continuous there, and zero at t = 0 (prop:pv-local-solution).

For each t the triple integral of |ψ_i(x)| |∂_jΓ(x - y, t - s)| |G_ij(y, s)| is finite: the x-integral is at most C (t - s)^{-1/2} (1 + |y|)^{-3}, and Hölder's inequality with exponents 5/2 and 5/3 closes the bound. Fubini's theorem then writes the pairing as ∫ ∑ K_ij(y, t - s) G_ij(y, s), where K_ij = testKernelPairing ψ i j is bounded by C (1 + |y|)^{-3} uniformly in time and continuous away from t = s; dominated convergence gives continuity.

theorem ESS.instIsAddHaarMeasureProdVec3RealVolume_2 : MeasureTheory.volume.IsAddHaarMeasure

theorem ESS.forcedHeat_pairing_continuous {τ : ℝ} (hτ : 0 < τ) {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal (5 / 2)) MeasureTheory.volume) (hsupp : ∀ (i j : Fin 3), ∀ z ∉ CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), G i j z = 0) {ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : (∀ t ∈ Set.Icc 0 τ, MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ i : Fin 3, forcedHeat G (x, t) i * ψ x i) MeasureTheory.volume) ∧ ContinuousOn (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, forcedHeat G (x, t) i * ψ x i) (Set.Icc 0 τ) ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, forcedHeat G (x, 0) i * ψ x i = 0

Time continuity of the forced heat response against a fixed test field (prop:pv-local-solution): for a tensor G ∈ L^{5/2} supported in ℝ³ × (0, τ) and a smooth compactly supported test field ψ, the pairing ∫ Z(x, t) · ψ(x) dx of Z = forcedHeat G is defined for every t ∈ [0, τ], continuous on [0, τ], and zero at t = 0.