Polyhedral convex functions

A convex function is polyhedral when its epigraph is a polyhedral convex set; equivalently, by Minkowski–Weyl, when it is the pointwise maximum of finitely many affine functions on a polyhedral effective domain. PolyhedralFn f is Polyhedral (epi f), and everything here is read off the epigraph through the polyhedral calculus of Polyhedral/Ops.lean.

PolyhedralFn does not by itself exclude f x = ⊥ — the epigraph of f ≡ ⊥ is all of E × ℝ, which is polyhedral — so PolyhedralFn.closedFn carries f ≠ ⊥, while lower semicontinuity holds regardless. The classical convention makes polyhedral convex functions proper.

Main results

• PolyhedralFn.convexFn, PolyhedralFn.lowerSemicontinuous, PolyhedralFn.closedFn — a polyhedral convex function is convex and closed.
• PolyhedralFn.polyhedral_dom, PolyhedralFn.polyhedral_sublevel — the effective domain and every sublevel set are polyhedral.
• polyhedralFn_indicatorFn — the indicator of a polyhedral set is a polyhedral function, which is what makes the polyhedral constraint qualifications apply to constraint sets.
• PolyhedralFn.add — a sum of polyhedral convex functions is polyhedral.
• PolyhedralFn.infConv, epi_infConv_of_polyhedralFn — an infimal convolute of polyhedral convex functions is polyhedral, and the infimum defining it is attained.

References

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

def Tdaf.ConvexAnalysis.PolyhedralFn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → EReal) : Prop

A polyhedral convex function: one whose epigraph is a polyhedral convex set.

Equations

• Tdaf.ConvexAnalysis.PolyhedralFn f = Tdaf.ConvexAnalysis.Polyhedral (Tdaf.ConvexAnalysis.epi f)

theorem Tdaf.ConvexAnalysis.PolyhedralFn.convexFn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} (hf : PolyhedralFn f) : ConvexFn f

theorem Tdaf.ConvexAnalysis.PolyhedralFn.isClosed_epi {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : PolyhedralFn f) : IsClosed (epi f)

theorem Tdaf.ConvexAnalysis.PolyhedralFn.lowerSemicontinuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : PolyhedralFn f) : LowerSemicontinuous f

theorem Tdaf.ConvexAnalysis.PolyhedralFn.closedFn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : PolyhedralFn f) (h : ∀ (x : E), f x ≠ ⊥) : ClosedFn f

theorem Tdaf.ConvexAnalysis.PolyhedralFn.polyhedral_dom {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : PolyhedralFn f) : Polyhedral (dom f)

The effective domain of a polyhedral convex function is a polyhedral convex set — it is the image of the epigraph under Prod.fst.

theorem Tdaf.ConvexAnalysis.PolyhedralFn.polyhedral_sublevel {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} (hf : PolyhedralFn f) (c : ℝ) : Polyhedral {x : E | f x ≤ ↑c}

Every sublevel set of a polyhedral convex function is polyhedral: it is the preimage of the epigraph under the affine map x ↦ (x, c).

theorem Tdaf.ConvexAnalysis.polyhedralFn_indicatorFn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} (hC : Polyhedral C) : PolyhedralFn (indicatorFn C)

The indicator of a polyhedral convex set is a polyhedral convex function. Its epigraph is the half-cylinder C ×ˢ [0, ∞), an intersection of the preimage of C with a half-space.

def Tdaf.ConvexAnalysis.addEpiMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] : (E × ℝ) × E × ℝ →ₗ[ℝ] E × ℝ

The linear map ((x, α), (y, β)) ↦ (x, α + β) used to build the epigraph of a sum.

Equations

• Tdaf.ConvexAnalysis.addEpiMap = { toFun := fun (p : (E × ℝ) × E × ℝ) => (p.1.1, p.1.2 + p.2.2), map_add' := ⋯, map_smul' := ⋯ }

def Tdaf.ConvexAnalysis.diagMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] : (E × ℝ) × E × ℝ →ₗ[ℝ] E

The linear map ((x, α), (y, β)) ↦ x - y, whose kernel is the "same first coordinate" condition.

Equations

• Tdaf.ConvexAnalysis.diagMap = { toFun := fun (p : (E × ℝ) × E × ℝ) => p.1.1 - p.2.1, map_add' := ⋯, map_smul' := ⋯ }

theorem Tdaf.ConvexAnalysis.PolyhedralFn.add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f g : E → EReal} (hf : PolyhedralFn f) (hg : PolyhedralFn g) (hf' : ∀ (x : E), f x ≠ ⊥) (hg' : ∀ (x : E), g x ≠ ⊥) : PolyhedralFn (f + g)

A sum of polyhedral convex functions is polyhedral.

The epigraph of the sum is the image, under ((x, α), (y, β)) ↦ (x, α + β), of the polyhedral set (epi f ×ˢ epi g) ∩ ker (x, y) ↦ x - y; the ⊥-freeness hypotheses make the splitting f x + g x ≤ μ ↔ ∃ α β, f x ≤ α ∧ g x ≤ β ∧ α + β = μ correct in EReal.

theorem Tdaf.ConvexAnalysis.epi_infConv_of_polyhedralFn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : PolyhedralFn f) {g : E → EReal} (hg : PolyhedralFn g) : epi (infConv f g) = epi f + epi g

The attainment half: for polyhedral f and g the sum of the epigraphs is the epigraph of the infimal convolute, so the infimum defining (f □ g) x is attained whenever it is finite. A sum of epigraphs is always upward closed, and here it is also closed, being polyhedral; those are the two halves of IsEpiLike.

theorem Tdaf.ConvexAnalysis.PolyhedralFn.infConv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : PolyhedralFn f) {g : E → EReal} (hg : PolyhedralFn g) : PolyhedralFn (ConvexAnalysis.infConv f g)

An infimal convolute of polyhedral convex functions is polyhedral: its epigraph is the sum of the two epigraphs.