nnHolderNorm

Mathlib.Topology.MetricSpace.HolderNorm

URI: https://scilib.ai/kg/mathlib#nnHolderNorm

Lean4

/-- The `r`-Hölder (semi)norm in `ℝ≥0`. -/
noncomputable def nnHolderNorm (r : ℝ≥0) (f : X → Y) : ℝ≥0 :=
  (eHolderNorm r f).toNNReal

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

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

Разделы

Аффилиация

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