testAgainstNN_lipschitz — Mathlib

English

For any μ, the map f ↦ μ.toFiniteMeasure.testAgainstNN f is 1-Lipschitz with respect to the sup-norm on bounded nonnegative functions.

Русский

Для любого μ отображение f ↦ μ.toFiniteMeasure.testAgainstNN f является 1-Липшицевым относительно нормы верхнего модуля на ограниченных неотрицательных функций.

LaTeX

$$$\\text{LipschitzWith } 1\\;\\bigl( f \\mapsto μ.toFiniteMeasure.testAgainstNN f \\bigr)$$$

Lean4

theorem testAgainstNN_lipschitz (μ : ProbabilityMeasure Ω) :
    LipschitzWith 1 fun f : Ω →ᵇ ℝ≥0 ↦ μ.toFiniteMeasure.testAgainstNN f :=
  μ.mass_toFiniteMeasure ▸ μ.toFiniteMeasure.testAgainstNN_lipschitz

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