The normal form of a polyhedral convex function

A polyhedral convex function is exactly a pointwise maximum of finitely many affine functions, restricted to a polyhedral convex set: f = h + δ(· | C) with

h x = max {⟨x, b₁⟩ - β₁, …, ⟨x, b_k⟩ - β_k} and C = {x | ⟨x, b_j⟩ ≤ β_j, j = k+1, …, m}.

The two descriptions are the two kinds of closed half-space that can appear in a polyhedral description of epi f ⊆ E × ℝ: those whose bounding hyperplane is non-vertical, which are the epigraphs of affine functions, and those that are vertical, which constrain only x. There is no third kind, because epi f is upward closed and so no constraint can bound the vertical variable above; reading a polyhedral system for epi f off in the two groups is the whole proof.

Main definitions

• maxAffineFn s — the pointwise maximum x ↦ ⨆ q ∈ s, (q.1 x - q.2) of a finite family of affine functions, valued in EReal. The empty family gives the constant ⊥.

Main results

• polyhedralFn_maxAffineFn, polyhedralFn_maxAffineFn_add_indicatorFn — a normal form is always polyhedral, with no hypothesis: the degenerate s = ∅ gives ⊥, whose epigraph is everything.
• PolyhedralFn.exists_maxAffineFn_add_indicatorFn_dom — every polyhedral convex function that nowhere takes ⊥ is in normal form, with dom f itself as the set. The vertical inequalities cut out a polyhedral set that may be strictly larger than dom f, but off dom f the function is ⊤ anyway.
• polyhedralFn_iff_maxAffineFn_add_indicatorFn — the two together, as an iff.

Implementation notes

The ⊥-freeness hypothesis is not decoration: EReal has ⊥ + ⊤ = ⊥, so a normal form can take the value ⊥ only on C. The function that is ⊥ on a proper nonempty polyhedral C and ⊤ elsewhere is convex with polyhedral epigraph C ×ˢ univ and has no normal form. The classical convention makes polyhedral convex functions proper, so ∀ x, f x ≠ ⊥ is the weaker hypothesis. The forward direction needs no finite-dimensionality; only the converse uses Minkowski–Weyl, through PolyhedralFn.add.

References

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

noncomputable def Tdaf.ConvexAnalysis.maxAffineFn {E : Type u_1} [AddCommGroup E] [Module ℝ E] (s : Finset ((E →ₗ[ℝ] ℝ) × ℝ)) : E → EReal

The pointwise maximum of the finite family of affine functions x ↦ q.1 x - q.2, q ∈ s, valued in EReal. The empty family gives the constant ⊥, which is the value the extended arithmetic assigns to an empty supremum.

Equations

• Tdaf.ConvexAnalysis.maxAffineFn s x = ⨆ q ∈ s, ↑(q.1 x - q.2)

theorem Tdaf.ConvexAnalysis.maxAffineFn_le_coe {E : Type u_1} [AddCommGroup E] [Module ℝ E] {s : Finset ((E →ₗ[ℝ] ℝ) × ℝ)} {x : E} {c : ℝ} : maxAffineFn s x ≤ ↑c ↔ ∀ q ∈ s, q.1 x - q.2 ≤ c

A real number bounds a finite maximum of affine functions exactly when it bounds each of them.

theorem Tdaf.ConvexAnalysis.coe_le_maxAffineFn {E : Type u_1} [AddCommGroup E] [Module ℝ E] {s : Finset ((E →ₗ[ℝ] ℝ) × ℝ)} {x : E} {q : (E →ₗ[ℝ] ℝ) × ℝ} (hq : q ∈ s) : ↑(q.1 x - q.2) ≤ maxAffineFn s x

Every value of a finite maximum of affine functions is a lower bound for that family.

theorem Tdaf.ConvexAnalysis.maxAffineFn_ne_bot {E : Type u_1} [AddCommGroup E] [Module ℝ E] {s : Finset ((E →ₗ[ℝ] ℝ) × ℝ)} (hs : s.Nonempty) (x : E) : maxAffineFn s x ≠ ⊥

A non-empty family of affine functions has a maximum that is nowhere ⊥.

@[simp]

theorem Tdaf.ConvexAnalysis.maxAffineFn_empty {E : Type u_1} [AddCommGroup E] [Module ℝ E] : maxAffineFn ∅ = fun (x : E) => ⊥

An empty family of affine functions has the constant ⊥ as its maximum.

theorem Tdaf.ConvexAnalysis.polyhedralFn_maxAffineFn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Finset ((E →ₗ[ℝ] ℝ) × ℝ)) : PolyhedralFn (maxAffineFn s)

A finite maximum of affine functions is a polyhedral convex function: its epigraph is cut out by the system q.1 x - μ ≤ q.2.

theorem Tdaf.ConvexAnalysis.polyhedralFn_bot {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] : PolyhedralFn fun (x : E) => ⊥

The constant ⊥ is a polyhedral convex function: its epigraph is everything.

theorem Tdaf.ConvexAnalysis.polyhedralFn_maxAffineFn_add_indicatorFn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (s : Finset ((E →ₗ[ℝ] ℝ) × ℝ)) {C : Set E} (hC : Polyhedral C) : PolyhedralFn (maxAffineFn s + indicatorFn C)

The normal form is always polyhedral. For any finite family of affine functions and any polyhedral convex set C, the function h + δ(· | C) is a polyhedral convex function.

For a non-empty family this is PolyhedralFn.add applied to polyhedralFn_maxAffineFn and polyhedralFn_indicatorFn; for the empty family h + δ(· | C) is the constant ⊥, because ⊥ + ⊤ = ⊥.

theorem Tdaf.ConvexAnalysis.PolyhedralFn.exists_maxAffineFn_add_indicatorFn_dom {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} (hf : PolyhedralFn f) (hb : ∀ (x : E), f x ≠ ⊥) : ∃ (s : Finset ((E →ₗ[ℝ] ℝ) × ℝ)), f = maxAffineFn s + indicatorFn (dom f)

The normal form of a polyhedral convex function. A polyhedral convex function that nowhere takes the value ⊥ is a pointwise maximum of finitely many affine functions plus the indicator of a polyhedral convex set, and the set may be taken to be dom f.

The affine pieces come from the non-vertical inequalities of a polyhedral system for epi f, each rescaled by minus its (negative) coefficient on the vertical variable. The vertical inequalities constrain x alone and hold throughout dom f, which is why dom f itself serves as the set; it is polyhedral by PolyhedralFn.polyhedral_dom. No inequality can have a positive vertical coefficient, since epi f is upward closed.

theorem Tdaf.ConvexAnalysis.polyhedralFn_iff_maxAffineFn_add_indicatorFn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hb : ∀ (x : E), f x ≠ ⊥) : PolyhedralFn f ↔ ∃ (s : Finset ((E →ₗ[ℝ] ℝ) × ℝ)) (C : Set E), Polyhedral C ∧ f = maxAffineFn s + indicatorFn C

The normal form characterises polyhedral convex functions. A function that nowhere takes the value ⊥ is polyhedral convex exactly when it is a pointwise maximum of finitely many affine functions plus the indicator of a polyhedral convex set.