Kadison–Singer problem

DefinitionMixed determinant polynomial#✓fully proved

For square complex matrices \(A_1, \dots, A_m\) whose rows and columns are indexed by a finite set \(d\), the mixed determinant polynomial is \(\det(x I + \sum_{i=1}^m z_i A_i)\), viewed as a polynomial with complex coefficients in the \(m + 1\) variables \(x, z_1, \dots, z_m\), where \(I\) is the identity matrix.

public noncomputable def mixedDetPolynomial {m : ℕ} {d : Type*} [Fintype d] [DecidableEq d]
    (A : Fin m → Matrix d d ℂ) : MvPolynomial (Unit ⊕ Fin m) ℂ :=
  Matrix.det
    (Matrix.scalar d (X (Sum.inl ())) +
      ∑ i, (X (Sum.inr i) : MvPolynomial (Unit ⊕ Fin m) ℂ) •
        (A i).map (C : ℂ → MvPolynomial (Unit ⊕ Fin m) ℂ))

Used by 12

Used byValues of the mixed determinant polynomial · Mixed characteristic polynomial · Mixed characteristic polynomials of outer products · Mixed characteristic polynomial of a single \(1 \times 1\) matrix · Mixed characteristic polynomials of positive semidefinite matrices are real-rooted · Marcus--Spielman--Srivastava barrier bound · Mixed characteristic polynomials are monic · Degree of a mixed characteristic polynomial · The mixed characteristic polynomial is affine in each matrix · Real stability of the determinant polynomial · Stability of the determinant polynomial · Rank-one coefficients make the mixed determinant polynomial affine

TheoremValues of the mixed determinant polynomial#✓fully proved

Let \(A_1, \dots, A_m\) be square complex matrices whose rows and columns are indexed by a finite set \(d\). For all complex numbers \(x, z_1, \dots, z_m\), the value of the mixed determinant polynomial of \(A_1, \dots, A_m\) at the point \((x, z_1, \dots, z_m)\) is \(\det(x I + \sum_{i=1}^m z_i A_i)\).

public theorem eval_mixedDetPolynomial {m : ℕ} {d : Type*} [Fintype d] [DecidableEq d]
    (A : Fin m → Matrix d d ℂ) (z : Unit ⊕ Fin m → ℂ) :
    MvPolynomial.eval z (mixedDetPolynomial A) =
      Matrix.det (Matrix.scalar d (z (Sum.inl ())) + ∑ i, z (Sum.inr i) • A i)

Uses 1 · Used by 5

Statement usesMixed determinant polynomial

Used byMixed characteristic polynomials of outer products · Marcus--Spielman--Srivastava barrier bound · The mixed characteristic polynomial is affine in each matrix · Stability of the determinant polynomial · Rank-one coefficients make the mixed determinant polynomial affine

TheoremRank-one coefficients make the mixed determinant polynomial affine#✓fully proved

Let \(A_1, \dots, A_m\) be square complex matrices whose rows and columns are indexed by a finite set \(d\), and suppose that \(A_i = u v^{\mathsf T}\) for some index \(i\) and vectors \(u, v \in \mathbb{C}^d\). Consider the mixed determinant polynomial \(\det(x I + \sum_{j=1}^m z_j A_j)\) in the variables \(x, z_1, \dots, z_m\), where \(I\) is the identity matrix. Then its second partial derivative with respect to \(z_i\) is zero; equivalently, it has degree at most one in \(z_i\).

public theorem mixedDetPolynomial_pderiv_sq_eq_zero_of_eq_vecMulVec
    {m : ℕ} {d : Type*} [Fintype d] [DecidableEq d]
    (A : Fin m → Matrix d d ℂ) (i : Fin m) (u v : d → ℂ)
    (hi : A i = Matrix.vecMulVec u v) :
    pderiv (Sum.inr i) (pderiv (Sum.inr i) (mixedDetPolynomial A)) = 0

Uses 3 · Used by 1

Statement usesMixed determinant polynomial

Proof usesValues of the mixed determinant polynomial · The determinant is affine along a rank-one direction

Used byMixed characteristic polynomials of outer products

DefinitionMixed characteristic polynomial#✓fully proved

For square complex matrices \(A_1, \dots, A_m\) whose rows and columns are indexed by a finite set \(d\), consider the mixed determinant polynomial \(\det(x I + \sum_{i=1}^m z_i A_i)\) in the variables \(x, z_1, \dots, z_m\), where \(I\) is the identity matrix. The mixed characteristic polynomial is the polynomial in \(x\) with complex coefficients obtained by applying the operator \(\prod_{i=1}^m (1 - \partial_{z_i})\) to it and then setting \(z_1 = \dots = z_m = 0\).

public noncomputable def mixedCharacteristicPolynomial {m : ℕ} {d : Type*}
    [Fintype d] [DecidableEq d] (A : Fin m → Matrix d d ℂ) : Polynomial ℂ :=
  eval₂Hom Polynomial.C
      (Sum.elim (fun _ ↦ Polynomial.X) (fun _ ↦ 0))
    (mixedDifferential (List.finRange m |>.map Sum.inr) (mixedDetPolynomial A))

Uses 2 · Used by 10

Statement usesMixed determinant polynomial · Mixed differential operator

Used byAn outcome bounded by the mixed characteristic polynomial · Marcus--Spielman--Srivastava bound, finite-support form · Mixed characteristic polynomials of outer products · Mixed characteristic polynomial of a single \(1 \times 1\) matrix · Mixed characteristic polynomials of positive semidefinite matrices are real-rooted · Marcus--Spielman--Srivastava barrier bound · Mixed characteristic polynomials are monic · Degree of a mixed characteristic polynomial · The mixed characteristic polynomial along a line · The mixed characteristic polynomial is affine in each matrix

TheoremThe mixed characteristic polynomial is affine in each matrix#✓fully proved

Let \(A_1, \dots, A_m\) be square complex matrices whose rows and columns are indexed by a finite set \(d\), and fix an index \(i\). Let \((C_a)_{a \in \iota}\) be a family of such matrices indexed by a finite set \(\iota\), with real weights \(w_a\), not necessarily nonnegative, such that \(\sum_a w_a = 1\). Then the mixed characteristic polynomial of the family obtained from \(A_1, \dots, A_m\) by replacing \(A_i\) with \(\sum_a w_a C_a\) equals \(\sum_a w_a \mu_a\), where \(\mu_a\) is the mixed characteristic polynomial of the family obtained by replacing \(A_i\) with \(C_a\).

public theorem mixedCharacteristicPolynomial_update_sum
    {m : ℕ} {d ι : Type*} [Fintype d] [DecidableEq d] [Fintype ι]
    (A : Fin m → Matrix d d ℂ) (i : Fin m) (w : ι → ℝ)
    (C : ι → Matrix d d ℂ) (hsum : ∑ a, w a = 1) :
    mixedCharacteristicPolynomial (Function.update A i (∑ a, (w a : ℂ) • C a)) =
      ∑ a, (w a : ℂ) • mixedCharacteristicPolynomial (Function.update A i (C a))

Uses 10 · Used by 2

Statement usesMixed characteristic polynomial

Proof usesValues of the mixed determinant polynomial · Mixed determinant polynomial · The coefficient of \(X\) in \(\det(B + XA)\) · First-order term of the determinant · Additivity of the first-order term of the determinant · Homogeneity of the first-order term of the determinant · Mixed differential operator · Mixed differential along a list with a given first index · The mixed differential ignores the order of the indices

Used byAn outcome bounded by the mixed characteristic polynomial · The mixed characteristic polynomial along a line

TheoremThe mixed characteristic polynomial along a line#✓fully proved

Let \(A_1, \dots, A_m\) be square complex matrices whose rows and columns are indexed by a finite set \(d\), fix an index \(i\), let \(B\) and \(C\) be two such matrices and let \(t\) be a real number. Write \(\mu_M\) for the mixed characteristic polynomial of the family obtained from \(A_1, \dots, A_m\) by replacing \(A_i\) with \(M\). Then \(\mu_{(1 - t) B + t C} = (1 - t)\, \mu_B + t\, \mu_C\).

public theorem mixedCharacteristicPolynomial_update_affine
    {m : ℕ} {d : Type*} [Fintype d] [DecidableEq d]
    (A : Fin m → Matrix d d ℂ) (i : Fin m) (B C : Matrix d d ℂ) (t : ℝ) :
    mixedCharacteristicPolynomial
        (Function.update A i ((1 - (t : ℂ)) • B + (t : ℂ) • C)) =
      (1 - (t : ℂ)) • mixedCharacteristicPolynomial (Function.update A i B) +
        (t : ℂ) • mixedCharacteristicPolynomial (Function.update A i C)

Uses 2 · Used by 1

Statement usesMixed characteristic polynomial

Proof usesThe mixed characteristic polynomial is affine in each matrix

Used byAn outcome bounded by the mixed characteristic polynomial

TheoremMixed characteristic polynomials of outer products#✓fully proved

Let \(A_1, \dots, A_m\) be square complex matrices whose rows and columns are indexed by a finite set \(d\), and suppose that \(A_i = u_i v_i^{\mathsf T}\) for vectors \(u_i, v_i \in \mathbb{C}^d\), for every \(i\). Then the mixed characteristic polynomial of \(A_1, \dots, A_m\) equals the characteristic polynomial of the sum \(\sum_{i=1}^m A_i\), that is, the polynomial \(\det(x I - \sum_{i=1}^m A_i)\) in the variable \(x\), where \(I\) is the identity matrix.

public theorem mixedCharacteristicPolynomial_eq_charpoly_sum_of_eq_vecMulVec
    {m : ℕ} {d : Type*} [Fintype d] [DecidableEq d]
    (A : Fin m → Matrix d d ℂ) (u v : Fin m → d → ℂ)
    (hA : ∀ i, A i = Matrix.vecMulVec (u i) (v i)) :
    mixedCharacteristicPolynomial A = Matrix.charpoly (∑ i, A i)

Uses 10 · Used by 1

Statement usesMixed characteristic polynomial

Proof usesValues of the mixed determinant polynomial · Mixed determinant polynomial · Rank-one coefficients make the mixed determinant polynomial affine · Mixed differential operator · Mixed differential along a concatenated list · Mixed differential along a list with a given first index · The mixed differential ignores the order of the indices · Mixed differential along the empty list · Partial derivatives commute with the mixed differential

Used byAn outcome bounded by the mixed characteristic polynomial

TheoremMixed characteristic polynomial of a single \(1 \times 1\) matrix#✓fully proved

For every complex number \(a\), the mixed characteristic polynomial of the family consisting of the single \(1 \times 1\) complex matrix \((a)\) is the polynomial \(x - a\) in the variable \(x\), which is the characteristic polynomial of \((a)\).

public theorem mixedCharacteristicPolynomial_fin_one (a : ℂ) :
    mixedCharacteristicPolynomial (m := 1) (d := Fin 1)
      (fun _ ↦ !![a]) = Polynomial.X - Polynomial.C a

Uses 3

Statement usesMixed characteristic polynomial

Proof usesMixed determinant polynomial · Mixed differential operator

DefinitionFinite-support Marcus–Spielman–Srivastava bound#✓fully proved

The proposition that the following holds for every natural number \(m\) and every finite index set \(D\). Let \(s_1, \dots, s_m\) be positive integers, let \(p_{i,a} \ge 0\) be reals and \(v_{i,a} \in \mathbb{C}^D\) be vectors for \(1 \le i \le m\) and \(1 \le a \le s_i\), and let \(\eta \ge 0\) be real. Suppose that \(\sum_a p_{i,a} = 1\) for each \(i\), that \(\sum_i \sum_a p_{i,a} v_{i,a} v_{i,a}^* = \mathrm{Id}_D\), and that \(\sum_a p_{i,a} \|v_{i,a}\|^2 \le \eta\) for each \(i\), where \(\|v_{i,a}\|\) is the Euclidean norm. Then there are choices \(a_i \in \{1, \dots, s_i\}\) for \(i = 1, \dots, m\) such that \(\left\|\sum_i v_{i,a_i} v_{i,a_i}^*\right\| \le (1 + \sqrt{\eta})^2\), where the norm of a matrix is the operator norm.

In probabilistic terms, \(p_{i,a}\) is the probability that an independent random vector \(v_i\) takes the value \(v_{i,a}\), and the conclusion is that some choice of values meets the bound.

public def FiniteMSSBound : Prop :=
  ∀ (m : ℕ) (d : Type u) [Fintype d] [DecidableEq d] (s : Fin m → ℕ),
    (∀ i, 0 < s i) →
    ∀ (p : (i : Fin m) → Fin (s i) → ℝ)
      (v : (i : Fin m) → Fin (s i) → d → ℂ) (η : ℝ),
      0 ≤ η →
      (∀ i a, 0 ≤ p i a) →
      (∀ i, ∑ a, p i a = 1) →
      (∑ i, ∑ a, (p i a : ℂ) • Matrix.vecMulVec (v i a) (star (v i a)) = 1) →
      (∀ i, ∑ a, p i a * ∑ k, ‖v i a k‖ ^ 2 ≤ η) →
      ∃ ω : (i : Fin m) → Fin (s i),
        ‖∑ i, Matrix.vecMulVec (v i (ω i)) (star (v i (ω i)))‖ ≤
          (1 + Real.sqrt η) ^ 2

Used by 4

Used byAnderson paving from the finite MSS bound · Partitioning a Parseval frame with the finite MSS bound · Marcus--Spielman--Srivastava bound, finite-support form · Anderson paving theorem

TheoremPartitioning a Parseval frame with the finite MSS bound#✓fully proved

Assume the finite-support Marcus–Spielman–Srivastava bound holds. Let \(I\) be a finite index set, let \(d\) and \(r\) be natural numbers with \(r > 0\), let \(\delta \ge 0\) be real, and let \(u_i \in \mathbb{C}^d\) for \(i \in I\) be vectors with \(\sum_{i \in I} u_i u_i^* = \mathrm{Id}_d\) and \(\|u_i\|^2 \le \delta\) for every \(i\). Then there is a map \(c : I \to \{1, \dots, r\}\) such that for every \(j\), \(\left\|\sum_{i \in I,\ c(i) = j} u_i u_i^*\right\| \le (1/\sqrt{r} + \sqrt{\delta})^2\), where \(\|u_i\|\) is the Euclidean norm of \(u_i\) and the norm of a matrix is the operator norm.

public theorem exists_frame_partition_of_finiteMSS
    (hMSS : FiniteMSSBound.{0}) {I : Type v} [Fintype I] {d r : ℕ}
    (hr : 0 < r) (u : I → Fin d → ℂ) (δ : ℝ) (hδ : 0 ≤ δ)
    (hframe : ∑ i, Matrix.vecMulVec (u i) (star (u i)) = 1)
    (hu : ∀ i, ∑ k, ‖u i k‖ ^ 2 ≤ δ) :
    ∃ c : I → Fin r, ∀ j,
      ‖((∑ i ∈ Finset.univ.filter (fun i ↦ c i = j),
        Matrix.vecMulVec (u i) (star (u i))) : Matrix (Fin d) (Fin d) ℂ)‖ ≤
          (1 / Real.sqrt r + Real.sqrt δ) ^ 2

Uses 1 · Used by 1

Statement usesFinite-support Marcus–Spielman–Srivastava bound

Used byAnderson paving from the finite MSS bound

TheoremAnderson paving from the finite MSS bound#✓fully proved

Assume the finite-support Marcus–Spielman–Srivastava bound holds. Let \(n\) and \(r\) be natural numbers with \(r > 0\), and let \(A\) be a Hermitian complex \(n \times n\) matrix with zero diagonal and operator norm \(\|A\| \le 1\). Then there is a coloring \(c\) of the indices \(\{1, \dots, n\}\) with \(r^2\) colors such that for every color \(j\), writing \(P_j\) for the diagonal matrix with entry \(1\) at the indices of color \(j\) and \(0\) elsewhere, \(\|P_j A P_j\| \le 2\left(1/\sqrt{r} + \sqrt{1/2}\right)^2 - 1\), where \(\|\cdot\|\) is the operator norm.

public theorem andersonPaving_of_finiteMSS
    (hMSS : FiniteMSSBound.{0}) {n r : ℕ} (hr : 0 < r)
    (A : Matrix (Fin n) (Fin n) ℂ) (hA : A.IsHermitian)
    (hdiagA : ∀ i, A i i = 0) (hnormA : ‖A‖ ≤ 1) :
    ∃ c : Fin n → Fin (r * r), ∀ j,
      ‖Matrix.diagonal (fun i ↦ if c i = j then (1 : ℂ) else 0) * A *
        Matrix.diagonal (fun i ↦ if c i = j then (1 : ℂ) else 0)‖ ≤
          2 * (1 / Real.sqrt r + Real.sqrt (1 / 2 : ℝ)) ^ 2 - 1

Uses 2 · Used by 1

Statement usesFinite-support Marcus–Spielman–Srivastava bound

Proof usesPartitioning a Parseval frame with the finite MSS bound

Used byAnderson paving theorem

TheoremStability of the determinant polynomial#✓fully proved

For every finite family \(A_1, \dots, A_m\) of positive semidefinite complex square matrices whose rows and columns are indexed by a finite set \(d\), the polynomial \(\det\left(x I + \sum_{i=1}^m z_i A_i\right)\) in the variables \(x, z_1, \dots, z_m\), where \(I\) is the identity matrix, is stable.

public theorem mixedDetPolynomial_isStable_of_posSemidef
    {m : ℕ} {d : Type*} [Fintype d] [DecidableEq d]
    (A : Fin m → Matrix d d ℂ) (hA : ∀ i, (A i).PosSemidef) :
    (mixedDetPolynomial A).IsStable

Uses 3 · Used by 1

Statement usesMixed determinant polynomial · Stable polynomials

Proof usesValues of the mixed determinant polynomial

Used byReal stability of the determinant polynomial

TheoremReal stability of the determinant polynomial#✓fully proved

For every finite family \(A_1, \dots, A_m\) of positive semidefinite complex square matrices whose rows and columns are indexed by a finite set \(d\), the polynomial \(\det\left(x I + \sum_{i=1}^m z_i A_i\right)\) in the variables \(x, z_1, \dots, z_m\), where \(I\) is the identity matrix, is real stable.

public theorem mixedDetPolynomial_isRealStable_of_posSemidef
    {m : ℕ} {d : Type*} [Fintype d] [DecidableEq d]
    (A : Fin m → Matrix d d ℂ) (hA : ∀ i, (A i).PosSemidef) :
    (mixedDetPolynomial A).IsRealStable

Uses 4 · Used by 2

Statement usesMixed determinant polynomial · Real stable polynomials

Proof usesStability of the determinant polynomial · Stable polynomials

Used byMixed characteristic polynomials of positive semidefinite matrices are real-rooted · Marcus--Spielman--Srivastava barrier bound

TheoremMixed characteristic polynomials are monic#✓fully proved

For every finite family \(A_1, \dots, A_m\) of complex square matrices of a common size, the mixed characteristic polynomial of \(A_1, \dots, A_m\) is monic.

public theorem mixedCharacteristicPolynomial_monic
    {m : ℕ} {d : Type*} [Fintype d] [DecidableEq d]
    (A : Fin m → Matrix d d ℂ) : (mixedCharacteristicPolynomial A).Monic

Uses 5 · Used by 2

Statement usesMixed characteristic polynomial

Proof usesMixed determinant polynomial · Mixed differential operator · Mixed differential along a list with a given first index · Univariate specialization

Used byAn outcome bounded by the mixed characteristic polynomial · Marcus--Spielman--Srivastava barrier bound

TheoremDegree of a mixed characteristic polynomial#✓fully proved

For every finite family \(A_1, \dots, A_m\) of complex square matrices whose rows and columns are indexed by a finite set \(d\), the mixed characteristic polynomial of \(A_1, \dots, A_m\) has degree \(|d|\), the number of elements of \(d\).

public theorem mixedCharacteristicPolynomial_natDegree
    {m : ℕ} {d : Type*} [Fintype d] [DecidableEq d]
    (A : Fin m → Matrix d d ℂ) :
    (mixedCharacteristicPolynomial A).natDegree = Fintype.card d

Uses 5 · Used by 2

Statement usesMixed characteristic polynomial

Proof usesMixed determinant polynomial · Mixed differential operator · Mixed differential along a list with a given first index · Univariate specialization

Used byAn outcome bounded by the mixed characteristic polynomial · Marcus--Spielman--Srivastava barrier bound

TheoremMixed characteristic polynomials of positive semidefinite matrices are real-rooted#✓fully proved

For every finite family \(A_1, \dots, A_m\) of positive semidefinite complex square matrices of a common size, the mixed characteristic polynomial of \(A_1, \dots, A_m\) is real-rooted.

public theorem mixedCharacteristicPolynomial_isRealRooted_of_posSemidef
    {m : ℕ} {d : Type*} [Fintype d] [DecidableEq d]
    (A : Fin m → Matrix d d ℂ) (hA : ∀ i, (A i).PosSemidef) :
    (mixedCharacteristicPolynomial A).IsRealRooted

Uses 10 · Used by 2

Statement usesMixed characteristic polynomial · Real-rooted polynomials

Proof usesMixed determinant polynomial · Real stability of the determinant polynomial · Real stable polynomials · The mixed differential preserves real stability · Real-rootedness of univariate specializations of real stable polynomials · Mixed differential operator · Mixed differential along a list with a given first index · Univariate specialization

Used byAn outcome bounded by the mixed characteristic polynomial · Marcus--Spielman--Srivastava barrier bound

TheoremMarcus--Spielman--Srivastava barrier bound#✓fully proved

Let \(d\) be a nonempty finite index set, let \(A_1, \dots, A_m\) be positive semidefinite complex \(d \times d\) matrices with \(\sum_i A_i = I\), and let \(\eta \ge 0\) be a real number such that \(\operatorname{Re} \operatorname{tr} A_i \le \eta\) for every \(i\). Then the largest real part of a root of the mixed characteristic polynomial of \(A_1, \dots, A_m\) is at most \((1 + \sqrt{\eta})^2\).

public theorem mixedCharacteristicPolynomial_maxRealRoot_le
    {m : ℕ} {d : Type*} [Fintype d] [DecidableEq d] [Nonempty d]
    (A : Fin m → Matrix d d ℂ) (η : ℝ) (hη : 0 ≤ η)
    (hA : ∀ i, (A i).PosSemidef) (hsum : ∑ i, A i = 1)
    (htrace : ∀ i, (Matrix.trace (A i)).re ≤ η) :
    (mixedCharacteristicPolynomial A).maxRealRoot ≤ (1 + Real.sqrt η) ^ 2

Uses 23 · Used by 1

Statement usesMixed characteristic polynomial · Largest real part of a root

Proof usesValues of the mixed determinant polynomial · Mixed characteristic polynomials of positive semidefinite matrices are real-rooted · Mixed characteristic polynomials are monic · Degree of a mixed characteristic polynomial · Mixed determinant polynomial · Real stability of the determinant polynomial · The coefficient of \(X\) in \(\det(B + XA)\) · First-order term of the determinant · Real stable polynomials · Subtracting a partial derivative preserves real stability · Stable polynomials · Roots of specializations of stable polynomials lie in the closed lower half-plane · Partial derivatives under univariate specialization · Evaluating a univariate specialization · Univariate specialization at real values preserves real coefficients · Mixed differential operator · Mixed differential along a list with a given first index · Univariate specialization · Real-rooted polynomials · For a real-rooted polynomial, the largest real part of a root is a root · Conjugation-invariant polynomials with roots in the closed lower half-plane are real-rooted

Used byMarcus--Spielman--Srivastava bound, finite-support form

TheoremAn outcome bounded by the mixed characteristic polynomial#✓fully proved

Let \(d\) be a nonempty finite index set. For \(i = 1, \dots, m\) let \(s_i \ge 1\), let \(v_{i,1}, \dots, v_{i,s_i} \in \mathbb{C}^d\), let \(p_{i,1}, \dots, p_{i,s_i} \ge 0\) be reals with \(\sum_a p_{i,a} = 1\), and put \(A_i = \sum_a p_{i,a} v_{i,a} v_{i,a}^*\). Then there is a choice of indices \(\omega_i \in \{1, \dots, s_i\}\), one for each \(i\), such that the largest real part of a root of the characteristic polynomial of \(\sum_i v_{i,\omega_i} v_{i,\omega_i}^*\) is at most the largest real part of a root of the mixed characteristic polynomial of \(A_1, \dots, A_m\).

public theorem exists_outcome_maxRealRoot_le_mixedCharacteristicPolynomial
    {m : ℕ} {d : Type*} [Fintype d] [DecidableEq d] [Nonempty d]
    {s : Fin m → ℕ} (hs : ∀ i, 0 < s i)
    (p : (i : Fin m) → Fin (s i) → ℝ)
    (v : (i : Fin m) → Fin (s i) → d → ℂ)
    (hp : ∀ i a, 0 ≤ p i a) (hsum : ∀ i, ∑ a, p i a = 1) :
    ∃ ω : (i : Fin m) → Fin (s i),
      (Matrix.charpoly
        (∑ i, Matrix.vecMulVec (v i (ω i)) (star (v i (ω i))))).maxRealRoot ≤
      (mixedCharacteristicPolynomial (fun i ↦
        ∑ a, p i a • Matrix.vecMulVec (v i a) (star (v i a)))).maxRealRoot

Uses 10 · Used by 1

Statement usesMixed characteristic polynomial · Largest real part of a root

Proof usesMixed characteristic polynomials of outer products · Mixed characteristic polynomials of positive semidefinite matrices are real-rooted · Mixed characteristic polynomials are monic · Degree of a mixed characteristic polynomial · The mixed characteristic polynomial along a line · The mixed characteristic polynomial is affine in each matrix · Real-rooted polynomials · Some member's largest root is at most that of a weighted sum, via real-rooted segments

Used byMarcus--Spielman--Srivastava bound, finite-support form

TheoremMarcus--Spielman--Srivastava bound, finite-support form#✓fully proved

Let \(d\) be a finite index set and, for \(i = 1, \dots, m\), let \(s_i \ge 1\), let \(v_{i,1}, \dots, v_{i,s_i} \in \mathbb{C}^d\), and let \(p_{i,1}, \dots, p_{i,s_i} \ge 0\) be reals with \(\sum_a p_{i,a} = 1\). Let \(\eta \ge 0\) be a real number, and suppose that \(\sum_i \sum_a p_{i,a} v_{i,a} v_{i,a}^* = I\) and \(\sum_a p_{i,a} \|v_{i,a}\|^2 \le \eta\) for every \(i\), where \(\|\cdot\|\) is the Euclidean norm. Then there is a choice of indices \(\omega_i \in \{1, \dots, s_i\}\), one for each \(i\), such that the operator norm of \(\sum_i v_{i,\omega_i} v_{i,\omega_i}^*\) with respect to the Euclidean norm on \(\mathbb{C}^d\) is at most \((1 + \sqrt{\eta})^2\).

public theorem finiteMSSBound : FiniteMSSBound.{u}

Uses 6 · Used by 1

Statement usesFinite-support Marcus–Spielman–Srivastava bound

Proof usesAn outcome bounded by the mixed characteristic polynomial · Mixed characteristic polynomial · Marcus--Spielman--Srivastava barrier bound · Spectral norm of a positive semidefinite matrix · Largest real part of a root

Used byAnderson paving theorem

DefinitionPaving projection#✓fully proved

Given a colouring \(c\) of the indices \(\{0, \dots, n-1\}\) with the colours \(\{0, \dots, r-1\}\) and a colour \(j\), the paving projection of \(c\) onto colour \(j\) is the diagonal complex \(n \times n\) matrix whose \(i\)-th diagonal entry is \(1\) if \(c(i) = j\) and \(0\) otherwise.

noncomputable def pavingProj (n r : ℕ) (c : Fin n → Fin r) (j : Fin r) :
    Matrix (Fin n) (Fin n) ℂ :=
  Matrix.diagonal (fun i => if c i = j then (1 : ℂ) else 0)

Used by 1

Used byAnderson paving theorem

TheoremAnderson paving theorem#✓fully proved

For every real \(\varepsilon > 0\) there is a positive integer \(r\) such that for every \(n \in \mathbb{N}\) and every Hermitian complex \(n \times n\) matrix \(A\) with zero diagonal and \(\|A\| \le 1\), where \(\|\cdot\|\) is the operator norm for the Euclidean norm on \(\mathbb{C}^n\), there is a colouring \(c\) of the indices \(\{0, \dots, n-1\}\) with the \(r\) colours \(\{0, \dots, r-1\}\) such that \(\|P_j A P_j\| \le \varepsilon\) for every colour \(j\), where \(P_j\) is the paving projection of \(c\) onto colour \(j\).

Proof: We formalize the Marcus--Spielman--Srivastava mixed-characteristic-polynomial bound via real stability, interlacing families, and the barrier argument, then use Timotin's projection dilation reduction to derive Anderson paving.

theorem kadison_singer_paving
    (ε : ℝ) (hε : 0 < ε) :
    ∃ (r : ℕ), 0 < r ∧
      ∀ (n : ℕ) (A : Matrix (Fin n) (Fin n) ℂ),
        A.IsHermitian → (∀ i : Fin n, A i i = 0) → ‖A‖ ≤ 1 →
        ∃ (c : Fin n → Fin r), ∀ (j : Fin r),
          ‖pavingProj n r c j * A * pavingProj n r c j‖ ≤ ε

Sources

• Anderson paving formulation equivalent to Kadison–Singer conjecture; proved by Marcus–Spielman–Srivastava, Ann. of Math. 182 (2015), 327–350; original Kadison–Singer, Amer. J. Math. 81 (1959) and Anderson, Trans. Amer. Math. Soc. 249 (1979); Lean is finite-dimensional Hermitian zero-diagonal paving with r(ε) independent of n.

Uses 4

Statement usesPaving projection

Proof usesFinite-support Marcus–Spielman–Srivastava bound · Anderson paving from the finite MSS bound · Marcus--Spielman--Srivastava bound, finite-support form

21 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.