Theorems · Theorem · measure theory

MeasureTheory.ProbabilityMeasure.limsup_measure_closed_le_of_tendsto

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

One implication of the portmanteau theorem: Weak convergence of probability measures implies that the limsup of the measures of any closed set is at most the measure of the closed set under the limit probability measure.

Defined in

Mathlib.MeasureTheory.Measure.Portmanteau

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceOpensMeasurableSpaceHasOuterApproxClosed