Ordered elimination residuals

The residual of symmetric Gaussian elimination of a principal index list is a ratio of minors (EL01). Eliminating idxZ0 leaves the z-block and its y-coupling unchanged (EL02). That z-block is a Gram matrix plus a positive diagonal, hence PD, so later pivots stay positive (EL03). The numerator minor expands in the I-diagonal as a sum of complementary Gram minors (EL04); those principal cofactors have sign +1 (EL05). Factoring s i > 0 and ρ > 0 leaves the unscaled kernel (1 + t_a t_b)² or a last row (t_b - x)₊² (EL06). An algebraic identity rewrites (1 + s t)² as a truncated square (EL07). Row arguments -1/t_a are increasing and lie below any x ≥ 0 (EL08–EL09). Those leftover minors are nonnegative by TN13 (EL10), so residual columns stay nonnegative (EL11). Scaled outer products of those columns yield a completely positive C₀ (EL12). The remainder is the T-Schur complement of E and is PSD (EL13–EL14).

noncomputable def BollobasNikiforov.schurComplementEntry {ι : Type u_1} {r : ℕ} (A : Matrix ι ι ℝ) (e : Fin r → ι) (α j : ι) : ℝ

The residual entry after eliminating the principal block indexed by e.

Equations

• BollobasNikiforov.schurComplementEntry A e α j = A α j - (fun (i : Fin r) => A α (e i)) ⬝ᵥ (A.submatrix e e)⁻¹.mulVec fun (i : Fin r) => A (e i) j

theorem BollobasNikiforov.submatrix_elim_eq_fromBlocks {ι : Type u_1} {r : ℕ} (A : Matrix ι ι ℝ) (e : Fin r → ι) (α j : ι) : A.submatrix (Sum.elim e fun (x : Fin 1) => α) (Sum.elim e fun (x : Fin 1) => j) = Matrix.fromBlocks (A.submatrix e e) (A.submatrix e fun (x : Fin 1) => j) (A.submatrix (fun (x : Fin 1) => α) e) (A.submatrix (fun (x : Fin 1) => α) fun (x : Fin 1) => j)

theorem BollobasNikiforov.snoc_eq_elim_comp_finSumFinEquiv_symm {ι : Type u_1} {r : ℕ} (e : Fin r → ι) (x : ι) : Fin.snoc e x = (Sum.elim e fun (x_1 : Fin 1) => x) ∘ ⇑finSumFinEquiv.symm

theorem BollobasNikiforov.det_submatrix_snoc_eq_det_elim {ι : Type u_1} {r : ℕ} (A : Matrix ι ι ℝ) (e : Fin r → ι) (α j : ι) : (A.submatrix (Fin.snoc e α) (Fin.snoc e j)).det = (A.submatrix (Sum.elim e fun (x : Fin 1) => α) (Sum.elim e fun (x : Fin 1) => j)).det

theorem BollobasNikiforov.mul_fin_one_apply {r : ℕ} (C : Matrix (Fin 1) (Fin r) ℝ) (M : Matrix (Fin r) (Fin r) ℝ) (B : Matrix (Fin r) (Fin 1) ℝ) : (C * M * B) 0 0 = (fun (i : Fin r) => C 0 i) ⬝ᵥ M.mulVec fun (i : Fin r) => B i 0

theorem BollobasNikiforov.schurComplementEntry_eq_minor_div_det {ι : Type u_1} {r : ℕ} (A : Matrix ι ι ℝ) (e : Fin r → ι) (_he : Function.Injective e) {α j : ι} (_hα : α ∉ Set.range e) (_hj : j ∉ Set.range e) (hdet : (A.submatrix e e).det ≠ 0) : schurComplementEntry A e α j = (A.submatrix (Fin.snoc e α) (Fin.snoc e j)).det / (A.submatrix e e).det

EL01: the residual after eliminating the principal block A[I] is a ratio of minors. Injectivity of e and α, j ∉ range e record the elimination setup.

theorem BollobasNikiforov.schurComplementEntry_elim0 {ι : Type u_1} (A : Matrix ι ι ℝ) (e : Fin 0 → ι) (α j : ι) : schurComplementEntry A e α j = A α j ∧ (A.submatrix e e).det = 1

Empty elimination: the residual is the original entry and the denominator is 1.

theorem BollobasNikiforov.schurComplementEntry_eq_of_row {ι : Type u_1} {r : ℕ} (A : Matrix ι ι ℝ) (e : Fin r → ι) {α j : ι} (h : ∀ (i : Fin r), A α (e i) = 0) : schurComplementEntry A e α j = A α j

A vanishing eliminated row leaves the residual equal to the original entry.

theorem BollobasNikiforov.schurComplementEntry_eq_of_col {ι : Type u_1} {r : ℕ} (A : Matrix ι ι ℝ) (e : Fin r → ι) {α j : ι} (h : ∀ (i : Fin r), A (e i) j = 0) : schurComplementEntry A e α j = A α j

A vanishing eliminated column leaves the residual equal to the original entry.

theorem BollobasNikiforov.schurComplementEntry_one {ι : Type u_1} (A : Matrix ι ι ℝ) (q α j : ι) : schurComplementEntry A (fun (x : Fin 1) => q) α j = A α j - A α q * (A.submatrix (fun (x : Fin 1) => q) fun (x : Fin 1) => q)⁻¹ 0 0 * A q j

Singleton Schur residual, before simplifying the 1 × 1 inverse.

theorem BollobasNikiforov.inv_fin_one_apply (A : Matrix (Fin 1) (Fin 1) ℝ) (hA : A 0 0 ≠ 0) : A⁻¹ 0 0 = (A 0 0)⁻¹

The inverse entry of a nonzero 1 × 1 matrix is the reciprocal.

theorem BollobasNikiforov.schurComplementEntry_one_div {ι : Type u_1} (A : Matrix ι ι ℝ) (q α j : ι) (hq : A q q ≠ 0) : schurComplementEntry A (fun (x : Fin 1) => q) α j = A α j - A α q * A q j / A q q

Singleton Schur residual as the rank-one update A α j - A α q * A q j / A q q.

theorem BollobasNikiforov.MX_z_z0 {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i : Fin k) : M (Xconfig s t ρ x) (idxZ i) idxZ0 = 0

The opposite z-z₀ block entry vanishes by symmetry of Xconfig.

theorem BollobasNikiforov.schurComplementEntry_elimZ0_z_z {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i h : Fin k) : schurComplementEntry (M (Xconfig s t ρ x)) (fun (x : Fin 1) => idxZ0) (idxZ i) (idxZ h) = M (Xconfig s t ρ x) (idxZ i) (idxZ h)

EL02: eliminating idxZ0 does not change a z-z entry. The eliminated column on {idxZ i} is zero (MX_z0_z).

theorem BollobasNikiforov.schurComplementEntry_elimZ0_z_y {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i : Fin k) (j : Fin p) : schurComplementEntry (M (Xconfig s t ρ x)) (fun (x : Fin 1) => idxZ0) (idxZ i) (idxY j) = M (Xconfig s t ρ x) (idxZ i) (idxY j)

EL02: eliminating idxZ0 does not change a z-y coupling. The eliminated row on {idxZ i} is zero (MX_z_z0), even if M idxZ0 (idxY j) is nonzero.

theorem BollobasNikiforov.schurComplementEntry_elimZ0_y_z {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (j : Fin p) (i : Fin k) : schurComplementEntry (M (Xconfig s t ρ x)) (fun (x : Fin 1) => idxZ0) (idxY j) (idxZ i) = M (Xconfig s t ρ x) (idxY j) (idxZ i)

EL02: the opposite y-z coupling is likewise unchanged (MX_z0_z).

theorem BollobasNikiforov.zVec_dot_sq {k : ℕ} (s t : Fin k → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (i h : Fin k) : (zVec s t i ⬝ᵥ zVec s t h) ^ 2 = s i * s h * (1 + t i * t h) ^ 2

Squared inner products of configuration z-vectors.

noncomputable def BollobasNikiforov.zKron {k : ℕ} (s t : Fin k → ℝ) : Matrix (Fin k) (Fin 2 × Fin 2) ℝ

Feature map i ↦ zᵢ ⊗ zᵢ on Fin 2 × Fin 2.

Equations

• BollobasNikiforov.zKron s t i p = BollobasNikiforov.zVec s t i p.1 * BollobasNikiforov.zVec s t i p.2

theorem BollobasNikiforov.zKron_mul_transpose {k : ℕ} (s t : Fin k → ℝ) : (Matrix.of fun (i h : Fin k) => (zVec s t i ⬝ᵥ zVec s t h) ^ 2) = zKron s t * (zKron s t).transpose

The squared-Gram matrix of the z-vectors is zKron * zKronᵀ.

theorem BollobasNikiforov.zGram_posSemidef {k : ℕ} (s t : Fin k → ℝ) : (Matrix.of fun (i h : Fin k) => (zVec s t i ⬝ᵥ zVec s t h) ^ 2).PosSemidef

The squared-Gram z-block is positive semidefinite.

theorem BollobasNikiforov.MX_zBlock_eq {k p : ℕ} (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) : (M (Xconfig s t ρ x)).submatrix idxZ idxZ = (Matrix.of fun (i h : Fin k) => (zVec s t i ⬝ᵥ zVec s t h) ^ 2) + Matrix.diagonal fun (i : Fin k) => s i * configD t ρ x i

EL03: the principal z-block is a Gram matrix plus diagonal (s i * d i).

theorem BollobasNikiforov.MX_zBlock_posDef {k p : ℕ} (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) : ((M (Xconfig s t ρ x)).submatrix idxZ idxZ).PosDef

EL03: the principal z-block is positive definite.

theorem BollobasNikiforov.schurComplementEntry_diag_pos_of_posDef {n : Type u_2} {A : Matrix n n ℝ} (hA : A.PosDef) {m : ℕ} (e : Fin m → n) (he : Function.Injective e) {α : n} (hα : α ∉ Set.range e) : 0 < schurComplementEntry A e α α

A diagonal Schur residual of a PD matrix is a ratio of positive principal minors, hence positive.

theorem BollobasNikiforov.MX_zBlock_schur_pivot_pos {k p : ℕ} (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) {m : ℕ} (e : Fin m → Fin k) (he : Function.Injective e) {i : Fin k} (hi : i ∉ Set.range e) : 0 < schurComplementEntry ((M (Xconfig s t ρ x)).submatrix idxZ idxZ) e i i

EL03: every Schur pivot inside the z-block is positive.

theorem BollobasNikiforov.MX_zBlock_leading_posDef {k p : ℕ} (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) {m : ℕ} (hm : m ≤ k) : (((M (Xconfig s t ρ x)).submatrix idxZ idxZ).submatrix (Fin.castLE hm) (Fin.castLE hm)).PosDef

EL03: leading principal submatrices of the z-block are PD.

theorem BollobasNikiforov.MX_zBlock_leading_det_pos {k p : ℕ} (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) {m : ℕ} (hm : m ≤ k) : 0 < (((M (Xconfig s t ρ x)).submatrix idxZ idxZ).submatrix (Fin.castLE hm) (Fin.castLE hm)).det

EL03: leading principal minors of the z-block are positive.

theorem BollobasNikiforov.schurComplementEntry_elimZ0_z_diag_pos {k p : ℕ} (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) (i : Fin k) : 0 < schurComplementEntry (M (Xconfig s t ρ x)) (fun (x : Fin 1) => idxZ0) (idxZ i) (idxZ i)

EL03: after removing idxZ0, each remaining z-diagonal pivot is positive.

EL04 — diagonal expansion of a numerator minor

def BollobasNikiforov.elimKernelZZ {k : ℕ} (t : Fin k → ℝ) : Matrix (Fin k) (Fin k) ℝ

Unscaled z-z kernel K_{ab} = (1 + t_a t_b)².

Equations

• BollobasNikiforov.elimKernelZZ t a b = (1 + t a * t b) ^ 2

def BollobasNikiforov.elimKernelZY {k : ℕ} (t : Fin k → ℝ) (x : ℝ) : Fin k → ℝ

Unscaled z-y kernel K_{a,y} = (t_a - x)₊².

Equations

• BollobasNikiforov.elimKernelZY t x a = max (t a - x) 0 ^ 2

def BollobasNikiforov.elimSnoc {k m : ℕ} (e : Fin m → Fin k) (z : Fin k) : Fin m.succ → Fin k

Non-dependent concatenation of a z-index list with a later index.

Equations

• BollobasNikiforov.elimSnoc e z a = if h : a = Fin.last m then z else e (a.castPred h)

theorem BollobasNikiforov.elimSnoc_last {k m : ℕ} (e : Fin m → Fin k) (z : Fin k) : elimSnoc e z (Fin.last m) = z

theorem BollobasNikiforov.elimSnoc_castSucc {k m : ℕ} (e : Fin m → Fin k) (z : Fin k) (i : Fin m) : elimSnoc e z i.castSucc = e i

theorem BollobasNikiforov.idxZ_inj {k p : ℕ} {i h : Fin k} : idxZ i = idxZ h ↔ i = h

idxZ is injective.

theorem BollobasNikiforov.det_submatrix_finset_eq {n : Type u_2} [DecidableEq n] (A : Matrix n n ℝ) {s t : Finset n} (h : s = t) : (A.submatrix Subtype.val Subtype.val).det = (A.submatrix Subtype.val Subtype.val).det

Equal index Finsets give equal principal minors.

theorem BollobasNikiforov.det_add_diagonal_eq_sum {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) (d : n → ℝ) : (A + Matrix.diagonal d).det = ∑ S : Finset n, (∏ i ∈ Sᶜ, d i) * (A.submatrix Subtype.val Subtype.val).det

EL04: det(A + diagonal d) expands over kept index sets S. The product runs over the complementary (deleted) diagonal entries, and the leftover minor is the principal submatrix of A on S.

theorem BollobasNikiforov.det_add_diagonal_eq_sum_subset {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) (d : n → ℝ) (I : Finset n) (hd : ∀ i ∉ I, d i = 0) : (A + Matrix.diagonal d).det = ∑ S ∈ I.powerset, (∏ i ∈ S, d i) * (A.submatrix Subtype.val Subtype.val).det

If d is supported on I, the expansion runs over deleted sets S ⊆ I.

def BollobasNikiforov.elimI (m : ℕ) : Finset (Fin m.succ)

The leading block I inside Fin (m + 1), excluding the last index.

Equations

• BollobasNikiforov.elimI m = Finset.map Fin.castSuccEmb Finset.univ

theorem BollobasNikiforov.mem_elimI_iff {m : ℕ} {a : Fin m.succ} : a ∈ elimI m ↔ a ≠ Fin.last m

theorem BollobasNikiforov.not_mem_elimI_last {m : ℕ} : Fin.last m ∉ elimI m

def BollobasNikiforov.elimIDiag {k : ℕ} (s d : Fin k → ℝ) {m : ℕ} (e : Fin m → Fin k) : Fin m.succ → ℝ

Diagonal weights s i * d i on I, and 0 on the last index.

Equations

• BollobasNikiforov.elimIDiag s d e a = if h : a = Fin.last m then 0 else s (e (a.castPred h)) * d (e (a.castPred h))

theorem BollobasNikiforov.elimIDiag_last {k : ℕ} (s d : Fin k → ℝ) {m : ℕ} (e : Fin m → Fin k) : elimIDiag s d e (Fin.last m) = 0

theorem BollobasNikiforov.elimIDiag_castSucc {k : ℕ} (s d : Fin k → ℝ) {m : ℕ} (e : Fin m → Fin k) (i : Fin m) : elimIDiag s d e i.castSucc = s (e i) * d (e i)

theorem BollobasNikiforov.elimIDiag_eq_zero_of_not_mem {k : ℕ} (s d : Fin k → ℝ) {m : ℕ} (e : Fin m → Fin k) {a : Fin m.succ} (ha : a ∉ elimI m) : elimIDiag s d e a = 0

def BollobasNikiforov.elimGramZZ {k : ℕ} (s t : Fin k → ℝ) {m : ℕ} (e : Fin m → Fin k) (αidx jidx : Fin k) : Matrix (Fin m.succ) (Fin m.succ) ℝ

Pure Gram block on elimSnoc e αidx vs elimSnoc e jidx (no I-diagonal extras).

Equations

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

def BollobasNikiforov.elimLastDiag {k : ℕ} (s d : Fin k → ℝ) {m : ℕ} (αidx jidx : Fin k) : Fin m.succ → ℝ

Last-entry correction when α = j (the pivot diagonal is not expanded).

Equations

• BollobasNikiforov.elimLastDiag s d αidx jidx a = if a = Fin.last m ∧ αidx = jidx then s αidx * d αidx else 0

theorem BollobasNikiforov.elimSnoc_eq_iff {k m : ℕ} {e : Fin m → Fin k} (he : Function.Injective e) {zα zj : Fin k} (hzα : zα ∉ Set.range e) (hzj : zj ∉ Set.range e) {a b : Fin m.succ} : elimSnoc e zα a = elimSnoc e zj b ↔ a = b ∧ (a = Fin.last m → zα = zj)

theorem BollobasNikiforov.MX_snoc_z_eq_gram_add_diag {k p : ℕ} (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) {m : ℕ} (e : Fin m → Fin k) (he : Function.Injective e) {αidx jidx : Fin k} (hα : αidx ∉ Set.range e) (hj : jidx ∉ Set.range e) : (M (Xconfig s t ρ x)).submatrix (idxZ ∘ elimSnoc e αidx) (idxZ ∘ elimSnoc e jidx) = elimGramZZ s t e αidx jidx + Matrix.diagonal (elimIDiag s (configD t ρ x) e) + Matrix.diagonal (elimLastDiag s (configD t ρ x) αidx jidx)

The z-z numerator minor is the Gram block plus the I-diagonal (and the unexpanded last diagonal if α = j).

theorem BollobasNikiforov.det_MX_snoc_z_eq_sum {k p : ℕ} (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) {m : ℕ} (e : Fin m → Fin k) (he : Function.Injective e) {αidx jidx : Fin k} (hα : αidx ∉ Set.range e) (hj : jidx ∉ Set.range e) : ((M (Xconfig s t ρ x)).submatrix (idxZ ∘ elimSnoc e αidx) (idxZ ∘ elimSnoc e jidx)).det = ∑ S ∈ (elimI m).powerset, (∏ i ∈ S, elimIDiag s (configD t ρ x) e i) * ((elimGramZZ s t e αidx jidx + Matrix.diagonal (elimLastDiag s (configD t ρ x) αidx jidx)).submatrix Subtype.val Subtype.val).det

EL04: expand a z-z numerator in the diagonal summands on I.

def BollobasNikiforov.elimGramZY {k : ℕ} (s t : Fin k → ℝ) (ρval xval : ℝ) {m : ℕ} (e : Fin m → Fin k) (jidx : Fin k) : Matrix (Fin m.succ) (Fin m.succ) ℝ

Gram/coupling block for a last y-row against columns snoc e j.

Equations

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

theorem BollobasNikiforov.MX_y_z {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (i : Fin k) (j : Fin p) : M (Xconfig s t ρ x) (idxY j) (idxZ i) = s i * ρ j * max (t i - x j) 0 ^ 2

The opposite y-z block equals the z-y formula.

def BollobasNikiforov.elimRowY {k p m : ℕ} (e : Fin m → Fin k) (ℓ : Fin p) : Fin m.succ → ConfigIdx k p

Row map for a last y-index after the I-block.

Equations

• BollobasNikiforov.elimRowY e ℓ a = if h : a = Fin.last m then BollobasNikiforov.idxY ℓ else BollobasNikiforov.idxZ (e (a.castPred h))

theorem BollobasNikiforov.elimRowY_last {k p m : ℕ} (e : Fin m → Fin k) (ℓ : Fin p) : elimRowY e ℓ (Fin.last m) = idxY ℓ

theorem BollobasNikiforov.elimRowY_castSucc {k p m : ℕ} (e : Fin m → Fin k) (ℓ : Fin p) (i : Fin m) : elimRowY e ℓ i.castSucc = idxZ (e i)

theorem BollobasNikiforov.MX_snoc_y_eq_gram_add_diag {k p : ℕ} (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) {m : ℕ} (e : Fin m → Fin k) (he : Function.Injective e) {jidx : Fin k} {ℓ : Fin p} (hj : jidx ∉ Set.range e) : (M (Xconfig s t ρ x)).submatrix (elimRowY e ℓ) (idxZ ∘ elimSnoc e jidx) = elimGramZY s t (ρ ℓ) (x ℓ) e jidx + Matrix.diagonal (elimIDiag s (configD t ρ x) e)

The y-row numerator minor is the Gram/coupling block plus the I-diagonal.

theorem BollobasNikiforov.det_MX_snoc_y_eq_sum {k p : ℕ} (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) {m : ℕ} (e : Fin m → Fin k) (he : Function.Injective e) {jidx : Fin k} {ℓ : Fin p} (hj : jidx ∉ Set.range e) : ((M (Xconfig s t ρ x)).submatrix (elimRowY e ℓ) (idxZ ∘ elimSnoc e jidx)).det = ∑ S ∈ (elimI m).powerset, (∏ i ∈ S, elimIDiag s (configD t ρ x) e i) * ((elimGramZY s t (ρ ℓ) (x ℓ) e jidx).submatrix Subtype.val Subtype.val).det

EL04: expand a y-row numerator in the diagonal summands on I.

EL05 — principal cofactor signs are +1

theorem BollobasNikiforov.principal_cofactor_sign (q : ℕ) : (-1) ^ (q + q) = 1

EL05: a principal cofactor sign is (-1)^{p+p} = 1.

theorem BollobasNikiforov.det_piecewise_one_eq_compl_minor {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) (S : Finset n) : (Matrix.of (Sᶜ.piecewise A.row (Matrix.row 1))).det = (A.submatrix Subtype.val Subtype.val).det

EL05: deleting the same row and column subset contributes sign +1. The leftover is the complementary principal minor, with no extra sign.

EL06 — factor positive s and ρ

theorem BollobasNikiforov.det_smul_row_col {n : Type u_2} [Fintype n] [DecidableEq n] (u v : n → ℝ) (A : Matrix n n ℝ) : (Matrix.of fun (i j : n) => u i * v j * A i j).det = ((∏ i : n, u i) * ∏ j : n, v j) * A.det

Homogeneity: row scales u and column scales v factor out of det.

theorem BollobasNikiforov.det_elimGramZZ_factor {k : ℕ} (s t : Fin k → ℝ) {m : ℕ} (e : Fin m → Fin k) (αidx jidx : Fin k) : (elimGramZZ s t e αidx jidx).det = ((∏ a : Fin m.succ, s (elimSnoc e αidx a)) * ∏ b : Fin m.succ, s (elimSnoc e jidx b)) * ((elimKernelZZ t).submatrix (elimSnoc e αidx) (elimSnoc e jidx)).det

EL06: a z-z Gram block factors as s-row and s-column times the unscaled kernel minor.

theorem BollobasNikiforov.det_elimGramZZ_submatrix_factor {k : ℕ} (s t : Fin k → ℝ) {m : ℕ} (e : Fin m → Fin k) (αidx jidx : Fin k) (S : Finset (Fin m.succ)) : ((elimGramZZ s t e αidx jidx).submatrix Subtype.val Subtype.val).det = ((∏ i : ↥Sᶜ, s (elimSnoc e αidx ↑i)) * ∏ i : ↥Sᶜ, s (elimSnoc e jidx ↑i)) * ((elimKernelZZ t).submatrix (elimSnoc e αidx ∘ Subtype.val) (elimSnoc e jidx ∘ Subtype.val)).det

EL06: the same factoring on a complementary leftover of the z-z Gram.

def BollobasNikiforov.elimKernelMinorZY {k : ℕ} (t : Fin k → ℝ) (xval : ℝ) {m : ℕ} (e : Fin m → Fin k) (jidx : Fin k) : Matrix (Fin m.succ) (Fin m.succ) ℝ

Unscaled leftover kernel with a last truncated-square row.

Equations

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

theorem BollobasNikiforov.det_elimGramZY_factor {k : ℕ} (s t : Fin k → ℝ) (ρval xval : ℝ) {m : ℕ} (e : Fin m → Fin k) (jidx : Fin k) : (elimGramZY s t ρval xval e jidx).det = ((∏ a : Fin (m + 1), if a = Fin.last m then ρval else s (elimSnoc e jidx a)) * ∏ b : Fin m.succ, s (elimSnoc e jidx b)) * (elimKernelMinorZY t xval e jidx).det

EL06: a y-row Gram/coupling block factors ρ from the last row and s from every z-row/column.

theorem BollobasNikiforov.one_add_mul_sq_eq_sq_mul_max_sub {s t : ℝ} (hs : 0 < s) (ht : 0 < t) : (1 + s * t) ^ 2 = s ^ 2 * max (t - -1 / s) 0 ^ 2

EL07: (1 + s t)² = s² (t - (-1/s))₊² for s, t > 0.

theorem BollobasNikiforov.neg_one_div_le_neg_one_div {s t : ℝ} (hs : 0 < s) (ht : 0 < t) (h : s ≤ t) : -1 / s ≤ -1 / t

Reciprocal is antitone on (0, ∞), so -1/t is increasing in t > 0.

theorem BollobasNikiforov.neg_one_div_lt_zero {t : ℝ} (ht : 0 < t) : -1 / t < 0

theorem BollobasNikiforov.monotone_neg_one_div {k : ℕ} {t : Fin k → ℝ} (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) : Monotone fun (i : Fin k) => -1 / t i

EL08: if t is positive and monotone, then i ↦ -1 / t i is monotone and negative.

theorem BollobasNikiforov.neg_one_div_apply_lt_zero {k : ℕ} {t : Fin k → ℝ} (ht : ∀ (i : Fin k), 0 < t i) (i : Fin k) : -1 / t i < 0

theorem BollobasNikiforov.neg_one_div_le_neg_one_div_of_ge {tα tj : ℝ} (hα : 0 < tα) (hj : 0 < tj) (h : tj ≤ tα) : -1 / tj ≤ -1 / tα

EL09: a later positive t α ≥ t j keeps -1/t nondecreasing.

theorem BollobasNikiforov.neg_one_div_le_of_nonneg {ta x : ℝ} (hta : 0 < ta) (hx : 0 ≤ x) : -1 / ta ≤ x

EL09: a last argument x ≥ 0 follows every -1 / t a.

EL10 — leftover kernel minors are nonnegative

theorem BollobasNikiforov.elimSnoc_eq_finSnoc {k m : ℕ} (e : Fin m → Fin k) (z : Fin k) : elimSnoc e z = Fin.snoc e z

theorem BollobasNikiforov.elimKernelZZ_eq_truncated {k : ℕ} (t : Fin k → ℝ) (ht : ∀ (i : Fin k), 0 < t i) (a b : Fin k) : elimKernelZZ t a b = t a ^ 2 * truncatedSquare (fun (i : Fin k) => -1 / t i) t a b

theorem BollobasNikiforov.det_elimKernelZZ_submatrix_nonneg {k : ℕ} (t : Fin k → ℝ) (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) {n : ℕ} {I J : Fin n → Fin k} (hI : StrictMono I) (hJ : StrictMono J) : 0 ≤ ((elimKernelZZ t).submatrix I J).det

EL10: a z-z kernel minor with strictly increasing index maps is nonnegative.

theorem BollobasNikiforov.det_elimKernelZZ_submatrix_monotone {k : ℕ} (t : Fin k → ℝ) (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) {n : ℕ} {I J : Fin n → Fin k} (hI : Monotone I) (hJ : Monotone J) : 0 ≤ ((elimKernelZZ t).submatrix I J).det

EL10: the same minor stays nonnegative for merely monotone maps.

theorem BollobasNikiforov.elimSnoc_monotone {k m : ℕ} {e : Fin m → Fin k} (he : Monotone e) {z : Fin k} (hz : ∀ (i : Fin m), e i ≤ z) : Monotone (elimSnoc e z)

theorem BollobasNikiforov.elimSnoc_strictMono {k m : ℕ} {e : Fin m → Fin k} (he : StrictMono e) {z : Fin k} (hz : ∀ (i : Fin m), e i < z) : StrictMono (elimSnoc e z)

theorem BollobasNikiforov.castLE_lt {k m : ℕ} (hm : m ≤ k) {z : Fin k} (hz : m ≤ ↑z) (i : Fin m) : Fin.castLE hm i < z

theorem BollobasNikiforov.det_elimKernelZZ_elimSnoc_nonneg {k : ℕ} (t : Fin k → ℝ) (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) {m : ℕ} {e : Fin m → Fin k} (he : StrictMono e) {αidx jidx : Fin k} (hα : ∀ (i : Fin m), e i < αidx) (hj : ∀ (i : Fin m), e i < jidx) : 0 ≤ ((elimKernelZZ t).submatrix (elimSnoc e αidx) (elimSnoc e jidx)).det

theorem BollobasNikiforov.det_submatrix_subtype_eq_orderEmb {n : Type u_2} [LinearOrder n] [DecidableEq n] (A : Matrix n n ℝ) (S : Finset n) : (A.submatrix Subtype.val Subtype.val).det = (A.submatrix ⇑(S.orderEmbOfFin ⋯) ⇑(S.orderEmbOfFin ⋯)).det

theorem BollobasNikiforov.det_elimKernelZZ_compl_nonneg {k : ℕ} (t : Fin k → ℝ) (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) {m : ℕ} {e : Fin m → Fin k} (he : StrictMono e) {αidx jidx : Fin k} (hα : ∀ (i : Fin m), e i < αidx) (hj : ∀ (i : Fin m), e i < jidx) (S : Finset (Fin m.succ)) : 0 ≤ ((elimKernelZZ t).submatrix (elimSnoc e αidx ∘ Subtype.val) (elimSnoc e jidx ∘ Subtype.val)).det

EL10: complementary leftover of a z-z kernel minor is nonnegative.

noncomputable def BollobasNikiforov.elimRowArg {k : ℕ} (t : Fin k → ℝ) (xval : ℝ) {m : ℕ} (e : Fin m → Fin k) (jidx : Fin k) : Fin m.succ → ℝ

Row argument of the elimination step: the vector on Fin m.succ whose last entry is xval and whose other entries are -1 / t along the indices selected by elimSnoc e jidx.

Equations

• BollobasNikiforov.elimRowArg t xval e jidx a = if a = Fin.last m then xval else -1 / t (BollobasNikiforov.elimSnoc e jidx a)

def BollobasNikiforov.elimColArg {k : ℕ} (t : Fin k → ℝ) {m : ℕ} (e : Fin m → Fin k) (jidx : Fin k) : Fin m.succ → ℝ

Column argument of the elimination step: t evaluated along elimSnoc e jidx.

Equations

• BollobasNikiforov.elimColArg t e jidx b = t (BollobasNikiforov.elimSnoc e jidx b)

theorem BollobasNikiforov.elimRowArg_monotone {k : ℕ} (t : Fin k → ℝ) (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) (xval : ℝ) (hx : 0 ≤ xval) {m : ℕ} {e : Fin m → Fin k} (he : Monotone e) {jidx : Fin k} (hj : ∀ (i : Fin m), e i ≤ jidx) : Monotone (elimRowArg t xval e jidx)

theorem BollobasNikiforov.elimColArg_monotone {k : ℕ} (t : Fin k → ℝ) (hmono : Monotone t) {m : ℕ} {e : Fin m → Fin k} (he : Monotone e) {jidx : Fin k} (hj : ∀ (i : Fin m), e i ≤ jidx) : Monotone (elimColArg t e jidx)

theorem BollobasNikiforov.elimKernelMinorZY_eq_scaled {k : ℕ} (t : Fin k → ℝ) (ht : ∀ (i : Fin k), 0 < t i) (xval : ℝ) {m : ℕ} (e : Fin m → Fin k) (jidx : Fin k) (a b : Fin m.succ) : elimKernelMinorZY t xval e jidx a b = (if a = Fin.last m then 1 else t (elimSnoc e jidx a) ^ 2) * truncatedSquare (elimRowArg t xval e jidx) (elimColArg t e jidx) a b

theorem BollobasNikiforov.det_elimKernelMinorZY_nonneg {k : ℕ} (t : Fin k → ℝ) (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) (xval : ℝ) (hx : 0 ≤ xval) {m : ℕ} {e : Fin m → Fin k} (he : Monotone e) {jidx : Fin k} (hj : ∀ (i : Fin m), e i ≤ jidx) : 0 ≤ (elimKernelMinorZY t xval e jidx).det

EL10: a last truncated-square row still gives a nonnegative minor.

theorem BollobasNikiforov.det_elimGramZY_submatrix_factor {k : ℕ} (s t : Fin k → ℝ) (ρval xval : ℝ) {m : ℕ} (e : Fin m → Fin k) (jidx : Fin k) (S : Finset (Fin m.succ)) : ((elimGramZY s t ρval xval e jidx).submatrix Subtype.val Subtype.val).det = ((∏ i : ↥Sᶜ, if ↑i = Fin.last m then ρval else s (elimSnoc e jidx ↑i)) * ∏ i : ↥Sᶜ, s (elimSnoc e jidx ↑i)) * ((elimKernelMinorZY t xval e jidx).submatrix Subtype.val Subtype.val).det

theorem BollobasNikiforov.det_elimKernelMinorZY_compl_nonneg {k : ℕ} (t : Fin k → ℝ) (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) (xval : ℝ) (hx : 0 ≤ xval) {m : ℕ} {e : Fin m → Fin k} (he : Monotone e) {jidx : Fin k} (hj : ∀ (i : Fin m), e i ≤ jidx) (S : Finset (Fin m.succ)) : 0 ≤ ((elimKernelMinorZY t xval e jidx).submatrix Subtype.val Subtype.val).det

EL10: complementary leftover of a y-row kernel minor is nonnegative.

EL11 — residual columns are nonnegative

theorem BollobasNikiforov.elimIDiag_nonneg {k : ℕ} (s d : Fin k → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hd : ∀ (i : Fin k), 0 ≤ d i) {m : ℕ} (e : Fin m → Fin k) (a : Fin m.succ) : 0 ≤ elimIDiag s d e a

theorem BollobasNikiforov.elimRowY_eq_snoc {k p m : ℕ} (e : Fin m → Fin k) (ℓ : Fin p) : elimRowY e ℓ = Fin.snoc (idxZ ∘ e) (idxY ℓ)

theorem BollobasNikiforov.idxZ_comp_snoc {k p m : ℕ} (e : Fin m → Fin k) (z : Fin k) : idxZ ∘ Fin.snoc e z = idxZ ∘ elimSnoc e z

theorem BollobasNikiforov.det_MX_snoc_z_nonneg {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) (hρ : ∀ (j : Fin p), 0 < ρ j) {m : ℕ} {e : Fin m → Fin k} (he : StrictMono e) {αidx jidx : Fin k} (hα : αidx ∉ Set.range e) (hj : jidx ∉ Set.range e) (hαlt : ∀ (i : Fin m), e i < αidx) (hjlt : ∀ (i : Fin m), e i < jidx) (hαj : αidx ≠ jidx) : 0 ≤ ((M (Xconfig s t ρ x)).submatrix (idxZ ∘ elimSnoc e αidx) (idxZ ∘ elimSnoc e jidx)).det

EL11: a later z-z numerator minor is nonnegative.

theorem BollobasNikiforov.det_MX_snoc_y_nonneg {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) (hρ : ∀ (j : Fin p), 0 < ρ j) (hx : ∀ (j : Fin p), 0 ≤ x j) {m : ℕ} {e : Fin m → Fin k} (he : StrictMono e) {jidx : Fin k} {ℓ : Fin p} (hj : jidx ∉ Set.range e) (hjlt : ∀ (i : Fin m), e i ≤ jidx) : 0 ≤ ((M (Xconfig s t ρ x)).submatrix (elimRowY e ℓ) (idxZ ∘ elimSnoc e jidx)).det

EL11: a y-row numerator minor is nonnegative.

theorem BollobasNikiforov.schurComplementEntry_z_later_nonneg {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) (hρ : ∀ (j : Fin p), 0 < ρ j) {m : ℕ} (hm : m ≤ k) {j α : Fin k} (hj : m ≤ ↑j) (hα : m ≤ ↑α) (hαj : α ≠ j) : 0 ≤ schurComplementEntry ((M (Xconfig s t ρ x)).submatrix idxZ idxZ) (Fin.castLE hm) α j

EL11: residual of a later z-index against a leading z-pivot is ≥ 0.

theorem BollobasNikiforov.schurComplementEntry_y_later_nonneg {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) (hρ : ∀ (j : Fin p), 0 < ρ j) (hx : ∀ (j : Fin p), 0 ≤ x j) {m : ℕ} (hm : m ≤ k) {j : Fin k} (hj : m ≤ ↑j) (ℓ : Fin p) : 0 ≤ schurComplementEntry (M (Xconfig s t ρ x)) (idxZ ∘ Fin.castLE hm) (idxY ℓ) (idxZ j)

EL11: residual of a y-index against a leading z-pivot is ≥ 0.

Index sets E and T for elimination

theorem BollobasNikiforov.elim_configIdx_cases {k p : ℕ} {P : ConfigIdx k p → Prop} (α : ConfigIdx k p) (h0 : P idxZ0) (hz : ∀ (i : Fin k), P (idxZ i)) (hy : ∀ (j : Fin p), P (idxY j)) : P α

Case split on a configuration index.

theorem BollobasNikiforov.idxY_inj {k p : ℕ} {j ℓ : Fin p} : idxY j = idxY ℓ ↔ j = ℓ

theorem BollobasNikiforov.MX_isHermitian {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : (M (Xconfig s t ρ x)).IsHermitian

theorem BollobasNikiforov.MX_isSymm {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : (M (Xconfig s t ρ x)).IsSymm

def BollobasNikiforov.elimEEmbed {k p : ℕ} : Option (Fin k) → ConfigIdx k p

E-embedding: none is z₀, some i is zᵢ.

Equations

• BollobasNikiforov.elimEEmbed none = BollobasNikiforov.idxZ0
• BollobasNikiforov.elimEEmbed (some i) = BollobasNikiforov.idxZ i

def BollobasNikiforov.elimT {k p : ℕ} : Fin p → ConfigIdx k p

T-embedding: the y-indices.

Equations

• BollobasNikiforov.elimT = BollobasNikiforov.idxY

theorem BollobasNikiforov.elimEEmbed_none {k p : ℕ} : elimEEmbed none = idxZ0

theorem BollobasNikiforov.elimEEmbed_some {k p : ℕ} (i : Fin k) : elimEEmbed (some i) = idxZ i

theorem BollobasNikiforov.elimT_apply {k p : ℕ} (j : Fin p) : elimT j = idxY j

theorem BollobasNikiforov.configIdxEquiv_idxZ0 {k p : ℕ} : (configIdxEquiv k p) idxZ0 = Sum.inl none

theorem BollobasNikiforov.configIdxEquiv_idxZ {k p : ℕ} (i : Fin k) : (configIdxEquiv k p) (idxZ i) = Sum.inl (some i)

theorem BollobasNikiforov.configIdxEquiv_idxY {k p : ℕ} (j : Fin p) : (configIdxEquiv k p) (idxY j) = Sum.inr j

theorem BollobasNikiforov.elimEEmbed_ne_elimT {k p : ℕ} (a : Option (Fin k)) (j : Fin p) : elimEEmbed a ≠ elimT j

noncomputable def BollobasNikiforov.elimEE {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : Matrix (Option (Fin k)) (Option (Fin k)) ℝ

The E-block of M (Xconfig s t ρ x): rows and columns indexed by the axis vector and the left vectors through elimEEmbed.

Equations

• BollobasNikiforov.elimEE s t ρ x = (BollobasNikiforov.M (BollobasNikiforov.Xconfig s t ρ x)).submatrix BollobasNikiforov.elimEEmbed BollobasNikiforov.elimEEmbed

noncomputable def BollobasNikiforov.elimET {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : Matrix (Option (Fin k)) (Fin p) ℝ

The block of M (Xconfig s t ρ x) with E-rows (via elimEEmbed) and right-vector columns (via elimT).

Equations

• BollobasNikiforov.elimET s t ρ x = (BollobasNikiforov.M (BollobasNikiforov.Xconfig s t ρ x)).submatrix BollobasNikiforov.elimEEmbed BollobasNikiforov.elimT

noncomputable def BollobasNikiforov.elimTE {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : Matrix (Fin p) (Option (Fin k)) ℝ

The block of M (Xconfig s t ρ x) with right-vector rows (via elimT) and E-columns (via elimEEmbed).

Equations

• BollobasNikiforov.elimTE s t ρ x = (BollobasNikiforov.M (BollobasNikiforov.Xconfig s t ρ x)).submatrix BollobasNikiforov.elimT BollobasNikiforov.elimEEmbed

noncomputable def BollobasNikiforov.elimTT {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : Matrix (Fin p) (Fin p) ℝ

The right-vector block of M (Xconfig s t ρ x): rows and columns indexed through elimT.

Equations

• BollobasNikiforov.elimTT s t ρ x = (BollobasNikiforov.M (BollobasNikiforov.Xconfig s t ρ x)).submatrix BollobasNikiforov.elimT BollobasNikiforov.elimT

theorem BollobasNikiforov.elimEE_none_none {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : elimEE s t ρ x none none = M (Xconfig s t ρ x) idxZ0 idxZ0

theorem BollobasNikiforov.elimEE_none_some {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i : Fin k) : elimEE s t ρ x none (some i) = 0

theorem BollobasNikiforov.elimEE_some_none {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i : Fin k) : elimEE s t ρ x (some i) none = 0

theorem BollobasNikiforov.elimEE_some_some {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i h : Fin k) : elimEE s t ρ x (some i) (some h) = M (Xconfig s t ρ x) (idxZ i) (idxZ h)

theorem BollobasNikiforov.elimEE_isHermitian {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : (elimEE s t ρ x).IsHermitian

theorem BollobasNikiforov.elimEE_isSymm {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : (elimEE s t ρ x).IsSymm

theorem BollobasNikiforov.elimEE_mulVec_none {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (v : Option (Fin k) → ℝ) : (elimEE s t ρ x).mulVec v none = M (Xconfig s t ρ x) idxZ0 idxZ0 * v none

theorem BollobasNikiforov.elimEE_mulVec_some {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (v : Option (Fin k) → ℝ) (i : Fin k) : (elimEE s t ρ x).mulVec v (some i) = ((M (Xconfig s t ρ x)).submatrix idxZ idxZ).mulVec (fun (h : Fin k) => v (some h)) i

theorem BollobasNikiforov.elimEE_quad {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (v : Option (Fin k) → ℝ) : v ⬝ᵥ (elimEE s t ρ x).mulVec v = M (Xconfig s t ρ x) idxZ0 idxZ0 * v none * v none + (fun (i : Fin k) => v (some i)) ⬝ᵥ ((M (Xconfig s t ρ x)).submatrix idxZ idxZ).mulVec fun (i : Fin k) => v (some i)

theorem BollobasNikiforov.elimEE_posDef {k p : ℕ} (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) : (elimEE s t ρ x).PosDef

EL13: the principal E-block is positive definite.

theorem BollobasNikiforov.elimTE_eq_conjTranspose {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : elimTE s t ρ x = (elimET s t ρ x).conjTranspose

theorem BollobasNikiforov.M_submatrix_sumElim {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : (M (Xconfig s t ρ x)).submatrix (Sum.elim elimEEmbed elimT) (Sum.elim elimEEmbed elimT) = Matrix.fromBlocks (elimEE s t ρ x) (elimET s t ρ x) (elimTE s t ρ x) (elimTT s t ρ x)

noncomputable def BollobasNikiforov.elimSchurR {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : Matrix (Fin p) (Fin p) ℝ

Schur complement of the E-block in the T-block.

Equations

• BollobasNikiforov.elimSchurR s t ρ x = BollobasNikiforov.elimTT s t ρ x - BollobasNikiforov.elimTE s t ρ x * (BollobasNikiforov.elimEE s t ρ x)⁻¹ * BollobasNikiforov.elimET s t ρ x

def BollobasNikiforov.extendByZeroT {k p : ℕ} (R : Matrix (Fin p) (Fin p) ℝ) : Matrix (ConfigIdx k p) (ConfigIdx k p) ℝ

Extension by zero off the T-indices.

Equations

• BollobasNikiforov.extendByZeroT R α β = match (BollobasNikiforov.configIdxEquiv k p) α, (BollobasNikiforov.configIdxEquiv k p) β with | Sum.inr j, Sum.inr ℓ => R j ℓ | x, x_1 => 0

theorem BollobasNikiforov.extendByZeroT_y_y {k p : ℕ} (R : Matrix (Fin p) (Fin p) ℝ) (j ℓ : Fin p) : extendByZeroT R (idxY j) (idxY ℓ) = R j ℓ

theorem BollobasNikiforov.extendByZeroT_z0_left {k p : ℕ} (R : Matrix (Fin p) (Fin p) ℝ) (β : ConfigIdx k p) : extendByZeroT R idxZ0 β = 0

theorem BollobasNikiforov.extendByZeroT_z_left {k p : ℕ} (R : Matrix (Fin p) (Fin p) ℝ) (i : Fin k) (β : ConfigIdx k p) : extendByZeroT R (idxZ i) β = 0

theorem BollobasNikiforov.extendByZeroT_z0_right {k p : ℕ} (R : Matrix (Fin p) (Fin p) ℝ) (α : ConfigIdx k p) : extendByZeroT R α idxZ0 = 0

theorem BollobasNikiforov.extendByZeroT_z_right {k p : ℕ} (R : Matrix (Fin p) (Fin p) ℝ) (α : ConfigIdx k p) (i : Fin k) : extendByZeroT R α (idxZ i) = 0

theorem BollobasNikiforov.elimSchurR_posSemidef {k p : ℕ} (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) : (elimSchurR s t ρ x).PosSemidef

EL13: the T-Schur complement of E is positive semidefinite.

Residual columns after ordered z-elimination

theorem BollobasNikiforov.isUnit_det_of_isUnit {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (h : IsUnit A) : IsUnit A.det

theorem BollobasNikiforov.mul_inv_of_isUnit_real {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (h : IsUnit A) : A * A⁻¹ = 1

theorem BollobasNikiforov.inv_mul_of_isUnit_real {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (h : IsUnit A) : A⁻¹ * A = 1

theorem BollobasNikiforov.schurComplementEntry_submatrix {ι : Type u_1} {r : ℕ} {n : Type u_2} (A : Matrix ι ι ℝ) (f : n → ι) (e : Fin r → n) (a b : n) : schurComplementEntry (A.submatrix f f) e a b = schurComplementEntry A (f ∘ e) (f a) (f b)

theorem BollobasNikiforov.schurComplementEntry_eq_zero_of_mem {r : ℕ} {n : Type u_2} (A : Matrix n n ℝ) (e : Fin r → n) (hU : IsUnit (A.submatrix e e)) (i : Fin r) (j : n) : schurComplementEntry A e (e i) j = 0

theorem BollobasNikiforov.castLE_proof_irrel {k n : ℕ} (h1 h2 : n ≤ k) : Fin.castLE h1 = Fin.castLE h2

noncomputable def BollobasNikiforov.elimRes {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (j : Fin k) (α : ConfigIdx k p) : ℝ

Residual of column idxZ j after eliminating earlier z-indices.

Equations

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

noncomputable def BollobasNikiforov.elimPivot {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (j : Fin k) : ℝ

Pivot at z-index j after eliminating earlier z-indices.

Equations

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

theorem BollobasNikiforov.elimPivot_pos {k p : ℕ} (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) (j : Fin k) : 0 < elimPivot s t ρ x j

theorem BollobasNikiforov.elimRes_idxZ {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (j β : Fin k) : elimRes s t ρ x j (idxZ β) = schurComplementEntry ((M (Xconfig s t ρ x)).submatrix idxZ idxZ) (Fin.castLE ⋯) β j

theorem BollobasNikiforov.elimRes_eq_pivot {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (j : Fin k) : elimRes s t ρ x j (idxZ j) = elimPivot s t ρ x j

theorem BollobasNikiforov.elimRes_nonneg {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) (hρ : ∀ (j : Fin p), 0 < ρ j) (hx : ∀ (j : Fin p), 0 ≤ x j) (j : Fin k) (α : ConfigIdx k p) : 0 ≤ elimRes s t ρ x j α

EL11: every residual column on ConfigIdx is nonnegative.

EL12 — C₀ is completely positive

noncomputable def BollobasNikiforov.elimVec0 {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : ConfigIdx k p → ℝ

The idxZ0 column of M (Xconfig s t ρ x) divided by the square root of its diagonal entry: the first factor of C₀.

Equations

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

noncomputable def BollobasNikiforov.elimVec {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (j : Fin k) : ConfigIdx k p → ℝ

The j-th elimination residual elimRes divided by the square root of its pivot elimPivot: the j.succ-th factor of C₀.

Equations

• BollobasNikiforov.elimVec s t ρ x j α = BollobasNikiforov.elimRes s t ρ x j α / √(BollobasNikiforov.elimPivot s t ρ x j)

noncomputable def BollobasNikiforov.elimC0Factor {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : Fin (k + 1) → ConfigIdx k p → ℝ

The k + 1 factors of C₀: elimVec0 followed by the vectors elimVec s t ρ x j.

Equations

• BollobasNikiforov.elimC0Factor s t ρ x = Fin.cons (BollobasNikiforov.elimVec0 s t ρ x) (BollobasNikiforov.elimVec s t ρ x)

noncomputable def BollobasNikiforov.elimC0 {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : Matrix (ConfigIdx k p) (ConfigIdx k p) ℝ

Sum of scaled residual outer products.

Equations

• BollobasNikiforov.elimC0 s t ρ x = ∑ a : Fin (k + 1), Matrix.vecMulVec (BollobasNikiforov.elimC0Factor s t ρ x a) (BollobasNikiforov.elimC0Factor s t ρ x a)

theorem BollobasNikiforov.elimVec0_nonneg {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hx : ∀ (j : Fin p), 0 ≤ x j) (α : ConfigIdx k p) : 0 ≤ elimVec0 s t ρ x α

theorem BollobasNikiforov.elimVec_nonneg {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) (hρ : ∀ (j : Fin p), 0 < ρ j) (hx : ∀ (j : Fin p), 0 ≤ x j) (j : Fin k) (α : ConfigIdx k p) : 0 ≤ elimVec s t ρ x j α

theorem BollobasNikiforov.elimC0Factor_nonneg {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) (hρ : ∀ (j : Fin p), 0 < ρ j) (hx : ∀ (j : Fin p), 0 ≤ x j) (a : Fin (k + 1)) (α : ConfigIdx k p) : 0 ≤ elimC0Factor s t ρ x a α

theorem BollobasNikiforov.isCompletelyPositive_elimC0 {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) (hρ : ∀ (j : Fin p), 0 < ρ j) (hx : ∀ (j : Fin p), 0 ≤ x j) : IsCompletelyPositive (elimC0 s t ρ x)

EL12: C₀ is completely positive.

Gram of the E-columns and the identity M = C₀ + pad R

noncomputable def BollobasNikiforov.elimColE {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (α : ConfigIdx k p) : Option (Fin k) → ℝ

Row α of M (Xconfig s t ρ x) restricted to the E-columns.

Equations

• BollobasNikiforov.elimColE s t ρ x α a = BollobasNikiforov.M (BollobasNikiforov.Xconfig s t ρ x) α (BollobasNikiforov.elimEEmbed a)

noncomputable def BollobasNikiforov.elimGramE {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : Matrix (ConfigIdx k p) (ConfigIdx k p) ℝ

P EE⁻¹ Pᵀ on configuration indices.

Equations

• BollobasNikiforov.elimGramE s t ρ x α β = BollobasNikiforov.elimColE s t ρ x α ⬝ᵥ (BollobasNikiforov.elimEE s t ρ x)⁻¹.mulVec (BollobasNikiforov.elimColE s t ρ x β)

noncomputable def BollobasNikiforov.elimZLead {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) {m : ℕ} (hm : m ≤ k) : Matrix (Fin m) (Fin m) ℝ

The leading m × m principal block of M (Xconfig s t ρ x) on the left-vector indices idxZ (Fin.castLE hm i).

Equations

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

noncomputable def BollobasNikiforov.elimColZLead {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) {m : ℕ} (hm : m ≤ k) (α : ConfigIdx k p) : Fin m → ℝ

Row α of M (Xconfig s t ρ x) restricted to the first m left-vector columns.

Equations

• BollobasNikiforov.elimColZLead s t ρ x hm α i = BollobasNikiforov.M (BollobasNikiforov.Xconfig s t ρ x) α (BollobasNikiforov.idxZ (Fin.castLE hm i))

noncomputable def BollobasNikiforov.elimGramZLead {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) {m : ℕ} (hm : m ≤ k) : Matrix (ConfigIdx k p) (ConfigIdx k p) ℝ

The matrix c_α ⬝ᵥ (elimZLead)⁻¹ *ᵥ c_β built from the columns elimColZLead: the part of M explained by the first m left vectors.

Equations

• BollobasNikiforov.elimGramZLead s t ρ x hm α β = BollobasNikiforov.elimColZLead s t ρ x hm α ⬝ᵥ (BollobasNikiforov.elimZLead s t ρ x hm)⁻¹.mulVec (BollobasNikiforov.elimColZLead s t ρ x hm β)

noncomputable def BollobasNikiforov.elimEEInv {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : Matrix (Option (Fin k)) (Option (Fin k)) ℝ

The block-diagonal matrix on Option (Fin k) with (M idxZ0 idxZ0)⁻¹ in the none corner and the inverse of the left-vector block of M (Xconfig s t ρ x) on the some indices.

Equations

• BollobasNikiforov.elimEEInv s t ρ x none none = (BollobasNikiforov.M (BollobasNikiforov.Xconfig s t ρ x) BollobasNikiforov.idxZ0 BollobasNikiforov.idxZ0)⁻¹
• BollobasNikiforov.elimEEInv s t ρ x none (some val) = 0
• BollobasNikiforov.elimEEInv s t ρ x (some val) none = 0
• BollobasNikiforov.elimEEInv s t ρ x (some i) (some h) = ((BollobasNikiforov.M (BollobasNikiforov.Xconfig s t ρ x)).submatrix BollobasNikiforov.idxZ BollobasNikiforov.idxZ)⁻¹ i h

theorem BollobasNikiforov.elimEE_mul_inv {k p : ℕ} (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) : elimEE s t ρ x * elimEEInv s t ρ x = 1

theorem BollobasNikiforov.elimEE_inv_eq {k p : ℕ} (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) : (elimEE s t ρ x)⁻¹ = elimEEInv s t ρ x

theorem BollobasNikiforov.elimEEInv_mulVec {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (v : Option (Fin k) → ℝ) : (elimEEInv s t ρ x).mulVec v = fun (a : Option (Fin k)) => match a with | none => (M (Xconfig s t ρ x) idxZ0 idxZ0)⁻¹ * v none | some i => ((M (Xconfig s t ρ x)).submatrix idxZ idxZ)⁻¹.mulVec (fun (h : Fin k) => v (some h)) i

theorem BollobasNikiforov.elimGramE_eq_z0_add_Z {k p : ℕ} (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) (α β : ConfigIdx k p) : elimGramE s t ρ x α β = M (Xconfig s t ρ x) α idxZ0 * ((M (Xconfig s t ρ x) idxZ0 idxZ0)⁻¹ * M (Xconfig s t ρ x) β idxZ0) + elimGramZLead s t ρ x ⋯ α β

theorem BollobasNikiforov.IsHermitian.nonsing_inv_real {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) (_hU : IsUnit A) : A⁻¹.IsHermitian

theorem BollobasNikiforov.dotProduct_nonsing_inv_comm {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) (hU : IsUnit A) (x y : n → ℝ) : x ⬝ᵥ A⁻¹.mulVec y = y ⬝ᵥ A⁻¹.mulVec x

theorem BollobasNikiforov.mulVec_sum_castSucc {m : ℕ} (Z : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) (x : Fin (m + 1) → ℝ) (i : Fin m) : Z.mulVec x i.castSucc = (Z.submatrix Fin.castSucc Fin.castSucc).mulVec (fun (j : Fin m) => x j.castSucc) i + Z i.castSucc (Fin.last m) * x (Fin.last m)

theorem BollobasNikiforov.mulVec_sum_last {m : ℕ} (Z : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) (x : Fin (m + 1) → ℝ) : Z.mulVec x (Fin.last m) = ((fun (i : Fin m) => Z (Fin.last m) i.castSucc) ⬝ᵥ fun (j : Fin m) => x j.castSucc) + Z (Fin.last m) (Fin.last m) * x (Fin.last m)

theorem BollobasNikiforov.dotProduct_sum_castSucc {m : ℕ} (P x : Fin (m + 1) → ℝ) : P ⬝ᵥ x = ((fun (i : Fin m) => P i.castSucc) ⬝ᵥ fun (j : Fin m) => x j.castSucc) + P (Fin.last m) * x (Fin.last m)

theorem BollobasNikiforov.gram_inv_castSucc_step {m : ℕ} (Z : Matrix (Fin (m + 1)) (Fin (m + 1)) ℝ) (hZ : Z.PosDef) (Pα Pβ : Fin (m + 1) → ℝ) : Pα ⬝ᵥ Z⁻¹.mulVec Pβ = ((fun (i : Fin m) => Pα i.castSucc) ⬝ᵥ (Z.submatrix Fin.castSucc Fin.castSucc)⁻¹.mulVec fun (i : Fin m) => Pβ i.castSucc) + 1 / schurComplementEntry Z Fin.castSucc (Fin.last m) (Fin.last m) * (Pα (Fin.last m) - (fun (i : Fin m) => Pα i.castSucc) ⬝ᵥ (Z.submatrix Fin.castSucc Fin.castSucc)⁻¹.mulVec fun (i : Fin m) => Z i.castSucc (Fin.last m)) * (Pβ (Fin.last m) - (fun (i : Fin m) => Pβ i.castSucc) ⬝ᵥ (Z.submatrix Fin.castSucc Fin.castSucc)⁻¹.mulVec fun (i : Fin m) => Z i.castSucc (Fin.last m))

theorem BollobasNikiforov.elimZLead_posDef {k p : ℕ} (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) {m : ℕ} (hm : m ≤ k) : (elimZLead s t ρ x hm).PosDef

theorem BollobasNikiforov.elimZLead_castSucc {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) {m : ℕ} (hm : m + 1 ≤ k) : (elimZLead s t ρ x hm).submatrix Fin.castSucc Fin.castSucc = elimZLead s t ρ x ⋯

theorem BollobasNikiforov.elimColZLead_castSucc {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) {m : ℕ} (hm : m + 1 ≤ k) (α : ConfigIdx k p) : (fun (i : Fin m) => elimColZLead s t ρ x hm α i.castSucc) = elimColZLead s t ρ x ⋯ α

theorem BollobasNikiforov.elimColZLead_last {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) {m : ℕ} (hm : m + 1 ≤ k) (α : ConfigIdx k p) : elimColZLead s t ρ x hm α (Fin.last m) = M (Xconfig s t ρ x) α (idxZ ⟨m, ⋯⟩)

theorem BollobasNikiforov.elimZLead_last_col {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) {m : ℕ} (hm : m + 1 ≤ k) (i : Fin m) : elimZLead s t ρ x hm i.castSucc (Fin.last m) = M (Xconfig s t ρ x) (idxZ (Fin.castLE ⋯ i)) (idxZ ⟨m, ⋯⟩)

theorem BollobasNikiforov.elimRes_succ {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) {m : ℕ} (hm : m + 1 ≤ k) (α : ConfigIdx k p) : elimRes s t ρ x ⟨m, ⋯⟩ α = elimColZLead s t ρ x hm α (Fin.last m) - elimColZLead s t ρ x ⋯ α ⬝ᵥ (elimZLead s t ρ x ⋯)⁻¹.mulVec fun (i : Fin m) => elimZLead s t ρ x hm i.castSucc (Fin.last m)

theorem BollobasNikiforov.elimPivot_succ {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) {m : ℕ} (hm : m + 1 ≤ k) : elimPivot s t ρ x ⟨m, ⋯⟩ = schurComplementEntry (elimZLead s t ρ x hm) Fin.castSucc (Fin.last m) (Fin.last m)

theorem BollobasNikiforov.elimGramZLead_succ {k p : ℕ} (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) {m : ℕ} (hm : m + 1 ≤ k) : elimGramZLead s t ρ x hm = elimGramZLead s t ρ x ⋯ + (1 / elimPivot s t ρ x ⟨m, ⋯⟩) • Matrix.vecMulVec (elimRes s t ρ x ⟨m, ⋯⟩) (elimRes s t ρ x ⟨m, ⋯⟩)

theorem BollobasNikiforov.elimGramZLead_eq_sum {k p : ℕ} (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) (m : ℕ) (hm : m ≤ k) : elimGramZLead s t ρ x hm = ∑ j : Fin m, (1 / elimPivot s t ρ x (Fin.castLE hm j)) • Matrix.vecMulVec (elimRes s t ρ x (Fin.castLE hm j)) (elimRes s t ρ x (Fin.castLE hm j))

theorem BollobasNikiforov.vecMulVec_div_sqrt {n : Type u_2} (v : n → ℝ) {d : ℝ} (hd : 0 < d) : (Matrix.vecMulVec (fun (i : n) => v i / √d) fun (i : n) => v i / √d) = d⁻¹ • Matrix.vecMulVec v v

theorem BollobasNikiforov.elimC0_eq_sum_scaled {k p : ℕ} (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) : elimC0 s t ρ x = ((M (Xconfig s t ρ x) idxZ0 idxZ0)⁻¹ • Matrix.vecMulVec (fun (α : ConfigIdx k p) => M (Xconfig s t ρ x) α idxZ0) fun (α : ConfigIdx k p) => M (Xconfig s t ρ x) α idxZ0) + ∑ j : Fin k, (elimPivot s t ρ x j)⁻¹ • Matrix.vecMulVec (elimRes s t ρ x j) (elimRes s t ρ x j)

theorem BollobasNikiforov.elimGramZLead_full {k p : ℕ} (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) : elimGramZLead s t ρ x ⋯ = ∑ j : Fin k, (elimPivot s t ρ x j)⁻¹ • Matrix.vecMulVec (elimRes s t ρ x j) (elimRes s t ρ x j)

theorem BollobasNikiforov.elimC0_eq_elimGramE {k p : ℕ} (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) : elimC0 s t ρ x = elimGramE s t ρ x

theorem BollobasNikiforov.elimColE_embed {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (a : Option (Fin k)) : elimColE s t ρ x (elimEEmbed a) = fun (b : Option (Fin k)) => elimEE s t ρ x a b

theorem BollobasNikiforov.elimGramE_embed {k p : ℕ} (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) (a b : Option (Fin k)) : elimGramE s t ρ x (elimEEmbed a) (elimEEmbed b) = elimEE s t ρ x a b

theorem BollobasNikiforov.elimGramE_embed_y {k p : ℕ} (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) (a : Option (Fin k)) (ℓ : Fin p) : elimGramE s t ρ x (elimEEmbed a) (idxY ℓ) = elimET s t ρ x a ℓ

theorem BollobasNikiforov.elimGramE_y_embed {k p : ℕ} (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) (j : Fin p) (b : Option (Fin k)) : elimGramE s t ρ x (idxY j) (elimEEmbed b) = elimTE s t ρ x j b

theorem BollobasNikiforov.mul_mul_col_apply {l : Type u_2} {m : Type u_3} {n : Type u_4} {o : Type u_5} [Fintype m] [Fintype n] (A : Matrix l m ℝ) (B : Matrix m n ℝ) (C : Matrix n o ℝ) (i : l) (j : o) : (A * B * C) i j = (fun (a : m) => A i a) ⬝ᵥ B.mulVec fun (k : n) => C k j

theorem BollobasNikiforov.elimGramE_y_y {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (j ℓ : Fin p) : elimGramE s t ρ x (idxY j) (idxY ℓ) = (elimTE s t ρ x * (elimEE s t ρ x)⁻¹ * elimET s t ρ x) j ℓ

theorem BollobasNikiforov.M_eq_elimGramE_add_extend {k p : ℕ} (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) : M (Xconfig s t ρ x) = elimGramE s t ρ x + extendByZeroT (elimSchurR s t ρ x)

EL13: M = C₀ + extendByZero R with R the T-Schur complement of E.

theorem BollobasNikiforov.M_eq_elimC0_add_extend {k p : ℕ} (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) : M (Xconfig s t ρ x) = elimC0 s t ρ x + extendByZeroT (elimSchurR s t ρ x)

theorem BollobasNikiforov.lem_elimination {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (ht : ∀ (i : Fin k), 0 < t i) (hmono : Monotone t) (hρ : ∀ (j : Fin p), 0 < ρ j) (hx : ∀ (j : Fin p), 0 ≤ x j) : ∃ (C₀ : Matrix (ConfigIdx k p) (ConfigIdx k p) ℝ), IsCompletelyPositive C₀ ∧ M (Xconfig s t ρ x) = C₀ + extendByZeroT (elimSchurR s t ρ x) ∧ (elimSchurR s t ρ x).PosSemidef

EL14 — lem:elimination.