English
For any μ, and bounded nonnegative functions f and g, the testAgainstNN functional satisfies a Lipschitz-type bound: μ.testAgainstNN f ≤ μ.testAgainstNN g + nndist(f,g) · μ.mass.
Русский
Для любой меры μ и функций f,g ограниченных неотрицательных выполняется оценка Липшица: μ.testAgainstNN f ≤ μ.testAgainstNN g + nndist(f,g) · μ.mass.
LaTeX
$$$ \forall f,g : \Omega \to^{} \mathbb{R}_{\ge 0}, \; μ.testAgainstNN f \le μ.testAgainstNN g + \mathrm{nndist}(f,g) \cdot μ.mass . $$$
Lean4
theorem testAgainstNN_lipschitz_estimate (μ : FiniteMeasure Ω) (f g : Ω →ᵇ ℝ≥0) :
μ.testAgainstNN f ≤ μ.testAgainstNN g + nndist f g * μ.mass :=
by
simp only [← μ.testAgainstNN_const (nndist f g), ← testAgainstNN_add, ← ENNReal.coe_le_coe,
BoundedContinuousFunction.coe_add, const_apply, ENNReal.coe_add, Pi.add_apply, coe_nnreal_ennreal_nndist,
testAgainstNN_coe_eq]
apply lintegral_mono
have le_dist : ∀ ω, dist (f ω) (g ω) ≤ nndist f g := BoundedContinuousFunction.dist_coe_le_dist
intro ω
have le' : f ω ≤ g ω + nndist f g := by
calc
f ω
_ ≤ g ω + nndist (f ω) (g ω) := (NNReal.le_add_nndist (f ω) (g ω))
_ ≤ g ω + nndist f g := (add_le_add_iff_left (g ω)).mpr (le_dist ω)
have le : (f ω : ℝ≥0∞) ≤ (g ω : ℝ≥0∞) + nndist f g := by simpa only [← ENNReal.coe_add] using (by exact_mod_cast le')
rwa [coe_nnreal_ennreal_nndist] at le
