Theorems · Theorem · measure theory

MeasureTheory.le_measure_liminf_of_limsup_measure_compl_le

∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω}
  {μs : ι → MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] {E : Set Ω},
  MeasurableSet E → Filter.limsup (fun i => (μs i) Eᶜ) L ≤ μ Eᶜ → μ E ≤ Filter.liminf (fun i => (μs i) E) L

Defined in

Mathlib.MeasureTheory.Measure.Portmanteau

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasureTheory.IsProbabilityMeasureMeasureTheory.IsProbabilityMeasure