nndist_le_of_le — Mathlib

English

For a HölderOnWith map, the bound on nndist(fx,fy) is given by C times nndist(x,y) to the r-th power when x,y ∈ s.

Русский

Для отображения ХолдерOnWith ограничение на nndist(fx,fy) задаётся как C · nndist(x,y)^{r} при x,y ∈ s.

LaTeX

$$$\operatorname{nndist}(f(x),f(y)) \le C \cdot (\operatorname{nndist}(x,y))^{r}$$$

Lean4

theorem nndist_le_of_le (hf : HolderOnWith C r f s) (hx : x ∈ s) (hy : y ∈ s) {d : ℝ≥0} (hd : nndist x y ≤ d) :
    nndist (f x) (f y) ≤ C * d ^ (r : ℝ) :=
  by
  rw [← ENNReal.coe_le_coe, ← edist_nndist, ENNReal.coe_mul, ENNReal.coe_rpow_of_nonneg _ r.coe_nonneg]
  apply hf.edist_le_of_le hx hy
  rwa [edist_nndist, ENNReal.coe_le_coe]

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