Gauges, polars of convex functions, and obverses #
The gauge of a set C is γ(x ∣ C) = inf {a ≥ 0 ∣ x ∈ a • C}: the least dilation of C that
swallows x, and +∞ when none does. Gauges are exactly the nonnegative positively homogeneous
convex functions vanishing at 0, and C ↦ γ(· ∣ C) is a bijection from closed convex sets
containing 0 to closed gauges. Three polarity operations act here, each an involution on its
class: the polar k°(y) = inf {μ ≥ 0 ∣ ⟨x, y⟩ ≤ μ k(x)} of a gauge, the polar
f°(y) = inf {μ ≥ 0 ∣ ⟨x, y⟩ ≤ 1 + μ f(x)} of a nonnegative closed convex f with f 0 = 0, and
the obverse fᵒ(x) = inf {λ > 0 ∣ λ f(x / λ) ≤ 1}. On a gauge the first two agree, and the obverse
ties them to the Fenchel conjugate: f* = (f°)ᵒ. Two facts about polar sets are proved here too,
because the gauge is what makes them short: the recession cone of a closed convex set containing the
origin is the polar of its polar, and the polar of a sublevel set of a nonnegative convex function
is within a factor of two of the corresponding sublevel set of the conjugate.
Main definitions #
gaugeFn C,IsGauge k— the gauge,EReal-valued, and its characterising properties.polarGauge B k,polarFn B f,obverse f— the three operations above.polarFninfimises overepi f;polarFn_apply_eqrecovers the book's formula.IsPolarFn f— nonnegative, closed, convex,f 0 = 0: the classpolarFninverts.IsNorm k— a gauge that is finite, symmetric and positive off0;IsNorm.toSeminormbuilds the MathlibSeminorm.AbsorbsAll CandRayFree Cmakeγ(· ∣ C)a norm.epiPairing B,vNeg X— the pairing ofE × ℝwithF × ℝ, and vertical reflection.UpClosed S— upward closed subsets ofℝ, the shape of every admissible-scalar set here.
Main results #
gaugeEquiv,isGauge_iff— the correspondencek = γ(· ∣ C),C = {k ≤ 1}.recessionCone_eq_polarCone_polarSet,polarCone_linealitySpace— the recession cone ofCis the polar ofC°, and the lineality space ofCis the annihilator ofC°;finrank_vectorSpan_polarSet_add_linealityand its companion read these throughfinrankasdim C° = n - lin Candlin C° = n - dim C.polarSet_setOf_le_subset_and_subsettrapsα⁻¹ {f* ≤ α}between{f ≤ α}°and2 {f ≤ α}°.polarGauge_eq_supportFn,polarGauge_polarGauge,polarGaugeEquiv— the polar of a gauge is the support function of its unit level set, andk°° = cl k(Theorem 15.1 in [^1]).isNorm_iffidentifies the norms among the gauges.polarFn_polarFn,polarFnEquiv—f°° = cl f, sof ↦ f°is an involution on the nonnegative closed convex functions vanishing at the origin (Theorem 15.4 in [^1]).obverse_obverse,conj_eq_obverse_polarFn,polarFn_eq_obverse_conj— the obverse is an involution, andf°andf*are obverses of each other (Theorem 15.5 in [^1]);polarFn_conj_eq_conj_polarFnisf*° = f°*, andsetOf_polarFn_leis{f° ≤ α⁻¹} = α⁻¹ {f* ≤ α}.
Implementation notes #
gaugeFn is EReal-valued and infimises over a ≥ 0, so it is +∞ off ⋃ a • C; that is what
makes {γ ≤ c} equal c • C. Mathlib's gauge infimises over a > 0 into ℝ and returns 0
there instead — the two agree under absorbency (gaugeFn_eq_gauge) — while egauge is this same
infimum taken in ℝ≥0∞, whereas every function in this library is EReal-valued.
The book's admissible set for f°, {μ ≥ 0 ∣ ⟨x, y⟩ ≤ 1 + μ f(x) ∀ x}, is not closed: at μ = 0
the convention 0 · (+∞) = 0 imposes ⟨x, y⟩ ≤ 1 where f x = +∞, which nearby positive μ do
not. Quantifying over epi f gives a closed, upward closed set with the same infimum.
Divergences from the reference #
The sublevel-set inclusions are stated for any nonnegative convex f with f 0 ≤ 0, with no
closedness. isNorm_iff uses AbsorbsAll C and RayFree C where the book has 0 ∈ int C and C
bounded — equivalent readings in ℝⁿ — and does not assert that a norm is closed, which the book
obtains from the continuity of a finite convex function on ℝⁿ. gaugeFn_level_one needs only
nonnegativity, positive homogeneity and k 0 = 0, and gaugeFn_polarSet (γ(· ∣ C°) = δ*(· ∣ C))
needs only 0 ∈ C.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §14 and §15.
Infima of upward closed sets of reals #
Every definition in this file is an infimum ⨅ a ∈ S, (a : EReal) of a set S ⊆ ℝ of admissible
scalars, and every proof about it needs to convert ⨅ a ∈ S, a ≤ c into a statement about
membership in S. The two lemmas here are that conversion: it is unconditional in the form "every
d > c lies in S" once S is upward closed, and becomes "c ∈ S" once S is also closed.
If z ≤ d for every real d above r, then z ≤ r. The ≤ companion of
Tdaf.EReal.le_coe_of_forall_lt.
The gauge of a convex set #
γ(x | C) = inf {a ≥ 0 | x ∈ a • C}. The scalar 0 is admitted, and
0 • C = {0} for nonempty C, so γ(0 | C) = 0 for every nonempty C — that is what makes a
gauge vanish at the origin even when C does not contain it.
The gauge of a set C: γ(x | C) = inf {a ≥ 0 | x ∈ a • C}.
Named gaugeFn because it is neither of Mathlib's two Minkowski functionals; gaugeFn_eq_gauge
and gaugeFn_eq_egauge are the bridges, and the module docstring says why the EReal-valued
version is the one this development needs.
Instances For
The witness extractor: a strict upper bound for the gauge is witnessed by an admissible scalar. The infimum is not attained in general, so this is the only way in.
A gauge vanishes at the origin: 0 ∈ 0 • C as soon as C is nonempty.
Gauges #
A gauge is a nonnegative positively homogeneous convex function vanishing at the origin —
equivalently, a function whose epigraph is a convex cone containing the origin and no (x, μ) with
μ < 0. isGauge_iff is the other description: the gauges are exactly the γ(· | C) for nonempty
convex C.
A gauge: a nonnegative positively homogeneous convex function that vanishes at the origin.
A gauge is nonnegative.
- posHomogeneous : PosHomogeneous k
A gauge is positively homogeneous.
- convexFn : ConvexFn k
A gauge is convex.
A gauge vanishes at the origin. This is a genuine extra condition: it rules out
k ≡ +∞, which satisfies the other three.
Instances For
A gauge is the gauge of its own unit level set: γ(· | {k ≤ 1}) = k. Convexity is not
used — only nonnegativity, positive homogeneity, and k 0 = 0.
This is the half of the gauge/set correspondence that needs no topology; the other half,
level_one_gaugeFn, does.
The gauges are exactly the gauge functions of the nonempty convex sets. {x | k x ≤ 1} is
the canonical choice of set, and it is the only closed one containing the origin (gaugeEquiv).
Gauges of sets containing the origin #
The admissible-scalar set {a ≥ 0 | x ∈ a • C} is upward closed exactly because a • C ⊆ b • C
for 0 ≤ a ≤ b when C is convex and contains the origin. Everything quantitative about gaugeFn
goes through that.
Closed gauges #
For a closed convex set containing the origin the level sets of the gauge are the dilates
themselves, {x | γ(x | C) ≤ c} = c • C for c > 0, and the gauge is closed. gaugeEquiv
packages the resulting one-to-one correspondence.
The level sets of a closed gauge are the dilates. γ(x | C) ≤ c exactly when x ∈ c • C,
for c > 0 and C closed convex containing the origin.
The restriction to c > 0 is essential: {x | γ(x | C) ≤ 0} is the recession cone of C, not
0 • C = {0}.
The sublevel sets of a closed gauge, for a positive level.
The unit level set of the gauge recovers the set: {x | γ(x | C) ≤ 1} = C for a closed
convex set containing the origin. Together with gaugeFn_level_one this is the one-to-one
correspondence between closed gauges and closed convex sets containing the origin.
The gauge of a closed convex set containing the origin is lower semicontinuous: each of its
sublevel sets is an intersection of dilates of C.
The gauge correspondence: the closed gauges on E are in bijection with the closed convex
subsets of E containing the origin, by C ↦ γ(· | C) and k ↦ {x | k x ≤ 1}.
This is the gauge analogue of supportEquiv (Duality/Support.lean).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The gauge of a polar set #
The gauge of C° is the support function of C. The book states this for a closed convex C
containing the origin, as part of the polarity theorem; only 0 ∈ C is used.
The gauge of the polar set is the support function: γ(· | C°) = δ*(· | C).
Only 0 ∈ C is needed — neither convexity nor closedness — because 0 ∈ C is exactly what makes
δ*(· | C) nonnegative, and the two infima then agree scalar by scalar.
The recession cone and the lineality space as polars #
0⁺C and the closed convex cone generated by C° are polar to each other, and the lineality space
of C is the annihilator of C°. The classical proof reads the recession cone off as the largest
closed convex cone inside C; the argument here identifies it directly as a polar, which needs only
the bipolar theorem.
The easy half: a recession direction of a set containing the origin is nonpositively paired with every element of the polar.
The recession cone is the polar of the polar set, for a closed convex set containing the origin.
The recession cone of a polar set is a polar cone: 0⁺(C°) = C° read as a cone polar
rather than a set polar, for a closed convex C containing the origin.
The previous result applied to C°, whose bipolar is C (polarSet_polarSet). Both spaces are
topologised here, because the recession cone being computed lives in F.
The recession cone of C and the closed convex cone generated by C° are polar to each
other.
The lineality space of a closed convex set containing the origin is the annihilator of its polar.
The polar of the lineality space of C is the closed subspace generated by C°, the dual
form of the previous result.
The dimension relations for a polar set #
dim C° = n - lin C and lin C° = n - dim C. They are the orthogonality above read through
finrank: the polar of a subspace is its annihilator, and the annihilator of a subspace of a
finite-dimensional space has the complementary dimension.
vectorSpan_eq_span_of_zero_mem — the affine and linear hulls of a set through the origin
agree — is Tdaf.vectorSpan_eq_span_of_zero_mem in Tdaf/LinearAlgebra/Subspace.lean. It has no
convexity in it and three unrelated developments want it.
The polar of a subspace has the complementary dimension. This is rank–nullity for the map
F → M* that a compatible pairing induces: it is onto because B.flip is onto E* (compatibility,
plus the automatic continuity of a functional in finite dimensions) and restriction E* → M* is
onto, and its kernel is the polar of M.
dim C° = n - lin C for a closed convex set containing the origin, stated without
truncated subtraction, as dim C° + lin C = n.
The subspace generated by C° is the polar of the lineality space of C
(polarCone_linealitySpace; the closure there is redundant in finite dimensions), and the affine
hull of C° is its linear hull because 0 ∈ C°.
lin C° = n - dim C, again without truncated subtraction. It is the first relation applied
to the polar pair the other way round, using C°° = C.
The book's third relation, rank C° = rank C, is the difference of the two: both dim C° + lin C
and dim C + lin C° equal n.
The polar of a sublevel set #
For a nonnegative convex function vanishing at the origin, the polar of a sublevel set and the
corresponding sublevel set of the conjugate are within a factor of 2 of each other.
A convex function that is nonpositive at the origin is subhomogeneous for factors in
[0, 1]: f (t • x) ≤ t * r whenever f x ≤ r.
The conjugate of a nonnegative function vanishing at the origin again vanishes at the origin.
The first inclusion (in scaled form): α • {f ≤ α}° ⊆ {f* ≤ α}.
The book proves this through the positively homogeneous function generated by f* + α. The direct
argument is shorter: for f x > α the point (α / f x) • x lies in the sublevel set, and rescaling
the inequality it satisfies gives ⟨x, y⟩ ≤ f x.
The second inclusion (in scaled form): {f* ≤ α} ⊆ (2α) • {f ≤ α}°. This half is
Fenchel's inequality and nothing else.
The two inclusions together: {f ≤ α}° ⊆ α⁻¹ • {f* ≤ α} ⊆ 2 • {f ≤ α}°.
The polar of a gauge #
k°(y) = inf {μ ≥ 0 | ⟨x, y⟩ ≤ μ k(x) for all x}. The content of this section is that k° is the
support function of {k ≤ 1}, hence a closed gauge, and that it is γ(· | C°) whenever
k = γ(· | C).
The polar of a gauge: k°(y) = inf {μ ≥ 0 | ⟨x, y⟩ ≤ μ k(x) for every x}.
The product μ * k x is EReal multiplication, so 0 * (+∞) = 0; that makes μ = 0 admissible
only when ⟨·, y⟩ ≤ 0 everywhere, which is the classical reading of the μ* = 0 case. The infimum
is insensitive to the convention, since the admissible set is an up-set in [0, ∞).
Equations
Instances For
The polar of a gauge is the support function of its unit level set.
Convexity of k is not used; nonnegativity, positive homogeneity and k 0 = 0 are.
The polar of a gauge is a gauge.
The polar of a gauge is a closed gauge.
Polarity of gauges is polarity of sets: if k = γ(· | C) for a nonempty convex set C,
then k° = γ(· | C°).
C is neither required to contain the origin nor to be closed — the polar set does not
distinguish C from {x | γ(x | C) ≤ 1}, which does contain the origin.
For a convex set containing the origin, the gauge function and the support function of C are
gauges polar to each other.
The pairing of E × ℝ with F × ℝ #
Polarity of a function is polarity of its epigraph, one dimension higher, so it needs a pairing of
E × ℝ with F × ℝ. prodPairing (Duality/Pairing.lean) supplies it once ℝ is paired with
itself, and mulPairing is that self-pairing.
The pairing under which epigraphs are polarised: ⟨(x, ν), (y, μ)⟩ = ⟨x, y⟩ + ν μ.
An abbrev so that the prodPairing instances of Duality/Pairing.lean remain visible to
instance search (a def would hide them — LinearMap.flip is the same trap).
Equations
Instances For
Vertical reflection: (x, μ) ↦ (x, -μ).
Equations
Instances For
Polarity commutes with vertical reflection: (A S)° = A (S°), because A is self-adjoint
for epiPairing.
The polar of a nonnegative convex function #
f°(y) = inf {μ ≥ 0 | ⟨x, y⟩ ≤ 1 + μ f(x) for all x}. The definition below is the ∞-free reading
of that formula, quantifying over the epigraph of f rather than over f itself: μ is admissible
when ⟨x, y⟩ - ν μ ≤ 1 for every (x, ν) ∈ epi f. This says exactly that (y, -μ) lies in the
polar of epi f, which is what the classical proof uses, and polarFn_apply_eq shows it agrees
with the original formula.
The polar of a nonnegative convex function vanishing at the origin:
f°(y) = inf {μ ≥ 0 | ⟨x, y⟩ ≤ 1 + μ f(x) for all x}, in the epigraph form.
Equations
Instances For
The admissible-multiplier set is upward closed: the vertical coordinates of epi f are
nonnegative because f is.
The admissible-multiplier set is closed: it is an intersection of closed half-lines.
The original formula for the polar, recovered from the epigraph form: f°(y) is the
infimum of the μ ≥ 0 with ⟨x, y⟩ ≤ 1 + μ f(x) for every x.
The two admissible sets differ only at μ = 0, where the convention 0 · (+∞) = 0 imposes a
condition off dom f that the epigraph form does not; since both are up-sets in [0, ∞), the
infima agree.
Closures of nonnegative functions #
A nonnegative function has a nonnegative lower semicontinuous hull, so the exceptional ⊥ branch
of clFn never fires and cl f is computed by the closure of the epigraph.
For a nonnegative function the closure is the lower semicontinuous hull: the exceptional
branch of clFn cannot fire.
A nonnegative function with a closed epigraph is closed.
For a nonnegative function the epigraph of the closure is the closure of the epigraph.
A nonnegative closed function has a closed epigraph.
Closedness of a nonnegative function, as a statement about its epigraph.
The bipolar of a function #
The epigraph of f° is the vertical reflection of the polar of the epigraph of f, so the
bipolar theorem of Duality/Polar.lean, applied in E × ℝ, gives f°° = cl f at once.
The polar of a nonnegative function vanishing at the origin is closed, because polar sets are closed.
The bipolar is the closure: for a nonnegative convex function vanishing at the origin,
f°° = cl f.
The outer polar is taken with respect to B.flip, since f° lives on F.
The class on which the polar is an involution #
The nonnegative closed convex functions that vanish at the origin.
The nonnegative closed convex functions vanishing at the origin. These are exactly the
functions that arise as polars (isPolarFn_polarFn and polarFn_polarFn), and f ↦ f° is an
involution on them.
A polar is nonnegative.
A polar vanishes at the origin.
- convexFn : ConvexFn f
A polar is convex.
- closedFn : ClosedFn f
A polar is closed.
Instances For
A closed gauge is an IsPolarFn.
The polar of an IsPolarFn is again one: the four conditions are inherited.
f ↦ f° is a symmetric one-to-one correspondence on the nonnegative closed convex
functions vanishing at the origin.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The involution k°° = cl k #
The book derives this from polarity of the unit level set. Here it is a special case of
polarFn_polarFn instead: on a gauge the two polar operations agree (polarFn_eq_polarGauge),
because the 1 + in the definition of f° is invisible to a positively homogeneous function.
The two polar operations agree on gauges: the 1 + in the definition of f° is invisible
to a positively homogeneous f.
The admissible set of polarGauge is contained in that of polarFn, and the two differ at most
at 0; since both are up-sets in [0, ∞), the infima agree.
k°° = cl k for a gauge k.
Polarity as a correspondence, for gauges and for sets #
k ↦ k° is a symmetric one-to-one correspondence on the closed gauges.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Two closed convex sets containing the origin are polar to each other exactly when their gauges are.
The obverse #
g(x) = inf {λ > 0 | (fλ)(x) ≤ 1}. The observation that replaces the geometric argument of the
book is that this is a gauge value one dimension higher: g(x) = γ((x, 1) | epi f). Everything
about the obverse then follows from the gauge API.
The obverse of f, Rockafellar's term: g(x) = inf {λ > 0 | (fλ)(x) ≤ 1}.
Equations
Instances For
The admissible set of the obverse is the admissible set of the gauge of epi f at height one:
the scalar 0 is never admissible, because (x, 1) ∉ 0 • S.
The obverse of a nonnegative closed convex function #
The epigraph of an IsPolarFn is convex, closed, and contains the origin — the hypotheses of
the closed gauge theory.
The defining inequality of the obverse, for an IsPolarFn: g(x) ≤ ν exactly when
(fν)(x) ≤ 1, for ν > 0.
The obverse vanishes at the origin.
The obverse of a nonnegative closed convex function vanishing at the origin is another one.
The obverse is an involution: f is the obverse of its obverse.
The polar, the conjugate and the obverse #
The book obtains these from the symmetry of a closed convex cone in R^(n+2) under exchanging two
coordinates. Here the single computation f* = (f°)ᵒ (conj_eq_obverse_polarFn) does the work: it
is a level-set comparison, and everything else follows from it together with obverse_obverse and
polarFn_polarFn.
The conjugate of an IsPolarFn is again one: nonnegativity, vanishing at the origin,
convexity and closedness are all apparent from the definition of f*.
The conjugate is the obverse of the polar: f* = (f°)ᵒ.
Both sides are nonnegative, so it suffices to compare them against the positive reals, and there
the statement unwinds to ⟨x, y⟩ - α ≤ ν for every (x, α) ∈ epi f.
The polar is the obverse of the conjugate: f° = (f*)ᵒ. Together with
conj_eq_obverse_polarFn, f° and f* are the obverses of each other.
The obverse of f is f*°, the expression from which the book derives the formula
g(x) = inf {λ > 0 | (fλ)(x) ≤ 1}.
g° = f*, where g is the obverse of f.
f° = g*, where g is the obverse of f.
The polar and the conjugate commute: f*° = f°*.
The level sets of the obverse: {g ≤ α} = α {f ≤ α⁻¹} for α > 0.
The level sets of the polar and of the conjugate: {f° ≤ α⁻¹} = α⁻¹ {f* ≤ α} for
α > 0. This is the middle set of polarSet_setOf_le_subset_and_subset.
Norms #
A gauge that is finite everywhere, symmetric, and positive away from the origin is a norm. The
book states the correspondence with the symmetric closed bounded convex sets C with
0 ∈ int C. Two of those three conditions on C are the finite-dimensional readings of conditions
that make sense in general, and it is the general readings that are proved here:
- "
0 ∈ int C", which inRⁿsays thatCcontains a positive multiple of every vector, isAbsorbsAll C; - "
Cis bounded", which inRⁿsays thatCcontains no half-line, isRayFree C.
Closedness is not part of the correspondence here. The book gets it from the continuity of a
finite convex function on Rⁿ, which is genuinely finite-dimensional; in an infinite-dimensional
space a finite symmetric positive gauge need not be lower semicontinuous.
C absorbs every point: every x lies in some nonnegative dilate of C. This is the
elementary form in which absorbency enters the gauge; absorbsAll_of_absorbent relates it to
Mathlib's Absorbent.
Instances For
C contains no ray: for every x ≠ 0 some positive multiple of x is outside C.
Instances For
A norm in Rockafellar's sense: a gauge that is finite everywhere, symmetric, and positive away from the origin.
A norm is finite.
A norm is symmetric.
A norm is positive away from the origin.
Instances For
The gauge of a symmetric convex set that absorbs every point and contains no ray is a norm.
The unit level set of a norm is a symmetric convex set that absorbs every point and contains no ray.
The norms are exactly the gauges of the symmetric convex sets that absorb every point and contain no ray.
A norm is a Seminorm #
Mathlib's Seminorm 𝕜 E is purely algebraic — subadditive, absolutely homogeneous, and nothing
about a topology — so a Rockafellar norm is one on the nose. It is not a NormedSpace norm
unless it happens to be continuous, which in general it is not; that is the distinction, and it is
the only one.
A norm is absolutely homogeneous, not merely positively homogeneous: symmetry upgrades
k (a • x) = a * k x for a > 0 to k (a • x) = |a| * k x for every real a.
A Rockafellar norm is a Seminorm. Seminorm ℝ E asks for subadditivity (which follows
from convexity and positive homogeneity), invariance under negation, and absolute homogeneity —
all three of which IsNorm carries, and none of which mentions a topology.
This is the bridge that lets a surface over ℝⁿ hand a Rockafellar norm to Mathlib's seminorm
API. What it does not give is a NormedSpace: for that the norm must be continuous, and
continuity of a finite convex function is a finite-dimensional fact.
Equations
- hk.toSeminorm = { toFun := fun (x : E) => (k x).toReal, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, smul' := ⋯ }
Instances For
The Seminorm really is k.
The polar of a norm #
The polar of a set on which every ⟨·, y⟩ is bounded above absorbs every point.
If the pairing separates the points of F using C alone, the polar of C contains no
ray.
The polar of a norm is a norm.
The two hypotheses are the general forms of "C is bounded" and "0 ∈ int C": boundedness in the
pairing sense makes the polar absorbing, and separation of F by C makes the polar ray-free.
gaugeFn is Mathlib's gauge, wherever the latter is meaningful. Mathlib's gauge takes
the infimum over positive scalars in ℝ, so on a set that does not absorb x it returns
sInf ∅ = 0 rather than +∞; under an absorbency hypothesis the two agree.
Mathlib's Absorbent implies the elementary absorbency AbsorbsAll.