OAI/Probability/InvariantIsing/Spectral/SpectralCanonicalSymbols.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Positive semidefinite array geometry supplies the diagonal bound needed for nonnegative canonical group symbols.

  1. lemma OAI.InvariantIsing.gramDiagonal_pair_le line 16
  2. lemma OAI.InvariantIsing.spectralGroupQuantilePath_le_diagonal line 25
  3. lemma OAI.InvariantIsing.OverlapPath.symbol_nonneg_ae line 49
  4. lemma OAI.InvariantIsing.sum_pathSymbols_ae line 66
  5. theorem OAI.InvariantIsing.spectralCanonical_symbols line 77