OAI/Probability/InvariantIsing/Spectral/SpectralPerturbedBlocks.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual diagonal perturbation preserves spectral blocks and vanishes in their limiting eigenvalues even when its minimizing coordinates vary.

  1. lemma OAI.InvariantIsing.diagonalPerturbedEigenvalues_block line 14
  2. lemma OAI.InvariantIsing.perturbedBlockEigenvalues_tendsto line 30