The three-column kernel lemma

Package of the sign bounds N ≥ 1, P ≥ 0, Z ≥ 0 with the bilinear factorization of docs/sol.tex §3 (lem:kernel, eq:factor), and the resulting three-column completely positive Gram of U.

KR26: lem:kernel

theorem BollobasNikiforov.kernel_lemma {k : ℕ} (t q : Fin k → ℝ) (γ : ℝ) (hq : ∀ (i : Fin k), 0 < q i) (hγ : 0 < γ) (htmono : Monotone t) (htpos : ∀ (i : Fin k), 0 < t i) {x : ℝ} (hx : 0 ≤ x) : 1 ≤ N t q x ∧ 0 ≤ P t q x ∧ 0 ≤ Z t q γ x ∧ ∀ (y : ℝ), U t q γ x ⬝ᵥ (𝒦 t q γ).mulVec (U t q γ y) = N t q x * N t q y / (Δ t q * D2 t q) + 2 * P t q x * P t q y / (a0 t q * D2 t q) + Z t q γ x * Z t q γ y / (γ * a0 t q * (γ + a0 t q))

For x ≥ 0, the auxiliaries satisfy N ≥ 1, P ≥ 0, Z ≥ 0, and the factorization eq:factor holds.

KR27: finite Gram of U is completely positive

noncomputable def BollobasNikiforov.kernelCoeffN {k : ℕ} (t q : Fin k → ℝ) : ℝ

Coefficient of the N rank-one term in eq:factor.

Equations

• BollobasNikiforov.kernelCoeffN t q = 1 / (BollobasNikiforov.Δ t q * BollobasNikiforov.D2 t q)

noncomputable def BollobasNikiforov.kernelCoeffP {k : ℕ} (t q : Fin k → ℝ) : ℝ

Coefficient of the P rank-one term in eq:factor.

Equations

• BollobasNikiforov.kernelCoeffP t q = 2 / (BollobasNikiforov.a0 t q * BollobasNikiforov.D2 t q)

noncomputable def BollobasNikiforov.kernelCoeffZ {k : ℕ} (t q : Fin k → ℝ) (γ : ℝ) : ℝ

Coefficient of the Z rank-one term in eq:factor.

Equations

• BollobasNikiforov.kernelCoeffZ t q γ = 1 / (γ * BollobasNikiforov.a0 t q * (γ + BollobasNikiforov.a0 t q))

theorem BollobasNikiforov.kernelCoeffN_nonneg {k : ℕ} (t q : Fin k → ℝ) (hq : ∀ (i : Fin k), 0 < q i) : 0 ≤ kernelCoeffN t q

theorem BollobasNikiforov.kernelCoeffP_nonneg {k : ℕ} (t q : Fin k → ℝ) (hq : ∀ (i : Fin k), 0 < q i) : 0 ≤ kernelCoeffP t q

theorem BollobasNikiforov.kernelCoeffZ_nonneg {k : ℕ} (t q : Fin k → ℝ) (γ : ℝ) (hq : ∀ (i : Fin k), 0 < q i) (hγ : 0 < γ) : 0 ≤ kernelCoeffZ t q γ

theorem BollobasNikiforov.kernel_gram_eq {k : ℕ} (t q : Fin k → ℝ) {κ : Type u_1} (γ : ℝ) (hq : ∀ (i : Fin k), 0 < q i) (hγ : 0 < γ) (x : κ → ℝ) : (fun (j ℓ : κ) => U t q γ (x j) ⬝ᵥ (𝒦 t q γ).mulVec (U t q γ (x ℓ))) = ((kernelCoeffN t q • Matrix.vecMulVec (fun (j : κ) => N t q (x j)) fun (j : κ) => N t q (x j)) + kernelCoeffP t q • Matrix.vecMulVec (fun (j : κ) => P t q (x j)) fun (j : κ) => P t q (x j)) + kernelCoeffZ t q γ • Matrix.vecMulVec (fun (j : κ) => Z t q γ (x j)) fun (j : κ) => Z t q γ (x j)

theorem BollobasNikiforov.kernel_gram_isCompletelyPositive {k : ℕ} (t q : Fin k → ℝ) {κ : Type u_1} (γ : ℝ) (hq : ∀ (i : Fin k), 0 < q i) (hγ : 0 < γ) (htmono : Monotone t) (htpos : ∀ (i : Fin k), 0 < t i) (x : κ → ℝ) (hx : ∀ (j : κ), 0 ≤ x j) : IsCompletelyPositive fun (j ℓ : κ) => U t q γ (x j) ⬝ᵥ (𝒦 t q γ).mulVec (U t q γ (x ℓ))