gauge — Mathlib

English

The Minkowski functional gauge s assigns to x the smallest positive real r such that x lies in r s.

Русский

Функционал Минковского gauge s присваивает вектору x наименьшее положительное число r такое, что x принадлежит r s.

LaTeX

$$$$\\operatorname{gauge}(s,x) = \\inf\\{ r>0 \\mid x \\in r\\cdot s \\}.$$$$

Lean4

/-- The Minkowski functional. Given a set `s` in a real vector space, `gauge s` is the functional
which sends `x : E` to the smallest `r : ℝ` such that `x` is in `s` scaled by `r`. -/
def gauge (s : Set E) (x : E) : ℝ :=
  sInf {r : ℝ | 0 < r ∧ x ∈ r • s}

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