Convex
Results named in Tau Ceti's TauCeti.Geometry.Convex modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremGordan'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.
TauCeti.exists_forall_dual_pos_iff.{u_1, u_2, u_3} {ι : Type u_1} {K : Type u_2} {V : Type u_3}
[Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommGroup V] [_root_.Module K V] [Fintype ι]
(a : ι → V) : (∃ y, ∀ (j : ι), 0 < y (a j)) ↔ ∀ (x : ι → K), 0 ≤ x → ∑ j, x j • a j = 0 → x = 0
Uses 1 · Used by 1
TheoremHoffman's error bound for a polyhedral cone#
Let a j be finitely many functionals on a
finite-dimensional space. There is a constant C such that every w with -c ≤ a j w for all
j, where 0 ≤ c, lies within C * c of the cone {w' | ∀ j, 0 ≤ a j w'}, as measured by
finitely many prescribed functionals b k. The constant C is nonnegative.
TauCeti.exists_forall_abs_apply_sub_le_of_forall_neg_le.{u_1, u_2, u_3, u_4} {ι : Type u_1}
{κ : Type u_2} {K : Type u_3} {V : Type u_4} [Field K] [AddCommGroup V] [_root_.Module K V]
[LinearOrder K] [IsStrictOrderedRing K] [Finite ι] [Finite κ] [FiniteDimensional K V]
(a : ι → Module.Dual K V) (b : κ → Module.Dual K V) :
∃ C,
0 ≤ C ∧
∀ (c : K),
0 ≤ c →
∀ (w : V),
(∀ (j : ι), -c ≤ (a j) w) →
∃ w', (∀ (j : ι), 0 ≤ (a j) w') ∧ ∀ (k : κ), |(b k) (w - w')| ≤ C * c
Lean
Formalized in Tau Ceti as TauCeti.exists_forall_abs_apply_sub_le_of_forall_neg_le.
Sources
Uses 1 · Used by 2
TheoremStiemke'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.
Submodule.exists_pos_dotProduct_eq_zero_iff.{u_4, u_5} {ι : Type u_4} {K : Type u_5} [Fintype ι]
[Field K] [LinearOrder K] [IsStrictOrderedRing K] (S : Submodule K (ι → K)) :
(∃ c, (∀ (i : ι), 0 < c i) ∧ ∀ x ∈ S, c ⬝ᵥ x = 0) ↔ ∀ x ∈ S, 0 ≤ x → x = 0
Uses 1
TheoremTucker'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.
TauCeti.exists_nonneg_sum_smul_eq_zero_and_coeff_add_dual_pos_at.{u_1, u_2, u_3} {ι : Type u_1}
{K : Type u_2} {V : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommGroup V]
[_root_.Module K V] [Fintype ι] (a : ι → V) (k : ι) :
∃ x y, 0 ≤ x ∧ ∑ j, x j • a j = 0 ∧ (∀ (j : ι), 0 ≤ y (a j)) ∧ 0 < x k + y (a k)
Lean
Formalized in Tau Ceti as TauCeti.exists_nonneg_sum_smul_eq_zero_and_coeff_add_dual_pos_at.
Sources
Used by 1
TheoremTucker'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.
TauCeti.exists_nonneg_sum_smul_eq_zero_and_forall_coeff_add_dual_pos.{u_1, u_2, u_3} {ι : Type u_1}
{K : Type u_2} {V : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [AddCommGroup V]
[_root_.Module K V] [Fintype ι] (a : ι → V) :
∃ x y, 0 ≤ x ∧ ∑ j, x j • a j = 0 ∧ (∀ (j : ι), 0 ≤ y (a j)) ∧ ∀ (j : ι), 0 < x j + y (a j)
Lean
Formalized in Tau Ceti as TauCeti.exists_nonneg_sum_smul_eq_zero_and_forall_coeff_add_dual_pos.
Other forms
Tucker's theorem over the integers. Formalized in Tau Ceti as TauCeti.exists_nat_sum_nsmul_eq_zero_and_forall_coeff_add_dual_pos.
TauCeti.exists_nat_sum_nsmul_eq_zero_and_forall_coeff_add_dual_pos.{u_1, u_4} {ι : Type u_1}
{N : Type u_4} [AddCommGroup N] [Module.Free ℤ N] [Module.Finite ℤ N] [Fintype ι] (a : ι → N) :
∃ x m, ∑ j, x j • a j = 0 ∧ (∀ (j : ι), 0 ≤ m (a j)) ∧ ∀ (j : ι), 0 < ↑(x j) + m (a j)
Sources
Uses 1 · Used by 9
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.