Conic Carathéodory: thinning positive dependences

A positive dependence on a finite set of vectors — strictly positive weights summing the vectors to zero — can be thinned to one supported on at most finrank + 1 of them. This is the conic counterpart of Carathéodory's theorem, proved by strong induction on the support cardinality with a single linear pivot step that strictly shrinks the positive support each round.

Main declarations

• Caratheodory.exists_posdep_card_le_finrank_add_one — the general bound over a linearly ordered field.
• Caratheodory.exists_posdep_card_le_five — the specialisation to Fin 4 → ℚ (bound 5) consumed by the Fin 4 cancellation proof.

theorem Caratheodory.exists_posdep_card_le_finrank_add_one {K : Type u_1} {E : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommGroup E] [Module K E] [Module.Finite K E] (s : Finset E) (c : E → K) (hpos : ∀ v ∈ s, 0 < c v) (hne : s.Nonempty) (hsum : ∑ v ∈ s, c v • v = 0) : ∃ t ⊆ s, t.Nonempty ∧ t.card ≤ Module.finrank K E + 1 ∧ ∃ (d : E → K), (∀ v ∈ t, 0 < d v) ∧ ∑ v ∈ t, d v • v = 0

Conic Carathéodory. A positive dependence among finitely many vectors of a finite-dimensional space over a linearly ordered field can be thinned to one supported on at most finrank + 1 of them.

theorem Caratheodory.exists_posdep_card_le_five (V : Finset (Fin 4 → ℚ)) (c : (Fin 4 → ℚ) → ℚ) (hpos : ∀ v ∈ V, 0 < c v) (hne : V.Nonempty) (hsum : ∑ v ∈ V, c v • v = 0) : ∃ S ⊆ V, S.Nonempty ∧ S.card ≤ 5 ∧ ∃ (d : (Fin 4 → ℚ) → ℚ), (∀ v ∈ S, 0 < d v) ∧ ∑ v ∈ S, d v • v = 0

Conic Carathéodory for Fin 4 → ℚ: a positive dependence thins to support ≤ 5.