English
For μ ≠ 0, Tendsto μ_s to μ is equivalent to the conjunction of Tendsto μ_s to μ.normalize and Tendsto μ_s.mass to μ.mass.
Русский
Для μ ≠ 0, сходение μ_s к μ эквивалентно одновременной сходимости μ_s к μ.normalize и μ_s.mass к μ.mass.
LaTeX
$$$\\text{Tendsto } μ_s F (\\mathcal{N} μ) \\\\iff \\\\ ( Tendsto μ_s F (\\mathcal{N} μ.normalize) \\land Tendsto (μ_s.mass) F (\\mathcal{N} μ.mass) ).$$$
Lean4
/-- 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. -/
theorem tendsto_normalize_iff_tendsto {γ : Type*} {F : Filter γ} {μs : γ → FiniteMeasure Ω} (nonzero : μ ≠ 0) :
Tendsto (fun i ↦ (μs i).normalize) F (𝓝 μ.normalize) ∧ Tendsto (fun i ↦ (μs i).mass) F (𝓝 μ.mass) ↔
Tendsto μs F (𝓝 μ) :=
by
constructor
· rintro ⟨normalized_lim, mass_lim⟩
exact tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass normalized_lim mass_lim
· intro μs_lim
exact ⟨tendsto_normalize_of_tendsto μs_lim nonzero, μs_lim.mass⟩
