OAI/Analysis/LaughlinGap/Basic.lean

GitHub source file

143 declarations, 0 contain sorry, 0 declared as axioms

Basic.

  1. def OAI.LaughlinGap.MainTarget line 15

    Also declared: ComparatorChallenges/LaughlinGap.lean:73 (same declaration text).

  2. theorem OAI.LaughlinGap.distanceToLaughlinSq_le line 20
  3. theorem OAI.LaughlinGap.distanceToLaughlinSq_nonneg line 28
  4. theorem OAI.LaughlinGap.distanceToLaughlinSq_le_normSq line 34
  5. theorem OAI.LaughlinGap.distanceToLaughlinSq_scalar line 38
  6. theorem OAI.LaughlinGap.bracket_ne_zero line 43
  7. theorem OAI.LaughlinGap.laughlinPolynomial_ne_zero line 53
  8. def OAI.LaughlinGap.spinorPermutation line 64
  9. theorem OAI.LaughlinGap.rename_bracket line 68
  10. theorem OAI.LaughlinGap.laughlinPolynomial_rename_swap line 72
  11. theorem OAI.LaughlinGap.monomialExponent_swap line 85
  12. theorem OAI.LaughlinGap.laughlinVector_antisymmetric line 92
  13. def OAI.LaughlinGap.particleWeight line 109
  14. theorem OAI.LaughlinGap.particleWeight_eq line 112
  15. theorem OAI.LaughlinGap.particle_pair_count line 118
  16. theorem OAI.LaughlinGap.bracket_isWeightedHomogeneous line 140
  17. theorem OAI.LaughlinGap.laughlinPolynomial_isWeightedHomogeneous line 150
  18. theorem OAI.LaughlinGap.laughlinPolynomial_support_exponents line 174
  19. theorem OAI.LaughlinGap.laughlinVector_ne_zero line 190
  20. abbrev OAI.LaughlinGap.TensorHilbert line 214
  21. def OAI.LaughlinGap.toTensorHilbert line 216
  22. def OAI.LaughlinGap.laughlinLine line 219
  23. def OAI.LaughlinGap.laughlinProjection line 222
  24. theorem OAI.LaughlinGap.toTensorHilbert_apply line 226
  25. theorem OAI.LaughlinGap.toTensorHilbert_norm_sq line 230
  26. theorem OAI.LaughlinGap.distanceToLaughlinSq_eq_projection line 234
  27. theorem OAI.LaughlinGap.distanceToLaughlinSq_eq_quadraticForm line 264
  28. def OAI.LaughlinGap.euler line 281
  29. theorem OAI.LaughlinGap.coeff_euler line 283
  30. theorem OAI.LaughlinGap.weighted_binomial_polynomial_identity line 289
  31. theorem OAI.LaughlinGap.weighted_binomial_antidiagonal line 310
  32. theorem OAI.LaughlinGap.pairCoefficient_sq line 331
  33. theorem OAI.LaughlinGap.pairCoefficient_swap line 358
  34. theorem OAI.LaughlinGap.sum_fin_pair_on_antidiagonal line 367
  35. theorem OAI.LaughlinGap.pairCoefficient_sum_sq line 389
  36. theorem OAI.LaughlinGap.pairCoefficient_sum_mul_of_ne line 405
  37. abbrev OAI.LaughlinGap.PairHilbert line 415
  38. def OAI.LaughlinGap.pairVector line 417
  39. theorem OAI.LaughlinGap.pairVector_inner line 420
  40. theorem OAI.LaughlinGap.pairVector_orthonormal line 426
  41. def OAI.LaughlinGap.pairChannel line 440
  42. theorem OAI.LaughlinGap.projection_span_orthonormal_eq_sum line 443
  43. theorem OAI.LaughlinGap.pairChannel_projection_eq line 463
  44. theorem OAI.LaughlinGap.pairChannel_projection_norm_sq line 468
  45. def OAI.LaughlinGap.pairSlice line 483
  46. theorem OAI.LaughlinGap.pairAmplitude_eq_inner line 487
  47. theorem OAI.LaughlinGap.energy_eq_sum_pair_projections line 493
  48. theorem OAI.LaughlinGap.kernel_distance_of_square_lower_bound line 517
  49. theorem OAI.LaughlinGap.kernel_projection_bound_of_square_lower_bound line 570
  50. theorem OAI.LaughlinGap.orthonormal_rows_coordinate_sq_le line 586
  51. theorem OAI.LaughlinGap.orthonormal_rows_sq_le line 603
  52. def OAI.LaughlinGap.OrbitalTriple line 611
  53. def OAI.LaughlinGap.orbitalTripleEquiv line 614
  54. instance OAI.LaughlinGap.(instance at line 640) line 640
  55. theorem OAI.LaughlinGap.orbitalTriple_card line 643
  56. theorem OAI.LaughlinGap.retained_orbitalTriple_count line 650
  57. def OAI.LaughlinGap.gammaStar line 655
  58. theorem OAI.LaughlinGap.final_margin_arithmetic line 657
  59. theorem OAI.LaughlinGap.one_div_twenty_five_lt_gammaStar line 662
  60. theorem OAI.LaughlinGap.bracket_irreducible line 665
  61. theorem OAI.LaughlinGap.bracket_not_dvd line 704
  62. theorem OAI.LaughlinGap.laughlinPolynomial_dvd_of_bracket_cubes_dvd line 726
  63. theorem OAI.LaughlinGap.isHomogeneous_of_particle_homogeneous line 745
  64. theorem OAI.LaughlinGap.laughlinPolynomial_totalDegree line 758
  65. theorem OAI.LaughlinGap.eq_scalar_laughlin_of_bracket_cubes_dvd line 763
  66. def OAI.LaughlinGap.tensorMonomialScale line 782
  67. theorem OAI.LaughlinGap.tensorMonomialScale_pos line 785
  68. def OAI.LaughlinGap.statePolynomial line 791
  69. theorem OAI.LaughlinGap.monomialExponent_injective line 796
  70. theorem OAI.LaughlinGap.coeff_statePolynomial line 805
  71. theorem OAI.LaughlinGap.coeff_statePolynomial_of_not_grid line 810
  72. theorem OAI.LaughlinGap.statePolynomial_injective line 816
  73. theorem OAI.LaughlinGap.statePolynomial_isWeightedHomogeneous line 825
  74. theorem OAI.LaughlinGap.statePolynomial_smul line 836
  75. theorem OAI.LaughlinGap.statePolynomial_laughlinVector line 849
  76. theorem OAI.LaughlinGap.state_eq_scalar_laughlin_of_bracket_cubes_dvd line 866
  77. theorem OAI.LaughlinGap.pairAmplitude_eq_of_spectators_eq line 875
  78. theorem OAI.LaughlinGap.pairAmplitude_anchor line 893
  79. theorem OAI.LaughlinGap.energy_eq_zero_iff line 901
  80. def OAI.LaughlinGap.antisymmetricSubmodule line 937
  81. abbrev OAI.LaughlinGap.SectorHilbert line 949
  82. abbrev OAI.LaughlinGap.ContractionIndex line 951
  83. def OAI.LaughlinGap.pairContractions line 954
  84. theorem OAI.LaughlinGap.pairContractions_norm_sq line 976
  85. def OAI.LaughlinGap.sectorContractions line 999
  86. def OAI.LaughlinGap.sectorHamiltonian line 1003
  87. theorem OAI.LaughlinGap.sectorHamiltonian_positive line 1008
  88. theorem OAI.LaughlinGap.sectorHamiltonian_inner line 1012
  89. theorem OAI.LaughlinGap.sectorHamiltonian_eq_zero_iff line 1020
  90. def OAI.LaughlinGap.Chart.difference line 1040
  91. def OAI.LaughlinGap.Chart.diagonal line 1042
  92. theorem OAI.LaughlinGap.Chart.difference_dvd_sub_diagonal line 1045
  93. theorem OAI.LaughlinGap.Chart.difference_dvd_of_diagonal_eq_zero line 1061
  94. lemma OAI.LaughlinGap.Chart.difference_ne_zero line 1065
  95. lemma OAI.LaughlinGap.Chart.diagonal_difference line 1072
  96. lemma OAI.LaughlinGap.Chart.diagonal_rename_swap line 1078
  97. theorem OAI.LaughlinGap.Chart.diagonal_eq_zero_of_antisymmetric line 1092
  98. lemma OAI.LaughlinGap.Chart.rename_difference_swap line 1105
  99. theorem OAI.LaughlinGap.Chart.difference_cube_dvd line 1109
  100. def OAI.LaughlinGap.pairWeightScale line 1136
  101. theorem OAI.LaughlinGap.pairWeightScale_pos line 1139
  102. theorem OAI.LaughlinGap.pairCoefficient_binomial line 1146
  103. def OAI.LaughlinGap.pairMoment line 1170
  104. theorem OAI.LaughlinGap.pair_contraction_eq_moment line 1176
  105. def OAI.LaughlinGap.localPairPolynomial line 1191
  106. theorem OAI.LaughlinGap.localPairPolynomial_antisymmetric line 1196
  107. theorem OAI.LaughlinGap.diagonal_difference_derivative_monomial line 1213
  108. theorem OAI.LaughlinGap.pairMoment_eq_zero_of_contractions line 1222
  109. theorem OAI.LaughlinGap.localPairPolynomial_diagonal_difference_derivative line 1242
  110. theorem OAI.LaughlinGap.localPairPolynomial_cubic_divisibility line 1265
  111. def OAI.LaughlinGap.Chart.spinorChart line 1291
  112. def OAI.LaughlinGap.Chart.exponent line 1295
  113. def OAI.LaughlinGap.Chart.statePolynomial line 1298
  114. def OAI.LaughlinGap.Chart.laughlinPolynomial line 1301
  115. lemma OAI.LaughlinGap.Chart.monomial_as_prod line 1304
  116. lemma OAI.LaughlinGap.Chart.exponent_injective line 1309
  117. theorem OAI.LaughlinGap.Chart.coeff_statePolynomial line 1315
  118. theorem OAI.LaughlinGap.Chart.statePolynomial_injective line 1320
  119. theorem OAI.LaughlinGap.Chart.statePolynomial_smul line 1328
  120. theorem OAI.LaughlinGap.Chart.spinorChart_statePolynomial line 1340
  121. theorem OAI.LaughlinGap.Chart.spinorChart_bracket line 1349
  122. theorem OAI.LaughlinGap.Chart.spinorChart_laughlinPolynomial line 1353
  123. theorem OAI.LaughlinGap.Chart.statePolynomial_laughlinVector line 1358
  124. theorem OAI.LaughlinGap.Chart.statePolynomial_degreeOf_le line 1363
  125. abbrev OAI.LaughlinGap.Chart.PairSpectators line 1376
  126. def OAI.LaughlinGap.Chart.pairConfigurationEquiv line 1379
  127. lemma OAI.LaughlinGap.Chart.prod_update_pair line 1402
  128. lemma OAI.LaughlinGap.Chart.monomial_as_normalized_prod line 1417
  129. def OAI.LaughlinGap.Chart.spectatorMonomial line 1424
  130. theorem OAI.LaughlinGap.Chart.statePolynomial_pair_decomposition line 1429
  131. lemma OAI.LaughlinGap.Chart.update_pair_swap line 1456
  132. theorem OAI.LaughlinGap.Chart.difference_cube_dvd_statePolynomial_of_energy_zero line 1468
  133. theorem OAI.LaughlinGap.Chart.difference_irreducible line 1486
  134. theorem OAI.LaughlinGap.Chart.difference_not_dvd line 1499
  135. theorem OAI.LaughlinGap.Chart.laughlinPolynomial_ne_zero line 1518
  136. theorem OAI.LaughlinGap.Chart.laughlinPolynomial_dvd_of_difference_cubes_dvd line 1528
  137. lemma OAI.LaughlinGap.Chart.difference_degreeOf line 1546
  138. theorem OAI.LaughlinGap.Chart.laughlinPolynomial_degreeOf line 1565
  139. lemma OAI.LaughlinGap.Chart.eq_constant_of_degreeOf_eq_zero line 1584
  140. theorem OAI.LaughlinGap.Chart.eq_scalar_laughlin_of_difference_cubes_dvd line 1602
  141. theorem OAI.LaughlinGap.energy_zero_imp_laughlin line 1621
  142. theorem OAI.LaughlinGap.laughlin_gap_of_sector_square_estimate line 1630
  143. theorem OAI.LaughlinGap.mainTarget_of_uniform_sector_square_estimate line 1654