Bilinear expansion of 𝒦

Completing squares in coordinates 2,1,0 yields eq:bilinear, and substituting U yields the factorization eq:factor of docs/sol.tex §3.

Fin 3 expansions

theorem BollobasNikiforov.mulVec_fin3 (M : Matrix (Fin 3) (Fin 3) ℝ) (z : Fin 3 → ℝ) (i : Fin 3) : M.mulVec z i = M i 0 * z 0 + M i 1 * z 1 + M i 2 * z 2

theorem BollobasNikiforov.dotProduct_mulVec_fin3 (M : Matrix (Fin 3) (Fin 3) ℝ) (z w : Fin 3 → ℝ) : z ⬝ᵥ M.mulVec w = z 0 * (M 0 0 * w 0 + M 0 1 * w 1 + M 0 2 * w 2) + z 1 * (M 1 0 * w 0 + M 1 1 * w 1 + M 1 2 * w 2) + z 2 * (M 2 0 * w 0 + M 2 1 * w 1 + M 2 2 * w 2)

theorem BollobasNikiforov.bilinear_complete_last (M : Matrix (Fin 3) (Fin 3) ℝ) (hM : M.IsHermitian) (z w : Fin 3 → ℝ) (h22 : M 2 2 ≠ 0) : z ⬝ᵥ M.mulVec w = M.mulVec z 2 * M.mulVec w 2 / M 2 2 + z 0 * w 0 * (M 0 0 - M 0 2 * M 2 0 / M 2 2) + z 0 * w 1 * (M 0 1 - M 0 2 * M 2 1 / M 2 2) + z 1 * w 0 * (M 1 0 - M 1 2 * M 2 0 / M 2 2) + z 1 * w 1 * (M 1 1 - M 1 2 * M 2 1 / M 2 2)

Completing the square in coordinate 2 for a real symmetric 3×3 form.

KR08: pivot 𝒦 2 2

theorem BollobasNikiforov.inv_𝒜_two_two {k : ℕ} (t q : Fin k → ℝ) (hq : ∀ (i : Fin k), 0 < q i) : (𝒜 t q)⁻¹ 2 2 = D2 t q / Δ t q

theorem BollobasNikiforov.𝒦_two_two {k : ℕ} (t q : Fin k → ℝ) (γ : ℝ) (hq : ∀ (i : Fin k), 0 < q i) (hγ : 0 < γ) : 𝒦 t q γ 2 2 = D2 t q / Δ t q

Leading 2×2 block of 𝒜

theorem BollobasNikiforov.leading2_𝒜_inv_one_one {k : ℕ} (t q : Fin k → ℝ) (hq : ∀ (i : Fin k), 0 < q i) : ((𝒜 t q).submatrix Fin.castSucc Fin.castSucc)⁻¹ 1 1 = a0 t q / D2 t q

theorem BollobasNikiforov.leading2_𝒜_inv_one_zero {k : ℕ} (t q : Fin k → ℝ) (hq : ∀ (i : Fin k), 0 < q i) : ((𝒜 t q).submatrix Fin.castSucc Fin.castSucc)⁻¹ 1 0 = √2 * m t q 1 / D2 t q

theorem BollobasNikiforov.leading2_mul_schur_inv_𝒜 {k : ℕ} (t q : Fin k → ℝ) (hq : ∀ (i : Fin k), 0 < q i) : ((𝒜 t q).submatrix Fin.castSucc Fin.castSucc * Matrix.of fun (i j : Fin 2) => (𝒜 t q)⁻¹ i.castSucc j.castSucc - (𝒜 t q)⁻¹ i.castSucc 2 * (𝒜 t q)⁻¹ 2 j.castSucc / (𝒜 t q)⁻¹ 2 2) = 1

The {0,1} Schur complement of 𝒜⁻¹ is (𝒜[{0,1}])⁻¹.

theorem BollobasNikiforov.schur_inv_𝒜 {k : ℕ} (t q : Fin k → ℝ) (hq : ∀ (i : Fin k), 0 < q i) (i j : Fin 2) : (𝒜 t q)⁻¹ i.castSucc j.castSucc - (𝒜 t q)⁻¹ i.castSucc 2 * (𝒜 t q)⁻¹ 2 j.castSucc / (𝒜 t q)⁻¹ 2 2 = ((𝒜 t q).submatrix Fin.castSucc Fin.castSucc)⁻¹ i j

KR09: {0,1} block of 𝒦⁻¹ = 𝒦Mat

theorem BollobasNikiforov.Vvec_one {k : ℕ} (t q : Fin k → ℝ) : Vvec t q 1 = -√2 * m t q 1

theorem BollobasNikiforov.𝒦Mat_zero_zero {k : ℕ} (t q : Fin k → ℝ) (γ : ℝ) (hγ : 0 < γ) : 𝒦Mat t q γ 0 0 = a0 t q * (γ + a0 t q) / γ

theorem BollobasNikiforov.𝒦Mat_one_zero {k : ℕ} (t q : Fin k → ℝ) (γ : ℝ) (hγ : 0 < γ) : 𝒦Mat t q γ 1 0 = -√2 * m t q 1 * (γ + a0 t q) / γ

theorem BollobasNikiforov.𝒦Mat_zero_one {k : ℕ} (t q : Fin k → ℝ) (γ : ℝ) (hγ : 0 < γ) : 𝒦Mat t q γ 0 1 = -√2 * m t q 1 * (γ + a0 t q) / γ

theorem BollobasNikiforov.𝒦Mat_one_one {k : ℕ} (t q : Fin k → ℝ) (γ : ℝ) (hγ : 0 < γ) : 𝒦Mat t q γ 1 1 = 1 + 2 * m t q 2 + 2 * m t q 1 ^ 2 / γ

theorem BollobasNikiforov.𝒦Mat01_det {k : ℕ} (t q : Fin k → ℝ) (γ : ℝ) (_hq : ∀ (i : Fin k), 0 < q i) (hγ : 0 < γ) : ((𝒦Mat t q γ).submatrix Fin.castSucc Fin.castSucc).det = D2 t q * (γ + a0 t q) / γ

theorem BollobasNikiforov.𝒦Mat01_inv_one_one {k : ℕ} (t q : Fin k → ℝ) (γ : ℝ) (hq : ∀ (i : Fin k), 0 < q i) (hγ : 0 < γ) : ((𝒦Mat t q γ).submatrix Fin.castSucc Fin.castSucc)⁻¹ 1 1 = a0 t q / D2 t q

theorem BollobasNikiforov.𝒦Mat01_inv_one_zero {k : ℕ} (t q : Fin k → ℝ) (γ : ℝ) (hq : ∀ (i : Fin k), 0 < q i) (hγ : 0 < γ) : ((𝒦Mat t q γ).submatrix Fin.castSucc Fin.castSucc)⁻¹ 1 0 = √2 * m t q 1 / D2 t q

theorem BollobasNikiforov.𝒦Mat01_inv_ratio {k : ℕ} (t q : Fin k → ℝ) (γ : ℝ) (hq : ∀ (i : Fin k), 0 < q i) (hγ : 0 < γ) : ((𝒦Mat t q γ).submatrix Fin.castSucc Fin.castSucc)⁻¹ 1 0 / ((𝒦Mat t q γ).submatrix Fin.castSucc Fin.castSucc)⁻¹ 1 1 = √2 * m t q 1 / a0 t q

KR10: last pivot

theorem BollobasNikiforov.inv_𝒦Mat_zero_zero {k : ℕ} (t q : Fin k → ℝ) (γ : ℝ) (hq : ∀ (i : Fin k), 0 < q i) (hγ : 0 < γ) : 1 / 𝒦Mat t q γ 0 0 = γ / (a0 t q * (γ + a0 t q))

Inverse bilinear form of 𝒜

theorem BollobasNikiforov.inv_𝒜_isHermitian {k : ℕ} (t q : Fin k → ℝ) (hq : ∀ (i : Fin k), 0 < q i) : (𝒜 t q)⁻¹.IsHermitian

theorem BollobasNikiforov.leading2_inv_bilinear {k : ℕ} (t q : Fin k → ℝ) (hq : ∀ (i : Fin k), 0 < q i) (z0 z1 w0 w1 : ℝ) : z0 * w0 * ((𝒜 t q).submatrix Fin.castSucc Fin.castSucc)⁻¹ 0 0 + z0 * w1 * ((𝒜 t q).submatrix Fin.castSucc Fin.castSucc)⁻¹ 0 1 + z1 * w0 * ((𝒜 t q).submatrix Fin.castSucc Fin.castSucc)⁻¹ 1 0 + z1 * w1 * ((𝒜 t q).submatrix Fin.castSucc Fin.castSucc)⁻¹ 1 1 = (a0 t q * z1 + √2 * m t q 1 * z0) * (a0 t q * w1 + √2 * m t q 1 * w0) / (a0 t q * D2 t q) + z0 * w0 / a0 t q

theorem BollobasNikiforov.dotProduct_inv_𝒜 {k : ℕ} (t q : Fin k → ℝ) (hq : ∀ (i : Fin k), 0 < q i) (z w : Fin 3 → ℝ) : z ⬝ᵥ (𝒜 t q)⁻¹.mulVec w = Δ t q * (𝒜 t q)⁻¹.mulVec z 2 * (Δ t q * (𝒜 t q)⁻¹.mulVec w 2) / (Δ t q * D2 t q) + (a0 t q * z 1 + √2 * m t q 1 * z 0) * (a0 t q * w 1 + √2 * m t q 1 * w 0) / (a0 t q * D2 t q) + z 0 * w 0 / a0 t q

KR11: eq:bilinear

theorem BollobasNikiforov.dotProduct_𝒦_eq_inv_𝒜 {k : ℕ} (t q : Fin k → ℝ) (γ : ℝ) (hq : ∀ (i : Fin k), 0 < q i) (hγ : 0 < γ) (z w : Fin 3 → ℝ) : z ⬝ᵥ (𝒦 t q γ).mulVec w = z ⬝ᵥ (𝒜 t q)⁻¹.mulVec w - z 0 * w 0 / (γ + a0 t q)

theorem BollobasNikiforov.𝒦_bilinear {k : ℕ} (t q : Fin k → ℝ) (γ : ℝ) (hq : ∀ (i : Fin k), 0 < q i) (hγ : 0 < γ) (z w : Fin 3 → ℝ) : z ⬝ᵥ (𝒦 t q γ).mulVec w = Δ t q * (𝒜 t q)⁻¹.mulVec z 2 * (Δ t q * (𝒜 t q)⁻¹.mulVec w 2) / (Δ t q * D2 t q) + (a0 t q * z 1 + √2 * m t q 1 * z 0) * (a0 t q * w 1 + √2 * m t q 1 * w 0) / (a0 t q * D2 t q) + γ * z 0 * w 0 / (a0 t q * (γ + a0 t q))

KR12: substituting U

theorem BollobasNikiforov.bhat_zero {k : ℕ} (t q : Fin k → ℝ) (x : ℝ) : bhat t q x 0 = x ^ 2 + h t q x

theorem BollobasNikiforov.bhat_one {k : ℕ} (t q : Fin k → ℝ) (x : ℝ) : bhat t q x 1 = √2 * x - √2 * h1 t q x

theorem BollobasNikiforov.N_eq_Δ_inv_U {k : ℕ} (t q : Fin k → ℝ) (γ : ℝ) (hq : ∀ (i : Fin k), 0 < q i) (x : ℝ) : N t q x = Δ t q * (𝒜 t q)⁻¹.mulVec (U t q γ x) 2

theorem BollobasNikiforov.U_zero {k : ℕ} (t q : Fin k → ℝ) (γ x : ℝ) (hγ : 0 < γ) : U t q γ x 0 = Z t q γ x / γ

theorem BollobasNikiforov.U_weighted {k : ℕ} (t q : Fin k → ℝ) (γ x : ℝ) (hγ : 0 < γ) : a0 t q * U t q γ x 1 + √2 * m t q 1 * U t q γ x 0 = √2 * P t q x

KR13: eq:factor

theorem BollobasNikiforov.𝒦_factor {k : ℕ} (t q : Fin k → ℝ) (γ : ℝ) (hq : ∀ (i : Fin k), 0 < q i) (hγ : 0 < γ) (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))