The regularity ladder of a strong solution

prop:lps-smoothing: a strong solution has, for every order M ≥ 1 and every δ > 0, an L²(t₀ + δ, T; H^{M+1}) family for each velocity component, whose spatial slices through order M are L²-continuous on [t₀ + δ, T] and represent the family for almost every time. The base of the induction is the H² bound of the slice equation; each step applies the whole-space heat gain to the convection source.

theorem ESS.lps_ladder_two {t₀ T : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsLpsStrongSolution t₀ T u Du p) (hderiv : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ T) u Du D2u Dtu) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (hDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (hD2u : MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (hDtu : MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) {δ : ℝ} (hδ : 0 < δ) (hδT : t₀ + δ < T) : ∃ (Z : Fin 3 → ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ) (DD : Fin 3 → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), (∀ (i : Fin 3), ∀ t ∈ Set.Icc (t₀ + δ) T, CKN.IsSobolevFamilyOn 2 Set.univ (Z i t []) (Z i t)) ∧ (∀ (i : Fin 3) (α : List (Fin 3)), α.length ≤ 2 → ∀ t ∈ Set.Icc (t₀ + δ) T, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (Z i s α - Z i t α) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc (t₀ + δ) T)) (nhds 0)) ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (t₀ + δ) T), ∀ (i : Fin 3) (α : List (Fin 3)), α.length ≤ 2 → Z i t α =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => DD i α (x, t)) ∧ (∀ (i : Fin 3), CKN.IsL2SobolevFamilyOn 3 Set.univ (Set.Ioo (t₀ + δ) T) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z i) (DD i)) ∧ (∀ (i k : Fin 3), DD i [k] =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo (t₀ + δ) T))] fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => Du z i k) ∧ ∀ (i k : Fin 3), DD i [k, k] =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo (t₀ + δ) T))] fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => D2u z i k k

The ladder at order two (prop:lps-smoothing).

theorem ESS.lps_ladder {t₀ T : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsLpsStrongSolution t₀ T u Du p) (hderiv : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ T) u Du D2u Dtu) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (hDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (hD2u : MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (hDtu : MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T)))) (M : ℕ) (hM : 1 ≤ M) {δ : ℝ} (hδ : 0 < δ) (hδT : t₀ + δ < T) : ∃ (Z : Fin 3 → ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ) (DD : Fin 3 → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), (∀ (i : Fin 3), ∀ t ∈ Set.Icc (t₀ + δ) T, CKN.IsSobolevFamilyOn M Set.univ (Z i t []) (Z i t)) ∧ (∀ (i : Fin 3) (α : List (Fin 3)), α.length ≤ M → ∀ t ∈ Set.Icc (t₀ + δ) T, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (Z i s α - Z i t α) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc (t₀ + δ) T)) (nhds 0)) ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (t₀ + δ) T), ∀ (i : Fin 3) (α : List (Fin 3)), α.length ≤ M → Z i t α =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => DD i α (x, t)) ∧ (∀ (i : Fin 3), CKN.IsL2SobolevFamilyOn (M + 1) Set.univ (Set.Ioo (t₀ + δ) T) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z i) (DD i)) ∧ (∀ (i k : Fin 3), DD i [k] =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo (t₀ + δ) T))] fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => Du z i k) ∧ ∀ (i k : Fin 3), DD i [k, k] =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo (t₀ + δ) T))] fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => D2u z i k k

The regularity ladder of a strong solution (prop:lps-smoothing): for every M ≥ 1 and δ > 0, each velocity component has an L²(t₀ + δ, T; H^{M+1}) family, agreeing with the given first and second derivatives, whose slices through order M are L²-continuous on [t₀ + δ, T] and represent the family for almost every time.