OAI/MathematicalPhysics/PEPSSubvolume/JointSpectrum.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Common eigenbases for positive commuting matrices.

  1. theorem OAI.PolynomialPEPS.Subvolume.JointDiagonalization.exists_subordinate line 21
  2. theorem OAI.PolynomialPEPS.Subvolume.JointDiagonalization.exists_basis line 39
  3. def OAI.PolynomialPEPS.Subvolume.JointDiagonalization.basisUnitary line 73
  4. theorem OAI.PolynomialPEPS.Subvolume.JointDiagonalization.conjugate_eq_diagonal line 78
  5. theorem OAI.PolynomialPEPS.Subvolume.JointDiagonalization.exists_unitary line 94
  6. theorem OAI.PolynomialPEPS.Subvolume.JointDiagonalization.diagonal_nonneg line 104
  7. theorem OAI.PolynomialPEPS.Subvolume.JointDiagonalization.exists_positive_unitary line 115