English
The egauge functional assigns to x the infimum of norms of scalars c such that x ∈ c · s.
Русский
Функционал egauge(x) задаёт инфимум нормы скаляров c таких, что x ∈ c · s.
LaTeX
$$$\mathrm{egauge}_{\mathbb{K}}(s,x) = \inf \{ \|c\|_e : x \in c \cdot s \}$$$
Lean4
/-- The Minkowski functional for vector spaces over normed fields.
Given a set `s` in a vector space over a normed field `𝕜`,
`egauge s` is the functional which sends `x : E`
to the infimum of `‖c‖ₑ` over `c` such that `x` belongs to `s` scaled by `c`.
The definition only requires `𝕜` to have a `ENorm` instance
and `(· • ·) : 𝕜 → E → E` to be defined.
This way the definition applies, e.g., to `𝕜 = ℝ≥0`.
For `𝕜 = ℝ≥0`, the function is equal (up to conversion to `ℝ`)
to the usual Minkowski functional defined in `gauge`. -/
noncomputable def egauge (𝕜 : Type*) [ENorm 𝕜] {E : Type*} [SMul 𝕜 E] (s : Set E) (x : E) : ℝ≥0∞ :=
⨅ (c : 𝕜) (_ : x ∈ c • s), ‖c‖ₑ
