Theorems · Theorem · measure theory

MeasureTheory.tendsto_of_forall_isOpen_le_liminf

∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {ι : Type u_2} {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ι → MeasureTheory.ProbabilityMeasure Ω} {L : Filter ι}
  [L.IsCountablyGenerated],
  (∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) L) → Filter.Tendsto (fun i => μs i) L (nhds μ)

One implication of the portmanteau theorem: if for all open sets G we have the liminf condition μ(G) ≤ liminf μsₙ(G), then the measures μsₙ converge weakly to the measure μ. Formulated here for countably generated filters.

Defined in

Mathlib.MeasureTheory.Measure.Portmanteau

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceOpensMeasurableSpaceFilter.IsCountablyGenerated