tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds

English

A net μ_s converges to μ in the weak topology if and only if toFiniteMeasure μ_s converges to μ.toFiniteMeasure in the finite measure topology.

Русский

Сходимость сетки μ_s к μ в слабой топологии эквивалентна сходящности toFiniteMeasure(μ_s) к μ.toFiniteMeasure в топологии конечных мер.

LaTeX

$$$\\mathrm{Tendsto}\,\\mu_s\\,F\\,(\\mathcal{N}\\mu) \\iff \\mathrm{Tendsto}\\,(\\mathrm{toFiniteMeasure} \\circ \\mu_s)\\,F\\,(\\mathcal{N}\\mu^{\\mathrm{toFiniteMeasure}})$$$

Lean4

theorem tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds {δ : Type*} (F : Filter δ) {μs : δ → ProbabilityMeasure Ω}
    {μ₀ : ProbabilityMeasure Ω} : Tendsto μs F (𝓝 μ₀) ↔ Tendsto (toFiniteMeasure ∘ μs) F (𝓝 μ₀.toFiniteMeasure) :=
  (toFiniteMeasure_isEmbedding Ω).tendsto_nhds_iff

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