English
If for every bounded continuous real-valued function f on Ω the integrals ∫ f dμ_s(i) converge to ∫ f dμ as i tends to F, then μ_s converges to μ in the finite-measure topology.
Русский
Если для каждого ограниченно непрерывного вещественнозначного функции f на Ω интегралы ∫ f dμ_s(i) сходятся к ∫ f dμ при i tending к F, то μ_s сходится к μ в топологии конечных мер.
LaTeX
$$$\\Big(\\forall f ∈ C_b(Ω, \\mathbb{R}),\\ \\lim_{i \\to F} \\int f \\, d(μ_s i) = \\int f \\, dμ \\Big) \\Rightarrow μ_s \\to μ \\,\\text{in the finite-measure topology}$$$
Lean4
theorem tendsto_of_forall_integral_tendsto {γ : Type*} {F : Filter γ} {μs : γ → FiniteMeasure Ω} {μ : FiniteMeasure Ω}
(h : ∀ f : Ω →ᵇ ℝ, Tendsto (fun i ↦ ∫ x, f x ∂(μs i : Measure Ω)) F (𝓝 (∫ x, f x ∂(μ : Measure Ω)))) :
Tendsto μs F (𝓝 μ) := by
apply tendsto_iff_forall_lintegral_tendsto.mpr
intro f
apply
(ENNReal.tendsto_toReal_iff (fi := F) (fun i ↦ (f.lintegral_lt_top_of_nnreal (μs i)).ne)
(f.lintegral_lt_top_of_nnreal μ).ne).mp
have lip : LipschitzWith 1 ((↑) : ℝ≥0 → ℝ) := isometry_subtype_coe.lipschitz
set f₀ := BoundedContinuousFunction.comp _ lip f with _def_f₀
have f₀_eq : ⇑f₀ = ((↑) : ℝ≥0 → ℝ) ∘ ⇑f := rfl
have f₀_nn : 0 ≤ ⇑f₀ := fun _ ↦ by simp only [f₀_eq, Pi.zero_apply, Function.comp_apply, NNReal.zero_le_coe]
have f₀_ae_nn : 0 ≤ᵐ[(μ : Measure Ω)] ⇑f₀ := .of_forall f₀_nn
have f₀_ae_nns : ∀ i, 0 ≤ᵐ[(μs i : Measure Ω)] ⇑f₀ := fun i ↦ .of_forall f₀_nn
have aux := integral_eq_lintegral_of_nonneg_ae f₀_ae_nn f₀.continuous.measurable.aestronglyMeasurable
have auxs := fun i ↦ integral_eq_lintegral_of_nonneg_ae (f₀_ae_nns i) f₀.continuous.measurable.aestronglyMeasurable
simp_rw [f₀_eq, Function.comp_apply, ENNReal.ofReal_coe_nnreal] at aux auxs
simpa only [← aux, ← auxs] using h f₀
