OAI/Probability/InvariantIsing/Cavity/CavityPhysicalProjection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Physical spectral projections and their exact signed-site action.

  1. lemma OAI.InvariantIsing.cavity_specialRotation_one line 13
  2. lemma OAI.InvariantIsing.cavity_specialRotation_symm line 19
  3. def OAI.InvariantIsing.cavitySpectralProjection line 26
  4. lemma OAI.InvariantIsing.cavitySpectralProjection_norm_sq_le line 30
  5. lemma OAI.InvariantIsing.cavitySpectralProjection_site_sq_le line 40
  6. lemma OAI.InvariantIsing.cavitySpectralProjection_permutation line 50
  7. lemma OAI.InvariantIsing.cavitySpectralProjection_permutation_sq line 63
  8. lemma OAI.InvariantIsing.measurable_cavitySpectralProjection_site line 74