English
For μ ≠ 0, the weak convergence of finite measures μ_s to μ is equivalent to the simultaneous convergence of their normalized versions and their masses.
Русский
Положим μ ≠ 0. Тогда слабая сходимость μ_s к μ эквивалентна одновременной сходимости нормированных версий и масс.
LaTeX
$$$\\Big( Tendsto μ_s F (\\mathcal{N} μ) \\Big) \\\\Longleftrightarrow \\\\ ( Tendsto μ_s F (\\mathcal{N} μ.normalize) \\land Tendsto (μ_s.mass) F (\\mathcal{N} μ.mass) ).$$$
Lean4
/-- If the normalized versions of finite measures converge weakly and their total masses
also converge, then the finite measures themselves converge weakly. -/
theorem tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass {γ : Type*} {F : Filter γ} {μs : γ → FiniteMeasure Ω}
(μs_lim : Tendsto (fun i ↦ (μs i).normalize) F (𝓝 μ.normalize))
(mass_lim : Tendsto (fun i ↦ (μs i).mass) F (𝓝 μ.mass)) : Tendsto μs F (𝓝 μ) :=
by
rw [tendsto_iff_forall_testAgainstNN_tendsto]
exact fun f ↦ tendsto_testAgainstNN_of_tendsto_normalize_testAgainstNN_of_tendsto_mass μs_lim mass_lim f
