OAI/Analysis/LaughlinGap/PhysicalSpinSpectrum.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Physical Spin Spectrum.

  1. def OAI.LaughlinGap.Spin.physicalThreeFamily line 15
  2. theorem OAI.LaughlinGap.Spin.physicalThreeFamily_orthonormal line 20
  3. def OAI.LaughlinGap.Spin.physicalThreeBasis line 38
  4. lemma OAI.LaughlinGap.Spin.physicalThreeBasis_apply line 51
  5. def OAI.LaughlinGap.Spin.physicalThreeRankOne line 56
  6. theorem OAI.LaughlinGap.Spin.physicalThreeRankOne_positive line 60
  7. def OAI.LaughlinGap.Spin.physicalThreeProjection line 64
  8. lemma OAI.LaughlinGap.Spin.physicalThreeProjection_positive line 68
  9. theorem OAI.LaughlinGap.Spin.physicalTripleGram_spectral line 73
  10. theorem OAI.LaughlinGap.Spin.physicalTripleGram_spin_blocks line 101
  11. lemma OAI.LaughlinGap.Spin.physicalThreeVector_inner line 109
  12. lemma OAI.LaughlinGap.Spin.physicalThreeRankOne_mul line 116
  13. theorem OAI.LaughlinGap.Spin.physicalThreeProjection_idempotent line 128
  14. theorem OAI.LaughlinGap.Spin.physicalThreeProjection_orthogonal line 140
  15. theorem OAI.LaughlinGap.Spin.physicalThreeProjection_wedge_null line 155
  16. def OAI.LaughlinGap.Occupation.physicalSpinThreeLift line 171
  17. theorem OAI.LaughlinGap.Occupation.physicalSpinThreeLift_positive line 176
  18. theorem OAI.LaughlinGap.Occupation.physical_spin_square line 181