Mollifier radii and almost-everywhere convergence

The approximate-identity sequence underlying the paper's mollification input (ext:mollify) is indexed by the outer radius sliceRadius n = 1 / (n + 1), which decreases to zero as n grows. The normalized kernel produced by standardMollifier has inner radius equal to half its outer radius, so the ratio of the two radii is bounded by the constant 2. Mathlib's almost-everywhere convergence theorem for mollifications of a locally integrable function therefore applies: for any g, the functions mollify g (sliceRadius n) _ converge to g almost everywhere.

noncomputable def CKN.sliceRadius (n : ℕ) : ℝ

The outer radius of the n-th mollifier in the approximate-identity sequence.

Equations

• CKN.sliceRadius n = 1 / (↑n + 1)

theorem CKN.sliceRadius_pos (n : ℕ) : 0 < sliceRadius n

theorem CKN.tendsto_sliceRadius_atTop : Filter.Tendsto sliceRadius Filter.atTop (nhds 0)

theorem CKN.ae_tendsto_mollify_sliceRadius {d : ℕ} {g : Vec d → ℝ} (hg : MeasureTheory.LocallyIntegrable g MeasureTheory.volume) : ∀ᵐ (x : Vec d), Filter.Tendsto (fun (n : ℕ) => mollify g (sliceRadius n) ⋯ x) Filter.atTop (nhds (g x))