English
If μs converge to μ in the sense of finite measures and μ ≠ 0, then the normalized measures μs.normalize converge 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
theorem tendsto_normalize_testAgainstNN_of_tendsto {γ : Type*} {F : Filter γ} {μs : γ → FiniteMeasure Ω}
(μs_lim : Tendsto μs F (𝓝 μ)) (nonzero : μ ≠ 0) (f : Ω →ᵇ ℝ≥0) :
Tendsto (fun i ↦ (μs i).normalize.toFiniteMeasure.testAgainstNN f) F
(𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f)) :=
by
have lim_mass := μs_lim.mass
have aux : {(0 : ℝ≥0)}ᶜ ∈ 𝓝 μ.mass := isOpen_compl_singleton.mem_nhds (μ.mass_nonzero_iff.mpr nonzero)
have eventually_nonzero : ∀ᶠ i in F, μs i ≠ 0 :=
by
simp_rw [← mass_nonzero_iff]
exact lim_mass aux
have eve : ∀ᶠ i in F, (μs i).normalize.toFiniteMeasure.testAgainstNN f = (μs i).mass⁻¹ * (μs i).testAgainstNN f :=
by
filter_upwards [eventually_iff.mp eventually_nonzero]
intro i hi
apply normalize_testAgainstNN _ hi
simp_rw [tendsto_congr' eve, μ.normalize_testAgainstNN nonzero]
have lim_pair :
Tendsto (fun i ↦ (⟨(μs i).mass⁻¹, (μs i).testAgainstNN f⟩ : ℝ≥0 × ℝ≥0)) F (𝓝 ⟨μ.mass⁻¹, μ.testAgainstNN f⟩) :=
by
refine (Prod.tendsto_iff _ _).mpr ⟨?_, ?_⟩
· exact (continuousOn_inv₀.continuousAt aux).tendsto.comp lim_mass
· exact tendsto_iff_forall_testAgainstNN_tendsto.mp μs_lim f
exact tendsto_mul.comp lim_pair
