The continuous L² curve of a weak heat solution

The mollified primitives Wₙ(t) are continuous curves in L²(ℝ³) on [a, τ]. The Cauchy estimate makes them uniformly Cauchy, so they converge uniformly to a continuous curve Z (lem:localized-vorticity-energy).

theorem ESS.vl_sq_setIntegral_le {u v : ℝ} (huv : u ≤ v) {g : ℝ → ℝ} (hg : MeasureTheory.IntegrableOn g (Set.Ioo u v) MeasureTheory.volume) (hg2 : MeasureTheory.IntegrableOn (fun (s : ℝ) => g s ^ 2) (Set.Ioo u v) MeasureTheory.volume) : (∫ (s : ℝ) in Set.Ioo u v, g s) ^ 2 ≤ (v - u) * ∫ (s : ℝ) in Set.Ioo u v, g s ^ 2

Cauchy–Schwarz on a bounded interval.

noncomputable def ESS.vlCurve {a τ : ℝ} {w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ} (sol : CKN.VlHeatSolution a τ w H f w₀) (n : ℕ) (t : ↑(Set.Icc a τ)) : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)

The mollified primitive as an L² curve on [a, τ].

Equations

• ESS.vlCurve sol n t = MeasureTheory.MemLp.toLp (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.vlPrim a (CKN.vlMoll n) w₀ w H f x ↑t) ⋯

theorem ESS.vlCurve_norm_sq {a τ : ℝ} {w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ} (sol : CKN.VlHeatSolution a τ w H f w₀) (n : ℕ) (t : ↑(Set.Icc a τ)) : ‖vlCurve sol n t‖ ^ 2 = ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlPrim a (CKN.vlMoll n) w₀ w H f x ↑t ^ 2

theorem ESS.vlCurve_sub_norm_sq {a τ : ℝ} {w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ} (sol : CKN.VlHeatSolution a τ w H f w₀) (n m : ℕ) (t : ↑(Set.Icc a τ)) : ‖vlCurve sol n t - vlCurve sol m t‖ ^ 2 = ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlPrim a (CKN.vlMoll n - CKN.vlMoll m) w₀ w H f x ↑t ^ 2

The difference of two curves at a time, squared.

theorem ESS.vlCurve_dist_sq_le {a τ : ℝ} {w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ} (sol : CKN.VlHeatSolution a τ w H f w₀) (n m : ℕ) (t : ↑(Set.Icc a τ)) : ‖vlCurve sol n t - vlCurve sol m t‖ ^ 2 ≤ 2 * vlErr w₀ w H f a τ n + 2 * vlErr w₀ w H f a τ m

The uniform Cauchy estimate.

theorem ESS.vlCurve_dist_sq_le_time {a τ : ℝ} {w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ} (sol : CKN.VlHeatSolution a τ w H f w₀) (n : ℕ) {t t' : ↑(Set.Icc a τ)} (htt : ↑t' ≤ ↑t) : ‖vlCurve sol n t - vlCurve sol n t'‖ ^ 2 ≤ (↑t - ↑t') * ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a τ, CKN.vlSource (CKN.vlMoll n) w H f p.1 p.2 ^ 2

Each mollified curve is Hölder continuous in time.

theorem ESS.vlCurve_continuous {a τ : ℝ} {w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ} (sol : CKN.VlHeatSolution a τ w H f w₀) (n : ℕ) : Continuous (vlCurve sol n)

theorem ESS.vlCurve_uniformCauchy {a τ : ℝ} {w f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ} (sol : CKN.VlHeatSolution a τ w H f w₀) : UniformCauchySeqOn (fun (n : ℕ) => vlCurve sol n) Filter.atTop Set.univ

The mollified curves converge uniformly on [a, τ].