Subgradients, normal cones and directional derivatives #
Over a dual pair B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ, a subgradient of f at x is a y : F for which the
affine function z ↦ f x + ⟨z - x, y⟩ minorizes f; equivalently, one whose graph is a
non-vertical supporting hyperplane to epi f at (x, f x). The set of them is the
subdifferential ∂f x. The definition is deliberately algebraic — a system of weak linear
inequalities, one for each z — and no topology enters until the closure of f does. This file
also introduces the normal cone N_C(x) and the one-sided directional derivative f'(x; y), and
develops the elementary theory of all three.
Main definitions #
subgradient B f x— the subdifferential∂f x, a subset ofF;subgradientRel B fis its graph as aSetRel E F, anddomSubgradient B fthe set of points where it is non-empty.normalCone B C x— the normal coneN_C(x), bundled bynormalPointedCone.dirDeriv f x y— the directional derivativef'(x; y), as the infimum of the difference quotient. Meaningful only wheref xis finite; see the implementation notes.
Main results #
Proper.mem_subgradient_tfae—y ∈ ∂f x, attainment of the supremum of⟨·, y⟩ - fatx, and equality in Fenchel's inequality at(x, y)say the same thing (Theorem 23.5 in [^1]). All the individual implications but the last are unconditional.subgradientRel_conj_eq_inv— for closed proper convexf, the graph of∂f*is the flip of the graph of∂f;subgradient_clFn—∂(cl f) x = ∂f xwhereverfis subdifferentiable.subgradient_indicatorFn—∂δ(· | C) x = N_C(x)forx ∈ C;subgradient_supportFn— the subgradients ofδ*(· | C)atyare the maximizers of⟨·, y⟩overC.monotoneOn_sub_div,posHomogeneous_dirDeriv,convexFn_dirDeriv— the difference quotient is nondecreasing in the step;f'(x; ·)is positively homogeneous and convex.mem_subgradient_iff_le_dirDeriv,conj_dirDeriv,clFn_dirDeriv—∂f xis where⟨·, y⟩ ≤ f'(x; ·), andcl f'(x; ·)is the support function of∂f x(Theorem 23.2 in [^1]).proper_of_mem_subgradient— subdifferentiability at a point of finiteness forces properness.
Implementation notes #
∂f is available both pointwise and as a relation. The monotonicity and Legendre theory is about
the graph, and with subgradientRel the inversion reads literally as ∂(f*) = (∂f)⁻¹. ∂f x is
not bundled as a convex set: convexity is unconditional but closedness needs a continuous pairing,
and a bundled object would carry that hypothesis as data. N_C(x) is bundled, being a cone for
every C and x.
The finiteness hypothesis on dirDeriv is not removable: EReal has ⊤ - ⊤ = ⊥, so off dom f
the difference quotient is ⊥ in every direction and f'(x; 0) = 0 fails. Statements that
mention a value of f'(x; ·) therefore carry f x ≠ ⊤ and f x ≠ ⊥; positive homogeneity is
the exception, being a reindexing of the infimum.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §23.
Definitions #
The subdifferential of f at x with respect to the pairing B: the set of y : F
satisfying the subgradient inequality f z ≥ f x + ⟨z - x, y⟩ for every z.
Geometrically, when f x is finite, y is a subgradient exactly when the graph of the affine
function z ↦ f x + ⟨z - x, y⟩ is a non-vertical supporting hyperplane to epi f at
(x, f x).
Instances For
The graph of the subdifferential: the multivalued mapping ∂f : x ↦ ∂f x, as a
SetRel E F. This is the object the monotonicity and duality theory is about, and what
conjugation inverts.
Equations
- Tdaf.ConvexAnalysis.subgradientRel B f = {p : E × F | p.2 ∈ Tdaf.ConvexAnalysis.subgradient B f p.1}
Instances For
The normal cone to C at x: the y : F making a non-acute angle with every direction
z - x pointing from x into C. Introducing N_C(x) as ∂δ(x | C) would leave it empty for
x ∉ C; here it is defined for every x, which is what makes it a pointed cone with no
hypothesis. The price is the x ∈ C in subgradient_indicatorFn.
Instances For
The normal cone as a pointed convex cone, with no hypothesis on C or on x.
Equations
- Tdaf.ConvexAnalysis.normalPointedCone B C x = { carrier := Tdaf.ConvexAnalysis.normalCone B C x, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Instances For
The subdifferential is a convex set, with no hypothesis on f: it is an intersection of
half-spaces of F, one for each z.
A point with a subgradient lies in the effective domain: were f x = ⊤, the subgradient
inequality would read ⊤ ≤ f z for every z and force f ≡ ⊤, which properness forbids.
dom ∂f: the set of points at which f has at least one subgradient.
Equations
- Tdaf.ConvexAnalysis.domSubgradient B f = {x : E | (Tdaf.ConvexAnalysis.subgradient B f x).Nonempty}
Instances For
Subgradients, conjugates and Fenchel's inequality #
Attainment written as an equation: y ∈ ∂f x exactly when f* y = ⟨x, y⟩ - f x. This is the
∞ - ∞-free reading of equality in Fenchel's inequality.
The same in the additive form f x + f* y ≤ ⟨x, y⟩. Unconditional: adding a real number is
an order isomorphism of EReal, so no ∞ - ∞ arises.
y ∈ ∂f x exactly when Fenchel's inequality holds with equality at (x, y). Properness is
not decorative: for f ≡ ⊤ every y is a subgradient at every x, while f* ≡ ⊥ and so
f x + f* y = ⊤ + ⊥ = ⊥ ≠ ⟨x, y⟩.
The four equivalent forms of subgradient membership: for a proper f the conditions
- (a)
y ∈ ∂f x; - (b)
⟨·, y⟩ - fattains its supremum atx; - (c)
f x + f* y ≤ ⟨x, y⟩; - (d)
f x + f* y = ⟨x, y⟩
are equivalent. Convexity of f is nowhere used; properness is needed only to close the loop back
from (d).
x ∈ ∂f* y and y ∈ ∂f x agree at every x where f coincides with its biconjugate — for a
closed proper convex f, everywhere.
At a point where f is subdifferentiable it agrees with its biconjugate. No topology and no
convexity are needed.
A function subdifferentiable at a point where it is finite is proper. The subgradient
inequality exhibits a finite affine minorant, ruling out the value ⊥.
The same in the "subdifferentiable" phrasing.
A proper function has no subgradients off its effective domain. Unlike the finer statements
about where ∂f is non-empty, this involves no relative interiors.
Indicator functions, normal cones and polar cones #
For a pointed convex cone K, y is a subgradient of δ(· | K) at x exactly when x ∈ K,
y lies in the polar cone K° = N_K(0), and ⟨x, y⟩ = 0. The classical route assumes K closed
and goes through δ(· | K)* = δ(· | K°); the direct argument — put z = 0 and z = x + x into
the subgradient inequality — needs no topology, so K is arbitrary here.
Closedness of the subdifferential #
The subdifferential is closed once every ⟨z, ·⟩ : F → ℝ is continuous — automatic in ℝⁿ,
and here the instance closedFn_conj also asks for.
The directional derivative #
The one-sided directional derivative f'(x; y), as the infimum over a > 0 of the
difference quotient. The quotient is nondecreasing in a for convex f finite at x, so the
infimum is the limit as a ↓ 0, the classical definition. Off dom f the expression degenerates
to ⊥ in every direction.
Instances For
f'(x; ·) is positively homogeneous. Unlike its other basic properties this needs no
hypothesis: it is the reindexing a ↦ a * c of the defining infimum.
For convex f finite at x, the difference quotient is nondecreasing in the step a. This
is what makes the infimum defining dirDeriv the limit as a ↓ 0.
The form in which that monotonicity is consumed: if f'(x; y) < m then
f (x + a • y) ≤ f x + m * a for every sufficiently small a > 0.
-f'(x; -y) ≤ f'(x; y). No ≠ ⊥ hypothesis on f'(x; ·) appears, although
PosHomogeneous.neg_le carries one: f'(x; ·) really can take the value ⊥.
The subdifferential and the directional derivative #
y is a subgradient of f at x exactly when the linear function ⟨·, y⟩ is majorized by
the directional derivative f'(x; ·). Neither convexity of f nor monotonicity of the difference
quotient is used.
Dually, the conjugate of f'(x; ·) is the indicator of ∂f x. Neither convexity of f nor
any topology is needed.
Conjugate subdifferentials, and the closure of the directional derivative #
Everything here consumes Fenchel–Moreau, so it carries the pairing hypotheses of
biconj_eq_clFn.
∂(cl f) x = ∂f x wherever (cl f) x = f x. Only continuity of the pairing is needed,
through conj_clFn.
Pointwise inversion: for a closed proper convex f, x ∈ ∂f* y and y ∈ ∂f x say the same
thing.
For a closed proper convex f, ∂f* is the inverse of ∂f as a multivalued mapping — the
graph of ∂f* is the flip of the graph of ∂f.
At a point where a convex f is subdifferentiable, (cl f) x = f x.
And then ∂(cl f) x = ∂f x.
For a nonempty closed convex set C, the subgradients at y of the support function
δ*(· | C) = δ(· | C)* are exactly the points of C at which ⟨·, y⟩ attains its maximum over
C.
The same in terms of supportFn: ∂δ*(· | C) y is the face of C on which ⟨·, y⟩ is
maximized.
The closure of f'(x; ·) is the support function of ∂f x, the conjugate of f'(x; ·)
being the indicator of that set.