Compact generators and the closed CP cone

The rank-one generators of unit mass form a compact set S not containing 0. The completely positive cone is the cone generated by S, and is closed.

instance BollobasNikiforov.instFirstCountableTopologyMatrixReal_leanPool {n : Type u_1} [Finite n] : FirstCountableTopology (Matrix n n ℝ)

instance BollobasNikiforov.instSequentialSpaceMatrixReal_leanPool {n : Type u_1} [Finite n] : SequentialSpace (Matrix n n ℝ)

def BollobasNikiforov.nonnegativeUnitSphere {n : Type u_1} [Fintype n] : Set (n → ℝ)

Nonnegative vectors of Euclidean mass 1.

Equations

• BollobasNikiforov.nonnegativeUnitSphere = {p : n → ℝ | 0 ≤ p ∧ ∑ i : n, p i ^ 2 = 1}

def BollobasNikiforov.rankOneGenerators {n : Type u_1} [Fintype n] : Set (Matrix n n ℝ)

Rank-one CP generators of unit Frobenius mass.

Equations

• BollobasNikiforov.rankOneGenerators = (fun (p : n → ℝ) => Matrix.vecMulVec p p) '' BollobasNikiforov.nonnegativeUnitSphere

theorem BollobasNikiforov.continuous_vecMulVec_self {n : Type u_1} : Continuous fun (p : n → ℝ) => Matrix.vecMulVec p p

theorem BollobasNikiforov.isClosed_nonnegativeUnitSphere {n : Type u_1} [Fintype n] : IsClosed nonnegativeUnitSphere

theorem BollobasNikiforov.isCompact_nonnegativeUnitSphere {n : Type u_1} [Fintype n] : IsCompact nonnegativeUnitSphere

theorem BollobasNikiforov.isCompact_rankOneGenerators {n : Type u_1} [Fintype n] : IsCompact rankOneGenerators

CP06: the unit-mass rank-one generators are compact.

theorem BollobasNikiforov.trace_eq_one_of_mem_rankOneGenerators {n : Type u_1} [Fintype n] {C : Matrix n n ℝ} (hC : C ∈ rankOneGenerators) : C.trace = 1

theorem BollobasNikiforov.zero_notMem_rankOneGenerators {n : Type u_1} [Fintype n] : 0 ∉ rankOneGenerators

CP06: the unit-mass rank-one generators do not contain the zero matrix.

theorem BollobasNikiforov.isCompletelyPositive_zero {n : Type u_1} : IsCompletelyPositive 0

theorem BollobasNikiforov.trace_sum_vecMulVec {n : Type u_1} [Fintype n] {q : ℕ} (p : Fin q → n → ℝ) : (∑ a : Fin q, Matrix.vecMulVec (p a) (p a)).trace = ∑ a : Fin q, ∑ i : n, p a i ^ 2

theorem BollobasNikiforov.exists_sum_vecMulVec_card_le {n : Type u_1} [Fintype n] (q : ℕ) (p : Fin q → n → ℝ) (hp : ∀ (a : Fin q) (i : n), 0 ≤ p a i) : ∃ q' ≤ Fintype.card n * Fintype.card n, ∃ (p' : Fin q' → n → ℝ), (∀ (a : Fin q') (i : n), 0 ≤ p' a i) ∧ ∑ a : Fin q, Matrix.vecMulVec (p a) (p a) = ∑ a : Fin q', Matrix.vecMulVec (p' a) (p' a)

Drop linearly dependent rank-one summands until at most card n * card n remain.

theorem BollobasNikiforov.IsCompletelyPositive.exists_repr_card_le {n : Type u_1} [Fintype n] {C : Matrix n n ℝ} (hC : IsCompletelyPositive C) : ∃ q ≤ Fintype.card n * Fintype.card n, ∃ (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.exists_repr_of_card {n : Type u_1} [Fintype n] {C : Matrix n n ℝ} (hC : IsCompletelyPositive C) : ∃ (p : Fin (Fintype.card n * Fintype.card n) → n → ℝ), (∀ (a : Fin (Fintype.card n * Fintype.card n)) (i : n), 0 ≤ p a i) ∧ C = ∑ a : Fin (Fintype.card n * Fintype.card n), Matrix.vecMulVec (p a) (p a)

A CP matrix is a sum of at most card n * card n nonnegative rank-ones, padded.

theorem BollobasNikiforov.continuous_sum_vecMulVec {n : Type u_1} {q : ℕ} : Continuous fun (p : Fin q → n → ℝ) => ∑ a : Fin q, Matrix.vecMulVec (p a) (p a)

theorem BollobasNikiforov.isClosed_isCompletelyPositive {n : Type u_1} [Finite n] : IsClosed {C : Matrix n n ℝ | IsCompletelyPositive C}

CP07: the completely positive cone is closed.