English
Weak convergence of finite measures is equivalent to the convergence of all integrals against bounded continuous real-valued test functions.
Русский
Слабое сходжение конечных мер эквивалентно сходимости интегралов по всем ограниченно непрерывным вещественным тест-функциям.
LaTeX
$$$Tendsto(μ_s, F, 𝓝(μ)) \\iff \\forall f ∈ C_b(Ω, \\mathbb{R}),\\ Tendsto\\big(i \\mapsto \\int f \\; d(μ_s i)\\big) F (𝓝(\\int f \\; dμ))$$$
Lean4
/-- A characterization of weak convergence in terms of integrals of bounded continuous
real-valued functions. -/
theorem tendsto_iff_forall_integral_tendsto {γ : Type*} {F : Filter γ} {μs : γ → FiniteMeasure Ω}
{μ : FiniteMeasure Ω} :
Tendsto μs F (𝓝 μ) ↔
∀ f : Ω →ᵇ ℝ, Tendsto (fun i ↦ ∫ x, f x ∂(μs i : Measure Ω)) F (𝓝 (∫ x, f x ∂(μ : Measure Ω))) :=
by
refine ⟨?_, tendsto_of_forall_integral_tendsto⟩
rw [tendsto_iff_forall_lintegral_tendsto]
intro h f
simp_rw [BoundedContinuousFunction.integral_eq_integral_nnrealPart_sub]
set f_pos := f.nnrealPart with _def_f_pos
set f_neg := (-f).nnrealPart with _def_f_neg
have tends_pos := (ENNReal.tendsto_toReal (f_pos.lintegral_lt_top_of_nnreal μ).ne).comp (h f_pos)
have tends_neg := (ENNReal.tendsto_toReal (f_neg.lintegral_lt_top_of_nnreal μ).ne).comp (h f_neg)
have aux :
∀ g : Ω →ᵇ ℝ≥0,
(ENNReal.toReal ∘ fun i : γ ↦ ∫⁻ x : Ω, ↑(g x) ∂(μs i : Measure Ω)) = fun i : γ ↦
(∫⁻ x : Ω, ↑(g x) ∂(μs i : Measure Ω)).toReal :=
fun _ ↦ rfl
simp_rw [aux, BoundedContinuousFunction.toReal_lintegral_coe_eq_integral] at tends_pos tends_neg
exact Tendsto.sub tends_pos tends_neg
