English
Tendsto μs F (nhds μ) is equivalent to 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
/-- Integration of (nonnegative bounded continuous) test functions against finite Borel measures
depends continuously on the measure. -/
theorem continuous_testAgainstNN_eval (f : Ω →ᵇ ℝ≥0) : Continuous fun μ : FiniteMeasure Ω ↦ μ.testAgainstNN f :=
by
change Continuous ((fun φ : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0) ↦ φ f) ∘ toWeakDualBCNN)
refine Continuous.comp ?_ (toWeakDualBCNN_continuous (Ω := Ω))
exact WeakBilin.eval_continuous _ _