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 #

Keywords #

convolution, smooth function, bump function

theorem ContDiffBump.convolution_eq_right {G : Type uG} {E' : Type uE'} [NormedAddCommGroup E'] {g : GE'} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace E'] [NormedAddCommGroup G] [NormedSpace G] [HasContDiffBump G] [CompleteSpace E'] {φ : ContDiffBump 0} {x₀ : G} (hg : xMetric.ball x₀ φ.rOut, 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'} [NormedAddCommGroup E'] {g : GE'} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace E'] [NormedAddCommGroup G] [NormedSpace G] [HasContDiffBump G] [CompleteSpace E'] {φ : ContDiffBump 0} [BorelSpace G] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] [FiniteDimensional G] {x₀ : G} (hg : xMetric.ball x₀ φ.rOut, g x = g x₀) :
MeasureTheory.convolution (φ.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 : GE'} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace E'] [NormedAddCommGroup G] [NormedSpace G] [HasContDiffBump G] [CompleteSpace E'] {φ : ContDiffBump 0} [BorelSpace G] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] [FiniteDimensional G] [μ.IsAddLeftInvariant] {x₀ : G} {ε : } (hmg : MeasureTheory.AEStronglyMeasurable g μ) (hg : xMetric.ball x₀ φ.rOut, dist (g x) (g x₀) ε) :
dist (MeasureTheory.convolution (φ.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 μ] [μ.IsOpenPosMeasure] [FiniteDimensional G] [μ.IsAddLeftInvariant] {ι : Type u_1} {φ : ιContDiffBump 0} {g : ιGE'} {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 : ι) => MeasureTheory.convolution ((φ i).normed μ) (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 : GE'} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace E'] [NormedAddCommGroup G] [NormedSpace G] [HasContDiffBump G] [CompleteSpace E'] [BorelSpace G] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] [FiniteDimensional G] [μ.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 : ι) => MeasureTheory.convolution ((φ i).normed μ) 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 : GE'} [MeasurableSpace G] {μ : MeasureTheory.Measure G} [NormedSpace E'] [NormedAddCommGroup G] [NormedSpace G] [HasContDiffBump G] [CompleteSpace E'] [BorelSpace G] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] [FiniteDimensional G] [μ.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 : ι) => MeasureTheory.convolution ((φ i).normed μ) 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.