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

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Closed finitely generated cones

  1. theorem OAI.MatrixMultiplication.AuxiliarySeparation.mem_pointedCone_hull_range_iff line 17

    Source documentation

    A finite conic combination is a sum with nonnegative coefficients.

    theorem mem_pointedCone_hull_range_iff {I E : Type*} [Fintype I]
    [AddCommGroup E] [Module ℝ E] (A : I → E) (x : E) :
    x ∈ PointedCone.hull ℝ (Set.range A) ↔
      ∃ c : I → ℝ, (∀ i, 0 ≤ c i) ∧ ∑ i, c i • A i = x := by
…
  2. theorem OAI.MatrixMultiplication.AuxiliarySeparation.isClosed_pointedCone_hull_range_of_linearIndependent line 29

    Source documentation

    The cone spanned by a finite linearly independent family is closed.

    theorem isClosed_pointedCone_hull_range_of_linearIndependent
    {I E : Type*} [Fintype I] [NormedAddCommGroup E] [NormedSpace ℝ E]
    (A : I → E) (hA : LinearIndependent ℝ A) :
    IsClosed (PointedCone.hull ℝ (Set.range A) : Set E) := by
…
  3. theorem OAI.MatrixMultiplication.AuxiliarySeparation.isClosed_pointedCone_hull_range line 51

    Source documentation

    A cone generated by a finite family of real vectors is closed.

    theorem isClosed_pointedCone_hull_range
    {I E : Type*} [Fintype I] [NormedAddCommGroup E] [NormedSpace ℝ E]
    (A : I → E) :
    IsClosed (PointedCone.hull ℝ (Set.range A) : Set E) := by
…