English
If g is locally integrable and is close to g(x0) within ball φ.rOut for all x, then the distance between convolution φ.normed μ ⋆ g and g at x0 is bounded by ε.
Русский
Локальная интегрируемость и близость к g(x0) внутри ball гарантирует ограничение по расстоянию конволюции и g.
LaTeX
$$$\\text{AEStronglyMeasurable } g μ \\to \\; dist((φ.normed μ ⋆ g)(x_0), g(x_0)) \\le ε$ при условии, что ∀ x ∈ ball x0 φ.rOut, dist(g(x), g(x0)) ≤ ε$$
Lean4
/-- Special case of `ContDiffBump.convolution_tendsto_right` where `g` is continuous,
and the limit is taken only in the first function. -/
theorem convolution_tendsto_right_of_continuous {ι} {φ : ι → ContDiffBump (0 : G)} {l : Filter ι}
(hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)) (hg : Continuous g) (x₀ : G) :
Tendsto (fun i => ((φ i).normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀) l (𝓝 (g x₀)) :=
convolution_tendsto_right hφ (Eventually.of_forall fun _ => hg.aestronglyMeasurable)
((hg.tendsto x₀).comp tendsto_snd) tendsto_const_nhds
