Planar configuration and block entries of M

The normalized configuration of docs/sol.tex §4 (eq:coordinates, eq:blocks): z₀ = (1,0), zᵢ = √sᵢ (-1, tᵢ), yⱼ = √ρⱼ (xⱼ, 1).

Indices are identified with Option (Fin k) ⊕ Fin p via configIdxEquiv: none is z₀, some i is zᵢ, and Sum.inr j is yⱼ. The carrier is Fin (k + 1 + p), which supplies LinearOrder for M.

@[reducible, inline]

abbrev BollobasNikiforov.ConfigIdx (k p : ℕ) : Type

Index type identified with Option (Fin k) ⊕ Fin p: 0 is z₀, 1..k are the zᵢ, and k+1.. are the yⱼ.

Equations

• BollobasNikiforov.ConfigIdx k p = Fin (k + 1 + p)

def BollobasNikiforov.configIdxEquiv (k p : ℕ) : ConfigIdx k p ≃ Option (Fin k) ⊕ Fin p

none = z₀, some i = zᵢ, inr j = yⱼ.

Equations

• BollobasNikiforov.configIdxEquiv k p = finSumFinEquiv.symm.trans ((finSuccEquiv k).sumCongr (Equiv.refl (Fin p)))

def BollobasNikiforov.idxZ0 {k p : ℕ} : ConfigIdx k p

The z₀ index (none).

Equations

• BollobasNikiforov.idxZ0 = (BollobasNikiforov.configIdxEquiv k p).symm (Sum.inl none)

def BollobasNikiforov.idxZ {k p : ℕ} (i : Fin k) : ConfigIdx k p

The zᵢ index (some i).

Equations

• BollobasNikiforov.idxZ i = (BollobasNikiforov.configIdxEquiv k p).symm (Sum.inl (some i))

def BollobasNikiforov.idxY {k p : ℕ} (j : Fin p) : ConfigIdx k p

The yⱼ index.

Equations

• BollobasNikiforov.idxY j = (BollobasNikiforov.configIdxEquiv k p).symm (Sum.inr j)

theorem BollobasNikiforov.idxZ0_eq {k p : ℕ} : idxZ0 = 0

theorem BollobasNikiforov.idxZ_val {k p : ℕ} (i : Fin k) : ↑(idxZ i) = ↑i + 1

theorem BollobasNikiforov.idxY_val {k p : ℕ} (j : Fin p) : ↑(idxY j) = k + 1 + ↑j

theorem BollobasNikiforov.idxZ0_lt_idxZ {k p : ℕ} (i : Fin k) : idxZ0 < idxZ i

theorem BollobasNikiforov.idxZ0_lt_idxY {k p : ℕ} (j : Fin p) : idxZ0 < idxY j

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

theorem BollobasNikiforov.idxZ_lt_idxZ_iff {k p : ℕ} {i h : Fin k} : idxZ i < idxZ h ↔ i < h

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

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

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

theorem BollobasNikiforov.not_lt_idxZ0 {k p : ℕ} (α : ConfigIdx k p) : ¬α < idxZ0

theorem BollobasNikiforov.sum_configIdx {k p : ℕ} (f : ConfigIdx k p → ℝ) : ∑ α : ConfigIdx k p, f α = f idxZ0 + ∑ i : Fin k, f (idxZ i) + ∑ j : Fin p, f (idxY j)

MX06 — configuration vectors and Gram matrix

def BollobasNikiforov.z0 : Fin 2 → ℝ

Feature vector z₀ = (1, 0).

Equations

• BollobasNikiforov.z0 = ![1, 0]

noncomputable def BollobasNikiforov.zVec {k : ℕ} (s t : Fin k → ℝ) (i : Fin k) : Fin 2 → ℝ

Feature vector zᵢ = √sᵢ (-1, tᵢ).

Equations

• BollobasNikiforov.zVec s t i = ![-√(s i), √(s i) * t i]

noncomputable def BollobasNikiforov.yVec {p : ℕ} (ρ x : Fin p → ℝ) (j : Fin p) : Fin 2 → ℝ

Feature vector yⱼ = √ρⱼ (xⱼ, 1).

Equations

• BollobasNikiforov.yVec ρ x j = ![√(ρ j) * x j, √(ρ j)]

@[simp]

theorem BollobasNikiforov.z0_zero : z0 0 = 1

@[simp]

theorem BollobasNikiforov.z0_one : z0 1 = 0

@[simp]

theorem BollobasNikiforov.zVec_zero {k : ℕ} (s t : Fin k → ℝ) (i : Fin k) : zVec s t i 0 = -√(s i)

@[simp]

theorem BollobasNikiforov.zVec_one {k : ℕ} (s t : Fin k → ℝ) (i : Fin k) : zVec s t i 1 = √(s i) * t i

@[simp]

theorem BollobasNikiforov.yVec_zero {p : ℕ} (ρ x : Fin p → ℝ) (j : Fin p) : yVec ρ x j 0 = √(ρ j) * x j

@[simp]

theorem BollobasNikiforov.yVec_one {p : ℕ} (ρ x : Fin p → ℝ) (j : Fin p) : yVec ρ x j 1 = √(ρ j)

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

The assembled configuration on ConfigIdx.

Equations

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

theorem BollobasNikiforov.configVec_z0 {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : configVec s t ρ x idxZ0 = z0

theorem BollobasNikiforov.configVec_z {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i : Fin k) : configVec s t ρ x (idxZ i) = zVec s t i

theorem BollobasNikiforov.configVec_y {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (j : Fin p) : configVec s t ρ x (idxY j) = yVec ρ x j

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

Rows of the configuration, as a ι × 2 matrix.

Equations

• BollobasNikiforov.configMat s t ρ x α c = BollobasNikiforov.configVec s t ρ x α c

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

Gram matrix of the configuration.

Equations

• BollobasNikiforov.Xconfig s t ρ x a b = BollobasNikiforov.configVec s t ρ x a ⬝ᵥ BollobasNikiforov.configVec s t ρ x b

theorem BollobasNikiforov.Xconfig_apply {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (a b : ConfigIdx k p) : Xconfig s t ρ x a b = configVec s t ρ x a ⬝ᵥ configVec s t ρ x b

theorem BollobasNikiforov.Xconfig_eq_mul_transpose {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : Xconfig s t ρ x = configMat s t ρ x * (configMat s t ρ x).transpose

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

theorem BollobasNikiforov.Xconfig_posSemidef {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : (Xconfig s t ρ x).PosSemidef

Inner products of configuration vectors

theorem BollobasNikiforov.z0_dot_z0 : z0 ⬝ᵥ z0 = 1

theorem BollobasNikiforov.z0_dot_zVec {k : ℕ} (s t : Fin k → ℝ) (i : Fin k) : z0 ⬝ᵥ zVec s t i = -√(s i)

theorem BollobasNikiforov.z0_dot_yVec {p : ℕ} (ρ x : Fin p → ℝ) (j : Fin p) : z0 ⬝ᵥ yVec ρ x j = √(ρ j) * x j

theorem BollobasNikiforov.zVec_dot_zVec {k : ℕ} (s t : Fin k → ℝ) (i h : Fin k) : zVec s t i ⬝ᵥ zVec s t h = √(s i) * √(s h) * (1 + t i * t h)

theorem BollobasNikiforov.zVec_dot_yVec {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i : Fin k) (j : Fin p) : zVec s t i ⬝ᵥ yVec ρ x j = √(s i) * √(ρ j) * (t i - x j)

theorem BollobasNikiforov.Xconfig_z0_z0 {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) : Xconfig s t ρ x idxZ0 idxZ0 = 1

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

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

theorem BollobasNikiforov.Xconfig_z_z {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (i h : Fin k) : Xconfig s t ρ x (idxZ i) (idxZ h) = √(s i) * √(s h) * (1 + t i * t h)

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

MX07 — auxiliary scalars

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

Hᵢ = ∑ⱼ ρⱼ (xⱼ - tᵢ)₊².

Equations

• BollobasNikiforov.configH t ρ x i = ∑ j : Fin p, ρ j * max (x j - t i) 0 ^ 2

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

dᵢ = 1 + Hᵢ.

Equations

• BollobasNikiforov.configD t ρ x i = 1 + BollobasNikiforov.configH t ρ x i

def BollobasNikiforov.configσ {k : ℕ} (s : Fin k → ℝ) : ℝ

σ = ∑ᵢ sᵢ.

Equations

• BollobasNikiforov.configσ s = ∑ i : Fin k, s i

theorem BollobasNikiforov.configH_nonneg {k p : ℕ} (t : Fin k → ℝ) {ρ : Fin p → ℝ} (hρ : ∀ (j : Fin p), 0 < ρ j) (x : Fin p → ℝ) (i : Fin k) : 0 ≤ configH t ρ x i

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

theorem BollobasNikiforov.configσ_nonneg {k : ℕ} {s : Fin k → ℝ} (hs : ∀ (i : Fin k), 0 < s i) : 0 ≤ configσ s

Diagonal expansion of M

theorem BollobasNikiforov.vecMulVec_sub_single_diag {n : Type u_1} [DecidableEq n] (u v a : n) : Matrix.vecMulVec (e u - e v) (e u - e v) a a = if u = v then 0 else if a = u ∨ a = v then 1 else 0

theorem BollobasNikiforov.M_diag {n : Type u_1} [Fintype n] [DecidableEq n] [LinearOrder n] (X : Matrix n n ℝ) (a : n) : M X a a = (X a a ^ 2 + ∑ q : n, if a < q ∧ X a q < 0 then X a q ^ 2 else 0) + ∑ u : n, if u < a ∧ X u a < 0 then X u a ^ 2 else 0

MX08 — block entries

theorem BollobasNikiforov.Xconfig_z0_z_neg {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (i : Fin k) : Xconfig s t ρ x idxZ0 (idxZ i) < 0

theorem BollobasNikiforov.Xconfig_z0_y_nonneg {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hx : ∀ (j : Fin p), 0 ≤ x j) (j : Fin p) : 0 ≤ Xconfig s t ρ x idxZ0 (idxY j)

theorem BollobasNikiforov.Xconfig_z_z_pos {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (ht : ∀ (i : Fin k), 0 < t i) (i h : Fin k) : 0 < Xconfig s t ρ x (idxZ i) (idxZ h)

theorem BollobasNikiforov.MX_z0_z0 {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hx : ∀ (j : Fin p), 0 ≤ x j) : M (Xconfig s t ρ x) idxZ0 idxZ0 = 1 + configσ s

M_{00} = 1 + σ.

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

M_{0i} = 0.

theorem BollobasNikiforov.MX_z0_y {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) : M (Xconfig s t ρ x) idxZ0 (idxY j) = ρ j * x j ^ 2

M_{0ybar} = ρⱼ xⱼ².

theorem BollobasNikiforov.MX_z_z_of_ne {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (ht : ∀ (i : Fin k), 0 < t i) {i h : Fin k} (hih : i ≠ h) : M (Xconfig s t ρ x) (idxZ i) (idxZ h) = s i * s h * (1 + t i * t h) ^ 2

Off-diagonal z-block: M_{ih} = sᵢ sₕ (1 + tᵢ tₕ)² for i ≠ h.

theorem BollobasNikiforov.MX_z_y {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) (idxZ i) (idxY j) = s i * ρ j * max (t i - x j) 0 ^ 2

M_{iybar} = sᵢ ρⱼ (tᵢ - xⱼ)₊².

theorem BollobasNikiforov.MX_z_z_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) (i : Fin k) : M (Xconfig s t ρ x) (idxZ i) (idxZ i) = s i * s i * (1 + t i * t i) ^ 2 + s i * configD t ρ x i

Diagonal z-block: M_{ii} = sᵢ² (1 + tᵢ²)² + sᵢ dᵢ.

theorem BollobasNikiforov.MX_z_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) (i h : Fin k) : M (Xconfig s t ρ x) (idxZ i) (idxZ h) = s i * s h * (1 + t i * t h) ^ 2 + if i = h then s i * configD t ρ x i else 0

Combined z-block formula, including the Kronecker term.

MX09 — first column

theorem BollobasNikiforov.MX_z0_z0_pos {k p : ℕ} (s t : Fin k → ℝ) (ρ x : Fin p → ℝ) (hs : ∀ (i : Fin k), 0 < s i) (hx : ∀ (j : Fin p), 0 ≤ x j) : 0 < M (Xconfig s t ρ x) idxZ0 idxZ0

theorem BollobasNikiforov.MX_z0_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 ≤ M (Xconfig s t ρ x) idxZ0 α