Theorems · Theorem · measure theory

MeasureTheory.tendsto_of_forall_isCompact_of_isTightMeasureSet

∀ {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [inst : TopologicalSpace Ω] [inst_1 : OpensMeasurableSpace Ω]
  {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ι → MeasureTheory.ProbabilityMeasure Ω} {L : Filter ι}
  [L.IsCountablyGenerated],
  MeasureTheory.IsTightMeasureSet (Set.range (MeasureTheory.ProbabilityMeasure.toMeasure ∘ μs)) →
    (∀ (F : Set Ω), IsCompact F → Filter.limsup (fun x => (μs x) F) L ≤ μ F) → Filter.Tendsto μs L (nhds μ)

A different version of the (C) → (T) implication of the portmanteau theorem: If the set of measures is tight, a limsup inequality for compact sets implies weak convergence.

Defined in

Mathlib.MeasureTheory.Measure.Portmanteau

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceOpensMeasurableSpaceFilter.IsCountablyGenerated