The mollified initial data converge in L²

The profile of eq:reg-mollifier is a nonnegative, normalized kernel supported in the unit ball, so its dilates form an approximate identity in L². This is the convergence J_ε a → a used in the proof of prop:leray-hopf-limit: it is first checked on continuous compactly supported fields by uniform continuity, and then extended by density and the L² contraction of the mollifier.

theorem CKN.Leray.lerayHopfLimit_regMollifyVector_eq_convolution (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (f : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3) : regMollifyVector ρ ε hε f = MeasureTheory.convolution (regMollifierKernel ρ ε hε) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

The vector mollifier is the convolution with the dilated kernel acting by scalar multiplication.

theorem CKN.Leray.lerayHopfLimit_regMollifyVector_tendsto_of_compact (ρ : RegMollifierProfile) {g : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3} (hg : Continuous g) (hgc : HasCompactSupport g) (εs : ℕ → ℝ) (hpos : ∀ (n : ℕ), 0 < εs n) (hlim : Filter.Tendsto εs Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (regMollifyVector ρ (εs n) ⋯ g - g) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

The mollifier converges in L² on continuous compactly supported fields.

theorem CKN.Leray.lerayHopfLimit_regMollifyVector_tendsto (ρ : RegMollifierProfile) {f : Foundation.Parabolic.L2Vec3 → Foundation.Parabolic.L2Vec3} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (εs : ℕ → ℝ) (hpos : ∀ (n : ℕ), 0 < εs n) (hlim : Filter.Tendsto εs Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (regMollifyVector ρ (εs n) ⋯ f - f) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

The mollifier converges in L² on every L² field.

theorem CKN.Leray.lerayHopfLimit_mollifiedInitial_pairing_tendsto (ρ : RegMollifierProfile) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (εs : ℕ → ℝ) (hpos : ∀ (n : ℕ), 0 < εs n) (hlim : Filter.Tendsto εs Filter.atTop (nhds 0)) (w : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hw : MeasureTheory.MemLp w 2 MeasureTheory.volume) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, regUniformMollifiedInitial ρ (εs n) ⋯ a x i * w x i) Filter.atTop (nhds (∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, a x i * w x i))

The mollified initial fields converge weakly in L²: their pairings with every L² field converge.