Finite generation and a finite set of faces

A closed convex set has only finitely many faces exactly when it is finitely generated. This is the third description of a polyhedral convex set: Polyhedral/Defs.lean identifies "polyhedral" with "finitely generated", and this module adds "closed, with a finite set of faces".

Main results

• FinitelyGenerated.finite_setOf_isFace, FinitelyGenerated.of_isFace — a finitely generated set has finitely many faces, each of them finitely generated. Both come from the description of a face as the hull of the generating points it contains and the generating directions in which it recedes, so the faces are indexed by pairs of subsets of the generators.
• finitelyGenerated_of_finite_setOf_isFace, polyhedral_of_finite_setOf_isFace — the converse for a closed convex set, by way of the lineality-zero case finitelyGenerated_of_finite_setOf_isFace_of_containsNoLine.
• polyhedral_iff_isClosed_finite_setOf_isFace — the characterisation the two halves give.

Implementation notes

Extreme directions are counted as rays, not as vectors: extremeDirections C is closed under positive rescaling and so is never finite. What a finite face set bounds is the number of half-line faces, and exists_finite_generating_extremeDirections turns that bound into a finite generating set by choosing a direction vector for each half-line face.

References

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

Counting extreme points and extreme directions

theorem Tdaf.ConvexAnalysis.finite_extremePoints_of_finite_setOf_isFace {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} (hfin : {C' : Set E | IsFace C C'}.Finite) : (Set.extremePoints ℝ C).Finite

A set with finitely many faces has finitely many extreme points, because the extreme points are exactly the singleton faces (isFace_singleton).

theorem Tdaf.ConvexAnalysis.exists_finite_generating_extremeDirections {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} (hfin : {C' : Set E | IsFace C C'}.Finite) : ∃ (D : Set E), D.Finite ∧ D ⊆ extremeDirections C ∧ extremeDirections C ⊆ ↑(PointedCone.hull ℝ D)

A set with finitely many faces has finitely many extreme rays: there is a finite subset of extremeDirections C generating all of it as a pointed cone. Every extreme direction is the direction of a half-line face, and every generator of one lies in that face's recession cone.

theorem Tdaf.ConvexAnalysis.FinitelyGenerated.finite_extremePoints {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} (hC : FinitelyGenerated C) : (Set.extremePoints ℝ C).Finite

A finitely generated set has only finitely many extreme points. extremePoints_convexHullPD_subset puts every extreme point among the generating points, so a Finset of generators bounds them. Nothing here is finite-dimensional or even normed.

The faces of a finitely generated set

theorem Tdaf.ConvexAnalysis.FinitelyGenerated.of_isFace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C C' : Set E} (hC : FinitelyGenerated C) (hface : IsFace C C') : FinitelyGenerated C'

A face of a finitely generated set is finitely generated. The face is the hull of the generating points it contains and the generating directions in which it recedes, both of which are a Finset.filter of the original generators.

theorem Tdaf.ConvexAnalysis.FinitelyGenerated.finite_setOf_isFace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} (hC : FinitelyGenerated C) : {C' : Set E | IsFace C C'}.Finite

A finitely generated set has only finitely many faces, the same description making the face map factor through the pairs of subsets of the two generating sets.

theorem Tdaf.ConvexAnalysis.Polyhedral.of_isFace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C C' : Set E} (hC : Polyhedral C) (hface : IsFace C C') : Polyhedral C'

theorem Tdaf.ConvexAnalysis.Polyhedral.finite_setOf_isFace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} (hC : Polyhedral C) : {C' : Set E | IsFace C C'}.Finite

Finitely many faces forces finite generation

theorem Tdaf.ConvexAnalysis.finitelyGenerated_of_finite_setOf_isFace_of_containsNoLine {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} (hC : Convex ℝ C) (hCcl : IsClosed C) (hnl : ContainsNoLine C) (hfin : {C' : Set E | IsFace C C'}.Finite) : FinitelyGenerated C

A closed convex set containing no lines and having only finitely many faces is finitely generated. The set is the hull of its extreme points and extreme directions, a finite face set bounds both, and replacing the extreme directions by a finite generating set keeps the hull.

theorem Tdaf.ConvexAnalysis.polyhedral_of_finite_setOf_isFace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} (hC : Convex ℝ C) (hCcl : IsClosed C) (hfin : {C' : Set E | IsFace C C'}.Finite) : Polyhedral C

A closed convex set with only finitely many faces is polyhedral. Rockafellar's reduction to lineality zero: with N the lineality space and M a complement, C = N + (C ∩ M), the faces of C ∩ M correspond to those of C, and C ∩ M contains no lines because a line inside it would have its direction in N ⊓ M = ⊥. So C ∩ M is finitely generated and C is a sum of two polyhedral sets.

theorem Tdaf.ConvexAnalysis.finitelyGenerated_of_finite_setOf_isFace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} (hC : Convex ℝ C) (hCcl : IsClosed C) (hfin : {C' : Set E | IsFace C C'}.Finite) : FinitelyGenerated C

A closed convex set with only finitely many faces is finitely generated.

theorem Tdaf.ConvexAnalysis.polyhedral_iff_isClosed_finite_setOf_isFace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} (hC : Convex ℝ C) : Polyhedral C ↔ IsClosed C ∧ {C' : Set E | IsFace C C'}.Finite

A convex set is polyhedral exactly when it is closed and has only finitely many faces. Together with polyhedral_iff_finitelyGenerated this is the full three-way characterisation.

theorem Tdaf.ConvexAnalysis.finitelyGenerated_iff_isClosed_finite_setOf_isFace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} (hC : Convex ℝ C) : FinitelyGenerated C ↔ IsClosed C ∧ {C' : Set E | IsFace C C'}.Finite