The planar Gram theorem for M

If planar vectors lie in a closed half-plane, M of their Gram matrix is completely positive (thm:matrix).

theorem BollobasNikiforov.matrix_theorem {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] (z : n → Fin 2 → ℝ) {w : Fin 2 → ℝ} (hw : w ≠ 0) (hwz : ∀ (i : n), 0 ≤ w ⬝ᵥ z i) : IsCompletelyPositive (M (gram z))

HP08. thm:matrix: a closed half-plane of planar Gram vectors makes M completely positive.