continuous_testAgainstNN_eval — Mathlib

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 _ _

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