Theorems · Theorem · measure theory

MeasureTheory.FiniteMeasure.tendsto_normalize_iff_tendsto

∀ {Ω : Type u_1} [inst : Nonempty Ω] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.FiniteMeasure Ω}
  [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ}
  {μs : γ → MeasureTheory.FiniteMeasure Ω},
  μ ≠ 0 →
    (Filter.Tendsto (fun i => (μs i).normalize) F (nhds μ.normalize) ∧
        Filter.Tendsto (fun i => (μs i).mass) F (nhds μ.mass) ↔
      Filter.Tendsto μs F (nhds μ))

The weak convergence of finite measures to a nonzero limit can be characterized by the weak convergence of both their normalized versions (probability measures) and their total masses.

Defined in

Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonemptyTopologicalSpaceOpensMeasurableSpace