tendsto_iff_forall_lintegral_tendsto

English

On spaces where indicators of closed sets have outer approximations by continuous functions, the weak convergence topology on FiniteMeasure Ω is Hausdorff.

Русский

На пространствах, где индикаторыClosed множеств имеют аппроксимации непрерывными функциями, слабая топология сходимости FiniteMeasure Ω является Hausdorff.

LaTeX

$$$ \text{T2Space} (\text{FiniteMeasure } \Omega) $ under the given hypotheses.$$

Lean4

/-- A characterization of weak convergence in terms of integrals of bounded continuous
nonnegative functions. -/
theorem tendsto_iff_forall_lintegral_tendsto {γ : Type*} {F : Filter γ} {μs : γ → FiniteMeasure Ω}
    {μ : FiniteMeasure Ω} :
    Tendsto μs F (𝓝 μ) ↔
      ∀ f : Ω →ᵇ ℝ≥0, Tendsto (fun i ↦ ∫⁻ x, f x ∂(μs i : Measure Ω)) F (𝓝 (∫⁻ x, f x ∂(μ : Measure Ω))) :=
  by
  rw [tendsto_iff_forall_toWeakDualBCNN_tendsto]
  simp_rw [toWeakDualBCNN_apply _ _, ← testAgainstNN_coe_eq, ENNReal.tendsto_coe, ENNReal.toNNReal_coe]

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