Completely positivity of M on a right-angle planar cone

If planar Gram vectors have pairwise nonnegative inner products, they can be rotated into the closed first quadrant. Then M X = X ⊙ X expands as a sum of three nonnegative rank-ones. Scaling X by a positive square does not change whether M X is completely positive. Zero Gram vectors may be deleted: M of the remaining principal submatrix is completely positive if and only if the original M is (pad a CP factor by zero coordinates). An open half-plane with a unique supporting vector reduces, after rotation and scaling, to the MX06 configuration (k ≥ 1). Unique and tied open-half-plane configurations are completely positive (HP04–HP05), as is the closed half-plane (HP06).

def BollobasNikiforov.gram {n : Type u_1} (z : n → Fin 2 → ℝ) : Matrix n n ℝ

The Gram matrix of a family of planar vectors.

Equations

• BollobasNikiforov.gram z = Matrix.of fun (i j : n) => z i ⬝ᵥ z j

@[simp]

theorem BollobasNikiforov.gram_apply {n : Type u_1} (z : n → Fin 2 → ℝ) (i j : n) : gram z i j = z i ⬝ᵥ z j

noncomputable def BollobasNikiforov.euclid (w : Fin 2 → ℝ) : ℝ

Euclidean length of a vector in ℝ².

Equations

• BollobasNikiforov.euclid w = √(w ⬝ᵥ w)

theorem BollobasNikiforov.euclid_inner_nonneg (w : Fin 2 → ℝ) : 0 ≤ w ⬝ᵥ w

theorem BollobasNikiforov.euclid_nonneg (w : Fin 2 → ℝ) : 0 ≤ euclid w

theorem BollobasNikiforov.euclid_sq (w : Fin 2 → ℝ) : euclid w ^ 2 = w ⬝ᵥ w

theorem BollobasNikiforov.euclid_eq_zero (w : Fin 2 → ℝ) : euclid w = 0 ↔ w = 0

theorem BollobasNikiforov.euclid_pos {w : Fin 2 → ℝ} (hw : w ≠ 0) : 0 < euclid w

noncomputable def BollobasNikiforov.normalize (w : Fin 2 → ℝ) : Fin 2 → ℝ

Unit vector in the direction of a nonzero planar vector.

Equations

• BollobasNikiforov.normalize w = (BollobasNikiforov.euclid w)⁻¹ • w

theorem BollobasNikiforov.normalize_inner {w : Fin 2 → ℝ} (hw : w ≠ 0) : normalize w ⬝ᵥ normalize w = 1

theorem BollobasNikiforov.smul_normalize {w : Fin 2 → ℝ} (hw : w ≠ 0) : euclid w • normalize w = w

def BollobasNikiforov.det2 (u v : Fin 2 → ℝ) : ℝ

The 2-dimensional determinant u₀ v₁ - u₁ v₀.

Equations

• BollobasNikiforov.det2 u v = u 0 * v 1 - u 1 * v 0

theorem BollobasNikiforov.det2_smul_left (c : ℝ) (u v : Fin 2 → ℝ) : det2 (c • u) v = c * det2 u v

theorem BollobasNikiforov.det2_smul_right (c : ℝ) (u v : Fin 2 → ℝ) : det2 u (c • v) = c * det2 u v

theorem BollobasNikiforov.det2_zero_right (u : Fin 2 → ℝ) : det2 u 0 = 0

def BollobasNikiforov.rotateTo (u x : Fin 2 → ℝ) : Fin 2 → ℝ

Rotate so that the unit vector u becomes the positive x-axis.

Equations

• BollobasNikiforov.rotateTo u x i = if i = 0 then u ⬝ᵥ x else BollobasNikiforov.det2 u x

theorem BollobasNikiforov.rotateTo_zero (u x : Fin 2 → ℝ) : rotateTo u x 0 = u ⬝ᵥ x

theorem BollobasNikiforov.rotateTo_one (u x : Fin 2 → ℝ) : rotateTo u x 1 = det2 u x

theorem BollobasNikiforov.rotateTo_apply_zero_vec (u : Fin 2 → ℝ) : rotateTo u 0 = 0

theorem BollobasNikiforov.rotateTo_inner (u x y : Fin 2 → ℝ) (hu : u ⬝ᵥ u = 1) : rotateTo u x ⬝ᵥ rotateTo u y = x ⬝ᵥ y

theorem BollobasNikiforov.rotateTo_eq_zero_iff (u x : Fin 2 → ℝ) (hu : u ⬝ᵥ u = 1) : rotateTo u x = 0 ↔ x = 0

theorem BollobasNikiforov.det2_nonneg_of_min_snd {α γ : Fin 2 → ℝ} (hα : α ⬝ᵥ α = 1) (hγ : γ ⬝ᵥ γ = 1) (hα0 : 0 ≤ α 0) (hγ0 : 0 ≤ γ 0) (hmin : α 1 ≤ γ 1) : 0 ≤ det2 α γ

If α is a right-half-plane unit vector of minimal second coordinate, then every other such unit vector γ is counterclockwise from α.

theorem BollobasNikiforov.exists_nonneg_gram_factor {n : Type u_1} [Finite n] (z : n → Fin 2 → ℝ) (hnn : ∀ (i j : n), 0 ≤ z i ⬝ᵥ z j) : ∃ (p : n → ℝ) (q : n → ℝ), 0 ≤ p ∧ 0 ≤ q ∧ gram z = Matrix.vecMulVec p p + Matrix.vecMulVec q q

theorem BollobasNikiforov.laplacianCoeff_eq_zero_of_nonneg {n : Type u_1} [LinearOrder n] {X : Matrix n n ℝ} (h : ∀ (i j : n), 0 ≤ X i j) (i j : n) : laplacianCoeff X i j = 0

theorem BollobasNikiforov.M_eq_hadamard_of_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] {X : Matrix n n ℝ} (h : ∀ (i j : n), 0 ≤ X i j) : M X = X.hadamard X

theorem BollobasNikiforov.hadamard_vecMulVec {n : Type u_1} (p q : n → ℝ) : (Matrix.vecMulVec p p).hadamard (Matrix.vecMulVec q q) = Matrix.vecMulVec (p * q) (p * q)

theorem BollobasNikiforov.hadamard_add_self {n : Type u_1} (A B : Matrix n n ℝ) : (A + B).hadamard (A + B) = A.hadamard A + B.hadamard B + 2 • A.hadamard B

theorem BollobasNikiforov.isCompletelyPositive_M_of_nonneg_inners {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] (z : n → Fin 2 → ℝ) (hnn : ∀ (i j : n), 0 ≤ z i ⬝ᵥ z j) : IsCompletelyPositive (M (gram z))

HP01. If all planar inner products are nonnegative, then M of the Gram matrix is completely positive.

theorem BollobasNikiforov.isCompletelyPositive_M_smul_sq_iff {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] {c : ℝ} (hc : 0 < c) (X : Matrix n n ℝ) : IsCompletelyPositive (M X) ↔ IsCompletelyPositive (M (c ^ 2 • X))

HP03. Completely positivity of M X is invariant under positive square scalings of X.

HP07 — delete zero Gram vectors

theorem BollobasNikiforov.gram_isSymm {n : Type u_1} (z : n → Fin 2 → ℝ) : (gram z).IsSymm

theorem BollobasNikiforov.gram_eq_zero_of_left {n : Type u_1} {z : n → Fin 2 → ℝ} {i : n} (hi : z i = 0) (j : n) : gram z i j = 0

theorem BollobasNikiforov.gram_eq_zero_of_right {n : Type u_1} {z : n → Fin 2 → ℝ} {j : n} (hj : z j = 0) (i : n) : gram z i j = 0

theorem BollobasNikiforov.gram_submatrix {n : Type u_1} {ι : Type u_2} (z : n → Fin 2 → ℝ) (e : ι → n) : (gram z).submatrix e e = gram (z ∘ e)

theorem BollobasNikiforov.laplacianCoeff_add_of_isSymm {n : Type u_1} [DecidableEq n] [LinearOrder n] (X : Matrix n n ℝ) (hX : X.IsSymm) (i j : n) : laplacianCoeff X i j + laplacianCoeff X j i = if i ≠ j ∧ X i j < 0 then X i j ^ 2 else 0

theorem BollobasNikiforov.vecMulVec_edge_diag {n : Type u_1} [DecidableEq n] (p q i : n) : Matrix.vecMulVec (e p - e q) (e p - e q) i i = if p ≠ q ∧ (p = i ∨ q = i) then 1 else 0

theorem BollobasNikiforov.M_apply_diag_of_isSymm {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] (X : Matrix n n ℝ) (hX : X.IsSymm) (i : n) : M X i i = X i i * X i i + ∑ j : n, if i ≠ j ∧ X i j < 0 then X i j ^ 2 else 0

theorem BollobasNikiforov.M_eq_zero_of_row_col_zero {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] {X : Matrix n n ℝ} {i0 : n} (hrow : ∀ (j : n), X i0 j = 0) (hcol : ∀ (j : n), X j i0 = 0) (j : n) : M X i0 j = 0

A zero row and column of X remain zero in M X.

theorem BollobasNikiforov.M_eq_zero_of_col_row_zero {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] {X : Matrix n n ℝ} {i0 : n} (hrow : ∀ (j : n), X i0 j = 0) (hcol : ∀ (j : n), X j i0 = 0) (j : n) : M X j i0 = 0

theorem BollobasNikiforov.sum_comp_injective {n : Type u_1} [Fintype n] {ι : Type u_2} [Fintype ι] (σ : ι → n) (hσ : Function.Injective σ) (f : n → ℝ) (hf : ∀ j ∉ Set.range σ, f j = 0) : ∑ j : n, f j = ∑ a : ι, f (σ a)

theorem BollobasNikiforov.M_eq_zero_of_not_mem_range {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] {ι : Type u_2} {X : Matrix n n ℝ} (hX : X.IsSymm) {e : ι → n} (hzero : ∀ i ∉ Set.range e, ∀ (j : n), X i j = 0) {i : n} (hi : i ∉ Set.range e) (j : n) : M X i j = 0

theorem BollobasNikiforov.M_eq_zero_of_not_mem_range_right {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] {ι : Type u_2} {X : Matrix n n ℝ} (hX : X.IsSymm) {e : ι → n} (hzero : ∀ i ∉ Set.range e, ∀ (j : n), X i j = 0) {j : n} (hj : j ∉ Set.range e) (i : n) : M X i j = 0

theorem BollobasNikiforov.M_submatrix_eq_of_zero_outside {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] {ι : Type u_2} [Fintype ι] [DecidableEq ι] [LinearOrder ι] {X : Matrix n n ℝ} (hX : X.IsSymm) {e : ι → n} (he : Function.Injective e) (hzero : ∀ i ∉ Set.range e, ∀ (j : n), X i j = 0) : (M X).submatrix e e = M (X.submatrix e e)

If X is symmetric and vanishes off the image of an injection e, then M commutes with taking the principal submatrix along e.

theorem BollobasNikiforov.isCompletelyPositive_M_iff_submatrix {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] {ι : Type u_2} [Fintype ι] [DecidableEq ι] [LinearOrder ι] {X : Matrix n n ℝ} (hX : X.IsSymm) {e : ι → n} (he : Function.Injective e) (hzero : ∀ i ∉ Set.range e, ∀ (j : n), X i j = 0) : IsCompletelyPositive (M X) ↔ IsCompletelyPositive (M (X.submatrix e e))

HP07. Completely positivity of M X is unchanged by deleting zero rows/columns along an injection.

theorem BollobasNikiforov.isCompletelyPositive_M_gram_iff_nonzero {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] (z : n → Fin 2 → ℝ) : IsCompletelyPositive (M (gram z)) ↔ IsCompletelyPositive (M (gram fun (i : { i : n // z i ≠ 0 }) => z ↑i))

HP07 for planar Grams: drop the zero vectors.

HP02 — unique supporting vector reduces to MX06

theorem BollobasNikiforov.eq_of_fin2 {v w : Fin 2 → ℝ} (h0 : v 0 = w 0) (h1 : v 1 = w 1) : v = w

theorem BollobasNikiforov.rotateTo_smul (u : Fin 2 → ℝ) (c : ℝ) (x : Fin 2 → ℝ) : rotateTo u (c • x) = c • rotateTo u x

theorem BollobasNikiforov.rotateTo_eq_z0 (u : Fin 2 → ℝ) (hu : u ⬝ᵥ u = 1) : rotateTo u u = z0

theorem BollobasNikiforov.rotateTo_normalize_self {v : Fin 2 → ℝ} (hv : v ≠ 0) : rotateTo (normalize v) v = euclid v • z0

theorem BollobasNikiforov.smul_rotateTo_normalize_self {v : Fin 2 → ℝ} (hv : v ≠ 0) : (euclid v)⁻¹ • rotateTo (normalize v) v = z0

theorem BollobasNikiforov.gram_rotateTo {n : Type u_1} (u : Fin 2 → ℝ) (hu : u ⬝ᵥ u = 1) (z : n → Fin 2 → ℝ) : (gram fun (i : n) => rotateTo u (z i)) = gram z

theorem BollobasNikiforov.gram_smul_vec {n : Type u_1} (c : ℝ) (z : n → Fin 2 → ℝ) : (gram fun (i : n) => c • z i) = c ^ 2 • gram z

theorem BollobasNikiforov.eq_zVec_coords {k : ℕ} (s t : Fin k → ℝ) (i : Fin k) {v : Fin 2 → ℝ} (h0 : v 0 < 0) (hs : s i = v 0 ^ 2) (ht : t i = v 1 / -v 0) : v = zVec s t i

theorem BollobasNikiforov.eq_yVec_coords {p : ℕ} (ρ x : Fin p → ℝ) (j : Fin p) {v : Fin 2 → ℝ} (h1 : 0 < v 1) (hρ : ρ j = v 1 ^ 2) (hx : x j = v 0 / v 1) : v = yVec ρ x j

noncomputable def BollobasNikiforov.configLeft {n : Type u_1} [Fintype n] (z : n → Fin 2 → ℝ) : Finset n

Left indices in the rotated frame: strictly negative first coordinate.

Equations

• BollobasNikiforov.configLeft z = {i : n | z i 0 < 0}

noncomputable def BollobasNikiforov.configRight {n : Type u_1} [Fintype n] [DecidableEq n] (z : n → Fin 2 → ℝ) (i0 : n) : Finset n

Right indices: nonnegative first coordinate, excluding the unique axis vector.

Equations

• BollobasNikiforov.configRight z i0 = {i : n | i ≠ i0 ∧ 0 ≤ z i 0}

theorem BollobasNikiforov.not_mem_configLeft_of_z0 {n : Type u_1} [Fintype n] {z : n → Fin 2 → ℝ} {i0 : n} (hz0 : z i0 = z0) : i0 ∉ configLeft z

theorem BollobasNikiforov.mem_configLeft_iff {n : Type u_1} [Fintype n] {z : n → Fin 2 → ℝ} {i : n} : i ∈ configLeft z ↔ z i 0 < 0

theorem BollobasNikiforov.mem_configRight_iff {n : Type u_1} [Fintype n] [DecidableEq n] {z : n → Fin 2 → ℝ} {i0 i : n} : i ∈ configRight z i0 ↔ i ≠ i0 ∧ 0 ≤ z i 0

theorem BollobasNikiforov.mem_configRight_of_not_left {n : Type u_1} [Fintype n] [DecidableEq n] {z : n → Fin 2 → ℝ} {i0 i : n} (hi0 : i ≠ i0) (hl : i ∉ configLeft z) : i ∈ configRight z i0

theorem BollobasNikiforov.exists_config_of_rotated_unique {n : Type u_1} [LinearOrder n] [Finite n] (z : n → Fin 2 → ℝ) (i0 : n) (hz0 : z i0 = z0) (hup : ∀ (i : n), i ≠ i0 → 0 < z i 1) (hleft : ∃ (i : n), z i 0 < 0) : ∃ (k : ℕ) (p : ℕ) (_ : 0 < k) (s : Fin k → ℝ) (t : Fin k → ℝ) (ρ : Fin p → ℝ) (x : Fin p → ℝ) (e : n ≃ ConfigIdx k p), (∀ (i : Fin k), 0 < s i) ∧ (∀ (i : Fin k), 0 < t i) ∧ (∀ (j : Fin p), 0 < ρ j) ∧ (∀ (j : Fin p), 0 ≤ x j) ∧ ∀ (i : n), z i = configVec s t ρ x (e i)

HP02, rotated frame: unique contact z i0 = (1,0), all other vectors strictly above the axis, and at least one left vector. The data match MX06.

theorem BollobasNikiforov.gram_eq_Xconfig_submatrix {n : Type u_1} {k p : ℕ} {s t : Fin k → ℝ} {ρ x : Fin p → ℝ} {e : n ≃ ConfigIdx k p} {z : n → Fin 2 → ℝ} (hz : ∀ (i : n), z i = configVec s t ρ x (e i)) : gram z = (Xconfig s t ρ x).submatrix ⇑e ⇑e

theorem BollobasNikiforov.exists_config_of_unique_minimizer {n : Type u_1} [LinearOrder n] [Finite n] (z : n → Fin 2 → ℝ) (hnz : ∀ (i : n), z i ≠ 0) (hopen : ∃ (w : Fin 2 → ℝ), w ≠ 0 ∧ ∀ (i : n), 0 < w ⬝ᵥ z i) (hneg : ∃ (i : n) (j : n), z i ⬝ᵥ z j < 0) (i0 : n) (hside : ∀ (i : n), 0 ≤ det2 (normalize (z i0)) (z i)) (huniq : ∀ (i : n), det2 (normalize (z i0)) (z i) = 0 → i = i0) : ∃ (k : ℕ) (p : ℕ) (_ : 0 < k) (s : Fin k → ℝ) (t : Fin k → ℝ) (ρ : Fin p → ℝ) (x : Fin p → ℝ) (e : n ≃ ConfigIdx k p) (c : ℝ), 0 < c ∧ (∀ (i : Fin k), 0 < s i) ∧ (∀ (i : Fin k), 0 < t i) ∧ (∀ (j : Fin p), 0 < ρ j) ∧ (∀ (j : Fin p), 0 ≤ x j) ∧ ∀ (i : n), c • rotateTo (normalize (z i0)) (z i) = configVec s t ρ x (e i)

HP02. Open half-plane, a negative pair, and a unique supporting direction: after rotation and positive scaling the vectors match MX06 with k ≥ 1.

HP04 — unique minimizer implies M (gram z) is CP

def BollobasNikiforov.permIdx {k p : ℕ} (σ : Equiv.Perm (Fin k)) : ConfigIdx k p ≃ ConfigIdx k p

Permute the left (zᵢ) indices of a configuration.

Equations

• One or more equations did not get rendered due to their size.

theorem BollobasNikiforov.permIdx_z0 {k p : ℕ} (σ : Equiv.Perm (Fin k)) : (permIdx σ) idxZ0 = idxZ0

theorem BollobasNikiforov.permIdx_z {k p : ℕ} (σ : Equiv.Perm (Fin k)) (i : Fin k) : (permIdx σ) (idxZ i) = idxZ (σ i)

theorem BollobasNikiforov.permIdx_y {k p : ℕ} (σ : Equiv.Perm (Fin k)) (j : Fin p) : (permIdx σ) (idxY j) = idxY j

theorem BollobasNikiforov.configVec_permIdx {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (σ : Equiv.Perm (Fin k)) (α : ConfigIdx k p) : configVec (s ∘ ⇑σ) (t ∘ ⇑σ) ρ x α = configVec s t ρ x ((permIdx σ) α)

theorem BollobasNikiforov.Xconfig_permIdx {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (σ : Equiv.Perm (Fin k)) : Xconfig (s ∘ ⇑σ) (t ∘ ⇑σ) ρ x = (Xconfig s t ρ x).submatrix ⇑(permIdx σ) ⇑(permIdx σ)

theorem BollobasNikiforov.Xconfig_unperm {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (σ : Equiv.Perm (Fin k)) : Xconfig s t ρ x = (Xconfig (s ∘ ⇑σ) (t ∘ ⇑σ) ρ x).submatrix ⇑(permIdx σ).symm ⇑(permIdx σ).symm

theorem BollobasNikiforov.isCompletelyPositive_M_Xconfig_sorted {k p : ℕ} [NeZero k] (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (ht : ∀ (i : Fin k), 0 < t i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hx : ∀ (j : Fin p), 0 ≤ x j) : IsCompletelyPositive (M (Xconfig s t ρ x))

theorem BollobasNikiforov.isCompletelyPositive_M_of_unique_minimizer {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] (z : n → Fin 2 → ℝ) (hnz : ∀ (i : n), z i ≠ 0) (hopen : ∃ (w : Fin 2 → ℝ), w ≠ 0 ∧ ∀ (i : n), 0 < w ⬝ᵥ z i) (hneg : ∃ (i : n) (j : n), z i ⬝ᵥ z j < 0) (i0 : n) (hside : ∀ (i : n), 0 ≤ det2 (normalize (z i0)) (z i)) (huniq : ∀ (i : n), det2 (normalize (z i0)) (z i) = 0 → i = i0) : IsCompletelyPositive (M (gram z))

HP04. Open half-plane, a negative pair, and a unique supporting direction: M of the Gram matrix is completely positive.

Supporting direction and HP05 — tied minimizers

theorem BollobasNikiforov.det2_rotateTo (u x y : Fin 2 → ℝ) (hu : u ⬝ᵥ u = 1) : det2 (rotateTo u x) (rotateTo u y) = det2 x y

theorem BollobasNikiforov.normalize_rotateTo (u x : Fin 2 → ℝ) (hu : u ⬝ᵥ u = 1) (_hx : x ≠ 0) : normalize (rotateTo u x) = rotateTo u (normalize x)

theorem BollobasNikiforov.det2_add_right (u x y : Fin 2 → ℝ) : det2 u (x + y) = det2 u x + det2 u y

def BollobasNikiforov.rotate90 (u : Fin 2 → ℝ) : Fin 2 → ℝ

Counterclockwise perpendicular: u ↦ (-u₁, u₀).

Equations

• BollobasNikiforov.rotate90 u i = if i = 0 then -u 1 else u 0

theorem BollobasNikiforov.rotate90_zero (u : Fin 2 → ℝ) : rotate90 u 0 = -u 1

theorem BollobasNikiforov.rotate90_one (u : Fin 2 → ℝ) : rotate90 u 1 = u 0

theorem BollobasNikiforov.det2_rotate90 (u : Fin 2 → ℝ) : det2 u (rotate90 u) = u ⬝ᵥ u

theorem BollobasNikiforov.det2_rotate90_of_unit {u : Fin 2 → ℝ} (hu : u ⬝ᵥ u = 1) : det2 u (rotate90 u) = 1

theorem BollobasNikiforov.rotate90_inner (u : Fin 2 → ℝ) : rotate90 u ⬝ᵥ rotate90 u = u ⬝ᵥ u

theorem BollobasNikiforov.euclid_rotate90_of_unit {u : Fin 2 → ℝ} (hu : u ⬝ᵥ u = 1) : euclid (rotate90 u) = 1

theorem BollobasNikiforov.exists_supporting_minimizer {n : Type u_1} [Finite n] [Nonempty n] (z : n → Fin 2 → ℝ) (hnz : ∀ (i : n), z i ≠ 0) {w : Fin 2 → ℝ} (hw : w ≠ 0) (hwz : ∀ (i : n), 0 < w ⬝ᵥ z i) : ∃ (i0 : n), ∀ (i : n), 0 ≤ det2 (normalize (z i0)) (z i)

Some vector realises a supporting ray of the open cone.

def BollobasNikiforov.perturbTied {n : Type u_1} [DecidableEq n] (z : n → Fin 2 → ℝ) (i0 : n) (v : Fin 2 → ℝ) (ε : ℝ) : n → Fin 2 → ℝ

Shift every vector except i0 by ε • v.

Equations

• BollobasNikiforov.perturbTied z i0 v ε i = if i = i0 then z i else z i + ε • v

theorem BollobasNikiforov.perturbTied_i0 {n : Type u_1} [DecidableEq n] (z : n → Fin 2 → ℝ) (i0 : n) (v : Fin 2 → ℝ) (ε : ℝ) : perturbTied z i0 v ε i0 = z i0

theorem BollobasNikiforov.perturbTied_of_ne {n : Type u_1} [DecidableEq n] (z : n → Fin 2 → ℝ) {i0 i : n} (hi : i ≠ i0) (v : Fin 2 → ℝ) (ε : ℝ) : perturbTied z i0 v ε i = z i + ε • v

theorem BollobasNikiforov.perturbTied_zero {n : Type u_1} [DecidableEq n] (z : n → Fin 2 → ℝ) (i0 : n) (v : Fin 2 → ℝ) : perturbTied z i0 v 0 = z

theorem BollobasNikiforov.continuous_perturbTied_apply {n : Type u_1} [DecidableEq n] (z : n → Fin 2 → ℝ) (i0 : n) (v : Fin 2 → ℝ) (i : n) : Continuous fun (ε : ℝ) => perturbTied z i0 v ε i

theorem BollobasNikiforov.continuous_gram_perturbTied {n : Type u_1} [DecidableEq n] (z : n → Fin 2 → ℝ) (i0 : n) (v : Fin 2 → ℝ) : Continuous fun (ε : ℝ) => gram (perturbTied z i0 v ε)

theorem BollobasNikiforov.perturbTied_ne_zero {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {z : n → Fin 2 → ℝ} {i0 : n} {v : Fin 2 → ℝ} (hnz : ∀ (i : n), z i ≠ 0) (hv : euclid v = 1) {ε : ℝ} (hε0 : 0 < ε) (hε : ε < Finset.univ.inf' ⋯ fun (i : n) => euclid (z i)) (i : n) : perturbTied z i0 v ε i ≠ 0

theorem BollobasNikiforov.det2_perturbTied {n : Type u_1} [DecidableEq n] {z : n → Fin 2 → ℝ} {i0 : n} {v : Fin 2 → ℝ} (hnz0 : z i0 ≠ 0) (hside : ∀ (i : n), 0 ≤ det2 (normalize (z i0)) (z i)) (hv : det2 (normalize (z i0)) v = 1) {ε : ℝ} (hε : 0 < ε) : (∀ (i : n), 0 ≤ det2 (normalize (perturbTied z i0 v ε i0)) (perturbTied z i0 v ε i)) ∧ ∀ (i : n), det2 (normalize (perturbTied z i0 v ε i0)) (perturbTied z i0 v ε i) = 0 → i = i0

theorem BollobasNikiforov.isCompletelyPositive_M_of_tied_minimizers {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] (z : n → Fin 2 → ℝ) (hnz : ∀ (i : n), z i ≠ 0) (hopen : ∃ (w : Fin 2 → ℝ), w ≠ 0 ∧ ∀ (i : n), 0 < w ⬝ᵥ z i) (hneg : ∃ (i : n) (j : n), z i ⬝ᵥ z j < 0) (i0 : n) (hside : ∀ (i : n), 0 ≤ det2 (normalize (z i0)) (z i)) (_htied : ¬∀ (i : n), det2 (normalize (z i0)) (z i) = 0 → i = i0) : IsCompletelyPositive (M (gram z))

HP05. Open half-plane with a tied supporting ray: perturb into the open cone so the contact is unique, apply HP04, and pass to the limit.

theorem BollobasNikiforov.isCompletelyPositive_M_of_open_halfplane {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] (z : n → Fin 2 → ℝ) (hnz : ∀ (i : n), z i ≠ 0) (hopen : ∃ (w : Fin 2 → ℝ), w ≠ 0 ∧ ∀ (i : n), 0 < w ⬝ᵥ z i) : IsCompletelyPositive (M (gram z))

Open half-plane (unique or tied supporting ray).

theorem BollobasNikiforov.continuous_gram_shiftBy {n : Type u_1} (z : n → Fin 2 → ℝ) (w : Fin 2 → ℝ) : Continuous fun (ε : ℝ) => gram fun (i : n) => z i + ε • w

theorem BollobasNikiforov.shiftBy_ne_zero {n : Type u_1} (z : n → Fin 2 → ℝ) {w : Fin 2 → ℝ} (hw : w ≠ 0) (hwz : ∀ (i : n), 0 ≤ w ⬝ᵥ z i) {ε : ℝ} (hε : 0 < ε) (i : n) : z i + ε • w ≠ 0

theorem BollobasNikiforov.isCompletelyPositive_M_of_closed_halfplane {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))

HP06. Vectors in a closed half-plane: M of the Gram matrix is CP.