OAI/Analysis/LaughlinGap/FourSpin.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Four Spin.

  1. lemma OAI.LaughlinGap.Spin.orbitalPair_orthonormal_twice line 15
  2. def OAI.LaughlinGap.Spin.pairFactorInclusion line 23
  3. lemma OAI.LaughlinGap.Spin.pairFactorInclusion_isometry line 28
  4. lemma OAI.LaughlinGap.Spin.pairFactorInclusion_orthogonal line 52
  5. def OAI.LaughlinGap.Spin.fourBodyCoupled line 78
  6. def OAI.LaughlinGap.Spin.fourBodyCoefficient line 83
  7. theorem OAI.LaughlinGap.Spin.fourBodyCoupled_coefficient line 89
  8. lemma OAI.LaughlinGap.Spin.fourBodyCoupled_norm_sq line 120
  9. lemma OAI.LaughlinGap.Spin.fourBodyCoupled_orthogonal line 127
  10. abbrev OAI.LaughlinGap.Spin.FourCopy line 132
  11. def OAI.LaughlinGap.Spin.fourBodyHighestFamily line 134
  12. theorem OAI.LaughlinGap.Spin.fourBodyHighestFamily_orthonormal line 138
  13. def OAI.LaughlinGap.Spin.balancedCouplingCoefficient line 154
  14. def OAI.LaughlinGap.Spin.fourBodyCoefficientStar line 158
  15. lemma OAI.LaughlinGap.Spin.affine_twice_spin_tendsto line 164
  16. lemma OAI.LaughlinGap.Spin.affine_twice_spin_ratio_tendsto line 170
  17. lemma OAI.LaughlinGap.Spin.equal_spin_ratio_tendsto line 187
  18. lemma OAI.LaughlinGap.Spin.balanced_coupling_limit line 193
  19. theorem OAI.LaughlinGap.Spin.fourBodyCoefficient_tendsto line 203