Documentation

LeanPool.EscauriazaSereginSverak.LPS.SmoothingAssembly

Assembly of the smoothing of strong solutions #

prop:lps-smoothing: the regularity ladder of a strong solution on a positive-time slab, together with the projected equation and the time continuity of the strong class, feeds the time chain and the joint smoothness step.

source
theorem ESS.lps_ae_slices_univ {a b : ℝ} {f g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : f =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b))] g) :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, t)) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, t)

Almost every time slice of an almost everywhere identity on a slab is an almost everywhere identity on ℝ³ (prop:lps-smoothing).

source
theorem ESS.lps_smoothing_data_of_ladder {t₀ t₁ δ : ℝ} (hδ : 0 < δ) (hδT : 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} (h : 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₁)))) (hlad : ∀ (M : ℕ), 1 ≤ M → ∃ (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) :
∃ (Z : ℕ → Fin 3 → ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ), (∀ (i : Fin 3) (j : ℕ), ∀ t ∈ Set.Icc (t₀ + δ) t₁, ∀ (m : ℕ), CKN.IsSobolevFamilyOn m Set.univ (Z j i t []) (Z j i t)) ∧ (∀ (i : Fin 3) (j : ℕ) (α : List (Fin 3)), ∀ t ∈ Set.Icc (t₀ + δ) t₁, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (Z j i s α - Z j i t α) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc (t₀ + δ) t₁)) (nhds 0)) ∧ (∀ (i : Fin 3) (j : ℕ) (α : List (Fin 3)) (ψ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∀ t ∈ Set.Icc (t₀ + δ) t₁, HasDerivWithinAt (fun (s : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), Z j i s α x * ψ x) (∫ (x : CKN.Foundation.Parabolic.Vec3), Z (j + 1) i t α x * ψ x) (Set.Icc (t₀ + δ) t₁) t) ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (t₀ + δ) t₁), ∀ (i : Fin 3), Z 0 i t [] =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, t) i

The data of lps_smoothing_of_curves on a positive-time slab, from the regularity ladder of all orders (prop:lps-smoothing).

source
theorem ESS.lps_smoothing_of_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} (h : 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₁)))) (hlad : ∀ (M : ℕ), 1 ≤ M → ∀ (δ : ℝ), 0 < δ → 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) :
∃ (R : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), R =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))] U ∧ ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => R z) (Set.univ ×ˢ Set.Ioc t₀ t₁)

prop:lps-smoothing, given the regularity ladder: a strong solution on [t₀, t₁] has a representative that is C^∞ on ℝ³ × (t₀, t₁].