Completely positive matrices

A real matrix is completely positive if it is a finite sum of rank-one matrices vecMulVec p p with entrywise nonnegative p.

def BollobasNikiforov.IsCompletelyPositive {n : Type u_1} (C : Matrix n n ℝ) : Prop

A real matrix is completely positive if it is a sum of outer products of entrywise nonnegative vectors.

Equations

• BollobasNikiforov.IsCompletelyPositive C = ∃ (q : ℕ) (p : Fin q → n → ℝ), (∀ (a : Fin q) (i : n), 0 ≤ p a i) ∧ C = ∑ a : Fin q, Matrix.vecMulVec (p a) (p a)

theorem BollobasNikiforov.isCompletelyPositive_vecMulVec {n : Type u_1} {p : n → ℝ} (hp : 0 ≤ p) : IsCompletelyPositive (Matrix.vecMulVec p p)

theorem BollobasNikiforov.IsCompletelyPositive.smul {n : Type u_1} {C : Matrix n n ℝ} {r : ℝ} (hr : 0 ≤ r) (hC : IsCompletelyPositive C) : IsCompletelyPositive (r • C)

theorem BollobasNikiforov.IsCompletelyPositive.add {n : Type u_1} {C D : Matrix n n ℝ} (hC : IsCompletelyPositive C) (hD : IsCompletelyPositive D) : IsCompletelyPositive (C + D)

theorem BollobasNikiforov.mul_transpose_eq_sum_vecMulVec {n : Type u_1} {r : Type u_2} [Fintype r] (A : Matrix n r ℝ) : A * A.transpose = ∑ a : r, Matrix.vecMulVec (A.col a) (A.col a)

theorem BollobasNikiforov.isCompletelyPositive_iff_exists_mul_transpose {n : Type u_1} {C : Matrix n n ℝ} : IsCompletelyPositive C ↔ ∃ (r : ℕ) (A : Matrix n (Fin r) ℝ), (∀ (i : n) (j : Fin r), 0 ≤ A i j) ∧ C = A * A.transpose

theorem BollobasNikiforov.posSemidef_vecMulVec_self {n : Type u_1} [Finite n] (p : n → ℝ) : (Matrix.vecMulVec p p).PosSemidef

theorem BollobasNikiforov.IsCompletelyPositive.posSemidef {n : Type u_1} [Finite n] {C : Matrix n n ℝ} (hC : IsCompletelyPositive C) : C.PosSemidef

theorem BollobasNikiforov.IsCompletelyPositive.isHermitian {n : Type u_1} [Finite n] {C : Matrix n n ℝ} (hC : IsCompletelyPositive C) : C.IsHermitian

theorem BollobasNikiforov.IsCompletelyPositive.isSymm {n : Type u_1} [Finite n] {C : Matrix n n ℝ} (hC : IsCompletelyPositive C) : C.IsSymm

theorem BollobasNikiforov.IsCompletelyPositive.nonneg {n : Type u_1} {C : Matrix n n ℝ} (hC : IsCompletelyPositive C) (i j : n) : 0 ≤ C i j

theorem BollobasNikiforov.IsCompletelyPositive.submatrix {n : Type u_1} {ι : Type u_2} {C : Matrix n n ℝ} (hC : IsCompletelyPositive C) (e : ι → n) : IsCompletelyPositive (C.submatrix e e)