# Documentation

Mathlib.Analysis.Calculus.BumpFunction.Convolution

# Convolution with a bump function #

In this file we prove lemmas about convolutions (φ.normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀, where φ : ContDiffBump 0 is a smooth bump function.

We prove that this convolution is equal to g x₀ if g is a constant on Metric.ball x₀ φ.rOut. We also provide estimates in the case if g x is close to g x₀ on this ball.

## Main results #

• ContDiffBump.convolution_tendsto_right_of_continuous: Let g be a continuous function; let φ i be a family of ContDiffBump 0 functions with. If (φ i).rOut tends to zero along a filter l, then ((φ i).normed μ ⋆[lsmul ℝ ℝ, μ] g) x₀ tends to g x₀ along the same filter.
• ContDiffBump.convolution_tendsto_right: generalization of the above lemma.
• ContDiffBump.ae_convolution_tendsto_right_of_locally_integrable: let g be a locally integrable function. Then the convolution of g with a family of bump functions with support tending to 0 converges almost everywhere to g.

## Keywords #

convolution, smooth function, bump function

theorem ContDiffBump.convolution_eq_right {G : Type uG} {E' : Type uE'} [] {g : GE'} [] {μ : } [] [] [] [] {φ : } {x₀ : G} (hg : ∀ (x : G), x Metric.ball x₀ φ.rOutg x = g x₀) :
convolution (φ) g () x₀ = g x₀

If φ is a bump function, compute (φ ⋆ g) x₀ if g is constant on Metric.ball x₀ φ.rOut.

theorem ContDiffBump.normed_convolution_eq_right {G : Type uG} {E' : Type uE'} [] {g : GE'} [] {μ : } [] [] [] [] {φ : } [] [] {x₀ : G} (hg : ∀ (x : G), x Metric.ball x₀ φ.rOutg x = g x₀) :
= g x₀

If φ is a normed bump function, compute φ ⋆ g if g is constant on Metric.ball x₀ φ.rOut.

theorem ContDiffBump.dist_normed_convolution_le {G : Type uG} {E' : Type uE'} [] {g : GE'} [] {μ : } [] [] [] [] {φ : } [] [] {x₀ : G} {ε : } (hmg : ) (hg : ∀ (x : G), x Metric.ball x₀ φ.rOutdist (g x) (g x₀) ε) :
dist () (g x₀) ε

If φ is a normed bump function, approximate (φ ⋆ g) x₀ if g is near g x₀ on a ball with radius φ.rOut around x₀.

theorem ContDiffBump.convolution_tendsto_right {G : Type uG} {E' : Type uE'} [] [] {μ : } [] [] [] [] [] [] {ι : Type u_1} {φ : ι} {g : ιGE'} {k : ιG} {x₀ : G} {z₀ : E'} {l : } (hφ : Filter.Tendsto (fun i => (φ i).rOut) l (nhds 0)) (hig : ∀ᶠ (i : ι) in l, ) (hcg : Filter.Tendsto () (l ×ˢ nhds x₀) (nhds z₀)) (hk : Filter.Tendsto k l (nhds x₀)) :
Filter.Tendsto (fun i => convolution (ContDiffBump.normed (φ i) μ) (g i) () (k i)) l (nhds z₀)

(φ i ⋆ g i) (k i) tends to z₀ as i tends to some filter l if

• φ is a sequence of normed bump functions such that (φ i).rOut tends to 0 as i tends to l;
• g i is μ-a.e. strongly measurable as i tends to l;
• g i x tends to z₀ as (i, x) tends to l ×ˢ 𝓝 x₀;
• k i tends to x₀.
theorem ContDiffBump.convolution_tendsto_right_of_continuous {G : Type uG} {E' : Type uE'} [] {g : GE'} [] {μ : } [] [] [] [] [] [] {ι : Type u_1} {φ : ι} {l : } (hφ : Filter.Tendsto (fun i => (φ i).rOut) l (nhds 0)) (hg : ) (x₀ : G) :
Filter.Tendsto (fun i => convolution (ContDiffBump.normed (φ i) μ) g () x₀) l (nhds (g x₀))

Special case of ContDiffBump.convolution_tendsto_right where g is continuous, and the limit is taken only in the first function.

theorem ContDiffBump.ae_convolution_tendsto_right_of_locally_integrable {G : Type uG} {E' : Type uE'} [] {g : GE'} [] {μ : } [] [] [] [] [] [] {ι : Type u_1} {φ : ι} {l : } {K : } (hφ : Filter.Tendsto (fun i => (φ i).rOut) l (nhds 0)) (h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut K * (φ i).rIn) (hg : ) :
∀ᵐ (x₀ : G) ∂μ, Filter.Tendsto (fun i => convolution (ContDiffBump.normed (φ i) μ) g () x₀) l (nhds (g x₀))

If a function g is locally integrable, then the convolution φ i * g converges almost everywhere to g if φ i is a sequence of bump functions with support tending to 0, provided that the ratio between the inner and outer radii of φ i remains bounded.