OAI/Analysis/LaughlinGap/WedgeIdentification.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Wedge Identification.

  1. lemma OAI.LaughlinGap.Occupation.annihilation_vacuum line 15
  2. lemma OAI.LaughlinGap.Occupation.annihilation_creation_apply line 20
  3. lemma OAI.LaughlinGap.Occupation.annihilation_creation_vacuum line 28
  4. lemma OAI.LaughlinGap.Occupation.double_creation_vacuum line 32
  5. lemma OAI.LaughlinGap.Occupation.triple_creation_vacuum line 40
  6. def OAI.LaughlinGap.Occupation.orbitalDelta line 55
  7. lemma OAI.LaughlinGap.Occupation.orbitalDelta_smul line 57
  8. lemma OAI.LaughlinGap.Occupation.annihilation_creation_vacuum_delta line 61
  9. lemma OAI.LaughlinGap.Occupation.double_creation_vacuum_delta line 65
  10. lemma OAI.LaughlinGap.Occupation.triple_creation_vacuum_delta line 71
  11. lemma OAI.LaughlinGap.Occupation.word_three_creation_vacuum line 78
  12. lemma OAI.LaughlinGap.Occupation.sum_increasing_pairs_add line 92
  13. lemma OAI.LaughlinGap.Occupation.pairContraction_adjoint_apply line 113
  14. lemma OAI.LaughlinGap.Occupation.pairContraction_ordered_adjoint line 120
  15. lemma OAI.LaughlinGap.Occupation.sum_orbitalDelta_mul line 150
  16. lemma OAI.LaughlinGap.Occupation.sum_mul_orbitalDelta line 154
  17. lemma OAI.LaughlinGap.Occupation.pair_times_three_determinant line 158
  18. lemma OAI.LaughlinGap.Occupation.rawReadout_three_pair line 189
  19. lemma OAI.LaughlinGap.Occupation.normalizedReadout_three_pair line 211
  20. lemma OAI.LaughlinGap.Occupation.normalizedReadout_inner_sector line 229
  21. def OAI.LaughlinGap.Spin.tupleThreeEquiv line 245
  22. def OAI.LaughlinGap.Spin.spinPairForms line 251
  23. lemma OAI.LaughlinGap.Spin.normalizedReadout_spin_three_column line 254
  24. lemma OAI.LaughlinGap.Spin.spinTripleGram_entry line 276
  25. lemma OAI.LaughlinGap.Spin.linearMap_apply_coordinates line 304
  26. theorem OAI.LaughlinGap.Spin.spinTripleGram_mulVec_real line 317
  27. theorem OAI.LaughlinGap.Spin.spinTripleGram_eigenvalue line 326
  28. def OAI.LaughlinGap.Spin.physicalPairIndexEquiv line 344
  29. def OAI.LaughlinGap.Spin.physicalThreeIndexEquiv line 347
  30. lemma OAI.LaughlinGap.Spin.spinPairForms_physical_index line 351
  31. lemma OAI.LaughlinGap.Spin.spinTripleWedge_physical_index line 354
  32. lemma OAI.LaughlinGap.Spin.physicalTripleGram_entry line 359
  33. theorem OAI.LaughlinGap.Spin.physicalTripleGram_mulVec_real line 368
  34. def OAI.LaughlinGap.Spin.physicalThreeVector line 381
  35. theorem OAI.LaughlinGap.Spin.physicalTripleGram_eigenvalue line 385
  36. theorem OAI.LaughlinGap.Spin.physicalTripleWedge_null line 396