English
If a sequence of bump functions φi with radii shrinking to zero and g_i converges appropriately, then ((φi.normed μ) ⋆ g_i)(k_i) converges to z0 as i → l.
Русский
Пусть φi — набор бамп-функций, радиусы которых стремятся к нулю, и g_i сходится к z0; тогда конволюция сходится к z0.
LaTeX
$$$\\text{If } \\{φ_i\\}, \\{g_i\\}, \\{k_i\\} satisfy the hypotheses, then\\ (φ_i.normed μ ⋆ g_i)(k_i) \\to z_0$.$$
Lean4
/-- If `φ` is a normed bump function, approximate `(φ ⋆ g) x₀`
if `g` is near `g x₀` on a ball with radius `φ.rOut` around `x₀`. -/
theorem dist_normed_convolution_le {x₀ : G} {ε : ℝ} (hmg : AEStronglyMeasurable g μ)
(hg : ∀ x ∈ ball x₀ φ.rOut, dist (g x) (g x₀) ≤ ε) : dist ((φ.normed μ ⋆[lsmul ℝ ℝ, μ] g : G → E') x₀) (g x₀) ≤ ε :=
dist_convolution_le (by simp_rw [← dist_self (g x₀), hg x₀ (mem_ball_self φ.rOut_pos)]) φ.support_normed_eq.subset
φ.nonneg_normed φ.integral_normed hmg hg
