Rockafellar, §15: Polars of Convex Functions #
Gauges and their polars, norms and Minkowski metrics, the gauge-like functions, and the polar f°
and obverse of a nonnegative convex function vanishing at the origin. All 11 numbered results of
§15 are formalized.
The section's definitions #
- A gauge is a nonnegative positively homogeneous convex
kwithk 0 = 0, the backbone'sIsGauge.gauge_iff_exists_gaugeFnis Rockafellar's other description — the gauges are exactly theγ(· | C) = inf {μ ≥ 0 | x ∈ μ C}for non-empty convexC— andgaugeFn_apply_rnis that infimum written out. - The polar
k°of a gauge ispolarGauge (pairing n) k, withpolarGauge_apply_rnthe book's formulainf {μ* ≥ 0 | ⟨x, x*⟩ ≤ μ* k(x) for all x}. - A norm is a gauge that is finite, symmetric and positive off the origin:
IsNorm, whose four fields are the book's conditions (a)–(d).IsNorm.toSeminormsays a Rockafellar norm is a MathlibSeminorm. - A Minkowski metric is
IsMinkowskiMetric, defined here: a metric invariant under translation and linear along segments. - Gauge-like is the backbone's
IsGaugeLike:f 0 = inf f, and the sublevel sets above that infimum are all positive multiples of a single set. - Positively homogeneous of degree
pisPosHomogeneousDeg. - The polar
f°of a nonnegative convex function vanishing at the origin ispolarFn (pairing n) f, withpolarFn_apply_rngiving the book'sinf {μ* ≥ 0 | ⟨x, x*⟩ ≤ 1 + μ* f(x) for all x}. - The obverse is
obverse f = inf {λ > 0 | (fλ)(x) ≤ 1}, unfolded byobverse_apply_rn.
The unnumbered running text is recorded too: a gauge recovered from its own unit level set and the
uniqueness of the closed convex set with a given closed gauge; the polar-pair inequality
⟨x, x*⟩ ≤ k(x) k°(x*) with its Schwarz instance, the Euclidean norm being self-polar; the
correspondence between norms and Minkowski metrics; the level sets of the obverse; and the closing
display {f° ≤ α⁻¹} = α⁻¹ {f* ≤ α}.
References #
- R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §15.
The definitions of §15 #
Rockafellar's gauge function (§15, p. 128): γ(x | C) = inf {μ ≥ 0 | x ∈ μ C}. This is the
backbone's gaugeFn C, and the equation is the definition unfolded.
Rockafellar §15, p. 128: the gauges are exactly the functions γ(· | C) for a non-empty
convex set C.
Rockafellar §15, p. 128: "one always has γ(· | C) = k for C = {x | k(x) ≤ 1}".
Closedness of k is not needed.
Rockafellar's polar of a gauge (§15, p. 128):
k°(x*) = inf {μ* ≥ 0 | ⟨x, x*⟩ ≤ μ* k(x), ∀ x}. This is the backbone's polarGauge (pairing n) k,
and the equation is the definition unfolded.
Rockafellar's polar of a nonnegative convex function vanishing at the origin (§15, p. 136):
f°(x*) = inf {μ* ≥ 0 | ⟨x, x*⟩ ≤ 1 + μ* f(x), ∀ x}.
The backbone's polarFn quantifies over epi f rather than over x, because Rockafellar's
admissible set is not closed at μ* = 0; polarFn_apply_eq is the identification.
Rockafellar's obverse (§15, p. 137): g(x) = inf {λ > 0 | (fλ)(x) ≤ 1}, where
(fλ)(x) = λ f(λ⁻¹x) is the right scalar multiple of §5.
Theorem 15.1 #
Theorem 15.1, third assertion: if k = γ(· | C) for a non-empty convex set
C, then k° = γ(· | C°).
Theorem 15.1, first assertion: the polar of a gauge is a gauge.
Theorem 15.1, first assertion: the polar of a gauge is closed.
Theorem 15.1, second assertion: k°° = cl k.
The backbone derives this from Theorem 15.4 rather than by Rockafellar's route through Theorem 14.5 and the unit level set.
Corollary 15.1.1 #
Rockafellar §15, p. 128, the correspondence k(x) = γ(x | C), C = {x | k(x) ≤ 1} between
the closed convex sets containing the origin and the closed gauges; Corollary 15.1.1 quantifies
over this class.
Equations
Instances For
Corollary 15.1.1, first assertion: k ↦ k° induces a one-to-one symmetric
correspondence in the class of all closed gauges on ℝⁿ.
Equations
Instances For
Corollary 15.1.1, second assertion: two closed convex sets containing the origin are polar to each other if and only if their gauge functions are polar to each other.
Corollary 15.1.2 #
Corollary 15.1.2: if C is a closed convex set containing the origin, the gauge function
of C and the support function of C are gauges polar to each other. Stated without the
closedness the book assumes.
Corollary 15.1.2, the other half of "polar to each other": the polar of the support function of a closed convex set containing the origin is its gauge function.
This is corollary_15_1_2 fed to theorem_15_1_polar_polar, closedness of γ(· | C) removing the
closure.
The polar-pair inequality #
Rockafellar §15, p. 129: gauges polar to each other satisfy ⟨x, x*⟩ ≤ k(x) k°(x*) for
every x ∈ dom k and x* ∈ dom k°. The two values are named as reals because the right-hand side
is a product of reals.
Theorem 15.2 #
Rockafellar §15, p. 131, the opening of the proof of Theorem 15.2: "norms, being finite convex functions, are continuous (Theorem 10.1)".
ConvexFn.continuous_of_dom_eq_univ is the backbone's Corollary 10.1.1.
Rockafellar §15, p. 131: a norm on ℝⁿ is a closed function. The backbone declines to
prove this in general — closedness of a norm comes from Theorem 10.1, which is
finite-dimensional.
The unit level set of a norm on ℝⁿ contains the origin in its interior — Rockafellar's
0 ∈ int C, obtained from continuity rather than from Corollary 6.4.1.
The unit level set of a norm on ℝⁿ is bounded — Rockafellar's "C is bounded", obtained from
Theorem 8.4 (isBounded_iff_recessionCone_eq_zero) and ray-freeness.
Theorem 15.2, first half: the gauge of a symmetric closed bounded convex set
C with 0 ∈ int C is a norm.
The book's two set conditions are translated into the backbone's AbsorbsAll and RayFree here —
Corollary 6.4.1 and Theorem 8.4, each in the easy direction.
Theorem 15.2, second half: the unit level set of a norm is a symmetric closed bounded convex set containing the origin in its interior.
Theorem 15.2: the correspondence, in the direction k ↦ C ↦ γ(· | C).
Theorem 15.2: the correspondence, in the direction C ↦ γ(· | C) ↦ C. This is
also the uniqueness clause of §15, p. 128: a closed gauge determines the closed convex set
containing the origin.
Theorem 15.2, last assertion: the polar of a norm is a norm. The two side conditions are the
pairing readings of "C is bounded" and "0 ∈ int C".
The Euclidean norm, and the Schwarz inequality #
The Euclidean norm is a norm in Rockafellar's sense (§15, p. 130).
Rockafellar §15, p. 130: the Euclidean norm is its own polar, being both the gauge function and the support function of the Euclidean unit ball.
Minkowski metrics #
A Minkowski metric on ℝⁿ (Rockafellar §15, p. 132): a metric ρ — conditions (a), (b),
(c) — that is in addition invariant under translation (d) and linear along line segments (e).
- pos (x y : TdafSurface.Rn n) : x ≠ y → 0 < rho x y
(a)
ρ(x, y) > 0whenx ≠ y. (a)
ρ(x, x) = 0.(b)
ρis symmetric.(c) the triangle inequality.
(d) distances are invariant under translation.
- segment (x y : TdafSurface.Rn n) (l : ℝ) : l ∈ Set.Icc 0 1 → rho x ((1 - l) • x + l • y) = l * rho x y
(e) distances behave linearly along line segments.
Instances For
Rockafellar §15, p. 132: a norm k defines a Minkowski metric ρ(x, y) = k(x - y).
Rockafellar leaves the verification to the reader. Written through IsNorm.toSeminorm, whose
subadditivity is Theorem 4.7 and whose absolute homogeneity is IsNorm.apply_smul.
Rockafellar §15, p. 132: a Minkowski metric is determined by the norm x ↦ ρ(x, 0), since
translation invariance gives ρ(x, y) = ρ(x - y, 0). This is the uniqueness half of the
correspondence.
Theorem 15.3 #
Theorem 15.3, first assertion: a function is a gauge-like closed proper convex
function if and only if it is g ∘ k for a closed gauge k and a non-constant nondecreasing lower
semicontinuous convex function g on [0, +∞] which is finite at some ζ > 0.
Theorem 15.3, second assertion: f* (x*) = g⁺(k°(x*)), where g⁺ is the monotone
conjugate of g.
Theorem 15.3, second assertion: "if f is of this type, then f* is
gauge-like too".
Corollary 15.3.1 #
Corollary 15.3.1, first assertion: a closed proper convex function f is positively
homogeneous of degree p, 1 < p < ∞, if and only if f = (1/p) k^p for a closed gauge k. The
book's (1/p) k^p is monotoneComp (powHalfLine p) k.
Corollary 15.3.1, second assertion: [(1/p) k^p]* = (1/q) (k°)^q, where
(1/p) + (1/q) = 1.
Corollary 15.3.2 #
Corollary 15.3.2, first assertion: (pf)^{1/p} is a closed gauge.
Corollary 15.3.2: the polar of the closed gauge (pf)^{1/p} is (qf*)^{1/q}.
Corollary 15.3.2, the Hölder-type inequality
⟨x, x*⟩ ≤ [p f(x)]^{1/p} [q f*(x*)]^{1/q} on dom f × dom f*.
Corollary 15.3.2, last assertion: the closed convex sets {f ≤ 1/p} and
{f* ≤ 1/q} are polar to each other.
Theorem 15.4 #
Theorem 15.4: the polar f° of a nonnegative convex function vanishing at the
origin is nonnegative.
Theorem 15.4: f° vanishes at the origin.
Theorem 15.4: f° is convex.
Theorem 15.4: f° is closed.
Theorem 15.4, second assertion: f°° = cl f.
Note that f is not assumed closed: this is the statement that makes f ↦ f° an involution on
the closed members of the class.
Corollary 15.4.1: f ↦ f° induces a symmetric one-to-one correspondence in
the class of all nonnegative closed convex functions vanishing at the origin.
IsPolarFn is that class.
Instances For
Theorem 15.5 #
Theorem 15.5, first assertion: the obverse g of a nonnegative closed convex
function f vanishing at the origin has those same three properties.
Theorem 15.5, first assertion: f is the obverse of its obverse.
Theorem 15.5: f° = g*, where g is the obverse of f.
Theorem 15.5: f* = g°, where g is the obverse of f.
Theorem 15.5, last assertion: f* is the obverse of f°.
Theorem 15.5, last assertion: f° is the obverse of f*.
Corollary 15.5.1: f*° = f°* for a nonnegative closed convex function f
vanishing at the origin.
The level sets at the end of §15 #
Rockafellar §15, p. 139: {g ≤ α} = α {f ≤ α⁻¹} for α > 0, where g is the obverse
of f.
Rockafellar §15, the last display of the section: {f° ≤ α⁻¹} = α⁻¹ {f* ≤ α} for α > 0.
This set is the middle set of the inclusions of Theorem 14.7.