Theorems · Theorem · measure theory

MeasureTheory.limsup_measure_closed_le_iff_liminf_measure_open_ge

∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [OpensMeasurableSpace Ω] {ι : Type u_2}
  {L : Filter ι} {μ : MeasureTheory.Measure Ω} {μs : ι → MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)],
  (∀ (F : Set Ω), IsClosed F → Filter.limsup (fun i => (μs i) F) L ≤ μ F) ↔
    ∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) L

One pair of implications of the portmanteau theorem: For a sequence of Borel probability measures, the following two are equivalent: (C) The limsup of the measures of any closed set is at most the measure of the closed set under a candidate limit measure. (O) The liminf of the measures of any open set is at least the measure of the open set under a candidate limit measure.

Defined in

Mathlib.MeasureTheory.Measure.Portmanteau

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceOpensMeasurableSpaceMeasureTheory.IsProbabilityMeasureMeasureTheory.IsProbabilityMeasure