The Minkowksi functional #
This file defines the Minkowski functional, aka gauge.
The Minkowski functional of a set
s is the function which associates each point to how much you
need to scale
x to be inside it. When
s is symmetric, convex and absorbent, its gauge is
a seminorm. Reciprocally, any seminorm arises as the gauge of some set, namely its unit ball. This
induces the equivalence of seminorms and locally convex topological vector spaces.
Main declarations #
For a real vector space,
gauge: Aka Minkowksi functional.
gauge s xis the least (actually, an infimum)
x ∈ r • s.
gauge_seminorm: The Minkowski functional as a seminorm, when
sis symmetric, convex and absorbent.
Minkowski functional, gauge
The Minkowski functional. Given a set
s in a real vector space,
gauge s is the functional
x : E to the smallest
r : ℝ such that
x is in
s scaled by
An alternative definition of the gauge using scalar multiplication on the element rather than on the set.
If the given subset is
absorbent then the set we take an infimum over in
gauge is nonempty,
which is useful for proving many properties about the gauge.
The gauge evaluated at
0 is always zero (mathematically this requires
0 to be in the set
but, the real infimum of the empty set in Lean being defined as
0, it holds unconditionally).
The gauge is always nonnegative.
gauge s as a seminorm when
s is balanced, convex and absorbent.
- gauge_seminorm hs₀ hs₁ hs₂ = seminorm.of (gauge s) _ _