tendsto_normalize_of_tendsto — Mathlib

English

If finite measures μs converge to μ and μ ≠ 0, then μs.normalize converges to μ.normalize.

Русский

Если μ_s сходятся к μ и μ ≠ 0, то μ_s.normalize сходится к μ.normalize.

LaTeX

$$$\\text{If } μ_s \\to μ \\text{ and } μ \\neq 0, \\text{ then } μ_s.\\mathrm{normalize} \\to μ.\\mathrm{normalize} .$$$

Lean4

/-- If finite measures themselves converge weakly to a nonzero limit measure, then their
normalized versions also converge weakly. -/
theorem tendsto_normalize_of_tendsto {γ : Type*} {F : Filter γ} {μs : γ → FiniteMeasure Ω} (μs_lim : Tendsto μs F (𝓝 μ))
    (nonzero : μ ≠ 0) : Tendsto (fun i ↦ (μs i).normalize) F (𝓝 μ.normalize) :=
  by
  rw [ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds, tendsto_iff_forall_testAgainstNN_tendsto]
  exact fun f ↦ tendsto_normalize_testAgainstNN_of_tendsto μs_lim nonzero f

Похожие утверждения