Polyhedral convex sets and the Minkowski–Weyl theorem

A convex set is polyhedral when it is the solution set of finitely many linear inequalities, and finitely generated when it is conv P + cone D for finite sets of points P and directions D. The Minkowski–Weyl theorem says the two agree in finite dimensions.

The proof is the cone case (Polyhedral/Cone.lean) plus homogenisation: a set C ⊆ E is the level-one slice {x | (1, x) ∈ K} of a cone K ⊆ ℝ × E, the two descriptions of C correspond to the two descriptions of K, and the correspondence is slice_hull_union.

Main definitions

• Polyhedral C — C is cut out by finitely many inequalities φ x ≤ b.
• FinitelyGenerated C — C = conv P + cone D for finite P, D.
• coneOver C hC — the convex cone in ℝ × E generated by {1} × C, for convex C.

Main results

• slice_hull_union — the level-one slice of the cone generated by {1} × P ∪ {0} × D is conv P + cone D. This is the whole of the homogenisation dictionary.
• polyhedral_iff_finitelyGenerated — the Minkowski–Weyl theorem (Theorem 19.1 in [^1]).
• Polyhedral.isClosed, Polyhedral.convex, and the same for FinitelyGenerated.

Implementation notes

Polyhedral is stated as {x | ∀ q ∈ s, q.1 x ≤ q.2} rather than as the equal ⋂ q ∈ s, {x | q.1 x ≤ q.2}, because that is the form every proof here manipulates; Polyhedral.eq_biInter records the other. The empty set is both polyhedral (a system can be inconsistent) and finitely generated (conv ∅ = ∅); the classical statement quietly assumes C ≠ ∅ in places, but the slice picture handles it, since (1, x) never lies in the cone generated by {0} × D.

References

[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §19.

Lifting a set to level 0 or level 1 of ℝ × E

def Tdaf.ConvexAnalysis.liftAt {E : Type u_1} (a : ℝ) (S : Set E) : Set (ℝ × E)

The copy of S at height a in ℝ × E.

Equations

• Tdaf.ConvexAnalysis.liftAt a S = (fun (x : E) => (a, x)) '' S

@[simp]

theorem Tdaf.ConvexAnalysis.mem_liftAt {E : Type u_1} {a : ℝ} {S : Set E} {p : ℝ × E} : p ∈ liftAt a S ↔ p.1 = a ∧ p.2 ∈ S

def Tdaf.ConvexAnalysis.inrₙ {E : Type u_1} [AddCommGroup E] [Module ℝ E] : E →ₗ[{ c : ℝ // 0 ≤ c }] ℝ × E

The height-0 lift, as a map of ℝ≥0-modules. Building it by hand rather than restricting scalars along ℝ≥0 → ℝ keeps Submodule.map_span applicable without an IsScalarTower detour.

Equations

• Tdaf.ConvexAnalysis.inrₙ = { toFun := fun (x : E) => (0, x), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Tdaf.ConvexAnalysis.inrₙ_apply {E : Type u_1} [AddCommGroup E] [Module ℝ E] (x : E) : inrₙ x = (0, x)

theorem Tdaf.ConvexAnalysis.coe_hull_liftZero {E : Type u_1} [AddCommGroup E] [Module ℝ E] (D : Set E) : ↑(PointedCone.hull ℝ (liftAt 0 D)) = liftAt 0 ↑(PointedCone.hull ℝ D)

The height-0 lift of a cone hull is the cone hull of the height-0 lift.

The cone over a convex set

def Tdaf.ConvexAnalysis.coneOver {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Set E) (hC : Convex ℝ C) : PointedCone ℝ (ℝ × E)

The convex cone in ℝ × E generated by the height-one copy of a convex set C: the pairs (a, x) with a > 0 and a⁻¹ • x ∈ C, together with the origin.

Equations

• Tdaf.ConvexAnalysis.coneOver C hC = { carrier := {p : ℝ × E | 0 < p.1 ∧ p.1⁻¹ • p.2 ∈ C ∨ p = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Tdaf.ConvexAnalysis.mem_coneOver {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} {hC : Convex ℝ C} {p : ℝ × E} : p ∈ coneOver C hC ↔ 0 < p.1 ∧ p.1⁻¹ • p.2 ∈ C ∨ p = 0

theorem Tdaf.ConvexAnalysis.slice_hull_liftOne {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P : Set E) : {x : E | (1, x) ∈ ↑(PointedCone.hull ℝ (liftAt 1 P))} = (convexHull ℝ) P

The level-one slice of the cone generated by a height-one lift is the convex hull.

theorem Tdaf.ConvexAnalysis.slice_hull_union {E : Type u_1} [AddCommGroup E] [Module ℝ E] (P D : Set E) : {x : E | (1, x) ∈ ↑(PointedCone.hull ℝ (liftAt 1 P ∪ liftAt 0 D))} = (convexHull ℝ) P + ↑(PointedCone.hull ℝ D)

The homogenisation dictionary. The level-one slice of the convex cone generated by {1} × P ∪ {0} × D is conv P + cone D. Both halves of Minkowski–Weyl go through this identity.

Polyhedral and finitely generated sets

def Tdaf.ConvexAnalysis.Polyhedral {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Set E) : Prop

A polyhedral convex set: the solution set of finitely many linear inequalities.

Equations

• Tdaf.ConvexAnalysis.Polyhedral C = ∃ (s : Finset ((E →ₗ[ℝ] ℝ) × ℝ)), C = {x : E | ∀ q ∈ s, q.1 x ≤ q.2}

def Tdaf.ConvexAnalysis.FinitelyGenerated {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Set E) : Prop

A finitely generated convex set: conv P + cone D for finite sets of points P and directions D.

Equations

• Tdaf.ConvexAnalysis.FinitelyGenerated C = ∃ (P : Finset E) (D : Finset E), C = (convexHull ℝ) ↑P + ↑(PointedCone.hull ℝ ↑D)

theorem Tdaf.ConvexAnalysis.Polyhedral.eq_biInter {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} (hC : Polyhedral C) : ∃ (s : Finset ((E →ₗ[ℝ] ℝ) × ℝ)), C = ⋂ q ∈ s, {x : E | q.1 x ≤ q.2}

The ⋂ form of the definition.

theorem Tdaf.ConvexAnalysis.Polyhedral.convex {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} (hC : Polyhedral C) : Convex ℝ C

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

Homogenisation of a polyhedral set

theorem Tdaf.ConvexAnalysis.Polyhedral.of_slice {E : Type u_1} [AddCommGroup E] [Module ℝ E] {K : Set (ℝ × E)} (hK : PolyhedralCone K) : Polyhedral {x : E | (1, x) ∈ K}

The level-one slice of a polyhedral cone is a polyhedral set: substituting 1 for the homogenising variable turns Ψ (a, x) ≤ 0 into ψ x ≤ b.

theorem Tdaf.ConvexAnalysis.Polyhedral.exists_polyhedralCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} (hC : Polyhedral C) : ∃ (K : Set (ℝ × E)), PolyhedralCone K ∧ K ⊆ {p : ℝ × E | 0 ≤ p.1} ∧ {x : E | (1, x) ∈ K} = C

A polyhedral set is the level-one slice of a polyhedral cone lying in the closed upper half-space. The cone is Rockafellar's homogenisation: a ≥ 0 together with φ x ≤ b a for each inequality φ x ≤ b of the original system.

theorem Tdaf.ConvexAnalysis.exists_liftOne_liftZero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : Finset (ℝ × E)} (hg : ∀ p ∈ g, 0 ≤ p.1) : ∃ (P : Finset E) (D : Finset E), ↑(PointedCone.hull ℝ ↑g) = ↑(PointedCone.hull ℝ (liftAt 1 ↑P ∪ liftAt 0 ↑D))

Rewriting a finite generating set of a cone contained in the closed upper half-space as a height-one part and a height-zero part: the generators with p.1 > 0 are rescaled to height one, those with p.1 = 0 are directions.

The Minkowski–Weyl theorem

theorem Tdaf.ConvexAnalysis.FinitelyGenerated.polyhedral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} (hC : FinitelyGenerated C) : Polyhedral C

Weyl's half: a finitely generated convex set is polyhedral.

theorem Tdaf.ConvexAnalysis.Polyhedral.finitelyGenerated {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} (hC : Polyhedral C) : FinitelyGenerated C

Minkowski's half: a polyhedral convex set is finitely generated.

theorem Tdaf.ConvexAnalysis.polyhedral_iff_finitelyGenerated {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} : Polyhedral C ↔ FinitelyGenerated C

The Minkowski–Weyl theorem: in a finite-dimensional space a convex set is polyhedral if and only if it is finitely generated.

theorem Tdaf.ConvexAnalysis.Polyhedral.isClosed {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} (hC : Polyhedral C) : IsClosed C

A polyhedral set is closed.

theorem Tdaf.ConvexAnalysis.FinitelyGenerated.isClosed {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} (hC : FinitelyGenerated C) : IsClosed C

A finitely generated convex set is closed; in particular the sum of a polytope and a finitely generated cone is closed.

theorem Tdaf.ConvexAnalysis.polyhedral_convexHull_finset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (P : Finset E) : Polyhedral ((convexHull ℝ) ↑P)

The convex hull of a finite set — a polytope — is polyhedral.