The regularity gain step of the ladder #
prop:lps-smoothing: if the components of a strong solution form an L²(I; H^{M+1}) family on
(t₀ + δ/2, T) and the convection field has an L²(I; H^M) family there, then the source
∂ₜu - Δu has an L²(I; H^M) family and the whole-space heat gain produces continuous slices
of order M + 1 and an L²(I; H^{M+2}) family on (t₀ + δ, T).
theorem
ESS.lps_ladder_gain
{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)
(DD : Fin 3 → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(hDD :
∀ (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))
(hDD1 :
∀ (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)
(hDD2 :
∀ (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)
(DB : Fin 3 → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(hB :
∀ (i : Fin 3),
CKN.IsL2SobolevFamilyOn M Set.univ (Set.Ioo (t₀ + δ / 2) T)
(fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ∑ j : Fin 3, u z j * Du z i j) (DB i))
:
∃ (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 heat-gain step of the regularity ladder (prop:lps-smoothing).