Theorems · Theorem · measure theory

MeasureTheory.tendsto_integral_thickenedIndicator_of_isClosed

∀ {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [inst : PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] {F : Set Ω},
  IsClosed F →
    ∀ {δs : ℕ → ℝ} (δs_pos : ∀ (n : ℕ), 0 < δs n),
      Filter.Tendsto δs Filter.atTop (nhds 0) →
        Filter.Tendsto (fun n => ∫ (ω : Ω), ↑((thickenedIndicator ⋯ F) ω) ∂μ) Filter.atTop (nhds (μ.real F))

The integrals of thickened indicators of a closed set against a finite measure tend to the measure of the closed set if the thickening radii tend to zero.

Defined in

Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpaceOpensMeasurableSpaceMeasureTheory.IsFiniteMeasure