Theorems · Theorem · abstract harmonic analysis

MeasureTheory.dist_convolution_le

∀ {G : Type uG} {E' : Type uE'} [inst : NormedAddCommGroup E'] {g : G → E'} [inst_1 : MeasurableSpace G]
  {μ : MeasureTheory.Measure G} [inst_2 : SeminormedAddCommGroup G] [BorelSpace G] [SecondCountableTopology G]
  [μ.IsAddLeftInvariant] [MeasureTheory.SFinite μ] [inst_7 : NormedSpace ℝ E'] [CompleteSpace E'] {f : G → ℝ} {x₀ : G}
  {R ε : ℝ} {z₀ : E'},
  0 ≤ ε →
    Function.support f ⊆ Metric.ball 0 R →
      (∀ (x : G), 0 ≤ f x) →
        ∫ (x : G), f x ∂μ = 1 →
          MeasureTheory.AEStronglyMeasurable g μ →
            (∀ x ∈ Metric.ball x₀ R, dist (g x) z₀ ≤ ε) →
              dist (MeasureTheory.convolution f g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀) z₀ ≤ ε

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.

Defined in

Mathlib.Analysis.Convolution

Cited by

2 results in Mathlib

Foundations

Depth 261 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupMeasurableSpaceSeminormedAddCommGroupBorelSpaceSecondCountableTopologyMeasureTheory.Measure.IsAddLeftInvariantMeasureTheory.SFiniteNormedSpaceCompleteSpace