OAI/Probability/InvariantIsing/Cavity/CavityHaarSpectralLabels.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Keep the complete finite spectral overlap block in the Haar approximation, using its canonical compact embedding into real coordinates.

  1. def OAI.InvariantIsing.spectralBlockReal line 16
  2. def OAI.InvariantIsing.spectralBlockClamp line 19
  3. lemma OAI.InvariantIsing.continuous_spectralBlockReal line 22
  4. lemma OAI.InvariantIsing.continuous_spectralBlockClamp line 27
  5. lemma OAI.InvariantIsing.spectralBlockClamp_real line 32
  6. theorem OAI.InvariantIsing.cavityGroupHaarFrame_spectral_uniform line 39
  7. lemma OAI.InvariantIsing.measurable_cavityGroupHaarFrame_spectral_mean line 67