Extended-real-valued convex functions

The basic theory of convex functions f : E → EReal on a real vector space. Convexity is defined geometrically, as convexity of the epigraph, rather than by the inequality f (a • x + b • y) ≤ a * f x + b * f y: the right-hand side can be the undefined ∞ - ∞ when f takes both infinite values, and improper functions are admitted throughout. The epigraph lives in E × ℝ, not E × EReal — the second coordinate ranges over the reals, unlike Mathlib's ConvexOn.convex_epigraph, which uses the codomain of the function.

Main definitions

• epi f — the epigraph of f, a subset of E × ℝ.
• dom f — the effective domain of f, where f < ⊤.
• Proper f — f is finite somewhere and never ⊥.
• restrict s f — f restricted to s, extended by ⊤.
• ConvexFn f — f is convex, meaning that epi f is a convex set.
• scaleSnd c — the vertical scaling (x, μ) ↦ (x, c μ) of E × ℝ, which is how a scalar multiple of f acts on epigraphs.

Main results

• convexFn_iff_forall_lt — convexity by strict inequalities: the form that avoids ∞ - ∞ entirely.
• convexFn_iff_le — the familiar inequality, valid when f never takes ⊥.
• convexFn_add_coe, ConvexFn.comp_add_left — adding a real-valued affine coordinate, and translating the argument, preserve convexity.
• ConvexFn.convex_lt, ConvexFn.convex_le, ConvexFn.convex_dom — sublevel sets and the effective domain of a convex function are convex.
• convexFn_coe_mul, dom_coe_mul, proper_coe_mul — a non-negative multiple cf.
• convexOn_iff_convexFn — the bridge to Mathlib's ConvexOn.
• ConvexFn.sum_le — Jensen's inequality for a finite convex combination.

References

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

Epigraphs, domains, properness

def Tdaf.ConvexAnalysis.epi {E : Type u_1} (f : E → EReal) : Set (E × ℝ)

The epigraph of f : E → EReal, {(x, μ) | μ ∈ ℝ, f x ≤ μ} ⊆ E × ℝ. The second coordinate ranges over the reals, not over EReal.

Equations

• Tdaf.ConvexAnalysis.epi f = {p : E × ℝ | f p.1 ≤ ↑p.2}

@[simp]

theorem Tdaf.ConvexAnalysis.mem_epi {E : Type u_1} {f : E → EReal} {p : E × ℝ} : p ∈ epi f ↔ f p.1 ≤ ↑p.2

theorem Tdaf.ConvexAnalysis.mk_mem_epi {E : Type u_1} {f : E → EReal} {x : E} {μ : ℝ} : (x, μ) ∈ epi f ↔ f x ≤ ↑μ

theorem Tdaf.ConvexAnalysis.epi_anti {E : Type u_1} {f g : E → EReal} (h : f ≤ g) : epi g ⊆ epi f

epi is antitone: a larger function has a smaller epigraph.

theorem Tdaf.ConvexAnalysis.le_iff_epi_subset {E : Type u_1} {f g : E → EReal} : f ≤ g ↔ epi g ⊆ epi f

The epigraph determines the function: f ≤ g exactly when epi g ⊆ epi f.

def Tdaf.ConvexAnalysis.dom {E : Type u_1} (f : E → EReal) : Set E

The effective domain of f: the set where f < ⊤. Equivalently the projection of epi f on E.

Equations

• Tdaf.ConvexAnalysis.dom f = {x : E | f x < ⊤}

@[simp]

theorem Tdaf.ConvexAnalysis.mem_dom {E : Type u_1} {f : E → EReal} {x : E} : x ∈ dom f ↔ f x < ⊤

theorem Tdaf.ConvexAnalysis.dom_eq_fst_image_epi {E : Type u_1} (f : E → EReal) : dom f = Prod.fst '' epi f

dom f is the projection of epi f, with no hypothesis on f and improper functions included. That is why dom must not be restricted to functions avoiding ⊥: the relative interior ri (dom f) carries statements about improper f too.

theorem Tdaf.ConvexAnalysis.epi_nonempty_iff {E : Type u_1} (f : E → EReal) : (epi f).Nonempty ↔ (dom f).Nonempty

The epigraph is nonempty exactly when the effective domain is: both say f ≢ +∞.

theorem Tdaf.ConvexAnalysis.epi_eq_empty_iff {E : Type u_1} (f : E → EReal) : epi f = ∅ ↔ dom f = ∅

@[simp]

theorem Tdaf.ConvexAnalysis.epi_top {E : Type u_1} : epi ⊤ = ∅

structure Tdaf.ConvexAnalysis.Proper {E : Type u_1} (f : E → EReal) : Prop

f is proper when it is finite somewhere and never takes the value ⊥; equivalently, epi f is nonempty and contains no vertical lines.

• dom_nonempty : (dom f).Nonempty

  f is not identically ⊤.

• ne_bot (x : E) : f x ≠ ⊥

  f never takes the value ⊥.

noncomputable def Tdaf.ConvexAnalysis.restrict {E : Type u_1} (s : Set E) (f : E → EReal) : E → EReal

f restricted to s and extended by ⊤ off s — the standing encoding of "a convex function given on a convex set". The ⨅ formulation avoids a decidability hypothesis; restrict_of_mem and restrict_of_notMem are the defining equations.

Equations

• Tdaf.ConvexAnalysis.restrict s f x = ⨅ (_ : x ∈ s), f x

@[simp]

theorem Tdaf.ConvexAnalysis.restrict_of_mem {E : Type u_1} {s : Set E} {f : E → EReal} {x : E} (hx : x ∈ s) : restrict s f x = f x

@[simp]

theorem Tdaf.ConvexAnalysis.restrict_of_notMem {E : Type u_1} {s : Set E} {f : E → EReal} {x : E} (hx : x ∉ s) : restrict s f x = ⊤

Non-negative scalar multiples

EReal obeys 0 · ∞ = 0, so 0 · f is the constant 0, which is proper and convex; only the effective domain statement needs 0 < c, because dom (0 · f) is all of E.

theorem Tdaf.ConvexAnalysis.dom_coe_mul {E : Type u_1} {c : ℝ} (hc : 0 < c) (f : E → EReal) : (dom fun (x : E) => ↑c * f x) = dom f

A positive multiple of f has the same effective domain as f. The hypothesis is 0 < c, not 0 ≤ c: at c = 0 the product is the constant 0 and its domain is everything.

theorem Tdaf.ConvexAnalysis.proper_coe_mul {E : Type u_1} {c : ℝ} (hc : 0 ≤ c) {f : E → EReal} (hp : Proper f) : Proper fun (x : E) => ↑c * f x

A non-negative multiple of a proper function is proper. At c = 0 the product is the constant 0, which is finite everywhere; at c > 0 the domain is unchanged (dom_coe_mul).

Convex functions

structure Tdaf.ConvexAnalysis.ConvexFn {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) : Prop

A function f : E → EReal is convex when its epigraph is a convex subset of E × ℝ. See convexFn_iff_forall_lt and convexFn_iff_le for the analytic forms.

• convex_epi : Convex ℝ (epi f)

  The epigraph of a convex function is convex.

@[simp]

theorem Tdaf.ConvexAnalysis.convexFn_iff_convex_epi {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} : ConvexFn f ↔ Convex ℝ (epi f)

theorem Tdaf.ConvexAnalysis.combo_of_pos {E : Type u_1} [AddCommGroup E] [Module ℝ E] {P : E → Prop} {x y : E} {a b : ℝ} (hx : P x) (hy : P y) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (h : 0 < a → 0 < b → P (a • x + b • y)) : P (a • x + b • y)

A convex-combination goal reduces to the case of two positive coefficients.

theorem Tdaf.ConvexAnalysis.ConvexFn.epi_combo {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : ConvexFn f) {x y : E} {μ ν : ℝ} (hx : f x ≤ ↑μ) (hy : f y ≤ ↑ν) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : f (a • x + b • y) ≤ ↑(a * μ + b * ν)

The defining property of convexity, in the form in which it is used: a convex combination of two points of the epigraph lies in the epigraph.

theorem Tdaf.ConvexAnalysis.convexFn_of_epi_combo {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (h : ∀ (x y : E) (μ ν : ℝ), f x ≤ ↑μ → f y ≤ ↑ν → ∀ (a b : ℝ), 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ ↑(a * μ + b * ν)) : ConvexFn f

Conversely, the combination property characterises convexity.

theorem Tdaf.ConvexAnalysis.convexFn_add_coe {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : ConvexFn f) {l : E → ℝ} (hl : ∀ (x y : E) (a b : ℝ), a + b = 1 → l (a • x + b • y) = a * l x + b * l y) : ConvexFn fun (x : E) => f x + ↑(l x)

A real-valued affine coordinate added to a convex function keeps it convex. The hypothesis is the combination law rather than linearity, so the same lemma serves a coordinate of a pairing, a projection of a product and an affine function alike.

theorem Tdaf.ConvexAnalysis.ConvexFn.comp_add_left {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : ConvexFn f) (a : E) : ConvexFn fun (x : E) => f (a + x)

Translating the argument preserves convexity. x ↦ f (a + x) is convex whenever f is, for any a; the epigraph of the translate is the translate of the epigraph.

Non-negative scalar multiples

noncomputable def Tdaf.ConvexAnalysis.scaleSnd {E : Type u_1} [AddCommGroup E] [Module ℝ E] (c : ℝ) : E × ℝ →ₗ[ℝ] E × ℝ

The linear map (x, μ) ↦ (x, c μ) of E × ℝ. It is the vertical scaling that carries epi f to epi (cf); see epi_coe_mul.

Equations

• Tdaf.ConvexAnalysis.scaleSnd c = (LinearMap.fst ℝ E ℝ).prod (c • LinearMap.snd ℝ E ℝ)

theorem Tdaf.ConvexAnalysis.scaleSnd_apply {E : Type u_1} [AddCommGroup E] [Module ℝ E] (c : ℝ) (p : E × ℝ) : (scaleSnd c) p = (p.1, c * p.2)

theorem Tdaf.ConvexAnalysis.epi_coe_mul {E : Type u_1} [AddCommGroup E] [Module ℝ E] {c : ℝ} (hc : 0 < c) (f : E → EReal) : (epi fun (x : E) => ↑c * f x) = ⇑(scaleSnd c⁻¹) ⁻¹' epi f

The epigraph of a positive multiple. epi (cf) is epi f pulled back along the vertical scaling (x, μ) ↦ (x, μ / c), which makes convexity and closedness of cf preimage arguments. The identity fails at c = 0, where the left side is E × Ici 0 and the right side is everything.

theorem Tdaf.ConvexAnalysis.convexFn_coe_mul {E : Type u_1} [AddCommGroup E] [Module ℝ E] {c : ℝ} (hc : 0 ≤ c) {f : E → EReal} (hf : ConvexFn f) : ConvexFn fun (x : E) => ↑c * f x

A non-negative multiple of a convex function is convex, the EReal-valued form of "λf is convex for λ ≥ 0".

Convexity as a strict inequality on values

theorem Tdaf.ConvexAnalysis.convexFn_iff_forall_lt {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) : ConvexFn f ↔ ∀ (x y : E) (a b : ℝ), 0 < a → 0 < b → a + b = 1 → ∀ (α β : ℝ), f x < ↑α → f y < ↑β → f (a • x + b • y) < ↑(a * α + b * β)

Convexity in strict inequalities. A function f : E → EReal is convex if and only if f ((1 - λ) x + λ y) < (1 - λ) α + λ β whenever f x < α, f y < β and 0 < λ < 1. The strict inequalities keep α and β real, so the forbidden ∞ - ∞ never arises.

Convexity as an inequality on values

theorem Tdaf.ConvexAnalysis.convexFn_iff_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : ∀ (x : E), f x ≠ ⊥) : ConvexFn f ↔ ∀ (x y : E) (a b : ℝ), 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ ↑a * f x + ↑b * f y

For a function f that never takes the value ⊥ — equivalently, a function into (-∞, +∞] — convexity is the familiar inequality.

Level sets and the effective domain

theorem Tdaf.ConvexAnalysis.ConvexFn.convex_lt {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : ConvexFn f) (α : EReal) : Convex ℝ {x : E | f x < α}

Strict sublevel sets of a convex function are convex.

theorem Tdaf.ConvexAnalysis.ConvexFn.convex_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : ConvexFn f) (α : EReal) : Convex ℝ {x : E | f x ≤ α}

Sublevel sets of a convex function are convex.

theorem Tdaf.ConvexAnalysis.ConvexFn.convex_dom {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : ConvexFn f) : Convex ℝ (dom f)

The effective domain of a convex function is convex.

The bridge to Mathlib's ConvexOn

theorem Tdaf.ConvexAnalysis.epi_restrict_coe {E : Type u_1} (s : Set E) (g : E → ℝ) : epi (restrict s fun (x : E) => ↑(g x)) = {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2}

theorem Tdaf.ConvexAnalysis.convexOn_iff_convexFn {E : Type u_1} [AddCommGroup E] [Module ℝ E] (s : Set E) (g : E → ℝ) : ConvexOn ℝ s g ↔ ConvexFn (restrict s fun (x : E) => ↑(g x))

Mathlib's ConvexOn for a real-valued function on a set agrees with ConvexFn for its extension by ⊤. This is the interface through which the surface layer reuses Mathlib.

Jensen's inequality for finite convex combinations

theorem Tdaf.ConvexAnalysis.ConvexFn.sum_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {ι : Type u_2} (hf : ConvexFn f) (t : Finset ι) (u : ι → E) (m wt : ι → ℝ) (hm : ∀ j ∈ t, f (u j) ≤ ↑(m j)) (hw : ∀ j ∈ t, 0 ≤ wt j) (hw1 : ∑ j ∈ t, wt j = 1) : f (∑ j ∈ t, wt j • u j) ≤ ↑(∑ j ∈ t, wt j * m j)

Jensen's inequality for a convex EReal-valued function, in the form the epigraph supplies it: a convex combination of points at which f is bounded above by reals m j is bounded above by the same combination of the m j. The bound is by reals, not by f (u j) directly; the EReal-valued form f (∑ wt j • u j) ≤ ∑ wt j • f (u j) needs the 0 · ∞ = 0 convention at indices where wt j = 0 and f (u j) = ⊤. Aliased as jensen.