Farkas.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite rational cone duality

A finite family of integral vectors admits a normalized nonnegative linear functional whenever the negative normalizing vector has no positive integral multiple in the monoid generated by the family.

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_normalized_nonneg_linear_of_no_nat_certificate_of_isClosed line 19

Source documentation

Closed-cone separation followed by rational certificate extraction yields a normalized nonnegative linear functional.

theorem exists_normalized_nonneg_linear_of_no_nat_certificate_of_isClosed
    {I J : Type*} [Fintype I] [Fintype J]
    (A : I → J → ℤ) (u : J → ℤ)
    (hclosed : IsClosed (PointedCone.hull ℝ
      (Set.range (fun i j ↦ (A i j : ℝ))) : Set (J → ℝ)))
    (hno : ¬ ∃ D : ℕ, 0 < D ∧ ∃ c : I → ℕ,
      ∀ j, ∑ i, (c i : ℤ) * A i j = -(D : ℤ) * u j) :
    ∃ L : (J → ℝ) →ₗ[ℝ] ℝ,
      L (fun j ↦ (u j : ℝ)) = 1 ∧
      ∀ i, 0 ≤ L (fun j ↦ (A i j : ℝ)) := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_normalized_nonneg_linear_of_no_nat_certificate line 59

Source documentation

A finite integral cone either contains a positive integer multiple of the negative normalizing vector, or admits a linear functional which is nonnegative on the generators and takes value one on that vector.

theorem exists_normalized_nonneg_linear_of_no_nat_certificate
    {I J : Type*} [Fintype I] [Fintype J]
    (A : I → J → ℤ) (u : J → ℤ)
    (hno : ¬ ∃ D : ℕ, 0 < D ∧ ∃ c : I → ℕ,
      ∀ j, ∑ i, (c i : ℤ) * A i j = -(D : ℤ) * u j) :
    ∃ L : (J → ℝ) →ₗ[ℝ] ℝ,
      L (fun j ↦ (u j : ℝ)) = 1 ∧
      ∀ i, 0 ≤ L (fun j ↦ (A i j : ℝ)) :=
…