Mollifier limits for the localized vorticity energy

The standard mollifiers ρₙ of radius 1/(n+1) are smooth compact kernels of unit L¹ norm. For a square-integrable spatial field h, ∫ (ρₙ ⋆ h - h)² → 0. For a square-integrable field on the slab, the time-integrated version holds by dominated convergence (lem:localized-vorticity-energy of the Escauriaza–Seregin–Šverák manuscript).

theorem CKN.vl_integral_sq_eq {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {g : α → ℝ} (hg : MeasureTheory.MemLp g 2 μ) : ∫ (x : α), g x ^ 2 ∂μ = (MeasureTheory.eLpNorm g 2 μ).toReal ^ 2

The squared L² integral is the square of the L² seminorm.

theorem CKN.vl_norm_toLp_sq {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {g : α → ℝ} (hg : MeasureTheory.MemLp g 2 μ) : ‖MeasureTheory.MemLp.toLp g hg‖ ^ 2 = ∫ (x : α), g x ^ 2 ∂μ

The L² norm of a representative, squared.

noncomputable def CKN.vlMoll (n : ℕ) : Foundation.Parabolic.Vec3 → ℝ

The mollifier of radius 1 / (n + 1).

Equations

• CKN.vlMoll n = CKN.mollifier (1 / (↑n + 1)) ⋯

theorem CKN.vlMoll_kernel (n : ℕ) : IsVlKernel (vlMoll n)

theorem CKN.vlMoll_abs_integral (n : ℕ) : ∫ (y : Foundation.Parabolic.Vec3), |vlMoll n y| = 1

theorem CKN.vlMoll_sq_le (n : ℕ) {h : Foundation.Parabolic.Vec3 → ℝ} (hh : MeasureTheory.MemLp h 2 MeasureTheory.volume) : ∫ (x : Foundation.Parabolic.Vec3), vlConv (vlMoll n) h x ^ 2 ≤ ∫ (x : Foundation.Parabolic.Vec3), h x ^ 2

theorem CKN.vlMoll_tendsto {h : Foundation.Parabolic.Vec3 → ℝ} (hh : MeasureTheory.MemLp h 2 MeasureTheory.volume) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : Foundation.Parabolic.Vec3), (vlConv (vlMoll n) h x - h x) ^ 2) Filter.atTop (nhds 0)

theorem CKN.vlMoll_slab_tendsto {a τ : ℝ} {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hgm : MeasureTheory.StronglyMeasurable g) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (vlSlab a τ))) : Filter.Tendsto (fun (n : ℕ) => ∫ (s : ℝ) in Set.Ioo a τ, ∫ (x : Foundation.Parabolic.Vec3), (vlConvT (vlMoll n) g x s - g (x, s)) ^ 2) Filter.atTop (nhds 0)

The time-integrated mollifier limit on a slab.

theorem CKN.vlMoll_sub_sq_le (n m : ℕ) {h : Foundation.Parabolic.Vec3 → ℝ} (hh : MeasureTheory.MemLp h 2 MeasureTheory.volume) : ∫ (x : Foundation.Parabolic.Vec3), vlConv (vlMoll n - vlMoll m) h x ^ 2 ≤ (2 * ∫ (x : Foundation.Parabolic.Vec3), (vlConv (vlMoll n) h x - h x) ^ 2) + 2 * ∫ (x : Foundation.Parabolic.Vec3), (vlConv (vlMoll m) h x - h x) ^ 2

A difference of two mollifications is controlled by the two mollifier errors.

noncomputable def CKN.vlMollErr (n : ℕ) (g : Foundation.Parabolic.Vec3 × ℝ → ℝ) (s : ℝ) : ℝ

The slice mollifier error of a slab field.

Equations

• CKN.vlMollErr n g s = ∫ (x : CKN.Foundation.Parabolic.Vec3), (CKN.vlConvT (CKN.vlMoll n) g x s - g (x, s)) ^ 2

theorem CKN.vlMollErr_integrableOn {a τ : ℝ} (n : ℕ) {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hgm : MeasureTheory.StronglyMeasurable g) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (vlSlab a τ))) : MeasureTheory.IntegrableOn (fun (s : ℝ) => vlMollErr n g s) (Set.Ioo a τ) MeasureTheory.volume