Sherman–Morrison formula for 𝒦

The rank-one update 𝒦 = (𝒜 + VVᵀ/γ)⁻¹ expands as 𝒜⁻¹ - e₀ e₀ᵀ / (γ + a₀), using 𝒜⁻¹ V = e₀ and V 0 = a₀.

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

a₀ = 1 + ∑ qᵢ is positive when each qᵢ is.

theorem BollobasNikiforov.γ_add_a0_pos {k : ℕ} (t q : Fin k → ℝ) (γ : ℝ) (hq : ∀ (i : Fin k), 0 < q i) (hγ : 0 < γ) : 0 < γ + a0 t q

theorem BollobasNikiforov.γ_add_a0_ne_zero {k : ℕ} (t q : Fin k → ℝ) (γ : ℝ) (hq : ∀ (i : Fin k), 0 < q i) (hγ : 0 < γ) : γ + a0 t q ≠ 0

theorem BollobasNikiforov.Vvec_zero {k : ℕ} (t q : Fin k → ℝ) : Vvec t q 0 = a0 t q

V = 𝒜 e₀, so the 0-coordinate is 𝒜 0 0 = a₀.

theorem BollobasNikiforov.Vvec_dotProduct_single {k : ℕ} (t q : Fin k → ℝ) : Vvec t q ⬝ᵥ Pi.single 0 1 = a0 t q

theorem BollobasNikiforov.𝒜_transpose {k : ℕ} (t q : Fin k → ℝ) (hq : ∀ (i : Fin k), 0 < q i) : (𝒜 t q).transpose = 𝒜 t q

𝒜 is real symmetric.

theorem BollobasNikiforov.vecMul_inv_Vvec {k : ℕ} (t q : Fin k → ℝ) (hq : ∀ (i : Fin k), 0 < q i) : Matrix.vecMul (Vvec t q) (𝒜 t q)⁻¹ = Pi.single 0 1

Vᵀ 𝒜⁻¹ = e₀ᵀ, equivalently V ᵥ* 𝒜⁻¹ = e₀.

theorem BollobasNikiforov.𝒦_shermanMorrison {k : ℕ} (t q : Fin k → ℝ) (γ : ℝ) (hq : ∀ (i : Fin k), 0 < q i) (hγ : 0 < γ) : 𝒦 t q γ = (𝒜 t q)⁻¹ - (1 / (γ + a0 t q)) • Matrix.vecMulVec (Pi.single 0 1) (Pi.single 0 1)

Sherman–Morrison: 𝒦 = 𝒜⁻¹ - e₀ e₀ᵀ / (γ + a₀).