Theorems · Theorem · measure theory

MeasureTheory.FiniteMeasure.tendsto_normalize_of_tendsto

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

If finite measures themselves converge weakly to a nonzero limit measure, then their normalized versions also converge weakly.

Defined in

Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Cited by

1 results in Mathlib

Foundations

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

Assumes

NonemptyTopologicalSpaceOpensMeasurableSpace