# 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.

## Keywords #

convolution, smooth function, bump function

theorem ContDiffBump.convolution_eq_right {G : Type uG} {E' : Type uE'} [] {g : GE'} [] {μ : } [] [] [] [] {φ : } {x₀ : G} (hg : xMetric.ball x₀ φ.rOut, g x = 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'} [] {μ : } [] [] [] [] {φ : } [] [μ.IsOpenPosMeasure] [] {x₀ : G} (hg : xMetric.ball x₀ φ.rOut, g x = g x₀) :
MeasureTheory.convolution (φ.normed μ) 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'} [] {μ : } [] [] [] [] {φ : } [] [μ.IsOpenPosMeasure] [] [μ.IsAddLeftInvariant] {x₀ : G} {ε : } (hmg : ) (hg : xMetric.ball x₀ φ.rOut, dist (g x) (g x₀) ε) :
dist (MeasureTheory.convolution (φ.normed μ) g μ x₀) (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'} [] [] {μ : } [] [] [] [] [] [μ.IsOpenPosMeasure] [] [μ.IsAddLeftInvariant] {ι : 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 : ι) => MeasureTheory.convolution ((φ i).normed μ) (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'} [] {μ : } [] [] [] [] [] [μ.IsOpenPosMeasure] [] [μ.IsAddLeftInvariant] {ι : Type u_1} {φ : ι} {l : } (hφ : Filter.Tendsto (fun (i : ι) => (φ i).rOut) l (nhds 0)) (hg : ) (x₀ : G) :
Filter.Tendsto (fun (i : ι) => MeasureTheory.convolution ((φ i).normed μ) 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_locallyIntegrable {G : Type uG} {E' : Type uE'} [] {g : GE'} [] {μ : } [] [] [] [] [] [μ.IsOpenPosMeasure] [] [μ.IsAddLeftInvariant] {ι : 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 : ι) => MeasureTheory.convolution ((φ i).normed μ) 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.