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