tendsto_iff_forall_testAgainstNN_tendsto

English

Tendsto μs F (nhds μ) iff for every f, Tendsto (fun i => μs i.testAgainstNN f) F (nhds μ.testAgainstNN f).

Русский

Сходимость μ_s эквивалентна сходимости каждого теста по f: μ_s i.testAgainstNN f → μ.testAgainstNN f.

LaTeX

$$$ \forall f : \Omega \to^{} \mathbb{R}_{\ge 0}, \; \text{Tendsto } (i \mapsto μ_s i.testAgainstNN f) F (\mathsf{nhds} (μ.testAgainstNN f)). $$$

Lean4

theorem tendsto_iff_forall_testAgainstNN_tendsto {γ : Type*} {F : Filter γ} {μs : γ → FiniteMeasure Ω}
    {μ : FiniteMeasure Ω} :
    Tendsto μs F (𝓝 μ) ↔ ∀ f : Ω →ᵇ ℝ≥0, Tendsto (fun i ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f)) := by
  rw [FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto]; rfl

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