English
If the normalized measures μs.i.normalize converge to μ.normalize and their masses converge to μ.mass, then for every bounded nonnegative function f, μs.i.testAgainstNN(f) converges to μ.testAgainstNN(f).
Русский
Если нормированные меры μs.i.normalize сходятся к μ.normalize, а их массы сходятся к μ.mass, то для любой ограниченной неотрицательной функции f, μs.i.testAgainstNN(f) сходится к μ.testAgainstNN(f).
LaTeX
$$$\\text{If } (μ_s i) \\xrightarrow{T} μ \\text{ in normalize and mass, then } (μ_s i).testAgainstNN f \\xrightarrow{T} μ.testAgainstNN f.$$$
Lean4
theorem tendsto_testAgainstNN_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)) (f : Ω →ᵇ ℝ≥0) :
Tendsto (fun i ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f)) :=
by
by_cases h_mass : μ.mass = 0
· simp only [μ.mass_zero_iff.mp h_mass, zero_testAgainstNN_apply, zero_mass] at mass_lim ⊢
exact tendsto_zero_testAgainstNN_of_tendsto_zero_mass mass_lim f
simp_rw [fun i ↦ (μs i).testAgainstNN_eq_mass_mul f, μ.testAgainstNN_eq_mass_mul f]
rw [ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds] at μs_lim
rw [tendsto_iff_forall_testAgainstNN_tendsto] at μs_lim
have lim_pair :
Tendsto (fun i ↦ (⟨(μs i).mass, (μs i).normalize.toFiniteMeasure.testAgainstNN f⟩ : ℝ≥0 × ℝ≥0)) F
(𝓝 ⟨μ.mass, μ.normalize.toFiniteMeasure.testAgainstNN f⟩) :=
(Prod.tendsto_iff _ _).mpr ⟨mass_lim, μs_lim f⟩
exact tendsto_mul.comp lim_pair
