OAI/Analysis/LaughlinGap/PairEnergy.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

Pair Energy.

  1. def OAI.LaughlinGap.Occupation.localPair line 16
  2. def OAI.LaughlinGap.Occupation.localPairStar line 19
  3. def OAI.LaughlinGap.Occupation.localDelta line 22
  4. def OAI.LaughlinGap.Occupation.localDeltaInv line 25
  5. lemma OAI.LaughlinGap.Occupation.localPair_eq_factored line 28
  6. theorem OAI.LaughlinGap.Occupation.localPair_conjugation line 40
  7. theorem OAI.LaughlinGap.Occupation.localFour_conjugation line 49
  8. theorem OAI.LaughlinGap.Occupation.localDelta_norm_le line 61
  9. theorem OAI.LaughlinGap.Occupation.localDelta_tendsto line 65
  10. theorem OAI.LaughlinGap.Occupation.localDeltaInv_tendsto line 71
  11. theorem OAI.LaughlinGap.Occupation.localDelta_mul_inv line 75
  12. def OAI.LaughlinGap.Occupation.localPairEnergyStar line 82
  13. def OAI.LaughlinGap.Occupation.localPairEnergy line 85
  14. theorem OAI.LaughlinGap.Occupation.localPairEnergy_transfer line 88
  15. def OAI.LaughlinGap.Occupation.joinEquiv line 104
  16. def OAI.LaughlinGap.Occupation.join line 107
  17. lemma OAI.LaughlinGap.Occupation.join_eq_map line 110
  18. lemma OAI.LaughlinGap.Occupation.mem_join_left line 113
  19. lemma OAI.LaughlinGap.Occupation.mem_join_right line 118
  20. lemma OAI.LaughlinGap.Occupation.join_card line 123
  21. lemma OAI.LaughlinGap.Occupation.prefix_ne_suffix line 126
  22. lemma OAI.LaughlinGap.Occupation.join_erase_left line 134
  23. lemma OAI.LaughlinGap.Occupation.join_insert_left line 142
  24. lemma OAI.LaughlinGap.Occupation.join_flip_left line 150
  25. lemma OAI.LaughlinGap.Occupation.join_filter_prefix line 156
  26. theorem OAI.LaughlinGap.Occupation.sign_join_left line 172
  27. def OAI.LaughlinGap.Occupation.slice line 176
  28. lemma OAI.LaughlinGap.Occupation.slice_apply line 181
  29. theorem OAI.LaughlinGap.Occupation.norm_sq_eq_sum_slice line 184
  30. lemma OAI.LaughlinGap.Occupation.inner_eq_sum_slice line 191
  31. theorem OAI.LaughlinGap.Occupation.slice_transition line 198
  32. def OAI.LaughlinGap.Occupation.extendLocal line 204
  33. lemma OAI.LaughlinGap.Occupation.slice_extendLocal line 211
  34. lemma OAI.LaughlinGap.Occupation.eq_of_slice_eq line 216
  35. theorem OAI.LaughlinGap.Occupation.extendLocal_transition line 222
  36. theorem OAI.LaughlinGap.Occupation.extendLocal_one line 230
  37. theorem OAI.LaughlinGap.Occupation.extendLocal_add line 238
  38. theorem OAI.LaughlinGap.Occupation.extendLocal_mul line 246
  39. theorem OAI.LaughlinGap.Occupation.extendLocal_quadraticForm_le line 254
  40. theorem OAI.LaughlinGap.Occupation.extendLocal_energy_le line 261
  41. theorem OAI.LaughlinGap.Occupation.extendLocal_zero line 269
  42. theorem OAI.LaughlinGap.Occupation.extendLocal_smul line 277
  43. theorem OAI.LaughlinGap.Occupation.extendLocal_adjoint line 285
  44. def OAI.LaughlinGap.Occupation.extendLocalHom line 293
  45. theorem OAI.LaughlinGap.Occupation.extendLocal_positive line 305
  46. def OAI.LaughlinGap.matrixLift line 325
  47. def OAI.LaughlinGap.contractCombination line 331
  48. theorem OAI.LaughlinGap.matrixLift_rankOne line 334
  49. theorem OAI.LaughlinGap.matrixLift_positive line 344
  50. theorem OAI.LaughlinGap.matrixLift_columns line 354
  51. theorem OAI.LaughlinGap.matrixLift_gram_positive line 375
  52. abbrev OAI.LaughlinGap.Occupation.BasisLabel line 393
  53. abbrev OAI.LaughlinGap.Occupation.ExteriorCoordinates line 395
  54. def OAI.LaughlinGap.Occupation.basisContraction line 397
  55. def OAI.LaughlinGap.Occupation.exteriorContraction line 400
  56. def OAI.LaughlinGap.Occupation.exteriorLift line 403
  57. theorem OAI.LaughlinGap.Occupation.exteriorLift_rankOne line 407
  58. theorem OAI.LaughlinGap.Occupation.exteriorLift_positive line 412
  59. def OAI.LaughlinGap.Occupation.Homogeneous line 422
  60. lemma OAI.LaughlinGap.Occupation.annihilation_homogeneous line 425
  61. lemma OAI.LaughlinGap.Occupation.annihilation_eq_zero_of_degree_zero line 434
  62. lemma OAI.LaughlinGap.Occupation.word_homogeneous line 444
  63. lemma OAI.LaughlinGap.Occupation.word_eq_zero_of_degree_lt line 451
  64. lemma OAI.LaughlinGap.Occupation.word_apply_empty_sorted line 461
  65. lemma OAI.LaughlinGap.Occupation.basisContraction_apply_empty line 478
  66. def OAI.LaughlinGap.Occupation.vacuum line 483
  67. lemma OAI.LaughlinGap.Occupation.vacuum_apply line 485
  68. lemma OAI.LaughlinGap.Occupation.vacuum_norm line 489
  69. lemma OAI.LaughlinGap.Occupation.degree_zero_eq_vacuum line 492
  70. lemma OAI.LaughlinGap.Occupation.basisContraction_degree line 500
  71. lemma OAI.LaughlinGap.Occupation.basisContraction_eq_zero_of_degree_lt line 506
  72. def OAI.LaughlinGap.Occupation.sectorInclusion line 510
  73. lemma OAI.LaughlinGap.Occupation.sectorInclusion_apply line 519
  74. lemma OAI.LaughlinGap.Occupation.sectorInclusion_apply_label line 523
  75. lemma OAI.LaughlinGap.Occupation.sectorInclusion_homogeneous line 527
  76. lemma OAI.LaughlinGap.Occupation.basisContraction_sectorInclusion line 530
  77. theorem OAI.LaughlinGap.Occupation.exteriorContraction_sectorInclusion line 534
  78. theorem OAI.LaughlinGap.Occupation.exteriorContraction_eq_zero_of_degree_lt line 541
  79. theorem OAI.LaughlinGap.Occupation.exteriorLift_eq_zero_of_degree_lt line 548
  80. theorem OAI.LaughlinGap.Occupation.exteriorLift_inner_sector line 555