Rockafellar, §12: Conjugates of Convex Functions

The conjugacy correspondence f ↦ f*, its involutivity on closed proper convex functions, and the elementary table of operations under which the conjugate transforms by a change of variable. All 9 numbered results of §12 are formalized.

The section's definitions

• The conjugate f* is conj (pairing n) f, the backbone's conj against the Euclidean self-pairing, defined by the book's own supremum for an arbitrary f : ℝⁿ → [-∞, +∞].
• Fenchel's inequality is fenchel_inequality, stated for a proper f exactly as the book states it; the hypothesis is not removable.
• Symmetry with respect to a set G of orthogonal transformations is transcribed literally as SymmetricWrt, with IsOrthogonalEquiv for "orthogonal linear transformation of ℝⁿ onto itself" — a linear bijection preserving the inner product.
• The monotone conjugate g⁺ is monotoneConjOrthant, acting on MonotoneOrthantFn: +∞ off the non-negative orthant, non-decreasing for the componentwise order, convex, closed, and finite at the origin. monotoneConjOrthant_apply is the book's formula g⁺(z*) = sup {⟨z, z*⟩ - g z | z ≥ 0}.

Rockafellar prints Theorem 12.4 with no proof at all. The argument here avoids the symmetrisation f x = g (abs x) that the surrounding prose suggests, and with it the question of whether x ↦ g (abs x) is convex. Writing K for the non-negative orthant, the one fact that makes the truncation g⁺ = restrict K f* harmless is conj_posPart: f* (y⁺) = f* y, where y⁺ is the componentwise positive part. The supremum defining f** may then be taken over K alone, and Fenchel–Moreau finishes.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §12.

Theorem 12.1

theorem Rockafellar.theorem_12_1 {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hc : Tdaf.ConvexAnalysis.ClosedFn f) : f = fun (x : TdafSurface.Rn n) => ⨆ p ∈ {p : TdafSurface.Rn n × ℝ | Tdaf.ConvexAnalysis.affineFn (TdafSurface.pairing n) p.1 p.2 ≤ f}, Tdaf.ConvexAnalysis.affineFn (TdafSurface.pairing n) p.1 p.2 x

Theorem 12.1. A closed convex function f on ℝⁿ is the pointwise supremum of the collection of all affine functions h such that h ≤ f.

An affine function on ℝⁿ is x ↦ ⟨x, b⟩ - β, indexed here by the pair (b, β); that every affine function has this form is the identification of ℝⁿ with its own dual that pairing n makes.

theorem Rockafellar.corollary_12_1_1 {n : ℕ} (f : TdafSurface.Rn n → EReal) : Tdaf.ConvexAnalysis.clFn (Tdaf.ConvexAnalysis.convHullFn f) = fun (x : TdafSurface.Rn n) => ⨆ p ∈ {p : TdafSurface.Rn n × ℝ | Tdaf.ConvexAnalysis.affineFn (TdafSurface.pairing n) p.1 p.2 ≤ f}, Tdaf.ConvexAnalysis.affineFn (TdafSurface.pairing n) p.1 p.2 x

Corollary 12.1.1. If f is any function from ℝⁿ to [-∞, ∞], then cl (conv f) is the pointwise supremum of the collection of all affine functions on ℝⁿ majorized by f. The affine minorants of cl (conv f) are exactly those of f.

theorem Rockafellar.corollary_12_1_2 {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hp : Tdaf.ConvexAnalysis.Proper f) : ∃ (b : TdafSurface.Rn n) (β : ℝ), ∀ (x : TdafSurface.Rn n), ↑(inner ℝ x b) - ↑β ≤ f x

Corollary 12.1.2. Given any proper convex function f on ℝⁿ, there exists some b ∈ ℝⁿ and β ∈ ℝ such that f x ≥ ⟨x, b⟩ - β for every x. The book states this corollary with no proof of its own.

Theorem 12.2: Fenchel–Moreau

theorem Rockafellar.theorem_12_2_convex {n : ℕ} (f : TdafSurface.Rn n → EReal) : Tdaf.ConvexAnalysis.ConvexFn (Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) f)

Theorem 12.2, first clause: the conjugate of a convex function is convex.

Convexity of f is not needed — f* is a pointwise supremum of affine functions whatever f is — so the hypothesis of the book's statement is dropped.

theorem Rockafellar.theorem_12_2_closed {n : ℕ} (f : TdafSurface.Rn n → EReal) : Tdaf.ConvexAnalysis.ClosedFn (Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) f)

Theorem 12.2, second clause: the conjugate of a convex function is closed. Again no hypothesis on f is needed.

theorem Rockafellar.theorem_12_2_proper {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) : Tdaf.ConvexAnalysis.Proper (Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) f) ↔ Tdaf.ConvexAnalysis.Proper f

Theorem 12.2, third clause: f* is proper if and only if f is.

Strengthens proper_conj_iff, which asks for f closed as well as convex: on ℝⁿ the closure of a proper convex function is again proper (Theorem 7.4), so the hypothesis can be discharged, and conj_clFn transports the conclusion back.

theorem Rockafellar.theorem_12_2_conj_clFn {n : ℕ} (f : TdafSurface.Rn n → EReal) : Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) (Tdaf.ConvexAnalysis.clFn f) = Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) f

Theorem 12.2, fourth clause: (cl f)* = f*. Convexity is not needed.

theorem Rockafellar.theorem_12_2_biconj {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) : Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) (Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) f) = Tdaf.ConvexAnalysis.clFn f

Theorem 12.2, the Fenchel–Moreau theorem: f** = cl f for convex f.

On ℝⁿ the two sides of the pairing coincide, so f** is literally conj (pairing n) applied twice; conj_flip_pairing is what removes the backbone's B.flip.

noncomputable def Rockafellar.corollary_12_2_1 (n : ℕ) : { f : TdafSurface.Rn n → EReal // Tdaf.ConvexAnalysis.ClosedProperConvexFn f } ≃ { g : TdafSurface.Rn n → EReal // Tdaf.ConvexAnalysis.ClosedProperConvexFn g }

Corollary 12.2.1. The conjugacy operation f ↦ f* induces a symmetric one-to-one correspondence in the class of all closed proper convex functions on ℝⁿ.

"Symmetric" is corollary_12_2_1_symm_apply below: the inverse of the correspondence is the correspondence itself.

Equations

• Rockafellar.corollary_12_2_1 n = Tdaf.ConvexAnalysis.conjEquiv (TdafSurface.pairing n)

@[simp]

theorem Rockafellar.corollary_12_2_1_apply {n : ℕ} (f : { f : TdafSurface.Rn n → EReal // Tdaf.ConvexAnalysis.ClosedProperConvexFn f }) : ↑((corollary_12_2_1 n) f) = Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) ↑f

@[simp]

theorem Rockafellar.corollary_12_2_1_symm_apply {n : ℕ} (g : { g : TdafSurface.Rn n → EReal // Tdaf.ConvexAnalysis.ClosedProperConvexFn g }) : ↑((corollary_12_2_1 n).symm g) = Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) ↑g

The correspondence of Corollary 12.2.1 is symmetric: its inverse is itself.

theorem Rockafellar.corollary_12_2_2 {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (y : TdafSurface.Rn n) : Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) f y = ⨆ x ∈ intrinsicInterior ℝ (Tdaf.ConvexAnalysis.dom f), ↑(inner ℝ x y) - f x

Corollary 12.2.2. For any convex function f on ℝⁿ, f* x* = sup {⟨x, x*⟩ - f x ∣ x ∈ ri (dom f)}.

Fenchel's inequality

theorem Rockafellar.fenchel_inequality {n : ℕ} {f : TdafSurface.Rn n → EReal} (hp : Tdaf.ConvexAnalysis.Proper f) (x y : TdafSurface.Rn n) : ↑(inner ℝ x y) ≤ f x + Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) f y

Fenchel's inequality (Rockafellar, §12, p. 105): ⟨x, x*⟩ ≤ f x + f* x* for any proper convex function f and its conjugate.

Properness is the book's hypothesis and it is not removable: for f ≡ +∞ the right-hand side is ⊤ + ⊥ = ⊥.

Theorem 12.3

theorem Rockafellar.theorem_12_3 {n : ℕ} (A A' : TdafSurface.Rn n ≃ₗ[ℝ] TdafSurface.Rn n) (hA : ∀ (x z : TdafSurface.Rn n), inner ℝ (A x) z = inner ℝ x (A' z)) (h : TdafSurface.Rn n → EReal) (a b : TdafSurface.Rn n) (α : ℝ) (y : TdafSurface.Rn n) : Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) (fun (x : TdafSurface.Rn n) => h (A (x - a)) + ↑(inner ℝ x b) + ↑α) y = Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) h (A'.symm (y - b)) + ↑(inner ℝ a y) + ↑(-α - inner ℝ a b)

Theorem 12.3. Let h be a convex function on ℝⁿ and f x = h (A (x - a)) + ⟨x, a*⟩ + α with A a one-to-one linear transformation from ℝⁿ onto ℝⁿ. Then f* x* = h* (A*⁻¹ (x* - a*)) + ⟨x*, a⟩ + α*, where α* = -α - ⟨a, a*⟩.

The book writes A*⁻¹; the adjoint is taken as data, so A' and ⟨A x, z⟩ = ⟨x, A' z⟩ are hypotheses — over ℝⁿ the adjoint exists and is unique, but it must still be supplied. No convexity of h is needed.

Corollary 12.3.1

def Rockafellar.IsOrthogonalEquiv {n : ℕ} (A : TdafSurface.Rn n ≃ₗ[ℝ] TdafSurface.Rn n) : Prop

An orthogonal linear transformation of ℝⁿ onto itself (Rockafellar, §12, p. 109): a linear bijection preserving the inner product. The bridge to the backbone's IsAdjointPair is orthogonalEquiv_adjoint below, which is Rockafellar's A*⁻¹ = A.

Equations

• Rockafellar.IsOrthogonalEquiv A = ∀ (x y : TdafSurface.Rn n), inner ℝ (A x) (A y) = inner ℝ x y

theorem Rockafellar.orthogonalEquiv_adjoint {n : ℕ} {A : TdafSurface.Rn n ≃ₗ[ℝ] TdafSurface.Rn n} (hA : IsOrthogonalEquiv A) (x z : TdafSurface.Rn n) : inner ℝ (A x) z = inner ℝ x (A.symm z)

The bridge for IsOrthogonalEquiv: for an orthogonal A the adjoint A* is A⁻¹.

def Rockafellar.SymmetricWrt {n : ℕ} (f : TdafSurface.Rn n → EReal) (G : Set (TdafSurface.Rn n ≃ₗ[ℝ] TdafSurface.Rn n)) : Prop

Symmetry with respect to a set G of transformations (Rockafellar, §12, p. 109): f (A x) = f x for every x and every A ∈ G.

Equations

• Rockafellar.SymmetricWrt f G = ∀ A ∈ G, ∀ (x : TdafSurface.Rn n), f (A x) = f x

theorem Rockafellar.conj_comp_orthogonal {n : ℕ} {f : TdafSurface.Rn n → EReal} {A : TdafSurface.Rn n ≃ₗ[ℝ] TdafSurface.Rn n} (hA : IsOrthogonalEquiv A) (hfA : ∀ (x : TdafSurface.Rn n), f (A x) = f x) (y : TdafSurface.Rn n) : Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) f (A y) = Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) f y

The half of Corollary 12.3.1 that needs no closedness: if f is symmetric under the orthogonal transformation A, so is f*. This is Theorem 12.3 with h = f, a = 0 = a*, α = 0, together with A*⁻¹ = A.

theorem Rockafellar.corollary_12_3_1 {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hc : Tdaf.ConvexAnalysis.ClosedFn f) {G : Set (TdafSurface.Rn n ≃ₗ[ℝ] TdafSurface.Rn n)} (hG : ∀ A ∈ G, IsOrthogonalEquiv A) : SymmetricWrt f G ↔ SymmetricWrt (Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) f) G

Corollary 12.3.1. A closed convex function f is symmetric with respect to a given set G of orthogonal linear transformations if and only if f* is symmetric with respect to G.

Theorem 12.4: monotone conjugacy on the non-negative orthant

def Rockafellar.nonnegOrthant (n : ℕ) : Set (TdafSurface.Rn n)

The non-negative orthant of ℝⁿ (Rockafellar, §12, p. 111): the set {z | z ≥ 0} for the componentwise order.

Equations

• Rockafellar.nonnegOrthant n = {z : TdafSurface.Rn n | ∀ (j : Fin n), 0 ≤ z.ofLp j}

theorem Rockafellar.mem_nonnegOrthant {n : ℕ} {z : TdafSurface.Rn n} : z ∈ nonnegOrthant n ↔ ∀ (j : Fin n), 0 ≤ z.ofLp j

theorem Rockafellar.inner_rn {n : ℕ} (x y : TdafSurface.Rn n) : inner ℝ x y = ∑ j : Fin n, x.ofLp j * y.ofLp j

The inner product of ℝⁿ in coordinates, which is what the componentwise order interacts with.

theorem Rockafellar.convex_nonnegOrthant (n : ℕ) : Convex ℝ (nonnegOrthant n)

theorem Rockafellar.isClosed_nonnegOrthant (n : ℕ) : IsClosed (nonnegOrthant n)

theorem Rockafellar.zero_mem_nonnegOrthant (n : ℕ) : 0 ∈ nonnegOrthant n

noncomputable def Rockafellar.posPart {n : ℕ} (y : TdafSurface.Rn n) : TdafSurface.Rn n

The componentwise positive part of y, which is y itself on the orthant.

Equations

• Rockafellar.posPart y = WithLp.toLp 2 fun (j : Fin n) => max (y.ofLp j) 0

@[simp]

theorem Rockafellar.posPart_apply {n : ℕ} (y : TdafSurface.Rn n) (j : Fin n) : (posPart y).ofLp j = max (y.ofLp j) 0

theorem Rockafellar.posPart_mem {n : ℕ} (y : TdafSurface.Rn n) : posPart y ∈ nonnegOrthant n

theorem Rockafellar.le_posPart {n : ℕ} (y : TdafSurface.Rn n) (j : Fin n) : y.ofLp j ≤ (posPart y).ofLp j

theorem Rockafellar.posPart_of_mem {n : ℕ} {y : TdafSurface.Rn n} (hy : y ∈ nonnegOrthant n) : posPart y = y

noncomputable def Rockafellar.maskNonneg {n : ℕ} (y z : TdafSurface.Rn n) : TdafSurface.Rn n

z with the coordinates on which y is negative set to zero. It is the competitor that makes the truncation in monotoneConjOrthant harmless.

Equations

• Rockafellar.maskNonneg y z = WithLp.toLp 2 fun (j : Fin n) => if 0 ≤ y.ofLp j then z.ofLp j else 0

@[simp]

theorem Rockafellar.maskNonneg_apply {n : ℕ} (y z : TdafSurface.Rn n) (j : Fin n) : (maskNonneg y z).ofLp j = if 0 ≤ y.ofLp j then z.ofLp j else 0

theorem Rockafellar.maskNonneg_mem {n : ℕ} {z : TdafSurface.Rn n} (y : TdafSurface.Rn n) (hz : z ∈ nonnegOrthant n) : maskNonneg y z ∈ nonnegOrthant n

theorem Rockafellar.maskNonneg_le {n : ℕ} {z : TdafSurface.Rn n} (y : TdafSurface.Rn n) (hz : z ∈ nonnegOrthant n) (j : Fin n) : (maskNonneg y z).ofLp j ≤ z.ofLp j

theorem Rockafellar.inner_maskNonneg {n : ℕ} (y z : TdafSurface.Rn n) : inner ℝ (maskNonneg y z) y = inner ℝ z (posPart y)

theorem Rockafellar.inner_le_inner_posPart {n : ℕ} {z : TdafSurface.Rn n} (hz : z ∈ nonnegOrthant n) (y : TdafSurface.Rn n) : inner ℝ y z ≤ inner ℝ (posPart y) z

structure Rockafellar.MonotoneOrthantFn {n : ℕ} (f : TdafSurface.Rn n → EReal) : Prop

A non-decreasing closed convex function on the non-negative orthant, in the encoding the book's §4 convention prescribes: a function on all of ℝⁿ that is +∞ off the orthant. Rockafellar's hypotheses on g (p. 111) are exactly these.

• top_of_notMem ⦃z : TdafSurface.Rn n⦄ : z ∉ nonnegOrthant n → f z = ⊤

  f is +∞ off the non-negative orthant; the book's "function on the orthant".

• mono ⦃z z' : TdafSurface.Rn n⦄ : z ∈ nonnegOrthant n → (∀ (j : Fin n), z.ofLp j ≤ z'.ofLp j) → f z ≤ f z'

  f z ≤ f z' whenever 0 ≤ z ≤ z': the book's non-decreasing.

• convex : Tdaf.ConvexAnalysis.ConvexFn f

  f is convex.

• closed : Tdaf.ConvexAnalysis.ClosedFn f

  f is lower semicontinuous, i.e. closed.

• zero_ne_top : f 0 ≠ ⊤

  f 0 is finite: not +∞ …

• zero_ne_bot : f 0 ≠ ⊥

  … and not -∞.

theorem Rockafellar.MonotoneOrthantFn.zero_le {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : MonotoneOrthantFn f) {z : TdafSurface.Rn n} (hz : z ∈ nonnegOrthant n) : f 0 ≤ f z

theorem Rockafellar.MonotoneOrthantFn.proper {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : MonotoneOrthantFn f) : Tdaf.ConvexAnalysis.Proper f

noncomputable def Rockafellar.monotoneConjOrthant {n : ℕ} (f : TdafSurface.Rn n → EReal) : TdafSurface.Rn n → EReal

The monotone conjugate g⁺ of Rockafellar's p. 111: the conjugate, truncated back to the non-negative orthant so that the correspondence is one between functions on the orthant.

Equations

• Rockafellar.monotoneConjOrthant f = Tdaf.ConvexAnalysis.restrict (Rockafellar.nonnegOrthant n) (Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) f)

theorem Rockafellar.monotoneConjOrthant_apply {n : ℕ} {f : TdafSurface.Rn n → EReal} (htop : ∀ ⦃z : TdafSurface.Rn n⦄, z ∉ nonnegOrthant n → f z = ⊤) {y : TdafSurface.Rn n} (hy : y ∈ nonnegOrthant n) : monotoneConjOrthant f y = ⨆ z ∈ nonnegOrthant n, ↑(inner ℝ z y) - f z

Rockafellar's formula g⁺(z*) = sup {⟨z, z*⟩ - g z ∣ z ≥ 0} (p. 111), on the orthant.

theorem Rockafellar.monotoneConjOrthant_of_notMem {n : ℕ} (f : TdafSurface.Rn n → EReal) {y : TdafSurface.Rn n} (hy : y ∉ nonnegOrthant n) : monotoneConjOrthant f y = ⊤

theorem Rockafellar.conj_le_monotoneConjOrthant {n : ℕ} (f : TdafSurface.Rn n → EReal) (y : TdafSurface.Rn n) : Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) f y ≤ monotoneConjOrthant f y

theorem Rockafellar.conj_mono_of_top_of_notMem {n : ℕ} {f : TdafSurface.Rn n → EReal} (htop : ∀ ⦃z : TdafSurface.Rn n⦄, z ∉ nonnegOrthant n → f z = ⊤) {y y' : TdafSurface.Rn n} (h : ∀ (j : Fin n), y.ofLp j ≤ y'.ofLp j) : Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) f y ≤ Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) f y'

The conjugate of an orthant function is monotone in the dual variable.

theorem Rockafellar.conj_posPart {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : MonotoneOrthantFn f) (y : TdafSurface.Rn n) : Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) f (posPart y) = Tdaf.ConvexAnalysis.conj (TdafSurface.pairing n) f y

The one fact that makes the truncation harmless: f* does not distinguish y from its positive part. See the module docstring.

theorem Rockafellar.theorem_12_4_mem {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : MonotoneOrthantFn f) : MonotoneOrthantFn (monotoneConjOrthant f)

Theorem 12.4, first half: the monotone conjugate g⁺ of a non-decreasing lower semicontinuous convex function on the non-negative orthant, finite at the origin, is another such function.

The book states Theorem 12.4 with no proof at all. Note g⁺(0) = -g(0), because g attains its infimum over the orthant at the origin.

theorem Rockafellar.theorem_12_4_involutive {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : MonotoneOrthantFn f) : monotoneConjOrthant (monotoneConjOrthant f) = f

Theorem 12.4, second half: the monotone conjugate of g⁺ is in turn g. The book states Theorem 12.4 with no proof at all; see the module docstring.