OAI/Probability/InvariantIsing/Spectral/HermitianEigenvalueLimits.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Limits of ordered Hermitian roots, with multiplicities retained.

  1. lemma OAI.InvariantIsing.hermitian_eigenvaluesâ‚€_limit_unique line 11
  2. theorem OAI.InvariantIsing.hermitian_eigenvaluesâ‚€_tendsto line 34