OAI/Probability/InvariantIsing/Cavity/CavitySpinIsometry.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Signed site permutations act on the actual Ising cube and its projected overlaps. Their pair-spin observables have no sign factor.

  1. lemma OAI.InvariantIsing.spinValue_not line 15
  2. def OAI.InvariantIsing.cavitySignedSpinPermutation line 18
  3. lemma OAI.InvariantIsing.cavitySignedSpinPermutation_pair line 29
  4. def OAI.InvariantIsing.cavityPermutationFlip line 37
  5. lemma OAI.InvariantIsing.cavityPermutationSpin_vector line 40
  6. lemma OAI.InvariantIsing.cavity_specialRotation_mul_apply line 56
  7. lemma OAI.InvariantIsing.cavityPermutationSpin_cancel line 64
  8. lemma OAI.InvariantIsing.projectedOverlap_cavityPermutation line 72
  9. lemma OAI.InvariantIsing.rotatedEnergy_cavityPermutation line 81
  10. lemma OAI.InvariantIsing.projectedOverlap_spin_isometry line 88
  11. lemma OAI.InvariantIsing.rotatedEnergy_spin_isometry line 95
  12. lemma OAI.InvariantIsing.cavityPerturbationCovariance_spin_isometry line 101