Rockafellar, §32: The Maximum of a Convex Function

Maximising a convex function, which behaves nothing like minimising one. The maximum principle (Theorem 32.1) says that a relative interior maximiser forces constancy, so the maximum lives on the relative boundary — on a face, and ultimately at an extreme point (Theorem 32.3 and its four corollaries). Theorem 32.4 reads the same fact through subgradients: at a maximiser every subgradient is a non-zero normal vector.

All 11 numbered results of §32 are formalized: Theorems 32.1, 32.2, 32.3 and 32.4 and Corollaries 32.1.1, 32.2.1, 32.3.1, 32.3.2, 32.3.3, 32.3.4 and 32.4.1, together with the section's two examples and the unnumbered remarks that carry mathematical content.

Main definitions

• maximumSet f C — Rockafellar's W, the set of points where the supremum of f relative to C is attained. Corollary 32.1.1 is then the set equation W = ⋃₀ {C' | IsFace C C' ∧ C' ⊆ W}.
• NoUnboundedHalfLine f C — the standing hypothesis of Theorem 32.3, quantified over genuine half-lines (v ≠ 0). bddAboveOnRays_iff is the bridge to the backbone's BddAboveOnRays, which folds the book's other standing hypothesis C ⊆ dom f into the same predicate by allowing v = 0; the two agree exactly when C ⊆ dom f, so every statement below carries Rockafellar's two hypotheses separately, as he writes them.
• linearSystem a α — the solution set of a finite system ⟨x, aᵢ⟩ ≤ αᵢ, so that corollary_32_3_4_linearSystem can be the book's own sentence on the basis of the simplex method.
• parabolicSet, parabolicFn, parabolicCap, quarticCap — the section's two examples.

Corollary 32.3.2's finiteness clause is false as printed. "Then the supremum of f relative to C is finite" fails for the improper f ≡ −∞, whose domain is ℝⁿ, so that ri (dom f) contains every compact convex C while the supremum is −∞. corollary_32_3_2 and corollary_32_3_2_finite therefore carry Proper f; the attainment clause needs no repair.

The two examples both use parabolicFn, f(ξ₁, ξ₂) = ξ₁²/ξ₂ − ξ₂ for ξ₂ > 0, 0 at the origin and +∞ elsewhere, which is convex, closed and proper because it is the support function of parabolicSet. They show that C ⊆ ri (dom f) in Corollary 32.3.2 cannot be weakened to C ⊆ dom f even for closed f: on parabolicCap the supremum is 1 and unattained, and on quarticCap it is +∞. Both weakenings are stated and refuted in Lean, as corollary_32_3_2_not_attained_of_subset_dom and corollary_32_3_2_not_bddAbove_of_subset_dom.

Two statements are stronger than the book's: theorem_32_1 drops the convexity of C, which its proof does not use, and corollary_32_4_1 applies Theorem 32.4 to S directly instead of passing to conv S.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §32 (pp. 342–348).

Theorem 32.1: the maximum principle

theorem Rockafellar.theorem_32_1 {n : ℕ} {f : TdafSurface.Rn n → EReal} {C : Set (TdafSurface.Rn n)} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hCdom : C ⊆ Tdaf.ConvexAnalysis.dom f) {z : TdafSurface.Rn n} (hz : z ∈ intrinsicInterior ℝ C) (hmax : ∀ w ∈ C, f w ≤ f z) {x : TdafSurface.Rn n} (hx : x ∈ C) : f x = f z

Theorem 32.1, the maximum principle: if a convex function attains its supremum relative to a set C ⊆ dom f at a point of ri C, it takes the same value everywhere on C.

Rockafellar assumes C convex; the proof does not use it. All that is needed is that a relative interior point can be prolonged past itself inside C (Theorem 6.4), which exhibits z as a proper convex combination of x and a further point of C.

theorem Rockafellar.theorem_32_1_const {n : ℕ} {f : TdafSurface.Rn n → EReal} {C : Set (TdafSurface.Rn n)} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hCdom : C ⊆ Tdaf.ConvexAnalysis.dom f) {z : TdafSurface.Rn n} (hz : z ∈ intrinsicInterior ℝ C) (hmax : ∀ w ∈ C, f w ≤ f z) {x y : TdafSurface.Rn n} (hx : x ∈ C) (hy : y ∈ C) : f x = f y

Theorem 32.1: "f is actually constant throughout C", stated as constancy rather than as "every value equals the maximum".

theorem Rockafellar.theorem_32_1_affineSubspace {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) {M : AffineSubspace ℝ (TdafSurface.Rn n)} (hMdom : ↑M ⊆ Tdaf.ConvexAnalysis.dom f) {z : TdafSurface.Rn n} (hz : z ∈ M) (hmax : ∀ w ∈ ↑M, f w ≤ f z) {x : TdafSurface.Rn n} (hx : x ∈ M) : f x = f z

§32, first sentence of the remark after Theorem 32.1: a convex function attaining its supremum relative to an affine set M ⊆ dom f is constant on M. Theorem 32.1 at C = M, where ri M = M so the relative interior hypothesis is free.

theorem Rockafellar.theorem_32_1_affineSubspace_of_le {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) {M : AffineSubspace ℝ (TdafSurface.Rn n)} {α : ℝ} (hM : ∀ w ∈ M, f w ≤ ↑α) {x z : TdafSurface.Rn n} (hx : x ∈ M) (hz : z ∈ M) : f z = f x

§32, second sentence, which is Corollary 8.6.2: the conclusion holds as soon as the supremum over M is finite, attained or not.

def Rockafellar.maximumSet {n : ℕ} (f : TdafSurface.Rn n → EReal) (C : Set (TdafSurface.Rn n)) : Set (TdafSurface.Rn n)

Corollary 32.1.1: Rockafellar's W, the set of points at which the supremum of f relative to C is attained.

Equations

• Rockafellar.maximumSet f C = {x : TdafSurface.Rn n | x ∈ C ∧ ∀ w ∈ C, f w ≤ f x}

theorem Rockafellar.mem_maximumSet {n : ℕ} {f : TdafSurface.Rn n → EReal} {C : Set (TdafSurface.Rn n)} {x : TdafSurface.Rn n} : x ∈ maximumSet f C ↔ x ∈ C ∧ ∀ w ∈ C, f w ≤ f x

theorem Rockafellar.corollary_32_1_1 {n : ℕ} {f : TdafSurface.Rn n → EReal} {C : Set (TdafSurface.Rn n)} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hC : Convex ℝ C) (hCdom : C ⊆ Tdaf.ConvexAnalysis.dom f) : maximumSet f C = ⋃₀ {C' : Set (TdafSurface.Rn n) | Tdaf.ConvexAnalysis.IsFace C C' ∧ C' ⊆ maximumSet f C}

Corollary 32.1.1: W is a union of faces of C, stated as the set equation it is.

The inclusion ⊇ is free. For ⊆, Theorem 18.2 produces the unique face C' having a given maximiser in its relative interior, and Theorem 32.1 applied to C' makes f constant on it, so C' consists of maximisers too.

Theorem 32.2: passing to the convex hull

theorem Rockafellar.theorem_32_2 {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (S : Set (TdafSurface.Rn n)) : ⨆ x ∈ (convexHull ℝ) S, f x = ⨆ x ∈ S, f x

Theorem 32.2: the convex hull does not raise the supremum of a convex function, sup_{conv S} f = sup_S f.

The sublevel set {x | f x ≤ sup_S f} is convex and contains S, so it contains conv S. This is convexHull_min, not a Carathéodory decomposition, and it needs neither a topology nor a dimension bound.

theorem Rockafellar.theorem_32_2_attained {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) {S : Set (TdafSurface.Rn n)} {x : TdafSurface.Rn n} (hx : x ∈ (convexHull ℝ) S) (hmax : ∀ z ∈ (convexHull ℝ) S, f z ≤ f x) : ∃ z ∈ S, f z = f x

Theorem 32.2: "the first supremum is attained only when the second (more restrictive) supremum is attained". The strict sublevel set does the same job: a convex function staying strictly below its maximum throughout S stays below it throughout conv S.

theorem Rockafellar.corollary_32_2_1 {n : ℕ} {f : TdafSurface.Rn n → EReal} {C : Set (TdafSurface.Rn n)} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hC : Convex ℝ C) (hCcl : IsClosed C) (hhalf : ¬Tdaf.ConvexAnalysis.IsAffineHalf C) : ⨆ x ∈ C, f x = ⨆ x ∈ C \ intrinsicInterior ℝ C, f x

Corollary 32.2.1: for a closed convex C that is not an affine set or half of one, the supremum over C is already the supremum over the relative boundary.

Rockafellar's two exceptional cases are one predicate in the backbone, IsAffineHalf — the degenerate functional φ = 0 gives the affine sets — and the exclusion cannot be dropped: over [0, ∞) the relative boundary is {0} while f x = x has supremum ⊤. The proof is Theorem 18.4 in hull form (convexHull ℝ (C \ ri C) = C) fed to Theorem 32.2.

theorem Rockafellar.corollary_32_2_1_attained {n : ℕ} {f : TdafSurface.Rn n → EReal} {C : Set (TdafSurface.Rn n)} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hC : Convex ℝ C) (hCcl : IsClosed C) (hhalf : ¬Tdaf.ConvexAnalysis.IsAffineHalf C) {x : TdafSurface.Rn n} (hx : x ∈ C) (hmax : ∀ z ∈ C, f z ≤ f x) : ∃ z ∈ C \ intrinsicInterior ℝ C, f z = f x

Corollary 32.2.1: "the former is attained only when the latter is attained" — Theorem 32.2's attainment clause read through Theorem 18.4.

Theorem 32.3: the extreme point principle

def Rockafellar.NoUnboundedHalfLine {n : ℕ} (f : TdafSurface.Rn n → EReal) (C : Set (TdafSurface.Rn n)) : Prop

Theorem 32.3, the standing hypothesis "there are no half-lines in C on which f is unbounded above", read over genuine half-lines (v ≠ 0).

Equations

• Rockafellar.NoUnboundedHalfLine f C = ∀ (u v : TdafSurface.Rn n), v ≠ 0 → (∀ (t : ℝ), 0 ≤ t → u + t • v ∈ C) → ∃ (β : ℝ), ∀ (t : ℝ), 0 ≤ t → f (u + t • v) ≤ ↑β

theorem Rockafellar.bddAboveOnRays_iff {n : ℕ} {f : TdafSurface.Rn n → EReal} {C : Set (TdafSurface.Rn n)} (hCdom : C ⊆ Tdaf.ConvexAnalysis.dom f) : Tdaf.ConvexAnalysis.BddAboveOnRays f C ↔ NoUnboundedHalfLine f C

The bridge to the backbone's BddAboveOnRays. The backbone folds Rockafellar's two standing hypotheses of Theorem 32.3 into one predicate by letting the direction v be 0, so that the degenerate "half-line" {u} carries the condition f u < ⊤; under C ⊆ dom f the degenerate case is automatic and the two predicates agree.

theorem Rockafellar.theorem_32_3 {n : ℕ} {f : TdafSurface.Rn n → EReal} {C : Set (TdafSurface.Rn n)} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hC : Convex ℝ C) (hCcl : IsClosed C) (hCdom : C ⊆ Tdaf.ConvexAnalysis.dom f) (hray : NoUnboundedHalfLine f C) : ⨆ x ∈ C, f x = ⨆ x ∈ Set.extremePoints ℝ (C ∩ ↑(Tdaf.ConvexAnalysis.linealitySubmodule C)ᗮ), f x

Theorem 32.3, in the book's own form: sup_C f = sup_E f, where E is the set of extreme points of C ∩ L⊥ and L is the lineality space of C.

The backbone states this for an arbitrary complement N of L, since fixing L⊥ would need an inner product it does not assume. Here the inner product is available, so this is that theorem at N = L⊥ — the book's form.

theorem Rockafellar.theorem_32_3_attained {n : ℕ} {f : TdafSurface.Rn n → EReal} {C : Set (TdafSurface.Rn n)} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hC : Convex ℝ C) (hCcl : IsClosed C) (hCdom : C ⊆ Tdaf.ConvexAnalysis.dom f) (hray : NoUnboundedHalfLine f C) {x : TdafSurface.Rn n} (hx : x ∈ C) (hmax : ∀ w ∈ C, f w ≤ f x) : ∃ z ∈ Set.extremePoints ℝ (C ∩ ↑(Tdaf.ConvexAnalysis.linealitySubmodule C)ᗮ), f z = f x

Theorem 32.3: "the supremum relative to C is attained only when the supremum relative to E is attained". The maximiser is transported to C ∩ L⊥ along the lineality space, where Corollary 32.3.1 applies. Rockafellar's C ⊆ dom f is what supplies f x ≠ ⊤ there.

theorem Rockafellar.corollary_32_3_1 {n : ℕ} {f : TdafSurface.Rn n → EReal} {C : Set (TdafSurface.Rn n)} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hC : Convex ℝ C) (hCcl : IsClosed C) (hCdom : C ⊆ Tdaf.ConvexAnalysis.dom f) (hnl : Tdaf.ConvexAnalysis.ContainsNoLine C) {x : TdafSurface.Rn n} (hx : x ∈ C) (hmax : ∀ z ∈ C, f z ≤ f x) : ∃ z ∈ Set.extremePoints ℝ C, f z = f x

Corollary 32.3.1: if the supremum of a convex function over a closed convex set containing no lines is attained at all, it is attained at an extreme point. No boundedness is needed — a finite maximum is itself a bound — but f x ≠ ⊤ is, and that is what C ⊆ dom f supplies.

theorem Rockafellar.corollary_32_3_2 {n : ℕ} {f : TdafSurface.Rn n → EReal} {C : Set (TdafSurface.Rn n)} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hp : Tdaf.ConvexAnalysis.Proper f) (hne : C.Nonempty) (hCcl : IsClosed C) (hCbdd : Bornology.IsBounded C) (hCconv : Convex ℝ C) (hCri : C ⊆ intrinsicInterior ℝ (Tdaf.ConvexAnalysis.dom f)) : ∃ z ∈ Set.extremePoints ℝ C, ∀ w ∈ C, f w ≤ f z

Corollary 32.3.2: a convex function attains its supremum relative to a non-empty closed bounded convex C ⊆ ri (dom f) at an extreme point of C. C ⊆ ri (dom f) makes f continuous relative to C (Theorem 10.1), closed and bounded makes C compact, and Corollary 32.3.1 moves the maximiser to an extreme point. Proper f is not in the book's statement; see corollary_32_3_2_finite.

theorem Rockafellar.corollary_32_3_2_finite {n : ℕ} {f : TdafSurface.Rn n → EReal} {C : Set (TdafSurface.Rn n)} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hp : Tdaf.ConvexAnalysis.Proper f) (hne : C.Nonempty) (hCcl : IsClosed C) (hCbdd : Bornology.IsBounded C) (hCconv : Convex ℝ C) (hCri : C ⊆ intrinsicInterior ℝ (Tdaf.ConvexAnalysis.dom f)) : ∃ (r : ℝ), ⨆ x ∈ C, f x = ↑r

Corollary 32.3.2: "the supremum of f relative to C is finite". This is the clause that needs Proper f, which the book omits: for f ≡ −∞ the printed hypotheses hold and the supremum is ⊥. Given properness the supremum is the value at the maximiser, a real number because the maximiser lies in dom f and f never takes −∞.

theorem Rockafellar.corollary_32_3_3 {n : ℕ} {f : TdafSurface.Rn n → EReal} {C : Set (TdafSurface.Rn n)} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hC : Tdaf.ConvexAnalysis.Polyhedral C) (hne : C.Nonempty) (hCdom : C ⊆ Tdaf.ConvexAnalysis.dom f) (hray : NoUnboundedHalfLine f C) : ∃ z ∈ C, ∀ w ∈ C, f w ≤ f z

Corollary 32.3.3: on a non-empty polyhedral C ⊆ dom f with no half-line on which f is unbounded above, the supremum of f relative to C is attained. Nothing is claimed about extreme points, and nothing is assumed about lines in C — a set containing a line has none.

theorem Rockafellar.corollary_32_3_4 {n : ℕ} {f : TdafSurface.Rn n → EReal} {C : Set (TdafSurface.Rn n)} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hC : Tdaf.ConvexAnalysis.Polyhedral C) (hne : C.Nonempty) (hnl : Tdaf.ConvexAnalysis.ContainsNoLine C) {β : ℝ} (hbdd : ∀ x ∈ C, f x ≤ ↑β) : ∃ z ∈ Set.extremePoints ℝ C, ∀ w ∈ C, f w ≤ f z

Corollary 32.3.4: a convex function bounded above on a non-empty polyhedral convex set containing no lines attains its supremum at one of the (finitely many) extreme points.

This combines Corollaries 32.3.1 and 32.3.3, and is the theoretical basis of the simplex method: it "applies in particular to the problem of maximizing an affine function over the set of solutions to a finite system of weak linear inequalities", which is corollary_32_3_4_linearSystem. The uniform real bound carries Rockafellar's standing C ⊆ dom f with it.

theorem Rockafellar.corollary_32_3_4_finite {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Tdaf.ConvexAnalysis.Polyhedral C) : (Set.extremePoints ℝ C).Finite

Corollary 32.3.4: the parenthetical "(finitely many)". A polyhedral set is finitely generated (Theorem 19.1) and the extreme points of conv P + cone D lie in P (Corollary 18.3.1).

theorem Rockafellar.theorem_32_2_extremePoints_add_coneHull {n : ℕ} {f : TdafSurface.Rn n → EReal} {C : Set (TdafSurface.Rn n)} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hC : Convex ℝ C) (hCcl : IsClosed C) (hnl : Tdaf.ConvexAnalysis.ContainsNoLine C) : ⨆ x ∈ C, f x = ⨆ x ∈ Set.extremePoints ℝ C + ↑(PointedCone.hull ℝ (Tdaf.ConvexAnalysis.extremeDirections C)), f x

§32: "Theorem 32.2 can be applied to a given closed convex set C by representing C as the convex hull of its extreme points and extreme directions as in §18." Unlike Theorem 32.3 this needs no boundedness: keeping the extreme directions in the index set is what makes the identity unconditional.

theorem Rockafellar.theorem_32_3_const_on_lineality {n : ℕ} {f : TdafSurface.Rn n → EReal} {C : Set (TdafSurface.Rn n)} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hCdom : C ⊆ Tdaf.ConvexAnalysis.dom f) (hray : NoUnboundedHalfLine f C) {u v : TdafSurface.Rn n} (hu : u ∈ C) (hv : v ∈ Tdaf.ConvexAnalysis.linealitySpace C) : f (u + v) = f u

§32: the step of Theorem 32.3's proof that cites Corollary 8.6.2 — f is constant along every line in C.

theorem Rockafellar.theorem_32_3_containsNoLine {n : ℕ} {f : TdafSurface.Rn n → EReal} {C : Set (TdafSurface.Rn n)} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hC : Convex ℝ C) (hCcl : IsClosed C) (hCdom : C ⊆ Tdaf.ConvexAnalysis.dom f) (hray : NoUnboundedHalfLine f C) (hnl : Tdaf.ConvexAnalysis.ContainsNoLine C) : ⨆ x ∈ C, f x = ⨆ x ∈ Set.extremePoints ℝ C, f x

Theorem 32.3 when C contains no lines: then L = 0 and C ∩ L⊥ = C, so the supremum over C is the supremum over the extreme points of C itself. This is the form Corollary 32.3.1 is read off.

theorem Rockafellar.corollary_32_3_2_iSup {n : ℕ} {f : TdafSurface.Rn n → EReal} {C : Set (TdafSurface.Rn n)} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hCcl : IsClosed C) (hCbdd : Bornology.IsBounded C) (hCconv : Convex ℝ C) : ⨆ x ∈ C, f x = ⨆ x ∈ Set.extremePoints ℝ C, f x

Corollary 32.3.2, supremum form: over a compact convex set the supremum of a convex function is already the supremum over the extreme points. This is Minkowski's theorem (Corollary 18.5.1) fed to Theorem 32.2, and it needs neither C ⊆ ri (dom f) nor properness — only the attainment clause does.

def Rockafellar.linearSystem {n m : ℕ} (a : Fin m → TdafSurface.Rn n) (α : Fin m → ℝ) : Set (TdafSurface.Rn n)

§32. The solution set of a finite system of weak linear inequalities ⟨x, aᵢ⟩ ≤ αᵢ, i < m — the feasible region of a linear program.

Equations

• Rockafellar.linearSystem a α = {x : TdafSurface.Rn n | ∀ (i : Fin m), ((TdafSurface.pairing n) x) (a i) ≤ α i}

theorem Rockafellar.polyhedral_linearSystem {n m : ℕ} (a : Fin m → TdafSurface.Rn n) (α : Fin m → ℝ) : Tdaf.ConvexAnalysis.Polyhedral (linearSystem a α)

A finite system of weak linear inequalities has a polyhedral solution set — this is the definition of Polyhedral, transcribed at the book's index type.

theorem Rockafellar.corollary_32_3_4_affine {n : ℕ} {C : Set (TdafSurface.Rn n)} (b : TdafSurface.Rn n) (γ : ℝ) (hC : Tdaf.ConvexAnalysis.Polyhedral C) (hne : C.Nonempty) (hnl : Tdaf.ConvexAnalysis.ContainsNoLine C) {β : ℝ} (hbdd : ∀ x ∈ C, ((TdafSurface.pairing n) x) b - γ ≤ β) : ∃ z ∈ Set.extremePoints ℝ C, ∀ w ∈ C, ((TdafSurface.pairing n) w) b - γ ≤ ((TdafSurface.pairing n) z) b - γ

§32: Corollary 32.3.4 for an affine objective ⟨x, b⟩ − γ. An affine function is convex (convexFn_affineFn) and real-valued, so both of Rockafellar's standing hypotheses reduce to the boundedness assumption.

theorem Rockafellar.corollary_32_3_4_linearSystem {n m : ℕ} (a : Fin m → TdafSurface.Rn n) (α : Fin m → ℝ) (b : TdafSurface.Rn n) (γ : ℝ) (hne : (linearSystem a α).Nonempty) (hnl : Tdaf.ConvexAnalysis.ContainsNoLine (linearSystem a α)) {β : ℝ} (hbdd : ∀ x ∈ linearSystem a α, ((TdafSurface.pairing n) x) b - γ ≤ β) : ∃ z ∈ Set.extremePoints ℝ (linearSystem a α), ∀ w ∈ linearSystem a α, ((TdafSurface.pairing n) w) b - γ ≤ ((TdafSurface.pairing n) z) b - γ

§32: maximising an affine function over the solutions of a finite system of weak linear inequalities — the theoretical basis of the simplex method.

Theorem 32.4: subgradients at a maximiser

theorem Rockafellar.theorem_32_4_proper {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) {x : TdafSurface.Rn n} (hxri : x ∈ intrinsicInterior ℝ (Tdaf.ConvexAnalysis.dom f)) (hxb : f x ≠ ⊥) : Tdaf.ConvexAnalysis.Proper f

Theorem 32.4: "here f must be proper by Theorem 7.2, since f is assumed to be finite at a point of ri (dom f)." Properness is a consequence of the theorem's hypotheses, not one of them, and this is the step that produces it.

theorem Rockafellar.theorem_32_4_nonempty {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) {x : TdafSurface.Rn n} (hxri : x ∈ intrinsicInterior ℝ (Tdaf.ConvexAnalysis.dom f)) (hxb : f x ≠ ⊥) : (Tdaf.ConvexAnalysis.subgradient (TdafSurface.pairing n) f x).Nonempty

Theorem 32.4: "the set ∂f(x) is non-empty, because x ∈ ri (dom f) (Theorem 23.4)" — which is what makes the theorem's conclusion about every subgradient a statement with content.

theorem Rockafellar.theorem_32_4_normal {n : ℕ} {f : TdafSurface.Rn n → EReal} {C : Set (TdafSurface.Rn n)} (hfin : ∀ z ∈ C, f z ≠ ⊥ ∧ f z ≠ ⊤) {x : TdafSurface.Rn n} (hx : x ∈ C) (hmax : ∀ z ∈ C, f z ≤ f x) {y : TdafSurface.Rn n} (hy : y ∈ Tdaf.ConvexAnalysis.subgradient (TdafSurface.pairing n) f x) : y ∈ Tdaf.ConvexAnalysis.normalCone (TdafSurface.pairing n) C x

Theorem 32.4: at a point where f attains its supremum relative to C, every x* ∈ ∂f(x) is normal to C at x.

Rockafellar routes this through the sublevel set D = {z | f z ≤ α} and Theorem 23.7. Read directly it is one line: the subgradient inequality at z and maximality at z sandwich ⟨z − x, x*⟩ between 0 and 0. Only finiteness of f x is used, so neither convexity of C nor x ∈ ri (dom f) appears.

theorem Rockafellar.theorem_32_4_ne_zero {n : ℕ} {f : TdafSurface.Rn n → EReal} {C : Set (TdafSurface.Rn n)} {x : TdafSurface.Rn n} (hmax : ∀ z ∈ C, f z ≤ f x) {z₀ : TdafSurface.Rn n} (hz₀ : z₀ ∈ C) (hne : f z₀ ≠ f x) {y : TdafSurface.Rn n} (hy : y ∈ Tdaf.ConvexAnalysis.subgradient (TdafSurface.pairing n) f x) : y ≠ 0

Theorem 32.4: the vector is non-zero. Rockafellar's argument is that inf f < f x because f is not constant on C, hence 0 ∉ ∂f(x); here the witness of non-constancy is passed directly, since a set on which f is not constant supplies one at every one of its points.

theorem Rockafellar.corollary_32_4_1 {n : ℕ} {f : TdafSurface.Rn n → EReal} (hp : Tdaf.ConvexAnalysis.Proper f) {S : Set (TdafSurface.Rn n)} {x : TdafSurface.Rn n} (hxri : x ∈ intrinsicInterior ℝ (Tdaf.ConvexAnalysis.dom f)) (hmax : ∀ z ∈ S, f z ≤ f x) {z₀ : TdafSurface.Rn n} (hz₀ : z₀ ∈ S) (hne : f z₀ ≠ f x) {y : TdafSurface.Rn n} (hy : y ∈ Tdaf.ConvexAnalysis.subgradient (TdafSurface.pairing n) f x) : y ≠ 0 ∧ ∀ z ∈ S, ((TdafSurface.pairing n) z) y ≤ ((TdafSurface.pairing n) x) y

Corollary 32.4.1: for a proper convex f and a non-empty S on which f is not constant, if the supremum of f relative to S is attained at x ∈ ri (dom f), then every x* ∈ ∂f(x) is non-zero and the linear function ⟨·, x*⟩ attains its supremum relative to S at x.

Rockafellar passes to C = conv S so that Theorem 32.4 applies to a convex set. That detour is unnecessary: theorem_32_4_normal asks nothing of C, so it applies to S itself.

theorem Rockafellar.normalCone_closedBall {n : ℕ} {x : TdafSurface.Rn n} (hx : ‖x‖ = 1) : Tdaf.ConvexAnalysis.normalCone (TdafSurface.pairing n) (Metric.closedBall 0 1) x = {y : TdafSurface.Rn n | ∃ (lam : ℝ), 0 ≤ lam ∧ y = lam • x}

§32: the vectors normal to the Euclidean unit ball at a boundary point x are exactly the λx with λ ≥ 0.

pairing n is an abbrev for innerₗ (Rn n), so this is the backbone's normalCone_innerₗ_closedBall, which holds in any real inner-product space.

theorem Rockafellar.theorem_32_4_ball {n : ℕ} {f : TdafSurface.Rn n → EReal} {x : TdafSurface.Rn n} (hx : ‖x‖ = 1) (hfin : ∀ z ∈ Metric.closedBall 0 1, f z ≠ ⊥ ∧ f z ≠ ⊤) (hmax : ∀ z ∈ Metric.closedBall 0 1, f z ≤ f x) {z₀ : TdafSurface.Rn n} (hz₀ : z₀ ∈ Metric.closedBall 0 1) (hne : f z₀ ≠ f x) {y : TdafSurface.Rn n} (hy : y ∈ Tdaf.ConvexAnalysis.subgradient (TdafSurface.pairing n) f x) : ∃ (lam : ℝ), 0 < lam ∧ y = lam • x

§32: at a maximiser of f over the unit Euclidean ball, maximisation leads to the "eigenvalue" condition λx ∈ ∂f(x), |x| = 1.

def Rockafellar.parabolicSet : Set (TdafSurface.Rn 2)

§32. The parabolic convex set K = {(ξ₁, ξ₂) | ξ₁² + 4ξ₂ + 4 ≤ 0}, whose support function is parabolicFn.

Equations

• Rockafellar.parabolicSet = {y : TdafSurface.Rn 2 | y.ofLp 0 ^ 2 + 4 * y.ofLp 1 + 4 ≤ 0}

theorem Rockafellar.mem_parabolicSet {y : TdafSurface.Rn 2} : y ∈ parabolicSet ↔ y.ofLp 0 ^ 2 + 4 * y.ofLp 1 + 4 ≤ 0

noncomputable def Rockafellar.parabolicFn (x : TdafSurface.Rn 2) : EReal

§32. The closed proper convex function f(ξ₁, ξ₂) = ξ₁²/ξ₂ − ξ₂ for ξ₂ > 0, 0 at the origin, +∞ elsewhere. Lean's x / 0 = 0 makes the first branch compute the second, so one ⨅ _ : p, … suffices.

Equations

• Rockafellar.parabolicFn x = ⨅ (_ : 0 ≤ x.ofLp 1 ∧ (x.ofLp 1 = 0 → x.ofLp 0 = 0)), ↑(x.ofLp 0 ^ 2 / x.ofLp 1 - x.ofLp 1)

theorem Rockafellar.parabolicFn_of_mem {x : TdafSurface.Rn 2} (hx : 0 ≤ x.ofLp 1 ∧ (x.ofLp 1 = 0 → x.ofLp 0 = 0)) : parabolicFn x = ↑(x.ofLp 0 ^ 2 / x.ofLp 1 - x.ofLp 1)

theorem Rockafellar.parabolicFn_of_notMem {x : TdafSurface.Rn 2} (hx : ¬(0 ≤ x.ofLp 1 ∧ (x.ofLp 1 = 0 → x.ofLp 0 = 0))) : parabolicFn x = ⊤

theorem Rockafellar.supportFn_parabolicSet : Tdaf.ConvexAnalysis.supportFn (TdafSurface.pairing 2) parabolicSet = parabolicFn

§32: f is the support function of the parabolic set, which is the verification of convexity and closedness the book suggests in its own parenthesis.

theorem Rockafellar.convexFn_parabolicFn : Tdaf.ConvexAnalysis.ConvexFn parabolicFn

theorem Rockafellar.closedFn_parabolicFn : Tdaf.ConvexAnalysis.ClosedFn parabolicFn

theorem Rockafellar.proper_parabolicFn : Tdaf.ConvexAnalysis.Proper parabolicFn

The two caps

def Rockafellar.parabolicCap : Set (TdafSurface.Rn 2)

§32. C = {(ξ₁, ξ₂) | ξ₁² ≤ ξ₂ ≤ 1}.

Equations

• Rockafellar.parabolicCap = {x : TdafSurface.Rn 2 | x.ofLp 0 ^ 2 ≤ x.ofLp 1 ∧ x.ofLp 1 ≤ 1}

def Rockafellar.quarticCap : Set (TdafSurface.Rn 2)

§32. D = {(ξ₁, ξ₂) | ξ₁⁴ ≤ ξ₂ ≤ 1}.

Equations

• Rockafellar.quarticCap = {x : TdafSurface.Rn 2 | x.ofLp 0 ^ 4 ≤ x.ofLp 1 ∧ x.ofLp 1 ≤ 1}

theorem Rockafellar.zero_mem_parabolicCap : 0 ∈ parabolicCap

theorem Rockafellar.isClosed_parabolicCap : IsClosed parabolicCap

theorem Rockafellar.isBounded_parabolicCap : Bornology.IsBounded parabolicCap

theorem Rockafellar.convex_parabolicCap : Convex ℝ parabolicCap

theorem Rockafellar.parabolicCap_subset_dom : parabolicCap ⊆ Tdaf.ConvexAnalysis.dom parabolicFn

theorem Rockafellar.zero_mem_quarticCap : 0 ∈ quarticCap

theorem Rockafellar.isClosed_quarticCap : IsClosed quarticCap

theorem Rockafellar.isBounded_quarticCap : Bornology.IsBounded quarticCap

theorem Rockafellar.convex_quarticCap : Convex ℝ quarticCap

theorem Rockafellar.quarticCap_subset_dom : quarticCap ⊆ Tdaf.ConvexAnalysis.dom parabolicFn

The first example: a supremum that is not attained

theorem Rockafellar.parabolicFn_lt_one_of_mem_parabolicCap {x : TdafSurface.Rn 2} (hx : x ∈ parabolicCap) : parabolicFn x < ↑1

§32: "clearly f(ξ₁, ξ₂) < 1 throughout C". On C one has ξ₁² ≤ ξ₂, so ξ₁²/ξ₂ ≤ 1 and f ≤ 1 − ξ₂ < 1 when ξ₂ > 0; and ξ₂ = 0 forces the origin, where f = 0.

theorem Rockafellar.parabolicFn_capPoint {t : ℝ} (ht : t ≠ 0) (ht1 : t ^ 2 ≤ 1) : parabolicFn (Rockafellar.capPoint✝ 2 t) = ↑(1 - t ^ 2)

§32: "the value of f(ξ₁, ξ₂) approaches 1 as (ξ₁, ξ₂) moves toward (0, 0) along the boundary of C." On the boundary parabola ξ₂ = ξ₁² the value is exactly 1 − t².

theorem Rockafellar.parabolicCap_not_attained : ¬∃ z ∈ parabolicCap, ∀ w ∈ parabolicCap, parabolicFn w ≤ parabolicFn z

§32: "thus 1 is the supremum of f relative to C, and this supremum is not attained." Given a candidate maximiser with value r < 1, the boundary point (t, t²) with t = min 1 ((1 − r)/2) lies in C and carries the strictly larger value 1 − t².

The second example: a supremum that is not finite

theorem Rockafellar.quarticCap_not_bddAbove : ¬∃ (r : ℝ), ∀ w ∈ quarticCap, parabolicFn w ≤ ↑r

§32: "along the boundary curve ξ₁⁴ = ξ₂ of D, the value of f(ξ₁, ξ₂) is ξ₁⁻² − ξ₂, and this rises to +∞ as (ξ₁, ξ₂) moves toward the origin. Thus f is not even bounded above on D." Given a candidate bound r, the boundary point (t, t⁴) with t = min 1 (1/(|r| + 2)) lies in D and carries a value at least (|r| + 2)² − 1 > r.

The weakening of Corollary 32.3.2 that the two examples refute

theorem Rockafellar.corollary_32_3_2_not_attained_of_subset_dom : ¬∀ (g : TdafSurface.Rn 2 → EReal) (D : Set (TdafSurface.Rn 2)), Tdaf.ConvexAnalysis.ConvexFn g → Tdaf.ConvexAnalysis.ClosedFn g → Tdaf.ConvexAnalysis.Proper g → D.Nonempty → IsClosed D → Bornology.IsBounded D → Convex ℝ D → D ⊆ Tdaf.ConvexAnalysis.dom g → ∃ z ∈ D, ∀ w ∈ D, g w ≤ g z

§32, first half of the remark the two examples exist for, stated and refuted: Corollary 32.3.2 with C ⊆ ri (dom f) weakened to C ⊆ dom f would say that the supremum is still attained. It is not, and adding ClosedFn and Proper — the book's "even when f is closed" — does not save it. The witness is parabolicCap.

theorem Rockafellar.corollary_32_3_2_not_bddAbove_of_subset_dom : ¬∀ (g : TdafSurface.Rn 2 → EReal) (D : Set (TdafSurface.Rn 2)), Tdaf.ConvexAnalysis.ConvexFn g → Tdaf.ConvexAnalysis.ClosedFn g → Tdaf.ConvexAnalysis.Proper g → D.Nonempty → IsClosed D → Bornology.IsBounded D → Convex ℝ D → D ⊆ Tdaf.ConvexAnalysis.dom g → ∃ (r : ℝ), ∀ w ∈ D, g w ≤ ↑r

§32, second half, stated and refuted: the same weakening would say that the supremum is still finite. The witness is quarticCap, on which f is not even bounded above.