Conjugates of convex functions #
The conjugate of f : E → EReal with respect to a pairing B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ is
f*(y) = sup_x (⟨x, y⟩ - f x). Read through epigraphs, f* is a description of the affine
minorants of f: f*(y) ≤ c says exactly that x ↦ ⟨x, y⟩ - c lies below f. It is defined for
an arbitrary f, and is always a closed convex function. The theorem the rest of the library rests
on is Fenchel–Moreau, f** = cl f for convex f: conjugacy is an involution on the closed
convex functions, and a closed convex function is the pointwise supremum of the affine functions
below it.
Main definitions #
conj B f,biconj B f— the conjugatef*and biconjugatef**.conjClosure B— conjugacy as aClosureOperatoron(E → EReal)ᵒᵈ, whose closed elements are exactly the closed convex functions.conjEquiv— conjugacy as an involution on the closed proper convex functions.
Main results #
sub_le_conj,conj_le_coe_iff,conj_le_iff— the unconditional forms of Fenchel's inequality. The last says thatconj Bandconj B.flipare an antitone Galois connection.le_add_conj— Fenchel's inequality⟨x, y⟩ ≤ f x + f* y. InERealthis needsProper f, and the hypothesis is not removable; see the implementation notes.convexFn_conj,closedFn_conj— the conjugate of an arbitrary function is closed and convex.conj_clFn—(cl f)* = f*: closure does not change the conjugate.exists_affineFn_le_of_lt,eq_biSup_affineFn— a closed convex function is the pointwise supremum of the affine functions below it.biconj_eq_clFn— the Fenchel–Moreau theorem:f** = cl ffor convexf;proper_conj_iffis its properness half.biconj_eq_clFn_topDualandbiconj_eq_clFn_innerdischarge every hypothesis, for a locally convex space paired with its own continuous dual and for a real Hilbert space paired with itself, both in the space's own topology.gc_conj_conj,conjClosure,conjOrderIso— the Galois connection, the closure operator it induces, and the order anti-isomorphism between the biconjugation-fixed functions.conj_comp_sub,conj_comp_add,conj_add_pairing,conj_sub_pairing,conj_add_const,conj_comp_linearEquiv— the four elementary rows (translation, tilting, an added constant, an invertible substitution), withconj_comp_affinecomposing them (Theorem 12.3 in [^1]).
Implementation notes #
Fenchel–Moreau does not care which topology E carries, so long as its continuous dual is the F
side of the pairing: that is IsCompatiblePairing B. Its weaker companion IsContinuousPairing,
asking only that every ⟨·, y⟩ be continuous, is all the closedness half of this file needs —
closedFn_conj, conj_clFn, biconj_le_clFn — which matters because a Banach space paired with
its norm-topology dual is continuous on both sides but compatible only if it is reflexive.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §12.
The conjugate #
The convex conjugate of f with respect to the pairing B:
f*(y) = sup_x (⟨x, y⟩ - f x). epi f* is the set of pairs (y, c) for which the affine function
x ↦ ⟨x, y⟩ - c is majorized by f. No hypothesis is placed on f.
Equations
- Tdaf.ConvexAnalysis.conj B f y = ⨆ (x : E), ↑((B x) y) - f x
Instances For
The biconjugate, back on E. Using B.flip rather than a second copy of B makes the
correspondence symmetric with no reflexivity assumption; B.flip.flip = B holds by rfl.
Equations
Instances For
Fenchel's inequality, ∞ - ∞-free: it holds for every f, x and y, and it is the
form the proofs below use rather than the additive le_add_conj.
The adjunction. f* ≤ g and g* ≤ f say the same thing — that ⟨x, y⟩ ≤ f x + g y for
all x and y, in the ∞ - ∞-free reading.
The improper cases #
f* takes the value ⊥ at a point exactly when f ≡ ⊤ — a condition independent of the
point. So f* is either the constant ⊥ or never ⊥, which is why it is always closed.
Fenchel's inequality: ⟨x, y⟩ ≤ f x + f*(y) for a proper f.
Properness is not decorative: if f ≡ +∞ then f* ≡ -∞ and the right-hand side is ⊤ + ⊥ = ⊥,
and if f takes -∞ then it is ⊥ + ⊤ = ⊥. Use sub_le_conj when properness is unavailable.
If the conjugate is proper then so is the original function; no hypothesis is needed for this
direction. The converse is proper_conj, and needs closedness.
Convexity of the conjugate #
The x-th term of the supremum defining f* is, as a function of y, either constant or one
of the affine functions of the flipped pairing, according to the value of f x.
Why Fenchel's inequality needs properness #
In EReal the value ⊥ is absorbing for addition, so ⊤ + ⊥ = ⊥ + ⊤ = ⊥ and the additive form of
Fenchel's inequality collapses at each of the two improper functions.
Closedness of the conjugate #
The conjugate is closed in any topology on F for which the pairing is continuous — in
particular in σ(F, E), hence also in the norm topology of a normed space paired with its dual.
The conjugate is a closed convex function, with no hypothesis on f: if f ≡ +∞ it is
the constant ⊥, and otherwise it is lower semicontinuous and never takes ⊥.
The conjugate sees only the closure #
Closure does not change the conjugate: (cl f)* = f*. The affine functions below f and
below cl f are the same, because an affine function of a continuous pairing is itself closed.
The biconjugate is a closed convex minorant of f, hence a minorant of cl f: the easy half
of Fenchel–Moreau, needing no convexity.
Affine minorants of a closed convex function #
The affine-minorant lemma, in its working form: below any value strictly under a closed convex function there is an affine minorant of the pairing.
A closed convex function is the pointwise supremum of all the affine functions of the pairing that lie below it.
The Fenchel–Moreau theorem #
The Fenchel–Moreau theorem. For a convex function, f** = cl f.
The improper cases are why clFn branches on lscHull f rather than on f: if f takes -∞
anywhere then f* ≡ +∞ and f** ≡ -∞, which is cl f only under that branching.
The properness half: the conjugate of a closed proper convex function is proper.
With proper_of_proper_conj, "f* is proper if and only if f is".
Conjugacy as a Galois connection #
conj_le_iff says that conj B and conj B.flip are antitonely adjoint; Fenchel–Moreau then
identifies the closed elements of the induced closure operator with the closed convex functions.
The OrderDual on the domain is what makes an antitone adjunction fit Mathlib's monotone
GaloisConnection.
The closure operator f ↦ f** induced by the adjunction. Its closed elements are the functions
equal to their own biconjugate, which by Fenchel–Moreau are exactly the closed convex functions.
Equations
Instances For
Conjugacy is an order anti-isomorphism between the biconjugation-fixed functions.
Neither this nor conjEquiv below subsumes the other: this one needs no topology and carries the
order, while conjEquiv is about the proper closed convex functions, a strictly smaller class
that f** = f does not pin down — the improper f ≡ +∞ and f ≡ -∞ are fixed by biconjugation
too.
Equations
Instances For
The involution on closed proper convex functions #
Both spaces carry topologies compatible with the pairing, and everything is symmetric under
B ↦ B.flip.
Conjugacy is a symmetric one-to-one correspondence between the closed proper convex functions
on E and those on F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Translation, tilting, constants and an invertible substitution #
The elementary conjugacy operations, those under which h* changes by a change of variable rather
than by a change of function. There are four independent rows —
| primal | dual |
|---|---|
h (x - a) | h* y + ⟨a, y⟩ |
h x + ⟨x, b⟩ | h* (y - b) |
h x + α | h* y - α |
h (A x), A invertible | h* (A'⁻¹ y) |
— and conj_comp_affine composes all four into a single formula. The two scaling rows of the
same table are conj_smul and conj_smulRight in Duality/Ops.lean. Each
identity holds for an arbitrary h : E → EReal, improper ones included, with no topology,
properness or convexity: ⟨a, y⟩, ⟨x, b⟩ and α are real, so sliding them across the
difference ⟨x, y⟩ - h x never produces ∞ - ∞.
Rockafellar writes the substitution row with A*⁻¹, presuming that A has an adjoint and that the
adjoint is invertible. Over a general pairing neither is automatic, so conj_comp_linearEquiv
takes the inverse pair A, A' and the adjointness datum IsAdjointPair B B' A A' as
hypotheses; with B and B' separating, A' is determined by A, so nothing is lost.
The translation row with the translation on the left: h (a + ·) is
h (· - (-a)), so its conjugate is h* - ⟨a, ·⟩.
The substitution row: precomposing h with a linear isomorphism A precomposes the
conjugate with the inverse of the transpose. Contrast conj_mapLin, which drops invertibility at
the cost of stating the dual side as an image.
The four rows composed. For f x = h (A (x - a)) + ⟨x, a*⟩ + α with A an invertible
linear transformation, f* y = h* (A*⁻¹ (y - a*)) + ⟨a, y⟩ + α* where α* = -α - ⟨a, a*⟩.
Translation and tilting composed: for f = h (z + ·) - ⟨·, z*⟩,
f* = h* (z* + ·) - ⟨z, ·⟩ - ⟨z, z*⟩. The constant ⟨z, z*⟩ is what makes the two infima it is
used for add to ⟨z, z*⟩ rather than to zero.
Fenchel–Moreau for a locally convex space paired with its own topological dual, in the
original topology of E and with no hypothesis beyond convexity.
Fenchel–Moreau for a real Hilbert space paired with itself by the inner product, in the norm topology. Compatibility is the Fréchet–Riesz representation theorem.