Patching the jointly smooth representatives over positive-time slabs #
lem:lps-Bochner-joint-smooth: representatives built on the slabs
ℝ³ × [t₀ + δ, t₁] that agree almost everywhere with the same field agree
everywhere on the common slab.
theorem
ESS.lps_eqOn_slab_of_slices_ae
{a b : ℝ}
(hab : a < b)
{R R' : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3}
(hR : ContinuousOn R (Set.univ ×ˢ Set.Icc a b))
(hR' : ContinuousOn R' (Set.univ ×ˢ Set.Icc a b))
(h :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), (fun (x : CKN.Foundation.Parabolic.Vec3) => R (x, t)) =ᵐ[MeasureTheory.volume]
fun (x : CKN.Foundation.Parabolic.Vec3) => R' (x, t))
:
Two vector fields continuous on a slab whose slices agree almost everywhere for almost every time agree everywhere on the slab.
theorem
ESS.lps_slab_rep_of_data
{t₀ t₁ : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{δ : ℝ}
(hδ1 : t₀ + δ < t₁)
(Z : ℕ → Fin 3 → ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ)
(hfam :
∀ (i : Fin 3) (j : ℕ), ∀ t ∈ Set.Icc (t₀ + δ) t₁, ∀ (m : ℕ), CKN.IsSobolevFamilyOn m Set.univ (Z j i t []) (Z j i t))
(hcont :
∀ (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))
(hderiv :
∀ (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)
(hae :
∀ᵐ (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)
:
∃ (R : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3),
ContDiffOn ℝ (↑⊤) R (Set.univ ×ˢ Set.Icc (t₀ + δ) t₁) ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (t₀ + δ) t₁), (fun (x : CKN.Foundation.Parabolic.Vec3) => R (x, t)) =ᵐ[MeasureTheory.volume]
fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)
The slab representatives of the strong solution, one for each positive-time slab
(lem:lps-Bochner-joint-smooth).
theorem
ESS.lps_smoothing_of_curves
{t₀ t₁ : ℝ}
(hab : t₀ < t₁)
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hu :
∀ (i : Fin 3),
MeasureTheory.AEStronglyMeasurable (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => u z i)
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))))
(hData :
∀ (δ : ℝ),
0 < δ →
t₀ + δ < t₁ →
∃ (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)
:
∃ (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₁)
Joint smoothness of the strong solution from all-order slice curves on each positive-time
slab (prop:lps-smoothing, lem:lps-Bochner-joint-smooth).