Rockafellar, §4: Convex Functions

Convex functions on ℝⁿ with values in [-∞, +∞]: the secant and Jensen inequalities, the second-derivative tests, convexity of level sets, and positively homogeneous convex functions. All 11 numbered results of §4 are formalized.

Rockafellar's convex function is defined on all of ℝⁿ and is convex when its epigraph is, which is the backbone's ConvexFn exactly. Only Theorems 4.4 and 4.5 take a finite f, being about C² functions; anywhere else f : Rn n → ℝ would be a mistranslation. Properness is imposed only where the book imposes it: Corollaries 4.7.1 and 4.7.2 and Theorem 4.8.

The extended arithmetic

The conventions §4 lays down are content, not boilerplate.

• 0 · ∞ = 0 holds on the nose for Mathlib's EReal, and theorem_4_3 depends on it: the book's λ₁ f x₁ + ⋯ + λₘ f xₘ is well defined at an index with λᵢ = 0 and f xᵢ = +∞ only because that term is 0.
• inf ∅ = +∞ is what the backbone's restrict, ⨅ _ : x ∈ s, f x, computes off s — the book's own device for extending a function given on a convex set by +∞. theorem_4_1 is stated through it.
• ∞ − ∞ is undefined in the book, whereas Mathlib's EReal totalises it as ⊥. Nothing here relies on that totalisation: every statement whose right-hand side could produce the combination carries the book's own hypothesis ∀ x, f x ≠ ⊥, so the value is never consulted. theorem_4_2 is the one characterisation stated for the full range [-∞, +∞], and it uses strict inequalities between reals precisely so that no infinite sum appears; theorem_4_6 and corollary_4_6_1 are about level sets, where no sum occurs.

theorem_4_5 states positive semi-definiteness of the Hessian in the coordinate-free form 0 ≤ fderiv ℝ (fderiv ℝ f) x z z rather than through the matrix of second partial derivatives.

References

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

Theorem 4.1

theorem Rockafellar.theorem_4_1 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) {f : TdafSurface.Rn n → EReal} (hbot : ∀ (x : TdafSurface.Rn n), f x ≠ ⊥) : Tdaf.ConvexAnalysis.ConvexFn (Tdaf.ConvexAnalysis.restrict C f) ↔ ∀ x ∈ C, ∀ y ∈ C, ∀ (a b : ℝ), 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ ↑a * f x + ↑b * f y

Theorem 4.1. For f : C → (-∞, +∞] with C convex, f is convex on C iff f ((1 − λ) x + λ y) ≤ (1 − λ) f x + λ f y for all x, y ∈ C and 0 < λ < 1.

"Convex on C" is ConvexFn (restrict C f), the book's own convention that a function given on C is extended to ℝⁿ by +∞. The hypothesis ∀ x, f x ≠ ⊥ is "values in (-∞, +∞]", which keeps the right-hand side from being the forbidden ∞ − ∞.

Theorem 4.2

theorem Rockafellar.theorem_4_2 {n : ℕ} (f : TdafSurface.Rn n → EReal) : Tdaf.ConvexAnalysis.ConvexFn f ↔ ∀ (x y : TdafSurface.Rn n) (a b : ℝ), 0 < a → 0 < b → a + b = 1 → ∀ (α β : ℝ), f x < ↑α → f y < ↑β → f (a • x + b • y) < ↑(a * α + b * β)

Theorem 4.2. f : ℝⁿ → [-∞, +∞] is convex iff f ((1 − λ) x + λ y) < (1 − λ) α + λ β for 0 < λ < 1 whenever f x < α and f y < β. This is the characterisation that survives for functions taking both infinite values, and Rockafellar remarks that it could serve as the definition in general; α and β are reals, so no infinite sum is formed.

Theorem 4.3

theorem Rockafellar.theorem_4_3 {n : ℕ} {f : TdafSurface.Rn n → EReal} (hbot : ∀ (x : TdafSurface.Rn n), f x ≠ ⊥) : Tdaf.ConvexAnalysis.ConvexFn f ↔ ∀ (m : ℕ) (l : Fin m → ℝ) (x : Fin m → TdafSurface.Rn n), (∀ (i : Fin m), 0 ≤ l i) → ∑ i : Fin m, l i = 1 → f (∑ i : Fin m, l i • x i) ≤ ∑ i : Fin m, ↑(l i) * f (x i)

Theorem 4.3 (Jensen's inequality). f : ℝⁿ → (-∞, +∞] is convex iff f (λ₁x₁ + ⋯ + λₘxₘ) ≤ λ₁ f x₁ + ⋯ + λₘ f xₘ whenever λᵢ ≥ 0 and ∑ λᵢ = 1.

The right-hand side is an EReal sum, well formed only under the convention 0 · ∞ = 0: an index with λᵢ = 0 and f xᵢ = +∞ must contribute 0, not ∞.

Theorem 4.4

theorem Rockafellar.theorem_4_4 {α β : ℝ} {f : ℝ → ℝ} (hf : ContDiffOn ℝ 2 f (Set.Ioo α β)) : ConvexOn ℝ (Set.Ioo α β) f ↔ ∀ x ∈ Set.Ioo α β, 0 ≤ deriv (deriv f) x

Theorem 4.4. A C² real function on an open interval (α, β) is convex iff f'' ≥ 0 throughout. One of the two results of §4 genuinely about a finite function, so f : ℝ → ℝ is correct here; Ioo α β is open, so the book's f'' is deriv (deriv f).

Theorem 4.5

The private lemmas below are backbone gaps patched locally; see the module docstring.

theorem Rockafellar.theorem_4_5 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCopen : IsOpen C) {f : TdafSurface.Rn n → ℝ} (hf : ContDiffOn ℝ 2 f C) : ConvexOn ℝ C f ↔ ∀ x ∈ C, ∀ (z : TdafSurface.Rn n), 0 ≤ ((fderiv ℝ (fderiv ℝ f) x) z) z

Theorem 4.5. A C² real function on an open convex C ⊆ ℝⁿ is convex on C iff its Hessian is positive semi-definite at every x ∈ C. Positive semi-definiteness is the book's own ⟨z, Q_x z⟩ ≥ 0 for every z, and that quadratic form is the second Fréchet derivative fderiv ℝ (fderiv ℝ f) x z z, which is how the condition is stated here.

Theorem 4.6 and Corollary 4.6.1

theorem Rockafellar.theorem_4_6 {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (α : EReal) : Convex ℝ {x : TdafSurface.Rn n | f x < α} ∧ Convex ℝ {x : TdafSurface.Rn n | f x ≤ α}

Theorem 4.6. For convex f and any α ∈ [-∞, +∞], the level sets {x | f x < α} and {x | f x ≤ α} are convex. α genuinely ranges over EReal, including ±∞, and no properness or finiteness hypothesis is needed.

theorem Rockafellar.corollary_4_6_1 {n : ℕ} {I : Type u_1} {f : I → TdafSurface.Rn n → EReal} (hf : ∀ (i : I), Tdaf.ConvexAnalysis.ConvexFn (f i)) (α : I → ℝ) : Convex ℝ {x : TdafSurface.Rn n | ∀ (i : I), f i x ≤ ↑(α i)}

Corollary 4.6.1. The solution set {x | fᵢ x ≤ αᵢ for all i} of an arbitrary system of convex inequalities is convex.

Theorem 4.7 and its corollaries

theorem Rockafellar.theorem_4_7 {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.PosHomogeneous f) (hbot : ∀ (x : TdafSurface.Rn n), f x ≠ ⊥) : Tdaf.ConvexAnalysis.ConvexFn f ↔ ∀ (x y : TdafSurface.Rn n), f (x + y) ≤ f x + f y

Theorem 4.7. A positively homogeneous f : ℝⁿ → (-∞, +∞] is convex iff it is subadditive, f (x + y) ≤ f x + f y.

theorem Rockafellar.corollary_4_7_1 {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.PosHomogeneous f) (hconv : Tdaf.ConvexAnalysis.ConvexFn f) (hproper : Tdaf.ConvexAnalysis.Proper f) {m : ℕ} (hm : 0 < m) {l : Fin m → ℝ} (hl : ∀ (i : Fin m), 0 < l i) (x : Fin m → TdafSurface.Rn n) : f (∑ i : Fin m, l i • x i) ≤ ∑ i : Fin m, ↑(l i) * f (x i)

Corollary 4.7.1. For positively homogeneous proper convex f, f (λ₁x₁ + ⋯ + λₘxₘ) ≤ λ₁ f x₁ + ⋯ + λₘ f xₘ whenever every λᵢ > 0.

The index range must be non-empty, which the book's λ₁, …, λₘ implies: the empty sum would assert f 0 ≤ 0, and such an f may have f 0 = +∞ — take δ(·|C) for a convex cone C missing the origin.

theorem Rockafellar.corollary_4_7_2 {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.PosHomogeneous f) (hconv : Tdaf.ConvexAnalysis.ConvexFn f) (hproper : Tdaf.ConvexAnalysis.Proper f) (x : TdafSurface.Rn n) : -f x ≤ f (-x)

Corollary 4.7.2. For positively homogeneous proper convex f, f (-x) ≥ -f x.

Theorem 4.8

theorem Rockafellar.theorem_4_8 {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.PosHomogeneous f) (hconv : Tdaf.ConvexAnalysis.ConvexFn f) (hproper : Tdaf.ConvexAnalysis.Proper f) (L : Submodule ℝ (TdafSurface.Rn n)) : (∃ (g : ↥L →ₗ[ℝ] ℝ), ∀ (x : ↥L), f ↑x = ↑(g x)) ↔ ∀ x ∈ L, f (-x) = -f x

Theorem 4.8. A positively homogeneous proper convex f is linear on a subspace L iff f (-x) = -f x for every x ∈ L. "Linear on L" is the existence of a genuine linear functional L →ₗ[ℝ] ℝ agreeing with f there; extracting one is part of the content, since a function odd at x is automatically finite there.

theorem Rockafellar.theorem_4_8_basis {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.PosHomogeneous f) (hconv : Tdaf.ConvexAnalysis.ConvexFn f) (hproper : Tdaf.ConvexAnalysis.Proper f) {L : Submodule ℝ (TdafSurface.Rn n)} {b : Set (TdafSurface.Rn n)} (hb : b.Nonempty) (hspan : Submodule.span ℝ b = L) (hodd : ∀ v ∈ b, f (-v) = -f v) (x : TdafSurface.Rn n) : x ∈ L → f (-x) = -f x

Theorem 4.8, final sentence: it suffices that f (-bᵢ) = -f bᵢ on a spanning set of L. Stated for an arbitrary non-empty spanning set rather than a basis. Non-emptiness is not decoration: the book's argument uses f 0 = 0, which is available only once some vector is known to be odd, so for L = {0} with an empty basis the statement fails as printed — a positively homogeneous proper convex f may have f 0 = +∞.