cauchy_interlace_theorem
Provedeigenvalueslinear-algebraspectral-theory
A consequence of Cauchy’s Interlace Theorem: If A is a symmetric N×N integer matrix with A² = cI, and S is a set of more than N/2 indices, then there exists a nonzero vector supported on S such that ||Av||² ≥ c·||v||². Equivalently, the principal submatrix A_S has an eigenvalue with absolute value ≥ √c. This is the key linear algebra tool in Huang’s proof of the Sensitivity Conjecture.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem cauchy_interlace_theorem (N : ℕ) (A : Fin N → Fin N → ℤ) (hA_symm : ∀ i j, A i j = A j i) (c : ℕ) (hA_sq : ∀ i j : Fin N, ∑ k : Fin N, A i k * A k j = if i = j then (↑c : ℤ) else 0) (S : Finset (Fin N)) (hS : 2 * S.card > N) : ∃ v : Fin N → ℤ, (∀ i, i ∉ S → v i = 0) ∧ (∃ i, v i ≠ 0) ∧ ↑c * ∑ i, v i ^ 2 ≤ ∑ i, (∑ j, A i j * v j) ^ 2 := by sorry
Source