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_locallyIntegrable: 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'} [NormedAddCommGroup E'] {g : G → E'} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ E'] [NormedAddCommGroup G] [NormedSpace ℝ G] [HasContDiffBump G] [CompleteSpace E'] {φ : ContDiffBump 0} {x₀ : G} (hg : ∀ x ∈ Metric.ball x₀ φ.rOut, g x = g x₀) : convolution (↑φ) g (ContinuousLinearMap.lsmul ℝ ℝ) x₀ = MeasureTheory.integral μ ↑φ • 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'} [NormedAddCommGroup E'] {g : G → E'} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ E'] [NormedAddCommGroup G] [NormedSpace ℝ G] [HasContDiffBump G] [CompleteSpace E'] {φ : ContDiffBump 0} [BorelSpace G] [MeasureTheory.IsLocallyFiniteMeasure μ] [MeasureTheory.Measure.IsOpenPosMeasure μ] [FiniteDimensional ℝ G] {x₀ : G} (hg : ∀ x ∈ Metric.ball x₀ φ.rOut, g x = g x₀) : convolution (ContDiffBump.normed φ μ) g (ContinuousLinearMap.lsmul ℝ ℝ) 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'} [NormedAddCommGroup E'] {g : G → E'} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ E'] [NormedAddCommGroup G] [NormedSpace ℝ G] [HasContDiffBump G] [CompleteSpace E'] {φ : ContDiffBump 0} [BorelSpace G] [MeasureTheory.IsLocallyFiniteMeasure μ] [MeasureTheory.Measure.IsOpenPosMeasure μ] [FiniteDimensional ℝ G] [MeasureTheory.Measure.IsAddLeftInvariant μ] {x₀ : G} {ε : ℝ} (hmg : MeasureTheory.AEStronglyMeasurable g μ) (hg : ∀ x ∈ Metric.ball x₀ φ.rOut, dist (g x) (g x₀) ≤ ε) : dist (convolution (ContDiffBump.normed φ μ) g (ContinuousLinearMap.lsmul ℝ ℝ) 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'} [NormedAddCommGroup E'] [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ E'] [NormedAddCommGroup G] [NormedSpace ℝ G] [HasContDiffBump G] [CompleteSpace E'] [BorelSpace G] [MeasureTheory.IsLocallyFiniteMeasure μ] [MeasureTheory.Measure.IsOpenPosMeasure μ] [FiniteDimensional ℝ G] [MeasureTheory.Measure.IsAddLeftInvariant μ] {ι : Type u_1} {φ : ι → ContDiffBump 0} {g : ι → G → E'} {k : ι → G} {x₀ : G} {z₀ : E'} {l : Filter ι} (hφ : Filter.Tendsto (fun (i : ι) => (φ i).rOut) l (nhds 0)) (hig : ∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (g i) μ) (hcg : Filter.Tendsto (Function.uncurry g) (l ×ˢ nhds x₀) (nhds z₀)) (hk : Filter.Tendsto k l (nhds x₀)) : Filter.Tendsto (fun (i : ι) => convolution (ContDiffBump.normed (φ i) μ) (g i) (ContinuousLinearMap.lsmul ℝ ℝ) (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'} [NormedAddCommGroup E'] {g : G → E'} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ E'] [NormedAddCommGroup G] [NormedSpace ℝ G] [HasContDiffBump G] [CompleteSpace E'] [BorelSpace G] [MeasureTheory.IsLocallyFiniteMeasure μ] [MeasureTheory.Measure.IsOpenPosMeasure μ] [FiniteDimensional ℝ G] [MeasureTheory.Measure.IsAddLeftInvariant μ] {ι : Type u_1} {φ : ι → ContDiffBump 0} {l : Filter ι} (hφ : Filter.Tendsto (fun (i : ι) => (φ i).rOut) l (nhds 0)) (hg : Continuous g) (x₀ : G) : Filter.Tendsto (fun (i : ι) => convolution (ContDiffBump.normed (φ i) μ) g (ContinuousLinearMap.lsmul ℝ ℝ) 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'} [NormedAddCommGroup E'] {g : G → E'} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace ℝ E'] [NormedAddCommGroup G] [NormedSpace ℝ G] [HasContDiffBump G] [CompleteSpace E'] [BorelSpace G] [MeasureTheory.IsLocallyFiniteMeasure μ] [MeasureTheory.Measure.IsOpenPosMeasure μ] [FiniteDimensional ℝ G] [MeasureTheory.Measure.IsAddLeftInvariant μ] {ι : Type u_1} {φ : ι → ContDiffBump 0} {l : Filter ι} {K : ℝ} (hφ : Filter.Tendsto (fun (i : ι) => (φ i).rOut) l (nhds 0)) (h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn) (hg : MeasureTheory.LocallyIntegrable g) : ∀ᵐ (x₀ : G) ∂μ, Filter.Tendsto (fun (i : ι) => convolution (ContDiffBump.normed (φ i) μ) g (ContinuousLinearMap.lsmul ℝ ℝ) 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.