OAI/Analysis/LaughlinGap/PhysicalAveraging.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Physical Averaging.

  1. def OAI.LaughlinGap.RealOccupation.fockLowering line 17
  2. def OAI.LaughlinGap.RealOccupation.physicalPair line 20
  3. lemma OAI.LaughlinGap.RealOccupation.complexify_physicalPair line 23
  4. lemma OAI.LaughlinGap.RealOccupation.physicalPair_embedding line 33
  5. theorem OAI.LaughlinGap.RealOccupation.physicalPair_covariant line 41
  6. def OAI.LaughlinGap.RealOccupation.physicalHamiltonian line 52
  7. lemma OAI.LaughlinGap.RealOccupation.complexify_physicalHamiltonian line 55
  8. lemma OAI.LaughlinGap.RealOccupation.lift_identity line 61
  9. lemma OAI.LaughlinGap.RealOccupation.physicalPair_sum line 65
  10. lemma OAI.LaughlinGap.RealOccupation.physicalPair_single line 71
  11. lemma OAI.LaughlinGap.RealOccupation.physicalPair_single_val line 84
  12. lemma OAI.LaughlinGap.RealOccupation.physicalHamiltonian_mem line 90
  13. def OAI.LaughlinGap.RealOccupation.physicalTriple line 100
  14. theorem OAI.LaughlinGap.RealOccupation.physicalTriple_covariant line 104