OAI/Probability/InvariantIsing/Spectral/SelectedSpectralExcess.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Turning a scalar edge-excess limit into the selected spectral hypotheses.

  1. lemma OAI.InvariantIsing.selected_no_outliers_of_excess line 12
  2. lemma OAI.InvariantIsing.selected_spectralRadius_bounded line 20