The Cauchy estimate for mollified weak heat solutions

The time primitive is linear in the kernel. Applied to the difference ρₙ - ρₘ of two mollifiers, the kernel energy inequality bounds, uniformly in t ∈ [a, τ], both ‖Wₙ(t) - Wₘ(t)‖² and the slab norm of the difference of the mollified gradients by twice the sum of the two mollifier errors, and these errors tend to zero (lem:localized-vorticity-energy).

theorem ESS.vlConvT_sub_kernel_ae {a τ : ℝ} {k l : CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : CKN.IsVlKernel k) (hl : CKN.IsVlKernel l) {g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hgm : MeasureTheory.StronglyMeasurable g) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (CKN.vlSlab a τ))) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a τ), ∀ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConvT (k - l) g x s = CKN.vlConvT k g x s - CKN.vlConvT l g x s

theorem ESS.vlSource_sub_kernel_ae {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₀) {k l : CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : CKN.IsVlKernel k) (hl : CKN.IsVlKernel l) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a τ), ∀ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlSource (k - l) w H f x s = CKN.vlSource k w H f x s - CKN.vlSource l w H f x s

theorem ESS.vlPrim_sub_kernel {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₀) {k l : CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : CKN.IsVlKernel k) (hl : CKN.IsVlKernel l) (x : CKN.Foundation.Parabolic.Vec3) {t : ℝ} (ht : t ∈ Set.Icc a τ) : CKN.vlPrim a (k - l) w₀ w H f x t = CKN.vlPrim a k w₀ w H f x t - CKN.vlPrim a l w₀ w H f x t

The time primitive is linear in the kernel.

noncomputable def ESS.vlErr (w₀ : CKN.Foundation.Parabolic.Vec3 → ℝ) (w : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (a τ : ℝ) (n : ℕ) : ℝ

The total mollifier error of the data.

Equations

• One or more equations did not get rendered due to their size.

theorem ESS.vlErr_tendsto {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₀) : Filter.Tendsto (fun (n : ℕ) => vlErr w₀ w H f a τ n) Filter.atTop (nhds 0)

theorem ESS.vlMoll_diff_rhs_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 : ℝ} (ht : t ∈ Set.Icc a τ) : (∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConv (CKN.vlMoll n - CKN.vlMoll m) w₀ x ^ 2) + ∫ (s : ℝ) in Set.Ioo a t, ((∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConvT (CKN.vlMoll n - CKN.vlMoll m) (H j) x s ^ 2) + ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConvT (CKN.vlMoll n - CKN.vlMoll m) w x s ^ 2) + ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConvT (CKN.vlMoll n - CKN.vlMoll m) f x s ^ 2 ≤ 2 * vlErr w₀ w H f a τ n + 2 * vlErr w₀ w H f a τ m

The kernel energy bound for a mollifier difference, in terms of the mollifier errors.