OAI/Probability/InvariantIsing/Spectral/SpectralExtremeLimits.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Convergence of the actual extreme eigenvalues implies the uniform no-outlier formulation used by the pressure theorem.

  1. def OAI.InvariantIsing.spectralMinimum line 14

    Also declared: ComparatorChallenges/InvariantIsing.lean:143 (same declaration text).

  2. def OAI.InvariantIsing.spectralMaximum line 17

    Also declared: ComparatorChallenges/InvariantIsing.lean:146 (same declaration text).

  3. lemma OAI.InvariantIsing.spectralMinimum_le line 20
  4. lemma OAI.InvariantIsing.le_spectralMaximum line 24
  5. lemma OAI.InvariantIsing.spectral_no_outliers_of_extreme_limits line 28