English
Weak convergence is characterized by convergence of integrals of every bounded real-valued bounded continuous function.
Русский
Слабая сходимость характеризуется сходящестью интегралов по каждой ограниченно‑значной ограниченно‑неотрицательной функции на ℝ.
LaTeX
$$Tendsto μ_s F (nhds μ) ↔ ∀ f : Ω →ᵇ ℝ, Tendsto (fun i => ∫ ω, f ω ∂(μ_s i : Measure Ω)) F (nhds (∫ ω, f ω ∂(μ : Measure Ω)))$$
Lean4
/-- The characterization of weak convergence of probability measures by the usual (defining)
condition that the integrals of every continuous bounded function converge to the integral of the
function against the limit measure. -/
theorem tendsto_iff_forall_integral_tendsto {γ : Type*} {F : Filter γ} {μs : γ → ProbabilityMeasure Ω}
{μ : ProbabilityMeasure Ω} :
Tendsto μs F (𝓝 μ) ↔
∀ f : Ω →ᵇ ℝ, Tendsto (fun i ↦ ∫ ω, f ω ∂(μs i : Measure Ω)) F (𝓝 (∫ ω, f ω ∂(μ : Measure Ω))) :=
by simp [tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds, FiniteMeasure.tendsto_iff_forall_integral_tendsto]
