English
The map f ↦ μ.testAgainstNN f is Lipschitz with constant μ.mass.
Русский
Отображение f ↦ μ.testAgainstNN f является Lipschitz-ограниченным константой μ.mass.
LaTeX
$$$ \text{LipschitzWith} (μ.mass) (\lambda f: Ω \to^{} \mathbb{R}_{\ge 0}) \; f \mapsto μ.testAgainstNN f. $$$
Lean4
theorem testAgainstNN_lipschitz (μ : FiniteMeasure Ω) : LipschitzWith μ.mass fun f : Ω →ᵇ ℝ≥0 ↦ μ.testAgainstNN f :=
by
rw [lipschitzWith_iff_dist_le_mul]
intro f₁ f₂
suffices abs (μ.testAgainstNN f₁ - μ.testAgainstNN f₂ : ℝ) ≤ μ.mass * dist f₁ f₂ by rwa [NNReal.dist_eq]
apply abs_le.mpr
constructor
· have key := μ.testAgainstNN_lipschitz_estimate f₂ f₁
rw [mul_comm] at key
suffices ↑(μ.testAgainstNN f₂) ≤ ↑(μ.testAgainstNN f₁) + ↑μ.mass * dist f₁ f₂ by linarith
simpa [nndist_comm] using NNReal.coe_mono key
· have key := μ.testAgainstNN_lipschitz_estimate f₁ f₂
rw [mul_comm] at key
suffices ↑(μ.testAgainstNN f₁) ≤ ↑(μ.testAgainstNN f₂) + ↑μ.mass * dist f₁ f₂ by linarith
simpa using NNReal.coe_mono key
