Nonnegativity of N

The identity N = det(I + Q W) of docs/sol.tex §3, the factorization of W through two totally nonnegative three-column matrices, and 1 ≤ N x for x ≥ 0.

KR18: auxiliary matrix D(x)

def BollobasNikiforov.fromThreeCols (c0 c1 c2 : Fin 3 → ℝ) : Matrix (Fin 3) (Fin 3) ℝ

The matrix with columns c₀, c₁, c₂.

Equations

• BollobasNikiforov.fromThreeCols c0 c1 c2 i j = if j = 0 then c0 i else if j = 1 then c1 i else c2 i

theorem BollobasNikiforov.fromThreeCols_apply_zero (c0 c1 c2 : Fin 3 → ℝ) (i : Fin 3) : fromThreeCols c0 c1 c2 i 0 = c0 i

theorem BollobasNikiforov.fromThreeCols_apply_one (c0 c1 c2 : Fin 3 → ℝ) (i : Fin 3) : fromThreeCols c0 c1 c2 i 1 = c1 i

theorem BollobasNikiforov.fromThreeCols_apply_two (c0 c1 c2 : Fin 3 → ℝ) (i : Fin 3) : fromThreeCols c0 c1 c2 i 2 = c2 i

theorem BollobasNikiforov.fromThreeCols_add (u0 u1 u2 v0 v1 v2 : Fin 3 → ℝ) : fromThreeCols (u0 + v0) (u1 + v1) (u2 + v2) = fromThreeCols u0 u1 u2 + fromThreeCols v0 v1 v2

theorem BollobasNikiforov.fromThreeCols_smul (c : ℝ) (u0 u1 u2 : Fin 3 → ℝ) : fromThreeCols (c • u0) (c • u1) (c • u2) = c • fromThreeCols u0 u1 u2

theorem BollobasNikiforov.fromThreeCols_sum {ι : Type u_1} (s : Finset ι) (f0 f1 f2 : ι → Fin 3 → ℝ) : fromThreeCols (∑ i ∈ s, f0 i) (∑ i ∈ s, f1 i) (∑ i ∈ s, f2 i) = ∑ i ∈ s, fromThreeCols (f0 i) (f1 i) (f2 i)

noncomputable def BollobasNikiforov.D (x : ℝ) : Matrix (Fin 3) (Fin 3) ℝ

D(x) has columns e₀, e₁, b(x).

Equations

• BollobasNikiforov.D x = BollobasNikiforov.fromThreeCols (Pi.single 0 1) (Pi.single 1 1) (BollobasNikiforov.b x)

theorem BollobasNikiforov.det_D (x : ℝ) : (D x).det = 1

theorem BollobasNikiforov.D_isUnit (x : ℝ) : IsUnit (D x).det

noncomputable def BollobasNikiforov.Dinv (x : ℝ) : Matrix (Fin 3) (Fin 3) ℝ

Explicit inverse of the upper-triangular unipotent matrix D x.

Equations

• BollobasNikiforov.Dinv x = !![1, 0, -x ^ 2; 0, 1, -√2 * x; 0, 0, 1]

theorem BollobasNikiforov.D_mul_Dinv (x : ℝ) : D x * Dinv x = 1

theorem BollobasNikiforov.D_inv (x : ℝ) : (D x)⁻¹ = Dinv x

Feature columns cᵢ(x)

noncomputable def BollobasNikiforov.cVec (ti x : ℝ) : Fin 3 → ℝ

cᵢ(x) = (1, -√2 tᵢ, aᵢ(x))ᵀ.

Equations

• BollobasNikiforov.cVec ti x = ![1, -√2 * ti, BollobasNikiforov.truncSq ti x]

@[simp]

theorem BollobasNikiforov.cVec_zero (ti x : ℝ) : cVec ti x 0 = 1

@[simp]

theorem BollobasNikiforov.cVec_one (ti x : ℝ) : cVec ti x 1 = -√2 * ti

@[simp]

theorem BollobasNikiforov.cVec_two (ti x : ℝ) : cVec ti x 2 = truncSq ti x

theorem BollobasNikiforov.vecMulVec_eq_fromThreeCols (u v : Fin 3 → ℝ) : Matrix.vecMulVec u v = fromThreeCols (v 0 • u) (v 1 • u) (v 2 • u)

KR19: Cramer for N

theorem BollobasNikiforov.updateCol_two_eq_fromThreeCols (A : Matrix (Fin 3) (Fin 3) ℝ) (w : Fin 3 → ℝ) : A.updateCol 2 w = fromThreeCols (A.mulVec (Pi.single 0 1)) (A.mulVec (Pi.single 1 1)) w

theorem BollobasNikiforov.N_eq_det_fromThreeCols {k : ℕ} (t q : Fin k → ℝ) (hq : ∀ (i : Fin k), 0 < q i) (x : ℝ) : N t q x = (fromThreeCols ((𝒜 t q).mulVec (Pi.single 0 1)) ((𝒜 t q).mulVec (Pi.single 1 1)) (bhat t q x)).det

theorem BollobasNikiforov.𝒜_mulVec_single_zero {k : ℕ} (t q : Fin k → ℝ) : (𝒜 t q).mulVec (Pi.single 0 1) = Pi.single 0 1 + ∑ i : Fin k, q i • v (t i)

theorem BollobasNikiforov.𝒜_mulVec_single_one {k : ℕ} (t q : Fin k → ℝ) : (𝒜 t q).mulVec (Pi.single 1 1) = Pi.single 1 1 + ∑ i : Fin k, (q i * (-√2 * t i)) • v (t i)

theorem BollobasNikiforov.fromThreeCols_eq_D_add_sum {k : ℕ} (t q : Fin k → ℝ) (x : ℝ) : fromThreeCols ((𝒜 t q).mulVec (Pi.single 0 1)) ((𝒜 t q).mulVec (Pi.single 1 1)) (bhat t q x) = D x + ∑ i : Fin k, q i • Matrix.vecMulVec (v (t i)) (cVec (t i) x)

KR20: Sylvester N = det(I + Q W)

noncomputable def BollobasNikiforov.vCols {k : ℕ} (t : Fin k → ℝ) : Matrix (Fin 3) (Fin k) ℝ

Columns are the feature vectors v(tⱼ).

Equations

• BollobasNikiforov.vCols t r j = BollobasNikiforov.v (t j) r

noncomputable def BollobasNikiforov.qcRows {k : ℕ} (t q : Fin k → ℝ) (x : ℝ) : Matrix (Fin k) (Fin 3) ℝ

Rows are qᵢ cᵢ(x)ᵀ.

Equations

• BollobasNikiforov.qcRows t q x i s = q i * BollobasNikiforov.cVec (t i) x s

noncomputable def BollobasNikiforov.W {k : ℕ} (t : Fin k → ℝ) (x : ℝ) : Matrix (Fin k) (Fin k) ℝ

W(x)ᵢⱼ = cᵢ(x)ᵀ D(x)⁻¹ v(tⱼ).

Equations

• BollobasNikiforov.W t x i j = BollobasNikiforov.cVec (t i) x ⬝ᵥ (BollobasNikiforov.D x)⁻¹.mulVec (BollobasNikiforov.v (t j))

theorem BollobasNikiforov.vCols_mul_qcRows {k : ℕ} (t q : Fin k → ℝ) (x : ℝ) : vCols t * qcRows t q x = ∑ i : Fin k, q i • Matrix.vecMulVec (v (t i)) (cVec (t i) x)

theorem BollobasNikiforov.qcRows_mul_invD_vCols {k : ℕ} (t q : Fin k → ℝ) (x : ℝ) : qcRows t q x * (D x)⁻¹ * vCols t = Matrix.diagonal q * W t x

theorem BollobasNikiforov.N_eq_det_one_add {k : ℕ} (t q : Fin k → ℝ) (hq : ∀ (i : Fin k), 0 < q i) (x : ℝ) : N t q x = (1 + Matrix.diagonal q * W t x).det

KR21: formula for W

def BollobasNikiforov.fKernel (x t : ℝ) : ℝ

Paper f_x(t) = t² - (t-x)₊².

Equations

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

theorem BollobasNikiforov.fKernel_eq_sq {x t : ℝ} (htx : t ≤ x) : fKernel x t = t ^ 2

theorem BollobasNikiforov.fKernel_eq_linear {x t : ℝ} (hxt : x ≤ t) : fKernel x t = 2 * x * t - x ^ 2

theorem BollobasNikiforov.fKernel_eq_trunc (ti x : ℝ) : fKernel x ti = 2 * ti * x - x ^ 2 + truncSq ti x

theorem BollobasNikiforov.Dinv_mulVec_v (x tj : ℝ) : (Dinv x).mulVec (v tj) = ![1 - x ^ 2 * tj ^ 2, -√2 * tj - √2 * x * tj ^ 2, tj ^ 2]

theorem BollobasNikiforov.W_apply {k : ℕ} (t : Fin k → ℝ) (x : ℝ) (i j : Fin k) : W t x i j = 1 + 2 * t i * t j + fKernel x (t i) * t j ^ 2

KR22: convexity of fKernel x

theorem BollobasNikiforov.fKernel_zero {x : ℝ} (hx : 0 ≤ x) : fKernel x 0 = 0

theorem BollobasNikiforov.fKernel_nonneg {x t : ℝ} (hx : 0 ≤ x) (ht : 0 ≤ t) : 0 ≤ fKernel x t

theorem BollobasNikiforov.fKernel_convexOn (x : ℝ) : ConvexOn ℝ (Set.Ici 0) (fKernel x)

KR23: two 3-column TN matrices

theorem BollobasNikiforov.IsTotallyNonneg.mul_diagonal {ι : Type u_1} {κ : Type u_2} [LinearOrder ι] [LinearOrder κ] [Fintype κ] [DecidableEq κ] {A : Matrix ι κ ℝ} (hA : IsTotallyNonneg A) {d : κ → ℝ} (hd : ∀ (j : κ), 0 ≤ d j) : IsTotallyNonneg (A * Matrix.diagonal d)

def BollobasNikiforov.fKernelRows {k : ℕ} (t : Fin k → ℝ) (x : ℝ) : Matrix (Fin k) (Fin 3) ℝ

Rows (1, tᵢ, fₓ(tᵢ)).

Equations

• BollobasNikiforov.fKernelRows t x = BollobasNikiforov.convexRowMatrix (BollobasNikiforov.fKernel x) t

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

Rows (1, 2 tᵢ, tᵢ²).

Equations

• BollobasNikiforov.sqRows t i j = ![1, 2 * t i, t i ^ 2] j

theorem BollobasNikiforov.isTotallyNonneg_fKernelRows {k : ℕ} (t : Fin k → ℝ) (x : ℝ) (hx : 0 ≤ x) (htmono : Monotone t) (htpos : ∀ (i : Fin k), 0 < t i) : IsTotallyNonneg (fKernelRows t x)

theorem BollobasNikiforov.sqRows_eq_scale {k : ℕ} (t : Fin k → ℝ) : sqRows t = convexRowMatrix (fun (s : ℝ) => s ^ 2) t * Matrix.diagonal ![1, 2, 1]

theorem BollobasNikiforov.isTotallyNonneg_sqRows {k : ℕ} (t : Fin k → ℝ) (htmono : Monotone t) (htpos : ∀ (i : Fin k), 0 < t i) : IsTotallyNonneg (sqRows t)

KR24: W is TN

theorem BollobasNikiforov.W_eq_mul_transpose {k : ℕ} (t : Fin k → ℝ) (x : ℝ) : W t x = fKernelRows t x * (sqRows t).transpose

theorem BollobasNikiforov.W_isTotallyNonneg {k : ℕ} (t : Fin k → ℝ) (x : ℝ) (hx : 0 ≤ x) (htmono : Monotone t) (htpos : ∀ (i : Fin k), 0 < t i) : IsTotallyNonneg (W t x)

KR25: 1 ≤ N

theorem BollobasNikiforov.det_one_add_diagonal_mul {n : Type u_1} [Fintype n] [DecidableEq n] (d : n → ℝ) (M : Matrix n n ℝ) : (1 + Matrix.diagonal d * M).det = ∑ s : Finset n, (∏ i ∈ s, d i) * (M.submatrix Subtype.val Subtype.val).det

theorem BollobasNikiforov.IsTotallyNonneg.det_principal {n : Type u_1} [LinearOrder n] {A : Matrix n n ℝ} (hA : IsTotallyNonneg A) (s : Finset n) : 0 ≤ (A.submatrix Subtype.val Subtype.val).det

theorem BollobasNikiforov.N_ge_one {k : ℕ} (t q : Fin k → ℝ) (x : ℝ) (hq : ∀ (i : Fin k), 0 < q i) (hx : 0 ≤ x) (htmono : Monotone t) (htpos : ∀ (i : Fin k), 0 < t i) : 1 ≤ N t q x