Theorems · Theorem · measure theory

tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto_aux

∀ {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace α] [BorelSpace α] [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] {g : α → E}
  {l : Filter ι} {x₀ : α} {s t : Set α} {φ : ι → α → ℝ},
  MeasurableSet s →
    MeasurableSet t →
      t ⊆ s →
        t ∈ nhdsWithin x₀ s →
          (∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x) →
            (∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)) →
              Filter.Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (nhds 1) →
                (∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (φ i) (μ.restrict s)) →
                  MeasureTheory.IntegrableOn g s μ →
                    Filter.Tendsto g (nhdsWithin x₀ s) (nhds 0) →
                      Filter.Tendsto (fun i => ∫ (x : α) in s, φ i x • g x ∂μ) l (nhds 0)

If a sequence of peak functions φᵢ converges uniformly to zero away from a point x₀ and its integral on some finite-measure neighborhood of x₀ converges to 1, and g is integrable and has a limit a at x₀, then ∫ φᵢ • g converges to a. Auxiliary lemma where one assumes additionally a = 0.

Defined in

Mathlib.MeasureTheory.Integral.PeakFunction

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceBorelSpaceNormedAddCommGroupNormedSpace