Theorems · Theorem · abstract harmonic analysis

MeasureTheory.convolution_tendsto_right

∀ {G : Type uG} {E' : Type uE'} [inst : NormedAddCommGroup 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'] {ι : Type u_1}
  {g : ι → G → E'} {l : Filter ι} {x₀ : G} {z₀ : E'} {φ : ι → G → ℝ} {k : ι → G},
  (∀ᶠ (i : ι) in l, ∀ (x : G), 0 ≤ φ i x) →
    (∀ᶠ (i : ι) in l, ∫ (x : G), φ i x ∂μ = 1) →
      Filter.Tendsto (fun n => Function.support (φ n)) l (nhds 0).smallSets →
        (∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (g i) μ) →
          Filter.Tendsto (Function.uncurry g) (l ×ˢ nhds x₀) (nhds z₀) →
            Filter.Tendsto k l (nhds x₀) →
              Filter.Tendsto (fun i => MeasureTheory.convolution (φ 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 nonnegative functions with integral 1 as i tends to l; * The support of φ tends to small neighborhoods around (0 : G) as i tends to l; * g i is mu-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₀. See also ContDiffBump.convolution_tendsto_right.

Defined in

Mathlib.Analysis.Convolution

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupMeasurableSpaceSeminormedAddCommGroupBorelSpaceSecondCountableTopologyMeasureTheory.Measure.IsAddLeftInvariantMeasureTheory.SFiniteNormedSpaceCompleteSpace