Feature factorisation M = FFᵀ + L and the Schur complement of E

SC01–SC07 record the weights q i, γ, the feature matrix F, the weighted Laplacian L, the E-block L_EE and its inverse, and the reduced data L_red, 𝒰 of docs/sol.tex §4.

After block elimination replaces L by diag(L_EE, L_red) and the feature rows by (F_E, 𝒰), the Schur complement of the first block is L_red + 𝒰 (I - F_Eᵀ (L_EE + F_E F_Eᵀ)⁻¹ F_E) 𝒰ᵀ. The bracket equals (I + F_Eᵀ L_EE⁻¹ F_E)⁻¹ by the Woodbury companion identity (paper (eq:Schur)).

theorem BollobasNikiforov.woodbury_add_mul_transpose {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] {R : Type u_3} [CommRing R] (L : Matrix ι ι R) (F : Matrix ι κ R) (hL : IsUnit L) (hW : IsUnit (1 + F.transpose * L⁻¹ * F)) : (L + F * F.transpose)⁻¹ = L⁻¹ - L⁻¹ * F * (1 + F.transpose * L⁻¹ * F)⁻¹ * F.transpose * L⁻¹

Woodbury formula for a rank-κ update L + F Fᵀ.

theorem BollobasNikiforov.one_sub_transpose_mul_inv_mul {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] {R : Type u_3} [CommRing R] (L : Matrix ι ι R) (F : Matrix ι κ R) (hL : IsUnit L) (hW : IsUnit (1 + F.transpose * L⁻¹ * F)) : 1 - F.transpose * (L + F * F.transpose)⁻¹ * F = (1 + F.transpose * L⁻¹ * F)⁻¹

SC08. Woodbury companion identity: I - Fᵀ (L + F Fᵀ)⁻¹ F = (I + Fᵀ L⁻¹ F)⁻¹.

theorem BollobasNikiforov.mul_one_sub_conj {κ : Type u_2} [Fintype κ] [DecidableEq κ] {R : Type u_3} [CommRing R] {ε : Type u_4} {τ : Type u_5} [Fintype ε] [DecidableEq ε] (U : Matrix τ κ R) (FE : Matrix ε κ R) (A : Matrix ε ε R) : U * (1 - FE.transpose * A⁻¹ * FE) * U.transpose = U * U.transpose - U * FE.transpose * A⁻¹ * FE * U.transpose

Expanding 𝒰 (I - F_Eᵀ (L_EE + F_E F_Eᵀ)⁻¹ F_E) 𝒰ᵀ as a Schur remainder.

theorem BollobasNikiforov.schurComplement_diag_add_mul {κ : Type u_2} [Fintype κ] [DecidableEq κ] {R : Type u_3} [CommRing R] {ε : Type u_4} {τ : Type u_5} [Fintype ε] [DecidableEq ε] (Lred : Matrix τ τ R) (U : Matrix τ κ R) (FE : Matrix ε κ R) (A : Matrix ε ε R) : Lred + U * U.transpose - U * FE.transpose * A⁻¹ * FE * U.transpose = Lred + U * (1 - FE.transpose * A⁻¹ * FE) * U.transpose

After replacing L by diag(L_EE, L_red), the Schur complement of E in FFᵀ + L is L_red + 𝒰 (I - F_Eᵀ (L_EE + F_E F_Eᵀ)⁻¹ F_E) 𝒰ᵀ.

theorem BollobasNikiforov.schurComplement_woodbury {κ : Type u_2} [Fintype κ] [DecidableEq κ] {R : Type u_3} [CommRing R] {ε : Type u_4} {τ : Type u_5} [Fintype ε] [DecidableEq ε] (LEE : Matrix ε ε R) (Lred : Matrix τ τ R) (FE : Matrix ε κ R) (U : Matrix τ κ R) (hLEE : IsUnit LEE) (hW : IsUnit (1 + FE.transpose * LEE⁻¹ * FE)) : Lred + U * U.transpose - U * FE.transpose * (LEE + FE * FE.transpose)⁻¹ * FE * U.transpose = Lred + U * (1 + FE.transpose * LEE⁻¹ * FE)⁻¹ * U.transpose

SC08, reduced coordinates. The Schur complement of E in FFᵀ + L after block diagonalization of L equals L_red + 𝒰 (I + F_Eᵀ L_EE⁻¹ F_E)⁻¹ 𝒰ᵀ.

theorem BollobasNikiforov.fromBlocks_add_mul_transpose {κ : Type u_2} [Fintype κ] {R : Type u_3} [CommRing R] {ε : Type u_4} {τ : Type u_5} (LEE : Matrix ε ε R) (Lred : Matrix τ τ R) (FE : Matrix ε κ R) (U : Matrix τ κ R) : FE.fromRows U * (FE.fromRows U).transpose + Matrix.fromBlocks LEE 0 0 Lred = Matrix.fromBlocks (LEE + FE * FE.transpose) (FE * U.transpose) (U * FE.transpose) (Lred + U * U.transpose)

Assembling FFᵀ + diag(L_EE, L_red) as a 2×2 block matrix.

Configuration-dependent Schur data (SC01–SC07)

SC01 — weights q i and γ

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

qᵢ = sᵢ / dᵢ.

Equations

• BollobasNikiforov.configQ s t ρ x i = s i / BollobasNikiforov.configD t ρ x i

theorem BollobasNikiforov.configQ_pos {k p : ℕ} (s t : Fin k → ℝ) {ρ : Fin p → ℝ} (hρ : ∀ (j : Fin p), 0 < ρ j) (x : Fin p → ℝ) {i : Fin k} (hsi : 0 < s i) : 0 < configQ s t ρ x i

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

γ = σ - ∑ qᵢ.

Equations

• BollobasNikiforov.configγ s t ρ x = BollobasNikiforov.configσ s - ∑ i : Fin k, BollobasNikiforov.configQ s t ρ x i

theorem BollobasNikiforov.configγ_eq_sum {k p : ℕ} (s t : Fin k → ℝ) {ρ : Fin p → ℝ} (hρ : ∀ (j : Fin p), 0 < ρ j) (x : Fin p → ℝ) : configγ s t ρ x = ∑ i : Fin k, s i * configH t ρ x i / configD t ρ x i

theorem BollobasNikiforov.configγ_nonneg {k p : ℕ} (s t : Fin k → ℝ) {ρ : Fin p → ℝ} (hρ : ∀ (j : Fin p), 0 < ρ j) (x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) : 0 ≤ configγ s t ρ x

SC02 — feature matrix F

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

Rows: e₀ᵀ at z₀, sᵢ v(tᵢ)ᵀ at zᵢ, ρⱼ b(xⱼ)ᵀ at yⱼ.

Equations

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

theorem BollobasNikiforov.configF_z0 {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : configF s t ρ x idxZ0 = e 0

theorem BollobasNikiforov.configF_z {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i : Fin k) : configF s t ρ x (idxZ i) = s i • v (t i)

theorem BollobasNikiforov.configF_y {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (j : Fin p) : configF s t ρ x (idxY j) = ρ j • b (x j)

theorem BollobasNikiforov.configF_mul_transpose_apply {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (α β : ConfigIdx k p) : (configF s t ρ x * (configF s t ρ x).transpose) α β = configF s t ρ x α ⬝ᵥ configF s t ρ x β

Feature inner products

theorem BollobasNikiforov.v_dot_v (t₁ t₂ : ℝ) : v t₁ ⬝ᵥ v t₂ = (1 + t₁ * t₂) ^ 2

theorem BollobasNikiforov.v_dot_b (ti xj : ℝ) : v ti ⬝ᵥ b xj = (xj - ti) ^ 2

theorem BollobasNikiforov.b_dot_b (x₁ x₂ : ℝ) : b x₁ ⬝ᵥ b x₂ = (1 + x₁ * x₂) ^ 2

theorem BollobasNikiforov.e0_dot_v (ti : ℝ) : e 0 ⬝ᵥ v ti = 1

theorem BollobasNikiforov.e0_dot_b (xj : ℝ) : e 0 ⬝ᵥ b xj = xj ^ 2

theorem BollobasNikiforov.e0_dot_e0 : e 0 ⬝ᵥ e 0 = 1

theorem BollobasNikiforov.yVec_dot_yVec {p : ℕ} (ρ x : Fin p → ℝ) (j ℓ : Fin p) : yVec ρ x j ⬝ᵥ yVec ρ x ℓ = √(ρ j) * √(ρ ℓ) * (x j * x ℓ + 1)

theorem BollobasNikiforov.Xconfig_y_y {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (j ℓ : Fin p) : Xconfig s t ρ x (idxY j) (idxY ℓ) = √(ρ j) * √(ρ ℓ) * (x j * x ℓ + 1)

SC03 — Laplacian L and M = FFᵀ + L

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

Weighted Laplacian: weight sᵢ on z₀–zᵢ and sᵢ ρⱼ aᵢ(xⱼ) on zᵢ–yⱼ.

Equations

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

theorem BollobasNikiforov.configL_apply {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (α β : ConfigIdx k p) : configL s t ρ x α β = ∑ i : Fin k, s i * Matrix.vecMulVec (e idxZ0 - e (idxZ i)) (e idxZ0 - e (idxZ i)) α β + ∑ i : Fin k, ∑ j : Fin p, s i * ρ j * truncSq (t i) (x j) * Matrix.vecMulVec (e (idxZ i) - e (idxY j)) (e (idxZ i) - e (idxY j)) α β

theorem BollobasNikiforov.configH_eq_sum_truncSq {k p : ℕ} (t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i : Fin k) : configH t ρ x i = ∑ j : Fin p, ρ j * truncSq (t i) (x j)

theorem BollobasNikiforov.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 α

theorem BollobasNikiforov.idxY_injective {k p : ℕ} {j ℓ : Fin p} (h : idxY j = idxY ℓ) : j = ℓ

theorem BollobasNikiforov.idxZ_injective {k p : ℕ} {i h : Fin k} (heq : idxZ i = idxZ h) : i = h

@[simp]

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

@[simp]

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

@[simp]

theorem BollobasNikiforov.idxZ_ne_idxZ0 {k p : ℕ} (i : Fin k) : idxZ i ≠ idxZ0

@[simp]

theorem BollobasNikiforov.idxY_ne_idxZ0 {k p : ℕ} (j : Fin p) : idxY j ≠ idxZ0

@[simp]

theorem BollobasNikiforov.idxY_ne_idxZ {k p : ℕ} (i : Fin k) (j : Fin p) : idxY j ≠ idxZ i

theorem BollobasNikiforov.sub_edge_z0 {k p : ℕ} (i : Fin k) (α : ConfigIdx k p) : (e idxZ0 - e (idxZ i)) α = if α = idxZ0 then 1 else if α = idxZ i then -1 else 0

theorem BollobasNikiforov.sub_edge_zy {k p : ℕ} (i : Fin k) (j : Fin p) (α : ConfigIdx k p) : (e (idxZ i) - e (idxY j)) α = if α = idxZ i then 1 else if α = idxY j then -1 else 0

theorem BollobasNikiforov.edge_z0 {k p : ℕ} (i : Fin k) (α β : ConfigIdx k p) : Matrix.vecMulVec (e idxZ0 - e (idxZ i)) (e idxZ0 - e (idxZ i)) α β = (if α = idxZ0 then 1 else if α = idxZ i then -1 else 0) * if β = idxZ0 then 1 else if β = idxZ i then -1 else 0

theorem BollobasNikiforov.edge_zy {k p : ℕ} (i : Fin k) (j : Fin p) (α β : ConfigIdx k p) : Matrix.vecMulVec (e (idxZ i) - e (idxY j)) (e (idxZ i) - e (idxY j)) α β = (if α = idxZ i then 1 else if α = idxY j then -1 else 0) * if β = idxZ i then 1 else if β = idxY j then -1 else 0

theorem BollobasNikiforov.configL_z0_z0 {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : configL s t ρ x idxZ0 idxZ0 = configσ s

theorem BollobasNikiforov.configL_z0_z {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i : Fin k) : configL s t ρ x idxZ0 (idxZ i) = -s i

theorem BollobasNikiforov.configL_z0_y {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (j : Fin p) : configL s t ρ x idxZ0 (idxY j) = 0

theorem BollobasNikiforov.configL_z_z {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i h : Fin k) : configL s t ρ x (idxZ i) (idxZ h) = if i = h then s i * configD t ρ x i else 0

theorem BollobasNikiforov.configL_z_y {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i : Fin k) (j : Fin p) : configL s t ρ x (idxZ i) (idxY j) = -(s i * ρ j * truncSq (t i) (x j))

theorem BollobasNikiforov.configL_y_y {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (j ℓ : Fin p) : configL s t ρ x (idxY j) (idxY ℓ) = if j = ℓ then ∑ i : Fin k, s i * ρ j * truncSq (t i) (x j) else 0

theorem BollobasNikiforov.configL_symm {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (α β : ConfigIdx k p) : configL s t ρ x α β = configL s t ρ x β α

theorem BollobasNikiforov.M_Xconfig_symm {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (α β : ConfigIdx k p) : M (Xconfig s t ρ x) α β = M (Xconfig s t ρ x) β α

theorem BollobasNikiforov.FF_z0_z0 {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : (configF s t ρ x * (configF s t ρ x).transpose) idxZ0 idxZ0 = 1

theorem BollobasNikiforov.FF_z0_z {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i : Fin k) : (configF s t ρ x * (configF s t ρ x).transpose) idxZ0 (idxZ i) = s i

theorem BollobasNikiforov.FF_z0_y {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (j : Fin p) : (configF s t ρ x * (configF s t ρ x).transpose) idxZ0 (idxY j) = ρ j * x j ^ 2

theorem BollobasNikiforov.FF_z_z {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i h : Fin k) : (configF s t ρ x * (configF s t ρ x).transpose) (idxZ i) (idxZ h) = s i * s h * (1 + t i * t h) ^ 2

theorem BollobasNikiforov.FF_z_y {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i : Fin k) (j : Fin p) : (configF s t ρ x * (configF s t ρ x).transpose) (idxZ i) (idxY j) = s i * ρ j * (x j - t i) ^ 2

theorem BollobasNikiforov.FF_y_y {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (j ℓ : Fin p) : (configF s t ρ x * (configF s t ρ x).transpose) (idxY j) (idxY ℓ) = ρ j * ρ ℓ * (1 + x j * x ℓ) ^ 2

theorem BollobasNikiforov.truncSq_neg_id (ti xj : ℝ) : max (ti - xj) 0 ^ 2 = (xj - ti) ^ 2 - truncSq ti xj

theorem BollobasNikiforov.MX_y_y_of_ne {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hρ : ∀ (j : Fin p), 0 < ρ j) (hx : ∀ (j : Fin p), 0 ≤ x j) {j ℓ : Fin p} (hjl : j ≠ ℓ) : M (Xconfig s t ρ x) (idxY j) (idxY ℓ) = ρ j * ρ ℓ * (1 + x j * x ℓ) ^ 2

theorem BollobasNikiforov.MX_y_y_diag {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) (j : Fin p) : M (Xconfig s t ρ x) (idxY j) (idxY j) = ρ j * ρ j * (1 + x j * x j) ^ 2 + ∑ i : Fin k, s i * ρ j * truncSq (t i) (x j)

theorem BollobasNikiforov.M_eq_configF_mul_transpose_add_configL {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) = configF s t ρ x * (configF s t ρ x).transpose + configL s t ρ x

SC04 — the E-block of L

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

Embeds the E-indices into ConfigIdx k p: the axis vector none ↦ idxZ0 and the left vectors some i ↦ idxZ i.

Equations

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

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

The E-block of the weighted Laplacian configL s t ρ x.

Equations

• BollobasNikiforov.configLEE s t ρ x = (BollobasNikiforov.configL s t ρ x).submatrix BollobasNikiforov.configEEmbed BollobasNikiforov.configEEmbed

theorem BollobasNikiforov.configLEE_none_none {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : configLEE s t ρ x none none = configσ s

theorem BollobasNikiforov.configLEE_none_some {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i : Fin k) : configLEE s t ρ x none (some i) = -s i

theorem BollobasNikiforov.configLEE_some_none {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i : Fin k) : configLEE s t ρ x (some i) none = -s i

theorem BollobasNikiforov.configLEE_some_some {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i h : Fin k) : configLEE s t ρ x (some i) (some h) = if i = h then s i * configD t ρ x i else 0

theorem BollobasNikiforov.configL_posSemidef {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) : (configL s t ρ x).PosSemidef

theorem BollobasNikiforov.configLEE_posSemidef {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) : (configLEE s t ρ x).PosSemidef

theorem BollobasNikiforov.configLEE_mulVec_none {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (v : Option (Fin k) → ℝ) : (configLEE s t ρ x).mulVec v none = configσ s * v none - ∑ i : Fin k, s i * v (some i)

theorem BollobasNikiforov.configLEE_mulVec_some {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (v : Option (Fin k) → ℝ) (i : Fin k) : (configLEE s t ρ x).mulVec v (some i) = -s i * v none + s i * configD t ρ x i * v (some i)

theorem BollobasNikiforov.configLEE_dot {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (v : Option (Fin k) → ℝ) : v ⬝ᵥ (configLEE s t ρ x).mulVec v = configσ s * v none ^ 2 - 2 * v none * ∑ i : Fin k, s i * v (some i) + ∑ i : Fin k, s i * configD t ρ x i * v (some i) ^ 2

theorem BollobasNikiforov.configLEE_quad {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (v : Option (Fin k) → ℝ) : v ⬝ᵥ (configLEE s t ρ x).mulVec v = ∑ i : Fin k, s i * (v none - v (some i)) ^ 2 + ∑ i : Fin k, s i * configH t ρ x i * v (some i) ^ 2

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

theorem BollobasNikiforov.configLEE_posDef {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) : (configLEE s t ρ x).PosDef

SC05 — Schur complement of the lower-right of L_EE is γ

theorem BollobasNikiforov.configγ_eq_schur {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) : configσ s - s ⬝ᵥ (Matrix.diagonal fun (i : Fin k) => s i * configD t ρ x i)⁻¹.mulVec s = configγ s t ρ x

SC06 — inverse of L_EE

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

The weight vector on the E-indices: 1 at the axis vector and (configD t ρ x i)⁻¹ at the i-th left vector.

Equations

• BollobasNikiforov.configW t ρ x none = 1
• BollobasNikiforov.configW t ρ x (some i) = (BollobasNikiforov.configD t ρ x i)⁻¹

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

The diagonal matrix on the E-indices with 0 at the axis vector and (s i * configD t ρ x i)⁻¹ at the i-th left vector; it is the diagonal part of (configLEE s t ρ x)⁻¹.

Equations

• BollobasNikiforov.configLEEInvDiag s t ρ x = Matrix.diagonal fun (x_1 : Option (Fin k)) => match x_1 with | none => 0 | some i => (s i * BollobasNikiforov.configD t ρ x i)⁻¹

theorem BollobasNikiforov.configLEE_mulVec_w {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (_hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) : (configLEE s t ρ x).mulVec (configW t ρ x) = fun (a : Option (Fin k)) => if a = none then configγ s t ρ x else 0

theorem BollobasNikiforov.mul_vecMulVec {k : ℕ} (A : Matrix (Option (Fin k)) (Option (Fin k)) ℝ) (u w : Option (Fin k) → ℝ) : A * Matrix.vecMulVec u w = Matrix.vecMulVec (A.mulVec u) w

theorem BollobasNikiforov.configLEE_mul_invDiag_apply {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (a b : Option (Fin k)) : (configLEE s t ρ x * configLEEInvDiag s t ρ x) a b = match b with | none => 0 | some j => configLEE s t ρ x a (some j) * (s j * configD t ρ x j)⁻¹

theorem BollobasNikiforov.configLEE_inv {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) : (configLEE s t ρ x)⁻¹ = configLEEInvDiag s t ρ x + (configγ s t ρ x)⁻¹ • Matrix.vecMulVec (configW t ρ x) (configW t ρ x)

SC07 — L_red and 𝒰

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

The right-vector block of the weighted Laplacian configL s t ρ x.

Equations

• BollobasNikiforov.configLTT s t ρ x = (BollobasNikiforov.configL s t ρ x).submatrix BollobasNikiforov.idxY BollobasNikiforov.idxY

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

The block of the weighted Laplacian configL s t ρ x with right-vector rows and E-columns.

Equations

• BollobasNikiforov.configLTE s t ρ x = (BollobasNikiforov.configL s t ρ x).submatrix BollobasNikiforov.idxY BollobasNikiforov.configEEmbed

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

The block of the weighted Laplacian configL s t ρ x with E-rows and right-vector columns.

Equations

• BollobasNikiforov.configLET s t ρ x = (BollobasNikiforov.configL s t ρ x).submatrix BollobasNikiforov.configEEmbed BollobasNikiforov.idxY

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

The E-rows of the three-column factor configF s t ρ x.

Equations

• BollobasNikiforov.configFE s t ρ x = (BollobasNikiforov.configF s t ρ x).submatrix BollobasNikiforov.configEEmbed id

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

The right-vector rows of the three-column factor configF s t ρ x.

Equations

• BollobasNikiforov.configFT s t ρ x = (BollobasNikiforov.configF s t ρ x).submatrix BollobasNikiforov.idxY id

noncomputable def BollobasNikiforov.configLred {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (_hs : ∀ (i : Fin k), 0 < s i) (_hρ : ∀ (j : Fin p), 0 < ρ j) (_hγ : 0 < configγ s t ρ x) : Matrix (Fin p) (Fin p) ℝ

The Schur complement L_TT - L_TE L_EE⁻¹ L_ET of the E-block in the weighted Laplacian. The positivity hypotheses are the conditions under which L_EE is invertible.

Equations

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

noncomputable def BollobasNikiforov.configU {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (_hs : ∀ (i : Fin k), 0 < s i) (_hρ : ∀ (j : Fin p), 0 < ρ j) (_hγ : 0 < configγ s t ρ x) : Matrix (Fin p) (Fin 3) ℝ

The reduced three-column factor F_T - L_TE L_EE⁻¹ F_E. The positivity hypotheses are the conditions under which L_EE is invertible.

Equations

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

theorem BollobasNikiforov.configLEE_isUnit {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) : IsUnit (configLEE s t ρ x)

Feature / Laplacian blocks on E and T

theorem BollobasNikiforov.configFE_none {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : configFE s t ρ x none = e 0

theorem BollobasNikiforov.configFE_some {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i : Fin k) : configFE s t ρ x (some i) = s i • v (t i)

theorem BollobasNikiforov.configFT_apply {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (j : Fin p) : configFT s t ρ x j = ρ j • b (x j)

theorem BollobasNikiforov.configLTE_none {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (j : Fin p) : configLTE s t ρ x j none = 0

theorem BollobasNikiforov.configLTE_some {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (j : Fin p) (i : Fin k) : configLTE s t ρ x j (some i) = -(s i * ρ j * truncSq (t i) (x j))

theorem BollobasNikiforov.configLET_none {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (j : Fin p) : configLET s t ρ x none j = 0

theorem BollobasNikiforov.configLET_some {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i : Fin k) (j : Fin p) : configLET s t ρ x (some i) j = -(s i * ρ j * truncSq (t i) (x j))

theorem BollobasNikiforov.configLTT_apply {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (j ℓ : Fin p) : configLTT s t ρ x j ℓ = if j = ℓ then ∑ i : Fin k, s i * ρ j * truncSq (t i) (x j) else 0

theorem BollobasNikiforov.Vvec_eq_e0_add_sum {k : ℕ} (t q : Fin k → ℝ) : Vvec t q = e 0 + ∑ i : Fin k, q i • v (t i)

theorem BollobasNikiforov.configFE_transpose_mulVec_w {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : (configFE s t ρ x).transpose.mulVec (configW t ρ x) = Vvec t (configQ s t ρ x)

SC10 — center row of L_EE⁻¹ F_E

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

The product L_EE⁻¹ F_E of the inverse E-block with the E-rows of the three-column factor.

Equations

• BollobasNikiforov.configInvFE s t ρ x = (BollobasNikiforov.configLEE s t ρ x)⁻¹ * BollobasNikiforov.configFE s t ρ x

theorem BollobasNikiforov.configLEE_invDiag_mul_FE_none {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : (configLEEInvDiag s t ρ x * configFE s t ρ x) none = 0

theorem BollobasNikiforov.configLEE_invDiag_mul_FE_some {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) : (configLEEInvDiag s t ρ x * configFE s t ρ x) (some i) = (configD t ρ x i)⁻¹ • v (t i)

theorem BollobasNikiforov.vecMulVec_w_mul_FE {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (a : Option (Fin k)) : (Matrix.vecMulVec (configW t ρ x) (configW t ρ x) * configFE s t ρ x) a = configW t ρ x a • Vvec t (configQ s t ρ x)

theorem BollobasNikiforov.configInvFE_none {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) : configInvFE s t ρ x none = (configγ s t ρ x)⁻¹ • Vvec t (configQ s t ρ x)

theorem BollobasNikiforov.configInvFE_some {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) (i : Fin k) : configInvFE s t ρ x (some i) = (configD t ρ x i)⁻¹ • (v (t i) + (configγ s t ρ x)⁻¹ • Vvec t (configQ s t ρ x))

SC11 — I + F_Eᵀ L_EE⁻¹ F_E = 𝒜 + V Vᵀ / γ

theorem BollobasNikiforov.one_add_configFE_conj_inv {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) : 1 + (configFE s t ρ x).transpose * (configLEE s t ρ x)⁻¹ * configFE s t ρ x = 𝒦Mat t (configQ s t ρ x) (configγ s t ρ x)

SC12 — rows of 𝒰

theorem BollobasNikiforov.configLTE_mul_InvFE {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) (j : Fin p) : (configLTE s t ρ x * configInvFE s t ρ x) j = -ρ j • (∑ i : Fin k, (configQ s t ρ x i * truncSq (t i) (x j)) • v (t i) + (h t (configQ s t ρ x) (x j) / configγ s t ρ x) • Vvec t (configQ s t ρ x))

theorem BollobasNikiforov.configU_apply {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) (j : Fin p) : configU s t ρ x hs hρ hγ j = ρ j • U t (configQ s t ρ x) (configγ s t ρ x) (x j)

theorem BollobasNikiforov.mul_vecMulVec_mul_apply {m : Type u_4} {n : Type u_5} [Fintype n] (A : Matrix m n ℝ) (w : n → ℝ) (C : Matrix n m ℝ) (j ℓ : m) : (A * Matrix.vecMulVec w w * C) j ℓ = (∑ a : n, A j a * w a) * ∑ b : n, w b * C b ℓ

Expand (A * wwᵀ * C) j ℓ without unfolding the index type of w.

SC14 — off-diagonal of L_red

theorem BollobasNikiforov.configLred_of_ne {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) {j ℓ : Fin p} (hjl : j ≠ ℓ) : -configLred s t ρ x hs hρ hγ j ℓ = ρ j * ρ ℓ * (∑ i : Fin k, configQ s t ρ x i * truncSq (t i) (x j) * truncSq (t i) (x ℓ) + h t (configQ s t ρ x) (x j) * h t (configQ s t ρ x) (x ℓ) / configγ s t ρ x)

theorem BollobasNikiforov.configLred_of_ne_nonneg {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) {j ℓ : Fin p} (hjl : j ≠ ℓ) : 0 ≤ -configLred s t ρ x hs hρ hγ j ℓ

SC15 — L 1 = 0 implies L_red 1 = 0

theorem BollobasNikiforov.configL_mulVec_one {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : (configL s t ρ x).mulVec 1 = 0

theorem BollobasNikiforov.configLEE_mulVec_one_add {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (a : Option (Fin k)) : (configLEE s t ρ x).mulVec 1 a + (configLET s t ρ x).mulVec 1 a = (configL s t ρ x).mulVec 1 (configEEmbed a)

theorem BollobasNikiforov.configLTT_mulVec_one_add {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (j : Fin p) : (configLTT s t ρ x).mulVec 1 j + (configLTE s t ρ x).mulVec 1 j = (configL s t ρ x).mulVec 1 (idxY j)

theorem BollobasNikiforov.configLred_mulVec_one {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) : (configLred s t ρ x hs hρ hγ).mulVec 1 = 0

SC16 — L_red is a weighted Laplacian

theorem BollobasNikiforov.weighted_sum_offDiag {n : Type u_4} [Fintype n] [DecidableEq n] [LinearOrder n] (ℓ : n → n → ℝ) {i j : n} (hij : i ≠ j) : ∑ p : n, ∑ q : n, (if p < q then ℓ p q else 0) * Matrix.vecMulVec (e p - e q) (e p - e q) i j = if i < j then -ℓ i j else if j < i then -ℓ j i else 0

theorem BollobasNikiforov.weighted_sum_diag {n : Type u_4} [Fintype n] [DecidableEq n] [LinearOrder n] (ℓ : n → n → ℝ) (i : n) : ∑ p : n, ∑ q : n, (if p < q then ℓ p q else 0) * Matrix.vecMulVec (e p - e q) (e p - e q) i i = (∑ q : n, if i < q then ℓ i q else 0) + ∑ p : n, if p < i then ℓ p i else 0

theorem BollobasNikiforov.isSymm_mulVec_one_eq_weightedLaplacian {n : Type u_4} [Fintype n] [DecidableEq n] [LinearOrder n] (A : Matrix n n ℝ) (hA : A.IsSymm) (h1 : A.mulVec 1 = 0) : A = ∑ p : n, ∑ q : n, (if p < q then -A p q else 0) • Matrix.vecMulVec (e p - e q) (e p - e q)

theorem BollobasNikiforov.configLred_isSymm {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) : (configLred s t ρ x hs hρ hγ).IsSymm

theorem BollobasNikiforov.configLred_eq_weightedLaplacian {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) : configLred s t ρ x hs hρ hγ = ∑ j : Fin p, ∑ ℓ : Fin p, (if j < ℓ then -configLred s t ρ x hs hρ hγ j ℓ else 0) • Matrix.vecMulVec (e j - e ℓ) (e j - e ℓ)

SC09 — elimSchurR equals the Woodbury remainder

theorem BollobasNikiforov.configEEmbed_eq_elimEEmbed {k p : ℕ} : configEEmbed = elimEEmbed

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

theorem BollobasNikiforov.configLET_eq_transpose {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : configLET s t ρ x = (configLTE s t ρ x).transpose

theorem BollobasNikiforov.configLEE_nonsing_inv_mul {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) : (configLEE s t ρ x)⁻¹ * configLEE s t ρ x = 1

theorem BollobasNikiforov.configLEE_mul_nonsing_inv {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) : configLEE s t ρ x * (configLEE s t ρ x)⁻¹ = 1

theorem BollobasNikiforov.isUnit_one_add_configFE_conj {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) : IsUnit (1 + (configFE s t ρ x).transpose * (configLEE s t ρ x)⁻¹ * configFE s t ρ x)

theorem BollobasNikiforov.elimEE_eq_LEE_add_FE {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 = configLEE s t ρ x + configFE s t ρ x * (configFE s t ρ x).transpose

theorem BollobasNikiforov.elimET_eq_LET_add_FE_FT {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) : elimET s t ρ x = configLET s t ρ x + configFE s t ρ x * (configFT s t ρ x).transpose

theorem BollobasNikiforov.elimTE_eq_LTE_add_FT_FE {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) : elimTE s t ρ x = configLTE s t ρ x + configFT s t ρ x * (configFE s t ρ x).transpose

theorem BollobasNikiforov.elimTT_eq_LTT_add_FT_FT {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) : elimTT s t ρ x = configLTT s t ρ x + configFT s t ρ x * (configFT s t ρ x).transpose

theorem BollobasNikiforov.elimEE_isUnit {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) : IsUnit (elimEE s t ρ x)

theorem BollobasNikiforov.elimEE_nonsing_inv_mul {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)⁻¹ * elimEE s t ρ x = 1

theorem BollobasNikiforov.elimEE_mul_nonsing_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 * (elimEE s t ρ x)⁻¹ = 1

theorem BollobasNikiforov.configLEE_inv_transpose {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : (configLEE s t ρ x)⁻¹.transpose = (configLEE s t ρ x)⁻¹

theorem BollobasNikiforov.configTE_elim_factor {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) (hγ : 0 < configγ s t ρ x) : configLTE s t ρ x * (configLEE s t ρ x)⁻¹ * elimEE s t ρ x + configU s t ρ x hs hρ hγ * (configFE s t ρ x).transpose = elimTE s t ρ x

theorem BollobasNikiforov.configET_elim_factor {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) (hγ : 0 < configγ s t ρ x) : elimEE s t ρ x * (configLEE s t ρ x)⁻¹ * configLET s t ρ x + configFE s t ρ x * (configU s t ρ x hs hρ hγ).transpose = elimET s t ρ x

theorem BollobasNikiforov.schur_prod_expand {ε : Type u_4} {τ : Type u_5} {κ : Type u_6} [Fintype ε] [Fintype κ] [DecidableEq ε] (Z : Matrix τ ε ℝ) (EE : Matrix ε ε ℝ) (U : Matrix τ κ ℝ) (FE : Matrix ε κ ℝ) (Z' : Matrix ε τ ℝ) (hL : EE⁻¹ * EE = 1) (hR : EE * EE⁻¹ = 1) : (Z * EE + U * FE.transpose) * EE⁻¹ * (EE * Z' + FE * U.transpose) = Z * EE * Z' + Z * FE * U.transpose + U * FE.transpose * Z' + U * FE.transpose * EE⁻¹ * FE * U.transpose

theorem BollobasNikiforov.elimSchurR_eq_woodbury {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) (hγ : 0 < configγ s t ρ x) : elimSchurR s t ρ x = configLred s t ρ x hs hρ hγ + configU s t ρ x hs hρ hγ * (1 + (configFE s t ρ x).transpose * (configLEE s t ρ x)⁻¹ * configFE s t ρ x)⁻¹ * (configU s t ρ x hs hρ hγ).transpose

SC09.

SC13 — C₁ is completely positive

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

The matrix C₁ on the right-vector indices: ρ j * (U (x j) ⬝ᵥ 𝒦 *ᵥ U (x ℓ)) * ρ ℓ, a kernel Gram matrix with parameters configQ and configγ.

Equations

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

theorem BollobasNikiforov.configC1_eq_conj {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) : configC1 s t ρ x = configU s t ρ x hs hρ hγ * (1 + (configFE s t ρ x).transpose * (configLEE s t ρ x)⁻¹ * configFE s t ρ x)⁻¹ * (configU s t ρ x hs hρ hγ).transpose

theorem BollobasNikiforov.isCompletelyPositive_mul_conj_diagonal {n : Type u_4} {C : Matrix n n ℝ} (hC : IsCompletelyPositive C) {d : n → ℝ} (hd : ∀ (i : n), 0 ≤ d i) : IsCompletelyPositive fun (i j : n) => d i * C i j * d j

theorem BollobasNikiforov.isCompletelyPositive_configC1 {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) (hγ : 0 < configγ s t ρ x) : IsCompletelyPositive (configC1 s t ρ x)

SC13. C₁ is completely positive.

theorem BollobasNikiforov.isCompletelyPositive_of_submatrix_pad {ι : Type u_4} {n : Type u_5} [Finite ι] {C : Matrix n n ℝ} {D : Matrix ι ι ℝ} {e : ι → n} (he : Function.Injective e) (hCD : ∀ (a b : ι), C (e a) (e b) = D a b) (hzero : ∀ i ∉ Set.range e, ∀ (j : n), C i j = 0) (hC : C.IsSymm) (hD : IsCompletelyPositive D) : IsCompletelyPositive C

Pad a CP matrix by zeros along the complement of an injection.

theorem BollobasNikiforov.idxY_injective_fn {k p : ℕ} : Function.Injective idxY

theorem BollobasNikiforov.extendByZeroT_isSymm {k p : ℕ} {R : Matrix (Fin p) (Fin p) ℝ} (hR : R.IsSymm) : (extendByZeroT R).IsSymm

theorem BollobasNikiforov.isCompletelyPositive_extendByZeroT {k p : ℕ} {R : Matrix (Fin p) (Fin p) ℝ} (hR : IsCompletelyPositive R) : IsCompletelyPositive (extendByZeroT R)

theorem BollobasNikiforov.isCompletelyPositive_extend_configC1 {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) (hγ : 0 < configγ s t ρ x) : IsCompletelyPositive (extendByZeroT (configC1 s t ρ x))

SC17 — assembly for γ > 0

theorem BollobasNikiforov.extendByZeroT_add {k p : ℕ} (A B : Matrix (Fin p) (Fin p) ℝ) : extendByZeroT (A + B) = extendByZeroT A + extendByZeroT B

theorem BollobasNikiforov.elimSchurR_eq_C1_add_Lred {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) (hγ : 0 < configγ s t ρ x) : elimSchurR s t ρ x = configC1 s t ρ x + configLred s t ρ x hs hρ hγ

theorem BollobasNikiforov.M_eq_elimC0_add_C1_add_Lred {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) (hγ : 0 < configγ s t ρ x) : M (Xconfig s t ρ x) = elimC0 s t ρ x + extendByZeroT (configC1 s t ρ x) + extendByZeroT (configLred s t ρ x hs hρ hγ)

SC17. M = elimC0 + extend C₁ + extend L_red.

SC18 — cor:laplacian on the assembled remainder

theorem BollobasNikiforov.idxY_lt_idxY_iff {k p : ℕ} {j ℓ : Fin p} : idxY j < idxY ℓ ↔ j < ℓ

noncomputable def BollobasNikiforov.configLredWeights {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) : ConfigIdx k p → ConfigIdx k p → ℝ

The weights -(configLred j ℓ) on pairs j < ℓ of right-vector indices, and 0 on every other pair of ConfigIdx k p.

Equations

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

theorem BollobasNikiforov.configLredWeights_y_y {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) (j ℓ : Fin p) : configLredWeights s t ρ x hs hρ hγ (idxY j) (idxY ℓ) = if j < ℓ then -configLred s t ρ x hs hρ hγ j ℓ else 0

theorem BollobasNikiforov.configLredWeights_nonneg {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) (α β : ConfigIdx k p) (hαβ : α < β) : 0 ≤ configLredWeights s t ρ x hs hρ hγ α β

theorem BollobasNikiforov.extendByZeroT_smul {k p : ℕ} (c : ℝ) (A : Matrix (Fin p) (Fin p) ℝ) : extendByZeroT (c • A) = c • extendByZeroT A

theorem BollobasNikiforov.extendByZeroT_sum {k p : ℕ} {ι : Type u_4} [Fintype ι] (f : ι → Matrix (Fin p) (Fin p) ℝ) : extendByZeroT (∑ i : ι, f i) = ∑ i : ι, extendByZeroT (f i)

theorem BollobasNikiforov.extendByZeroT_vecMulVec_sub {k p : ℕ} (j ℓ : Fin p) : extendByZeroT (Matrix.vecMulVec (e j - e ℓ) (e j - e ℓ)) = Matrix.vecMulVec (e (idxY j) - e (idxY ℓ)) (e (idxY j) - e (idxY ℓ))

theorem BollobasNikiforov.extendByZeroT_configLred_eq_sum {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) : extendByZeroT (configLred s t ρ x hs hρ hγ) = ∑ j : Fin p, ∑ ℓ : Fin p, (if j < ℓ then -configLred s t ρ x hs hρ hγ j ℓ else 0) • Matrix.vecMulVec (e (idxY j) - e (idxY ℓ)) (e (idxY j) - e (idxY ℓ))

def BollobasNikiforov.pairLeft {n : Type u_4} [DecidableEq n] (p : n → ℝ) (i j : n) : n → ℝ

Move the mass of coordinate j of p onto coordinate i: p i + p j at i, 0 at j, and p elsewhere.

Equations

• BollobasNikiforov.pairLeft p i j k = if k = i then p i + p j else if k = j then 0 else p k

def BollobasNikiforov.pairRight {n : Type u_4} [DecidableEq n] (p : n → ℝ) (i j : n) : n → ℝ

Move the mass of coordinate i of p onto coordinate j: 0 at i, p i + p j at j, and p elsewhere.

Equations

• BollobasNikiforov.pairRight p i j k = if k = i then 0 else if k = j then p i + p j else p k

theorem BollobasNikiforov.pairLeft_nonneg {n : Type u_4} [DecidableEq n] {p : n → ℝ} (hp : 0 ≤ p) (i j : n) : 0 ≤ pairLeft p i j

theorem BollobasNikiforov.pairRight_nonneg {n : Type u_4} [DecidableEq n] {p : n → ℝ} (hp : 0 ≤ p) (i j : n) : 0 ≤ pairRight p i j

theorem BollobasNikiforov.pairLeft_eq {n : Type u_4} [DecidableEq n] (p : n → ℝ) {i j : n} (hij : i ≠ j) : pairLeft p i j = p + p j • (e i - e j)

theorem BollobasNikiforov.pairRight_eq {n : Type u_4} [DecidableEq n] (p : n → ℝ) {i j : n} (hij : i ≠ j) : pairRight p i j = p - p i • (e i - e j)

theorem BollobasNikiforov.vecMulVec_add_self {n : Type u_4} (x y : n → ℝ) : Matrix.vecMulVec (x + y) (x + y) = Matrix.vecMulVec x x + Matrix.vecMulVec x y + Matrix.vecMulVec y x + Matrix.vecMulVec y y

theorem BollobasNikiforov.vecMulVec_sub_self {n : Type u_4} (x y : n → ℝ) : Matrix.vecMulVec (x - y) (x - y) = Matrix.vecMulVec x x - Matrix.vecMulVec x y - Matrix.vecMulVec y x + Matrix.vecMulVec y y

theorem BollobasNikiforov.vecMulVec_smul_self {n : Type u_4} (c : ℝ) (x : n → ℝ) : Matrix.vecMulVec (c • x) (c • x) = (c * c) • Matrix.vecMulVec x x

theorem BollobasNikiforov.rankOne_pair_identity {n : Type u_4} [DecidableEq n] {p : n → ℝ} {i j : n} (hij : i ≠ j) (hab : 0 < p i + p j) : Matrix.vecMulVec p p + (p i * p j) • Matrix.vecMulVec (e i - e j) (e i - e j) = (p i / (p i + p j)) • Matrix.vecMulVec (pairLeft p i j) (pairLeft p i j) + (p j / (p i + p j)) • Matrix.vecMulVec (pairRight p i j) (pairRight p i j)

theorem BollobasNikiforov.IsCompletelyPositive.sum {n : Type u_4} {q : ℕ} (C : Fin q → Matrix n n ℝ) (hC : ∀ (a : Fin q), IsCompletelyPositive (C a)) : IsCompletelyPositive (∑ a : Fin q, C a)

theorem BollobasNikiforov.exists_split_of_le_sum {q : ℕ} (bound : Fin q → ℝ) (h : ℝ) (h0 : 0 ≤ h) (hb : ∀ (a : Fin q), 0 ≤ bound a) (hle : h ≤ ∑ a : Fin q, bound a) : ∃ (alloc : Fin q → ℝ), (∀ (a : Fin q), 0 ≤ alloc a) ∧ (∀ (a : Fin q), alloc a ≤ bound a) ∧ ∑ a : Fin q, alloc a = h

theorem BollobasNikiforov.interpolate_pair {n : Type u_4} [DecidableEq n] {p : n → ℝ} {i j : n} {h t : ℝ} (ht : t * (p i * p j) = h) : (1 - t) • Matrix.vecMulVec p p + t • (Matrix.vecMulVec p p + (p i * p j) • Matrix.vecMulVec (e i - e j) (e i - e j)) = Matrix.vecMulVec p p + h • Matrix.vecMulVec (e i - e j) (e i - e j)

theorem BollobasNikiforov.isCompletelyPositive_vecMulVec_add_smul_sub_single {n : Type u_4} [DecidableEq n] {p : n → ℝ} (hp : 0 ≤ p) {i j : n} (hij : i ≠ j) {h : ℝ} (h0 : 0 ≤ h) (hle : h ≤ p i * p j) : IsCompletelyPositive (Matrix.vecMulVec p p + h • Matrix.vecMulVec (e i - e j) (e i - e j))

theorem BollobasNikiforov.IsCompletelyPositive.add_smul_sub_single {n : Type u_4} [DecidableEq n] {C : Matrix n n ℝ} (hC : IsCompletelyPositive C) {i j : n} (hij : i ≠ j) {h : ℝ} (h0 : 0 ≤ h) (hle : h ≤ C i j) : IsCompletelyPositive (C + h • Matrix.vecMulVec (e i - e j) (e i - e j))

theorem BollobasNikiforov.pairOffDiag {n : Type u_4} [DecidableEq n] {p q x y : n} (hpq : p ≠ q) (hxy : x ≠ y) (hpair : {p, q} ≠ {x, y}) : Matrix.vecMulVec (e p - e q) (e p - e q) x y = 0

def BollobasNikiforov.offDiagLt {n : Type u_4} [Fintype n] [LinearOrder n] : Finset (n × n)

The pairs (i, j) with i < j.

Equations

• BollobasNikiforov.offDiagLt = {p ∈ Finset.univ.offDiag | p.1 < p.2}

theorem BollobasNikiforov.mem_offDiagLt {n : Type u_4} [Fintype n] [LinearOrder n] {i j : n} : (i, j) ∈ offDiagLt ↔ i < j

theorem BollobasNikiforov.eq_of_lt_pair {n : Type u_4} [LinearOrder n] {a b c d : n} (hab : a < b) (hcd : c < d) (h : {a, b} = {c, d}) : a = c ∧ b = d

def BollobasNikiforov.weightedLaplacian {n : Type u_4} [Fintype n] [DecidableEq n] [LinearOrder n] (ℓ : n → n → ℝ) : Matrix n n ℝ

The weighted Laplacian ∑_{i < j} ℓ i j • (eᵢ - eⱼ)(eᵢ - eⱼ)ᵀ.

Equations

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

theorem BollobasNikiforov.weightedLaplacian_apply_of_lt {n : Type u_4} [Fintype n] [DecidableEq n] [LinearOrder n] (ℓ : n → n → ℝ) {i j : n} (hij : i < j) : weightedLaplacian ℓ i j = -ℓ i j

theorem BollobasNikiforov.weightedLaplacian_sum_apply_of_ne {n : Type u_4} [Fintype n] [DecidableEq n] [LinearOrder n] (s : Finset (n × n)) (hs : s ⊆ offDiagLt) (ℓ : n → n → ℝ) {i j : n} (hij : i ≠ j) (hmiss : ∀ p ∈ s, {p.1, p.2} ≠ {i, j}) : (∑ p ∈ s, ℓ p.1 p.2 • Matrix.vecMulVec (e p.1 - e p.2) (e p.1 - e p.2)) i j = 0

theorem BollobasNikiforov.isCompletelyPositive_add_sum_pairs {n : Type u_4} [Fintype n] [DecidableEq n] [LinearOrder n] {C : Matrix n n ℝ} (hC : IsCompletelyPositive C) (ℓ : n → n → ℝ) (s : Finset (n × n)) (hs : s ⊆ offDiagLt) (hℓ : ∀ p ∈ s, 0 ≤ ℓ p.1 p.2) (hslack : ∀ p ∈ s, ℓ p.1 p.2 ≤ C p.1 p.2) : IsCompletelyPositive (C + ∑ p ∈ s, ℓ p.1 p.2 • Matrix.vecMulVec (e p.1 - e p.2) (e p.1 - e p.2))

theorem BollobasNikiforov.IsCompletelyPositive.add_weightedLaplacian {n : Type u_4} [Fintype n] [DecidableEq n] [LinearOrder n] {C : Matrix n n ℝ} (hC : IsCompletelyPositive C) {ℓ : n → n → ℝ} (hℓ : ∀ (i j : n), i < j → 0 ≤ ℓ i j) (hCL : ∀ (i j : n), 0 ≤ (C + weightedLaplacian ℓ) i j) : IsCompletelyPositive (C + weightedLaplacian ℓ)

theorem BollobasNikiforov.weightedLaplacian_eq_doubleSum {n : Type u_4} [Fintype n] [DecidableEq n] [LinearOrder n] (ℓ : n → n → ℝ) : weightedLaplacian ℓ = ∑ i : n, ∑ j : n, (if i < j then ℓ i j else 0) • Matrix.vecMulVec (e i - e j) (e i - e j)

theorem BollobasNikiforov.extendByZeroT_mulVec_one {k p : ℕ} (A : Matrix (Fin p) (Fin p) ℝ) (hA : A.mulVec 1 = 0) : (extendByZeroT A).mulVec 1 = 0

theorem BollobasNikiforov.extend_configLred_offDiag {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) {α β : ConfigIdx k p} (hlt : α < β) : extendByZeroT (configLred s t ρ x hs hρ hγ) α β = -configLredWeights s t ρ x hs hρ hγ α β

theorem BollobasNikiforov.extend_configLred_eq_weightedLaplacian {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hρ : ∀ (j : Fin p), 0 < ρ j) (hγ : 0 < configγ s t ρ x) : extendByZeroT (configLred s t ρ x hs hρ hγ) = weightedLaplacian (configLredWeights s t ρ x hs hρ hγ)

theorem BollobasNikiforov.isCompletelyPositive_M_Xconfig {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) (hγ : 0 < configγ s t ρ x) : IsCompletelyPositive (M (Xconfig s t ρ x))

SC18. If γ > 0 then M(Xconfig) is completely positive.