Whole-space heat gain of every order

The whole-space form of lem:local-heat-gain, for every order m ≥ 1, as used in prop:lps-smoothing. Let a < a + σ < a + β. If z ∈ L²((a, a + β); H^m(ℝ³)) solves ∂ₜ z - Δ z = G in distributions on ℝ³ × (a, a + β) with G ∈ L²((a, a + β); H^{m-1}(ℝ³)), then z ∈ C([a + σ, a + β]; H^m(ℝ³)) ∩ L²((a + σ, a + β); H^{m+1}(ℝ³)) with ‖z‖_{C H^m} + ‖z‖_{L² H^{m+1}} ≤ C (‖z‖_{L² H^m} + ‖G‖_{L² H^{m-1}}), where C depends only on m, σ and β.

The proof multiplies by a time cutoff c(t) vanishing for t ≤ a + σ/2 and equal to one for t ≥ a + σ. Each spatial derivative ∂^γ (c z), |γ| ≤ m, solves the heat equation on ℝ³ × (a, a + β) with a square-integrable source in source or divergence form built from c ∂^γ G + c' ∂^γ z, and has zero initial trace, so the energy estimate of lem:localized-vorticity-energy applies.

theorem ESS.lps_wholeHeatGain (m : ℕ) (hm : 1 ≤ m) {σ β : ℝ} (hσ : 0 < σ) (hσβ : σ < β) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (a : ℝ) (z G : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (Dz DG : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), CKN.IsL2SobolevFamilyOn m Set.univ (Set.Ioo a (a + β)) z Dz → CKN.IsL2SobolevFamilyOn (m - 1) Set.univ (Set.Ioo a (a + β)) G DG → CKN.IsHeatSolutionOn Set.univ (Set.Ioo a (a + β)) z G → ∃ (Z : ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ) (Dz' : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), (∀ t ∈ Set.Icc (a + σ) (a + β), CKN.IsSobolevFamilyOn m Set.univ (Z t []) (Z t)) ∧ (∀ (α : List (Fin 3)), α.length ≤ m → ∀ t ∈ Set.Icc (a + σ) (a + β), Filter.Tendsto (fun (t' : ℝ) => MeasureTheory.eLpNorm (Z t' α - Z t α) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc (a + σ) (a + β))) (nhds 0)) ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (a + σ) (a + β)), Z t [] =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => z (x, t)) ∧ CKN.IsL2SobolevFamilyOn (m + 1) Set.univ (Set.Ioo (a + σ) (a + β)) z Dz' ∧ (∀ (α : List (Fin 3)), α.length ≤ m → ∀ᵐ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo (a + σ) (a + β)), Dz' α p = Dz α p) ∧ ∀ t ∈ Set.Icc (a + σ) (a + β), √(CKN.sobolevNormSqOn m Set.univ (Z t)) + √(CKN.l2SobolevNormSqOn (m + 1) Set.univ (Set.Ioo (a + σ) (a + β)) Dz') ≤ C * (√(CKN.l2SobolevNormSqOn m Set.univ (Set.Ioo a (a + β)) Dz) + √(CKN.l2SobolevNormSqOn (m - 1) Set.univ (Set.Ioo a (a + β)) DG))

lem:local-heat-gain on the whole space and for every order m ≥ 1 (prop:lps-smoothing). The family Dz' of the gained regularity agrees with the given family Dz through order m.