Mollifier limits for the local energy inequality

Along the mollification radii 1/(n+1), mollifications of square-integrable functions converge in L², are bounded by the original L² norm, and commute with weak derivatives; L² convergence is preserved by multiplication with bounded continuous functions and by sums. These are the static limits of the local energy inequality eq:reg-local-energy-forced.

noncomputable def CKN.Leray.leRadius (n : ℕ) : ℝ

The mollification radii.

Equations

• CKN.Leray.leRadius n = 1 / (↑n + 1)

theorem CKN.Leray.leRadius_pos (n : ℕ) : 0 < leRadius n

theorem CKN.Leray.tendsto_leRadius : Filter.Tendsto leRadius Filter.atTop (nhds 0)

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

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

Equations

• CKN.Leray.leMol n = CKN.mollifier (CKN.Leray.leRadius n) ⋯

theorem CKN.Leray.leMol_contDiff (n : ℕ) : ContDiff ℝ (↑⊤) (leMol n)

theorem CKN.Leray.leMol_hasCompactSupport (n : ℕ) : HasCompactSupport (leMol n)

theorem CKN.Leray.tendsto_leConv_leMol {g : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (leConv (leMol n) g - g) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

theorem CKN.Leray.memLp_leConv_leMol {g : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (n : ℕ) : MeasureTheory.MemLp (leConv (leMol n) g) 2 MeasureTheory.volume

theorem CKN.Leray.eLpNorm_leConv_leMol_le {g : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (n : ℕ) : MeasureTheory.eLpNorm (leConv (leMol n) g) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm g 2 MeasureTheory.volume

theorem CKN.Leray.leConv_spatialDeriv_leMol {u g : Foundation.Parabolic.Vec3 → ℝ} (hu : MeasureTheory.MemLp u 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) {j : Fin 3} (hweak : HasWeakPartialDerivOn Set.univ j u g) (n : ℕ) (x : Foundation.Parabolic.Vec3) : leConv (spatialDeriv (leMol n) j) u x = leConv (leMol n) g x

Mollification commutes with a weak partial derivative.

theorem CKN.Leray.tendsto_eLpNorm_mul_bounded {X : ℕ → Foundation.Parabolic.Vec3 → ℝ} {X0 h : Foundation.Parabolic.Vec3 → ℝ} (hX : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (X n - X0) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) (hm : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (X n - X0) MeasureTheory.volume) (hh : MeasureTheory.AEStronglyMeasurable h MeasureTheory.volume) {M : ℝ} (hM : ∀ (x : Foundation.Parabolic.Vec3), ‖h x‖ ≤ M) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm ((fun (x : Foundation.Parabolic.Vec3) => X n x * h x) - fun (x : Foundation.Parabolic.Vec3) => X0 x * h x) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

L² convergence is preserved by multiplication with a bounded function.

theorem CKN.Leray.tendsto_eLpNorm_add {X Y : ℕ → Foundation.Parabolic.Vec3 → ℝ} {X0 Y0 : Foundation.Parabolic.Vec3 → ℝ} (hX : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (X n - X0) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) (hY : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (Y n - Y0) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (X n + Y n - (X0 + Y0)) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

L² convergence is preserved by sums.

theorem CKN.Leray.memLp_mul_bounded {g h : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (hh : MeasureTheory.AEStronglyMeasurable h MeasureTheory.volume) {M : ℝ} (hM : ∀ (x : Foundation.Parabolic.Vec3), ‖h x‖ ≤ M) : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => g x * h x) 2 MeasureTheory.volume

theorem CKN.Leray.tendsto_integral_leConv_mul {A : Foundation.Parabolic.Vec3 → ℝ} (hA : MeasureTheory.MemLp A 2 MeasureTheory.volume) {Y : ℕ → Foundation.Parabolic.Vec3 → ℝ} {Y0 : Foundation.Parabolic.Vec3 → ℝ} (hY : ∀ (n : ℕ), MeasureTheory.MemLp (Y n) 2 MeasureTheory.volume) (hY0 : MeasureTheory.MemLp Y0 2 MeasureTheory.volume) (hYc : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (Y n - Y0) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : Foundation.Parabolic.Vec3), leConv (leMol n) A x * Y n x) Filter.atTop (nhds (∫ (x : Foundation.Parabolic.Vec3), A x * Y0 x))

The limit of a pairing of a mollification with a mollified product.

theorem CKN.Leray.tendsto_mollified_productDeriv {uk Dj : Foundation.Parabolic.Vec3 → ℝ} (hu : MeasureTheory.MemLp uk 2 MeasureTheory.volume) (hD : MeasureTheory.MemLp Dj 2 MeasureTheory.volume) {j : Fin 3} (hweak : HasWeakPartialDerivOn Set.univ j uk Dj) {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm ((fun (x : Foundation.Parabolic.Vec3) => leConv (spatialDeriv (leMol n) j) uk x * ψ x + leConv (leMol n) uk x * (fderiv ℝ ψ x) (basisVec j)) - fun (x : Foundation.Parabolic.Vec3) => Dj x * ψ x + uk x * (fderiv ℝ ψ x) (basisVec j)) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

The mollified product derivative converges to the weak product derivative.