theorem PerronFrobeniusCorollary.QF_insertNth_zero {n : ℕ} (f : Fin (n + 1) → Fin (n + 1) → ℝ) (i₀ : Fin (n + 1)) (w : Fin n → ℝ) : PerronFrobeniusProof.QF f (i₀.insertNth 0 w) = PerronFrobeniusProof.QF (fun (i j : Fin n) => f (i₀.succAbove i) (i₀.succAbove j)) w

Inserting a zero in slot $i_0$ does not change the quadratic form value: $Q_f(\iota_{i_0}(0, w)) = Q_g(w)$ where $g$ is the submatrix obtained by deleting row/column $i_0$.

theorem PerronFrobeniusCorollary.restrictForm_offDiag {n : ℕ} (f : Fin (n + 1) → Fin (n + 1) → ℝ) (i₀ : Fin (n + 1)) (hOffDiag : ∀ (s t : Fin (n + 1)), s ≠ t → f s t ≤ 0) (s t : Fin n) : s ≠ t → f (i₀.succAbove s) (i₀.succAbove t) ≤ 0

The off-diagonal sign condition $f_{st} \le 0$ for $s \ne t$ is inherited by any principal submatrix.

theorem PerronFrobeniusCorollary.insertNth_abs_ne_zero {n : ℕ} (i₀ : Fin (n + 1)) (w : Fin n → ℝ) (hw : w ≠ 0) : (i₀.insertNth 0 fun (k : Fin n) => |w k|) ≠ 0

If $w \ne 0$ then inserting $0$ at $i_0$ in the absolute-value vector $|w|$ is still nonzero.

theorem PerronFrobeniusCorollary.insertNth_abs_nonneg {n : ℕ} (i₀ : Fin (n + 1)) (w : Fin n → ℝ) (b : Fin (n + 1)) : i₀.insertNth 0 (fun (k : Fin n) => |w k|) b ≥ 0

The "insert $0$ at $i_0$" version of $|w|$ has all components $\ge 0$.

theorem PerronFrobeniusCorollary.submatrix_positive_definite {n : ℕ} (f : Fin (n + 1) → Fin (n + 1) → ℝ) (hPSD : ∀ (u : Fin (n + 1) → ℝ), PerronFrobeniusProof.QF f u ≥ 0) (hOffDiag : ∀ (s t : Fin (n + 1)), s ≠ t → f s t ≤ 0) (hIndecomp : CoxeterGroup.FormIndecomposable f) (i₀ : Fin (n + 1)) (w : Fin n → ℝ) : w ≠ 0 → PerronFrobeniusProof.QF (fun (i j : Fin n) => f (i₀.succAbove i) (i₀.succAbove j)) w > 0

Perron–Frobenius corollary: any proper principal submatrix of an indecomposable, off-diagonal nonpositive, positive semidefinite Gram matrix is positive definite. Equivalently, the Coxeter form of an affine type becomes spherical on every proper parabolic.