Theorems · Theorem · measure theory

MeasureTheory.le_liminf_measure_open_of_forall_tendsto_measure

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

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 open sets G we have the limsup condition μ(G) ≤ liminf μsᵢ(G).

Defined in

Mathlib.MeasureTheory.Measure.Portmanteau

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceTopologicalSpace.PseudoMetrizableSpaceOpensMeasurableSpaceMeasureTheory.IsProbabilityMeasureMeasureTheory.IsProbabilityMeasure