Theorems · Theorem · measure theory

MeasureTheory.tendsto_measure_of_null_frontier

∀ {Ω : 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)],
  (∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) L) →
    ∀ {E : Set Ω}, μ (frontier E) = 0 → Filter.Tendsto (fun i => (μs i) E) L (nhds (μ E))

One implication of the portmanteau theorem: For a sequence of Borel probability measures, if the liminf of the measures of any open set is at least the measure of the open set under a candidate limit measure, then for any set whose boundary carries no probability mass under the candidate limit measure, then its measures under the sequence converge to its measure under the candidate limit measure.

Defined in

Mathlib.MeasureTheory.Measure.Portmanteau

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceOpensMeasurableSpaceMeasureTheory.IsProbabilityMeasureMeasureTheory.IsProbabilityMeasure