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}