Theorems of the alternative for nonnegative vectors

This file proves the classical theorems of the alternative of Gordan, Stiemke and Tucker over an arbitrary linearly ordered field, and Tucker's theorem for finite free ℤ-modules.

For a finite family of vectors a j in a vector space over a linearly ordered field K, Gordan's theorem says that either some linear functional is strictly positive on every a j, or the family admits a nontrivial linear relation with nonnegative coefficients, and not both. Applied to the images of the coordinate vectors in a quotient (ι → K) ⧸ S, it becomes Stiemke's theorem: a subspace S contains no nonzero nonnegative vector exactly when some strictly positive vector is orthogonal to all of S. Both are consequences of Tucker's key lemma, which for each index k produces a nonnegative relation x and a functional y that is nonnegative on the family, one of them strictly positive at k. Summing these over all k gives Tucker's theorem: a single nonnegative relation x and a single functional y, nonnegative on the family, such that x j + y (a j) > 0 for every j. Unlike Mathlib's separation-based Farkas lemma ProperCone.hyperplane_separation, these results apply over ℚ.

Clearing denominators in rational coordinates turns Tucker's theorem into a statement about a finite family in a finite free ℤ-module, with a relation with natural-number coefficients and an integer-valued functional. In toric geometry this integral form produces the character separating two cones along their common face.

The integer-lattice form of Stiemke's theorem is proved in TauCeti.Algebra.Group.AddSubgroup.PositiveWeights. The equivalent finiteness condition for nonnegative vectors in cosets is proved in TauCeti.Algebra.Group.AddSubgroup.NonnegativeCoset.

These results supply the field-level alternative needed for the integer-lattice admissibility lemmas of Heegaard Floer theory.

Main declarations

• TauCeti.exists_nonneg_sum_smul_eq_zero_and_coeff_add_dual_pos_at: Tucker's key lemma.
• TauCeti.exists_nonneg_sum_smul_eq_zero_and_forall_coeff_add_dual_pos: Tucker's theorem.
• TauCeti.exists_nat_sum_nsmul_eq_zero_and_forall_coeff_add_dual_pos: Tucker's theorem for a finite family in a finite free ℤ-module.
• TauCeti.exists_forall_dual_pos_iff: Gordan's theorem.
• Submodule.exists_pos_dotProduct_eq_zero_iff: Stiemke's theorem for a subspace of ι → K.

References

• A. W. Tucker, Dual systems of homogeneous linear relations, in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, 1956, Lemma 1.
• C. G. Broyden, A simple algebraic proof of Farkas's lemma and related theorems, Optimization Methods and Software 8 (1998).
• P. Ozsváth, Z. Szabó, Holomorphic disks and topological invariants for closed three-manifolds, Ann. of Math. 159 (2004), arXiv:math/0101206, Lemmas 4.12 and 4.13.

theorem TauCeti.exists_nonneg_sum_smul_eq_zero_and_coeff_add_dual_pos_at {ι : Type u_1} {K : Type u_2} {V : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommGroup V] [Module K V] [Fintype ι] (a : ι → V) (k : ι) : ∃ (x : ι → K) (y : Module.Dual K V), 0 ≤ x ∧ ∑ j : ι, x j • a j = 0 ∧ (∀ (j : ι), 0 ≤ y (a j)) ∧ 0 < x k + y (a k)

Tucker's key lemma. For a finite family of vectors a j and an index k, there are a nonnegative linear relation x among the a j and a linear functional y that is nonnegative on every a j, such that x k + y (a k) > 0: either a k occurs in a nonnegative relation, or some functional nonnegative on the family is strictly positive on a k.

theorem TauCeti.exists_nonneg_sum_smul_eq_zero_and_forall_coeff_add_dual_pos {ι : Type u_1} {K : Type u_2} {V : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommGroup V] [Module K V] [Fintype ι] (a : ι → V) : ∃ (x : ι → K) (y : Module.Dual K V), 0 ≤ x ∧ ∑ j : ι, x j • a j = 0 ∧ (∀ (j : ι), 0 ≤ y (a j)) ∧ ∀ (j : ι), 0 < x j + y (a j)

Tucker's theorem. For a finite family of vectors a j there are a nonnegative linear relation x among the a j and a linear functional y that is nonnegative on every a j, such that x j + y (a j) > 0 for every j: each vector either occurs in the relation or is strictly positive under y.

theorem TauCeti.exists_forall_dual_pos_iff {ι : Type u_1} {K : Type u_2} {V : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommGroup V] [Module K V] [Fintype ι] (a : ι → V) : (∃ (y : Module.Dual K V), ∀ (j : ι), 0 < y (a j)) ↔ ∀ (x : ι → K), 0 ≤ x → ∑ j : ι, x j • a j = 0 → x = 0

Gordan's theorem. Some linear functional is strictly positive on every vector of a finite family exactly when the only nonnegative linear relation among the vectors is the trivial one.

theorem Submodule.exists_pos_dotProduct_eq_zero_iff {ι : Type u_4} {K : Type u_5} [Fintype ι] [Field K] [LinearOrder K] [IsStrictOrderedRing K] (S : Submodule K (ι → K)) : (∃ (c : ι → K), (∀ (i : ι), 0 < c i) ∧ ∀ x ∈ S, c ⬝ᵥ x = 0) ↔ ∀ x ∈ S, 0 ≤ x → x = 0

Stiemke's theorem. A subspace S of ι → K contains no nonzero nonnegative vector exactly when some vector with strictly positive coordinates is orthogonal to all of S.

theorem TauCeti.exists_nat_sum_nsmul_eq_zero_and_forall_coeff_add_dual_pos {ι : Type u_1} {N : Type u_4} [AddCommGroup N] [Module.Free ℤ N] [Module.Finite ℤ N] [Fintype ι] (a : ι → N) : ∃ (x : ι → ℕ) (m : N →+ ℤ), ∑ j : ι, x j • a j = 0 ∧ (∀ (j : ι), 0 ≤ m (a j)) ∧ ∀ (j : ι), 0 < ↑(x j) + m (a j)

Tucker's theorem over the integers. For a finite family of vectors a j in a finite free ℤ-module there are a linear relation ∑ j, x j • a j = 0 with natural-number coefficients and an integer-valued additive functional m that is nonnegative on every a j, such that x j + m (a j) > 0 for every j.