toWeakDualBCNN_apply — Mathlib

English

Tendsto μs F (nhds μ) if and only if Tendsto (fun i => μs i.toWeakDualBCNN) F (nhds μ.toWeakDualBCNN).

Русский

Сходимость последовательности мер в слабой топологии эквивалентна сходящемуся в слабом двойственном образу.

LaTeX

$$$ \text{Tendsto } μ_s F (\mathsf{nhds} \mu) \iff \text{Tendsto } (\lambda i. (μ_s i).toWeakDualBCNN) F (\mathsf{nhds} (μ.toWeakDualBCNN)). $$$

Lean4

@[simp]
theorem toWeakDualBCNN_apply (μ : FiniteMeasure Ω) (f : Ω →ᵇ ℝ≥0) :
    μ.toWeakDualBCNN f = (∫⁻ x, f x ∂(μ : Measure Ω)).toNNReal :=
  rfl

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