The positively homogeneous convex function generated by finitely many points

A convex set generated by finitely many points and directions is polyhedral. This module proves the function-level form the Helly-type theorems on systems of inequalities consume: the positively homogeneous convex function generated by finitely many points is polyhedral.

That function is posHomGen f, whose epigraph is not the convex cone generated by epi f, because that cone is not upward closed at the origin: for posHomGen (δ(· | {a}) + α) the epigraph must also contain the vertical ray above the origin. This is why the generator list for epi k₀ carries the extra point (0, 1).

Main results

• epi_posHomGen_of_epi_eq — if epi f is conv P plus the vertical ray, for a finite P, then epi (posHomGen f) is the convex cone generated by P together with (0, 1); polyhedralFn_posHomGen_of_epi_eq is that this function is polyhedral.
• epi_convFn_of_epi_eq, polyhedralFn_posHomGen_convFn — the same for the function those theorems build, generated by the convex hull of finitely many functions whose epigraphs are single translated vertical rays.

Implementation notes

The hypothesis is epi f = conv P + cone {(0,1)}, not "f is polyhedral". For a general direction set D, epi (posHomGen f) = cone (P ∪ D ∪ {(0,1)}) is false: for f x = |x| + 1 on ℝ the point (1, 1) lies in epi (posHomGen f) = epi |·| but in no finite nonnegative combination of epi f ∪ {(0,1)}. A closure is needed unless the direction set is exactly the vertical ray — which is the case used there, the conjugate of an affine function being a point indicator.

References

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

noncomputable def Tdaf.ConvexAnalysis.verticalRay (E : Type u_2) [AddCommGroup E] [Module ℝ E] : PointedCone ℝ (E × ℝ)

The vertical ray {0} × [0, ∞) of E × ℝ, as a pointed cone: the cone generated by (0, 1). Adding it to a set is what makes the set upward closed.

Equations

• Tdaf.ConvexAnalysis.verticalRay E = PointedCone.hull ℝ {(0, 1)}

theorem Tdaf.ConvexAnalysis.mem_verticalRay_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] {p : E × ℝ} : p ∈ verticalRay E ↔ ∃ (c : ℝ), 0 ≤ c ∧ p = (0, c)

theorem Tdaf.ConvexAnalysis.epi_posHomGen_of_epi_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} {P : Finset (E × ℝ)} (hepi : epi f = (convexHull ℝ) ↑P + ↑(verticalRay E)) : epi (posHomGen f) = ↑(PointedCone.hull ℝ (insert (0, 1) ↑P))

The epigraph of the positively homogeneous convex function generated by finitely many points. If epi f is the convex hull of a finite set P plus the vertical ray, then epi (posHomGen f) is the convex cone generated by P together with (0, 1). The extra generator is not decoration: the cone generated by epi f alone meets the vertical axis in {0} only.

theorem Tdaf.ConvexAnalysis.polyhedralFn_posHomGen_of_epi_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} {P : Finset (E × ℝ)} (hepi : epi f = (convexHull ℝ) ↑P + ↑(verticalRay E)) : PolyhedralFn (posHomGen f)

The positively homogeneous convex function generated by finitely many points is polyhedral.

theorem Tdaf.ConvexAnalysis.epi_convFn_of_epi_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ι : Type u_2} [Finite ι] {g : ι → E → EReal} {p : ι → E × ℝ} (hg : ∀ (i : ι), epi (g i) = {p i} + ↑(verticalRay E)) : epi (convFn g) = (convexHull ℝ) (Set.range p) + ↑(verticalRay E)

The convex hull of finitely many translated vertical rays. If each g i has for epigraph the vertical ray above a single point p i — what the conjugate of an affine function looks like — then convFn g has for epigraph the convex hull of the p i plus the vertical ray. IsEpiLike is not automatic for a convex hull of a union; here it is paid for by finite generation, the right-hand side being conv P + cone {(0,1)}, hence closed and absorbing the vertical ray.

theorem Tdaf.ConvexAnalysis.polyhedralFn_posHomGen_convFn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {ι : Type u_2} [Finite ι] {g : ι → E → EReal} {p : ι → E × ℝ} (hg : ∀ (i : ι), epi (g i) = {p i} + ↑(verticalRay E)) : PolyhedralFn (posHomGen (convFn g))

The same, in the form the systems-of-inequalities theorems ask for: the positively homogeneous convex function generated by the convex hull of finitely many point indicators is polyhedral — the k₀ there, once the conjugates of the affine fᵢ are identified as point indicators.