The induction step of the regularity ladder #
prop:lps-smoothing: from the regularity H^M (M ≥ 2) on [t₀ + δ/2, T] to the regularity
H^{M+1} on [t₀ + δ, T]. The convection field is a product of L²(I; H^M) families with a
uniformly bounded factor, hence an L²(I; H^M) family, and the heat gain applies.
theorem
ESS.lps_ladder_step
{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 : 2 ≤ M)
{δ : ℝ}
(hδ : 0 < δ)
(hδT : t₀ + δ < T)
(hlad :
∃ (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₀ + δ / 2) T, CKN.IsSobolevFamilyOn M Set.univ (Z i t []) (Z i t)) ∧ (∀ (i : Fin 3) (α : List (Fin 3)),
α.length ≤ M →
∀ t ∈ Set.Icc (t₀ + δ / 2) T,
Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (Z i s α - Z i t α) 2 MeasureTheory.volume)
(nhdsWithin t (Set.Icc (t₀ + δ / 2) T)) (nhds 0)) ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (t₀ + δ / 2) 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₀ + δ / 2) 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₀ + δ / 2) 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₀ + δ / 2) T))]
fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => D2u z i k k)
:
∃ (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 + 1) Set.univ (Z i t []) (Z i t)) ∧ (∀ (i : Fin 3) (α : List (Fin 3)),
α.length ≤ M + 1 →
∀ 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 + 1 →
Z i t α =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => DD i α (x, t)) ∧ (∀ (i : Fin 3),
CKN.IsL2SobolevFamilyOn (M + 1 + 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 induction step of the regularity ladder for M ≥ 2 (prop:lps-smoothing).