tendsto_iff_forall_integral_rclike_tendsto

English

Weak convergence can be tested by bounded continuous functions valued in any RCLike field 𝕜 (e.g., ℝ, ℂ).

Русский

Слабую сходимость можно тестировать на ограниченно непрерывных функциях, принимающих значения в любом RCLike поле 𝕜 (например, ℝ, ℂ).

LaTeX

$$Tendsto μ_s F (nhds μ) ↔ ∀ f : Ω →ᵇ 𝕜, Tendsto (fun i => ∫ ω, f ω ∂(μ_s i : Measure Ω)) F (nhds (∫ ω, f ω ∂(μ : Measure Ω)))$$

Lean4

theorem tendsto_iff_forall_integral_rclike_tendsto {γ : Type*} (𝕜 : Type*) [RCLike 𝕜] {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_rclike_tendsto 𝕜]

Похожие утверждения