OAI/LinearAlgebra/MatrixMultiplication/AuxiliarySeparation/Convex/ConeSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_positive_relation line 18
2. theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_nonneg_representation_erase line 29
3. theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_nonneg_representation_linearIndependent line 67

   Source documentation

   A nonnegative finite combination uses a linearly independent subfamily after possibly changing its coefficients.

   theorem exists_nonneg_representation_linearIndependent (A : I → E) (s : Finset I)
       (w : I → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) :
       ∃ t : Finset I, t ⊆ s ∧ LinearIndependent ℝ (fun i : t ↦ A i) ∧
         ∃ v : I → ℝ, (∀ i ∈ t, 0 ≤ v i) ∧
           (∑ i ∈ t, v i • A i) = ∑ i ∈ s, w i • A i := by
   …

4. theorem OAI.MatrixMultiplication.AuxiliarySeparation.exists_linearIndependent_subcone line 83

   Source documentation

   Every element of a finitely generated cone belongs to the cone generated by some linearly independent subfamily of the given generators.

   theorem exists_linearIndependent_subcone [Fintype I] (A : I → E) {x : E}
       (hx : x ∈ PointedCone.hull ℝ (Set.range A)) :
       ∃ s : Finset I, LinearIndependent ℝ (fun i : s ↦ A i) ∧
         x ∈ PointedCone.hull ℝ (Set.range (fun i : s ↦ A i)) := by
   …