OAI/Analysis/LaughlinGap/Occupation.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

Occupation.

  1. abbrev OAI.LaughlinGap.Occupation.Hilbert line 14
  2. def OAI.LaughlinGap.Occupation.flip line 16
  3. lemma OAI.LaughlinGap.Occupation.flip_of_mem line 23
  4. lemma OAI.LaughlinGap.Occupation.flip_of_not_mem line 26
  5. lemma OAI.LaughlinGap.Occupation.flip_flip line 29
  6. lemma OAI.LaughlinGap.Occupation.mem_flip_self line 32
  7. lemma OAI.LaughlinGap.Occupation.mem_flip_other line 36
  8. lemma OAI.LaughlinGap.Occupation.flip_comm line 40
  9. def OAI.LaughlinGap.Occupation.sign line 53
  10. lemma OAI.LaughlinGap.Occupation.sign_norm line 56
  11. lemma OAI.LaughlinGap.Occupation.sign_star line 59
  12. lemma OAI.LaughlinGap.Occupation.sign_sq line 62
  13. lemma OAI.LaughlinGap.Occupation.sign_insert line 67
  14. lemma OAI.LaughlinGap.Occupation.sign_flip line 73
  15. lemma OAI.LaughlinGap.Occupation.sign_flip_self line 85
  16. lemma OAI.LaughlinGap.Occupation.sign_conj line 88
  17. lemma OAI.LaughlinGap.Occupation.sign_erase_self line 92
  18. lemma OAI.LaughlinGap.Occupation.sign_insert_self line 96
  19. def OAI.LaughlinGap.Occupation.transition line 100
  20. lemma OAI.LaughlinGap.Occupation.transition_apply line 110
  21. abbrev OAI.LaughlinGap.Occupation.annihilation line 114
  22. abbrev OAI.LaughlinGap.Occupation.creation line 116
  23. theorem OAI.LaughlinGap.Occupation.transition_norm_le line 118
  24. theorem OAI.LaughlinGap.Occupation.transition_adjoint line 132
  25. theorem OAI.LaughlinGap.Occupation.transition_anticommute_of_ne line 144
  26. theorem OAI.LaughlinGap.Occupation.transition_square line 159
  27. theorem OAI.LaughlinGap.Occupation.transition_complement line 165
  28. theorem OAI.LaughlinGap.Occupation.annihilation_creation_CAR line 173
  29. lemma OAI.LaughlinGap.Occupation.annihilation_adjoint line 182
  30. lemma OAI.LaughlinGap.Occupation.creation_adjoint line 185
  31. lemma OAI.LaughlinGap.Occupation.adjoint_mul line 188
  32. theorem OAI.LaughlinGap.Occupation.annihilation_creation line 191
  33. theorem OAI.LaughlinGap.Occupation.annihilation_creation_mul line 195
  34. theorem OAI.LaughlinGap.Occupation.pair_normal_order line 202
  35. theorem OAI.LaughlinGap.Occupation.auxiliary_normal_order line 220
  36. def OAI.LaughlinGap.Occupation.auxiliaryRow line 229
  37. theorem OAI.LaughlinGap.Occupation.auxiliaryRow_square line 234
  38. theorem OAI.LaughlinGap.Occupation.double_annihilation_norm_le line 260
  39. def OAI.LaughlinGap.Occupation.weight line 264
  40. def OAI.LaughlinGap.Occupation.diagonal line 267
  41. lemma OAI.LaughlinGap.Occupation.diagonal_apply line 272
  42. lemma OAI.LaughlinGap.Occupation.weight_nonneg line 275
  43. lemma OAI.LaughlinGap.Occupation.weight_le_one line 278
  44. theorem OAI.LaughlinGap.Occupation.diagonal_norm_le line 282
  45. theorem OAI.LaughlinGap.Occupation.diagonal_one line 292
  46. theorem OAI.LaughlinGap.Occupation.diagonal_comp line 296
  47. theorem OAI.LaughlinGap.Occupation.diagonal_comp_inv line 301
  48. theorem OAI.LaughlinGap.Occupation.annihilation_diagonal line 309
  49. def OAI.LaughlinGap.Occupation.word line 317
  50. theorem OAI.LaughlinGap.Occupation.word_diagonal line 321
  51. def OAI.LaughlinGap.Occupation.pairAnnihilator line 331
  52. lemma OAI.LaughlinGap.Occupation.pairAnnihilator_smul_real line 335
  53. theorem OAI.LaughlinGap.Occupation.pairAnnihilator_diagonal line 340
  54. theorem OAI.LaughlinGap.Occupation.pairAnnihilator_conjugation line 360
  55. theorem OAI.LaughlinGap.Occupation.fourAnnihilator_conjugation line 374
  56. theorem OAI.LaughlinGap.Occupation.pairAnnihilator_energy_transfer line 390
  57. def OAI.LaughlinGap.orbitalDiagonalFactor line 409
  58. def OAI.LaughlinGap.pairRescalingFactor line 412
  59. def OAI.LaughlinGap.sphericalExteriorPairCoefficient line 415
  60. def OAI.LaughlinGap.limitingExteriorPairCoefficient line 422
  61. lemma OAI.LaughlinGap.orbitalDiagonalFactor_nonneg line 428
  62. lemma OAI.LaughlinGap.orbitalDiagonalFactor_pos line 431
  63. lemma OAI.LaughlinGap.orbitalDiagonalFactor_le_one line 438
  64. lemma OAI.LaughlinGap.pairRescalingFactor_nonneg line 445
  65. lemma OAI.LaughlinGap.one_le_pairRescalingFactor line 448
  66. theorem OAI.LaughlinGap.sphericalExteriorPairCoefficient_factor line 457
  67. lemma OAI.LaughlinGap.normalizedFallingFactorial_eq_prod line 493
  68. lemma OAI.LaughlinGap.normalizedFallingFactor_tendsto line 498
  69. theorem OAI.LaughlinGap.orbitalDiagonalFactor_tendsto line 509
  70. lemma OAI.LaughlinGap.pairRescalingFactor_sq_eq_prod line 515
  71. lemma OAI.LaughlinGap.rescalingFactor_tendsto line 520
  72. theorem OAI.LaughlinGap.pairRescalingFactor_tendsto line 535
  73. theorem OAI.LaughlinGap.sphericalExteriorPairCoefficient_tendsto line 541
  74. def OAI.LaughlinGap.Occupation.diagonalCLM line 557
  75. lemma OAI.LaughlinGap.Occupation.diagonalCLM_apply line 560
  76. lemma OAI.LaughlinGap.Occupation.diagonalCLM_eq_matrix line 563
  77. theorem OAI.LaughlinGap.Occupation.diagonalCLM_tendsto line 570
  78. lemma OAI.LaughlinGap.Occupation.diagonalCLM_one line 592
  79. theorem OAI.LaughlinGap.Occupation.diagonalCLM_inv_tendsto_one line 596