English
A more general bound: the distance between f⋆g and the integral against z0 is bounded by (||L|| ∫ ||f||) ε.
Русский
Общее неравенство: расстояние между f⋆g и интегралом по z0 ограничено (||L|| ∫ ||f||) ε.
LaTeX
$$dist((f ⋆[L, μ] g : G → F) x0, ∫ t, L (f t) z0 ∂μ) ≤ (||L|| * ∫ x, ||f x|| ∂μ) * ε$$
Lean4
/-- Approximate `f ⋆ g` if the support of the `f` is bounded within a ball, and `g` is near `g x₀`
on a ball with the same radius around `x₀`.
This is a special case of `dist_convolution_le'` where `L` is `(•)`, `f` has integral 1 and `f` is
nonnegative. -/
theorem dist_convolution_le {f : G → ℝ} {x₀ : G} {R ε : ℝ} {z₀ : E'} (hε : 0 ≤ ε) (hf : support f ⊆ ball (0 : G) R)
(hnf : ∀ x, 0 ≤ f x) (hintf : ∫ x, f x ∂μ = 1) (hmg : AEStronglyMeasurable g μ)
(hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε) : dist ((f ⋆[lsmul ℝ ℝ, μ] g : G → E') x₀) z₀ ≤ ε :=
by
have hif : Integrable f μ := integrable_of_integral_eq_one hintf
convert (dist_convolution_le' (lsmul ℝ ℝ) hε hif hf hmg hg).trans _
· simp_rw [lsmul_apply, integral_smul_const, hintf, one_smul]
· simp_rw [Real.norm_of_nonneg (hnf _), hintf, mul_one]
exact (mul_le_mul_of_nonneg_right opNorm_lsmul_le hε).trans_eq (one_mul ε)
