Polyhedral convex cones and the Minkowski–Weyl theorem

A convex cone can be described in two ways: from outside, as the solution set of finitely many homogeneous linear inequalities (PolyhedralCone, an H-cone), or from inside, as the set of nonnegative combinations of finitely many vectors (FinitelyGeneratedCone, a V-cone). In finite dimensions the two descriptions are equivalent — the Minkowski–Weyl theorem, the foundation of the rest of the polyhedral theory. Mathlib has the two predicates for pointed cones (PointedCone.DualFG and PointedCone.FG) but not the equivalence.

Main results

• FinitelyGeneratedCone.polyhedralCone — Weyl's half, V ⇒ H, by Fourier–Motzkin elimination. Purely algebraic: no topology, only FiniteDimensional.
• PolyhedralCone.isClosed, FinitelyGeneratedCone.isClosed — a corollary of Weyl's half, and the reason Weyl is proved first.
• PolyhedralCone.finitelyGeneratedCone — Minkowski's half, H ⇒ V, by separation in the dual.
• polyhedralCone_iff_finitelyGeneratedCone — the Minkowski–Weyl theorem for cones (Theorem 19.1 in [^1]).

Implementation notes

Fourier–Motzkin is run once, for Weyl's half, in the form "adding a ray to a polyhedral cone leaves it polyhedral" (PolyhedralCone.add_ray); closedness of a finitely generated cone is then free, and Carathéodory is not needed. Minkowski's half pairs E with Module.Dual ℝ E directly and uses only geometric_hahn_banach_closed_point, which keeps the statement free of a pairing parameter. add_ray is stated with a difference, {x | ∃ t ≥ 0, x - t • v ∈ K}, rather than the equal K + {t • v | t ≥ 0}, because that is the form the elimination proof manipulates.

References

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

Homogeneous half-spaces cut out by linear functionals

def Tdaf.ConvexAnalysis.halfSpaceConeₗ {M : Type u_1} [AddCommGroup M] [Module ℝ M] (θ : M →ₗ[ℝ] ℝ) : PointedCone ℝ M

The homogeneous half-space {m | θ m ≤ 0} of a linear functional, bundled as a pointed cone.

Separation.lean's halfSpaceCone is the same construction for a continuous functional; the algebraic version is what Weyl's half of Minkowski–Weyl needs, since that half uses no topology.

Equations

• Tdaf.ConvexAnalysis.halfSpaceConeₗ θ = { carrier := {m : M | θ m ≤ 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Tdaf.ConvexAnalysis.mem_halfSpaceConeₗ {M : Type u_1} [AddCommGroup M] [Module ℝ M] {θ : M →ₗ[ℝ] ℝ} {m : M} : m ∈ halfSpaceConeₗ θ ↔ θ m ≤ 0

theorem Tdaf.ConvexAnalysis.forall_nonpos_of_mem_hull {M : Type u_1} [AddCommGroup M] [Module ℝ M] {θ : M →ₗ[ℝ] ℝ} {S : Set M} (h : ∀ m ∈ S, θ m ≤ 0) {m : M} (hm : m ∈ PointedCone.hull ℝ S) : θ m ≤ 0

A linear functional nonpositive on a set is nonpositive on the convex cone it generates.

This is the workhorse of the file: both halves of Minkowski–Weyl use it, once in E and once in the dual of E, which is why it is stated for an arbitrary module.

The two descriptions of a cone

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

A polyhedral convex cone: the solution set of finitely many homogeneous linear inequalities. Rockafellar's "polyhedral convex cone", and the H-cone of the linear-programming literature.

Equations

• Tdaf.ConvexAnalysis.PolyhedralCone K = ∃ (s : Finset (E →ₗ[ℝ] ℝ)), K = {x : E | ∀ φ ∈ s, φ x ≤ 0}

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

A finitely generated convex cone: the set of nonnegative combinations of finitely many vectors. The V-cone of the linear-programming literature.

Equations

• Tdaf.ConvexAnalysis.FinitelyGeneratedCone K = ∃ (s : Finset E), K = ↑(PointedCone.hull ℝ ↑s)

theorem Tdaf.ConvexAnalysis.PolyhedralCone.convex {E : Type u_1} [AddCommGroup E] [Module ℝ E] {K : Set E} (hK : PolyhedralCone K) : Convex ℝ K

theorem Tdaf.ConvexAnalysis.PolyhedralCone.zero_mem {E : Type u_1} [AddCommGroup E] [Module ℝ E] {K : Set E} (hK : PolyhedralCone K) : 0 ∈ K

theorem Tdaf.ConvexAnalysis.PolyhedralCone.smul_mem {E : Type u_1} [AddCommGroup E] [Module ℝ E] {K : Set E} (hK : PolyhedralCone K) {a : ℝ} (ha : 0 ≤ a) {x : E} (hx : x ∈ K) : a • x ∈ K

theorem Tdaf.ConvexAnalysis.FinitelyGeneratedCone.convex {E : Type u_1} [AddCommGroup E] [Module ℝ E] {K : Set E} (hK : FinitelyGeneratedCone K) : Convex ℝ K

theorem Tdaf.ConvexAnalysis.FinitelyGeneratedCone.zero_mem {E : Type u_1} [AddCommGroup E] [Module ℝ E] {K : Set E} (hK : FinitelyGeneratedCone K) : 0 ∈ K

theorem Tdaf.ConvexAnalysis.FinitelyGeneratedCone.smul_mem {E : Type u_1} [AddCommGroup E] [Module ℝ E] {K : Set E} (hK : FinitelyGeneratedCone K) {a : ℝ} (ha : 0 ≤ a) {x : E} (hx : x ∈ K) : a • x ∈ K

Weyl's half: a finitely generated cone is polyhedral

theorem Tdaf.ConvexAnalysis.coe_hull_insert {E : Type u_1} [AddCommGroup E] [Module ℝ E] (v : E) (S : Set E) : ↑(PointedCone.hull ℝ (insert v S)) = {x : E | ∃ (t : ℝ), 0 ≤ t ∧ x - t • v ∈ ↑(PointedCone.hull ℝ S)}

Adjoining a generator to a cone hull adds a ray to it.

theorem Tdaf.ConvexAnalysis.PolyhedralCone.add_ray {E : Type u_1} [AddCommGroup E] [Module ℝ E] {K : Set E} (hK : PolyhedralCone K) (v : E) : PolyhedralCone {x : E | ∃ (t : ℝ), 0 ≤ t ∧ x - t • v ∈ K}

Fourier–Motzkin elimination. Adding a ray to a polyhedral cone leaves it polyhedral.

The inequalities of the new cone are those old inequalities φ with φ v ≤ 0, kept unchanged, together with one combination (ψ v) • χ - (χ v) • ψ for each pair with ψ v > 0 and χ v < 0: those are exactly the consequences of the old system that do not mention the eliminated variable.

theorem Tdaf.ConvexAnalysis.polyhedralCone_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] [FiniteDimensional ℝ E] : PolyhedralCone {0}

In a finite-dimensional space the origin is a polyhedral cone: it is cut out by the 2 n inequalities ± bᵢ* x ≤ 0 for a basis b. This is the base of the induction in Weyl's half, and the only place finite-dimensionality enters it.

theorem Tdaf.ConvexAnalysis.FinitelyGeneratedCone.polyhedralCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : FinitelyGeneratedCone K) : PolyhedralCone K

Weyl's half of Minkowski–Weyl: a finitely generated convex cone is polyhedral.

The proof is an induction on the generators: the origin is polyhedral, and add_ray adds one generator at a time. No topology is involved.

Closedness

theorem Tdaf.ConvexAnalysis.PolyhedralCone.isClosed {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : PolyhedralCone K) : IsClosed K

A polyhedral cone is closed: it is a finite intersection of closed half-spaces, and in finite dimensions every linear functional is continuous.

theorem Tdaf.ConvexAnalysis.FinitelyGeneratedCone.isClosed {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : FinitelyGeneratedCone K) : IsClosed K

A finitely generated convex cone is closed. The classical route is Carathéodory's theorem, before Minkowski–Weyl; here it is a corollary of Weyl's half.

Minkowski's half, and the equivalence of the two descriptions

theorem Tdaf.ConvexAnalysis.PolyhedralCone.finitelyGeneratedCone {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : PolyhedralCone K) : FinitelyGeneratedCone K

Minkowski's half of Minkowski–Weyl: a polyhedral convex cone is finitely generated.

The generators are produced in the dual: the cone C generated by the constraint functionals is finitely generated, hence polyhedral by Weyl's half, and the functionals cutting C out are evaluations at points v₁, …, v_m of E because a finite-dimensional space is reflexive. Those points generate K. One inclusion is immediate; the other separates a point of K from the cone they generate — which is closed, again by Weyl's half — and observes that the separating functional lies in C.

theorem Tdaf.ConvexAnalysis.polyhedralCone_iff_finitelyGeneratedCone {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} : PolyhedralCone K ↔ FinitelyGeneratedCone K

The Minkowski–Weyl theorem, for cones. In a finite-dimensional space, a convex cone is cut out by finitely many homogeneous linear inequalities if and only if it is generated by finitely many vectors.