OAI/Probability/InvariantIsing/Cavity/CavitySpectralUpperEigenvalues.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual finite compression and diagonal base obey the spectral upper bound used by the full Gaussian moment calculation.

  1. lemma OAI.InvariantIsing.cavity_eigenvalues_le_of_upper line 14
  2. lemma OAI.InvariantIsing.cavity_compressed_eigenvalues_le line 36
  3. lemma OAI.InvariantIsing.cavity_diagonal_eigenvalues_le line 43