Closedness of a finitely generated cone (Weyl) #

The finitely generated cone cone{v k} = {∑ k, c k • v k : c ≥ 0} spanned by a finite family v : κ → E in a real normed space is closed. This is the nontrivial half of the Farkas–Minkowski–Weyl correspondence and the key topological input to the geometric Farkas lemma / finite LP strong duality.

Mathlib has ProperCone (whose closedness is part of the structure) and geometric hyperplane separation, but does not provide the closedness result proved here.

Main results #

LeanPool.Erdos81PaperIContrib.simplicial_cone_isClosed — a simplicial cone is closed.
LeanPool.Erdos81PaperIContrib.conic_caratheodory — conic Carathéodory reduction.
LeanPool.Erdos81PaperIContrib.fg_cone_isClosed — a finitely generated cone is closed.

Generalization vs. the source #

The Paper I version was stated over EuclideanSpace ℝ ι. None of the three proofs uses the inner product; they are ported here to an arbitrary real normed space E ([NormedAddCommGroup E] [NormedSpace ℝ E]), which is the natural Mathlib generality.

source

theorem LeanPool.Erdos81PaperIContrib.simplicial_cone_isClosed {κ : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (v : κ → E) (s : Finset κ) (hli : LinearIndepOn ℝ v ↑s) :

IsClosed {y : E | ∃ (c : κ → ℝ), (∀ (k : κ), 0 ≤ c k) ∧ (∀ k ∉ s, c k = 0) ∧ ∑ k ∈ s, c k • v k = y}

A simplicial cone — the nonnegative combinations of a linearly independent finite family — is closed: it is the image of the closed nonnegative orthant under an injective (hence closed-embedding) linear map from a finite-dimensional space.

source

theorem LeanPool.Erdos81PaperIContrib.conic_caratheodory {κ : Type u_1} {R : Type u_4} {M : Type u_5} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] [Fintype κ] (v : κ → M) (c : κ → R) (hc : ∀ (k : κ), 0 ≤ c k) :

∃ (d : κ → R) (s : Finset κ), (∀ (k : κ), 0 ≤ d k) ∧ (∀ k ∉ s, d k = 0) ∧ LinearIndepOn R v ↑s ∧ ∑ k ∈ s, d k • v k = ∑ k : κ, c k • v k

Conic Carathéodory. Over any linearly ordered field, a nonnegative combination of a finite family equals a nonnegative combination over a linearly independent subfamily with the same value. This algebraic reduction requires no topology on the ambient module.

source

theorem LeanPool.Erdos81PaperIContrib.fg_cone_isClosed {κ : Type u_1} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype κ] (v : κ → E) :

IsClosed {y : E | ∃ (c : κ → ℝ), (∀ (k : κ), 0 ≤ c k) ∧ ∑ k : κ, c k • v k = y}

Weyl. The finitely generated cone {∑ k, c k • v k : c ≥ 0} is closed.

Integration with the Mathlib `PointedCone` API #

We restate closedness in Mathlib's cone vocabulary. PointedCone ℝ E is Submodule {c : ℝ // 0 ≤ c} E; PointedCone.hull ℝ s is its conic hull. The bridge below identifies the span (as a set) with the engine's explicit conic-combination set, handling the ℝ≥0-vs-ℝ scalar action.

source