Theorems · Theorem · measure theory

MeasureTheory.limsup_measure_closed_le_of_forall_tendsto_measure

∀ {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω]
  [TopologicalSpace.PseudoMetrizableSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ] {μs : ι → MeasureTheory.Measure Ω},
  (∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Filter.Tendsto (fun i => (μs i) E) L (nhds (μ E))) →
    ∀ (F : Set Ω), IsClosed F → Filter.limsup (fun i => (μs i) F) L ≤ μ F

One implication of the portmanteau theorem: Assuming that for all Borel sets E whose boundary ∂E carries no probability mass under a candidate limit probability measure μ we have convergence of the measures μsᵢ(E) to μ(E), then for all closed sets F we have the limsup condition limsup μsᵢ(F) ≤ μ(F).

Defined in

Mathlib.MeasureTheory.Measure.Portmanteau

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceTopologicalSpace.PseudoMetrizableSpaceOpensMeasurableSpaceMeasureTheory.IsFiniteMeasure