nndist_le

Mathlib.Topology.MetricSpace.Holder

URI: https://scilib.ai/kg/mathlib#HolderOnWith.nndist_le

← MathLib Explorer

English

Extends the Hölder estimate to nndist in the metric space setting.

Русский

Расширение Холдер-оценки на nndist в метрике.

LaTeX

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

Lean4

theorem nndist_le (hf : HolderOnWith C r f s) (hx : x ∈ s) (hy : y ∈ s) :
    nndist (f x) (f y) ≤ C * nndist x y ^ (r : ℝ) :=
  hf.nndist_le_of_le hx hy le_rfl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru