ContDiffBump mollification

Adapted from PDEFoundation (EllipticRegularity, 2026) with the author's permission. The custom convex-approximation chain was not used here: Mathlib v4.34 already provides normalized ContDiffBump kernels, convolution regularity, and approximate-identity convergence. This direct port keeps the kernel and convolution API independent of the sibling geometry layer.

noncomputable def CKN.standardMollifier {d : ℕ} (ε : ℝ) (hε : 0 < ε) : ContDiffBump 0

A smooth bump centered at zero with outer radius ε.

Equations

• CKN.standardMollifier ε hε = { rIn := ε / 2, rOut := ε, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

noncomputable def CKN.mollifier {d : ℕ} (ε : ℝ) (hε : 0 < ε) : Vec d → ℝ

The normalized scalar kernel associated with standardMollifier.

Equations

• CKN.mollifier ε hε = (CKN.standardMollifier ε hε).normed MeasureTheory.volume

theorem CKN.mollifier_nonneg {d : ℕ} {ε : ℝ} (hε : 0 < ε) (x : Vec d) : 0 ≤ mollifier ε hε x

theorem CKN.mollifier_integral_one {d : ℕ} {ε : ℝ} (hε : 0 < ε) : ∫ (x : Vec d), mollifier ε hε x = 1

theorem CKN.mollifier_hasCompactSupport {d : ℕ} {ε : ℝ} (hε : 0 < ε) : HasCompactSupport (mollifier ε hε)

theorem CKN.mollifier_contDiff {d : ℕ} {ε : ℝ} (hε : 0 < ε) {n : ℕ∞} : ContDiff ℝ (↑n) (mollifier ε hε)

theorem CKN.mollifier_locallyIntegrable {d : ℕ} {ε : ℝ} (hε : 0 < ε) : MeasureTheory.LocallyIntegrable (mollifier ε hε) MeasureTheory.volume

noncomputable def CKN.mollify {d : ℕ} (u : Vec d → ℝ) (ε : ℝ) (hε : 0 < ε) : Vec d → ℝ

Convolution of u with the normalized radius-ε kernel.

Equations

• CKN.mollify u ε hε = MeasureTheory.convolution (CKN.mollifier ε hε) u (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

theorem CKN.mollify_contDiff {d : ℕ} {u : Vec d → ℝ} {ε : ℝ} (hε : 0 < ε) {n : ℕ∞} (hu : MeasureTheory.LocallyIntegrable u MeasureTheory.volume) : ContDiff ℝ (↑n) (mollify u ε hε)

theorem CKN.mollify_continuous {d : ℕ} {u : Vec d → ℝ} {ε : ℝ} (hε : 0 < ε) (hu : MeasureTheory.LocallyIntegrable u MeasureTheory.volume) : Continuous (mollify u ε hε)

theorem CKN.mollify_tendsto_of_continuous {ι : Type u_1} {l : Filter ι} {d : ℕ} {u : Vec d → ℝ} {ε : ι → ℝ} (hε : Filter.Tendsto ε l (nhds 0)) (hε_pos : ∀ (i : ι), 0 < ε i) (hu : Continuous u) (x : Vec d) : Filter.Tendsto (fun (i : ι) => mollify u (ε i) ⋯ x) l (nhds (u x))