OAI/Analysis/LaughlinGap/SpectralBound.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Spectral Bound.

  1. def OAI.LaughlinGap.Chart.splitPair line 16
  2. theorem OAI.LaughlinGap.Chart.splitPair_C line 20
  3. theorem OAI.LaughlinGap.Chart.splitPair_X line 24
  4. theorem OAI.LaughlinGap.Chart.splitPair_difference line 29
  5. theorem OAI.LaughlinGap.Chart.splitPair_rename line 33
  6. lemma OAI.LaughlinGap.Chart.spectatorMonomial_eq line 41
  7. lemma OAI.LaughlinGap.Chart.splitPair_spectatorMonomial line 54
  8. theorem OAI.LaughlinGap.Chart.coeff_splitPair_statePolynomial line 71
  9. theorem OAI.LaughlinGap.Chart.localPairPolynomial_cube_dvd_of_statePolynomial_cube_dvd line 90
  10. theorem OAI.LaughlinGap.Chart.diagonal_derivative_eq_zero_of_cube_dvd line 106
  11. theorem OAI.LaughlinGap.pairMoment_zero line 117
  12. theorem OAI.LaughlinGap.coeff_localPairPolynomial_diagonal_difference_derivative line 130
  13. theorem OAI.LaughlinGap.pair_contraction_eq_zero_of_cubic_divisibility line 143
  14. theorem OAI.LaughlinGap.energy_zero_of_difference_cubes_dvd line 156
  15. theorem OAI.LaughlinGap.Chart.difference_cube_dvd_laughlinPolynomial line 170
  16. theorem OAI.LaughlinGap.energy_scalar_laughlin line 182
  17. theorem OAI.LaughlinGap.energy_laughlin line 190
  18. theorem OAI.LaughlinGap.energy_zero_iff_laughlin line 194
  19. theorem OAI.LaughlinGap.sectorHamiltonian_ker_eq_laughlin line 202
  20. def OAI.LaughlinGap.fallingRatio line 222
  21. def OAI.LaughlinGap.threeBodyGramCoefficient line 225
  22. def OAI.LaughlinGap.threeBodyDimensionRatio line 229
  23. def OAI.LaughlinGap.threeBodyTailTerm line 232
  24. def OAI.LaughlinGap.threeBodyTail line 237
  25. def OAI.LaughlinGap.threeBodyTailStar line 240
  26. lemma OAI.LaughlinGap.fallingRatio_eq_prod line 245
  27. lemma OAI.LaughlinGap.fallingRatio_nonneg line 250
  28. theorem OAI.LaughlinGap.fallingRatio_le_two_thirds_pow line 254
  29. lemma OAI.LaughlinGap.fallingFactor_tendsto line 277
  30. theorem OAI.LaughlinGap.fallingRatio_tendsto line 296
  31. theorem OAI.LaughlinGap.threeBodyGramCoefficient_tendsto line 301
  32. theorem OAI.LaughlinGap.threeBodyDimensionRatio_tendsto line 313
  33. theorem OAI.LaughlinGap.threeBodyBracket_nonneg line 329
  34. theorem OAI.LaughlinGap.threeBodyGramCoefficient_abs_le line 339
  35. lemma OAI.LaughlinGap.threeBodyDimensionRatio_nonneg line 352
  36. lemma OAI.LaughlinGap.threeBodyDimensionRatio_le_two line 358
  37. lemma OAI.LaughlinGap.threeBodyTailTerm_nonneg line 366
  38. theorem OAI.LaughlinGap.threeBodyTailTerm_norm_le line 374
  39. lemma OAI.LaughlinGap.summable_threeBodyTail_majorant line 388
  40. theorem OAI.LaughlinGap.threeBodyTailTerm_tendsto line 394
  41. lemma OAI.LaughlinGap.hasSum_square_quarter line 420
  42. theorem OAI.LaughlinGap.hasSum_threeBodyTailStar_progression line 432
  43. theorem OAI.LaughlinGap.hasSum_threeBodyTailStar line 450
  44. theorem OAI.LaughlinGap.threeBodyTail_tendsto line 465
  45. theorem OAI.LaughlinGap.compression_positive_iff line 496
  46. theorem OAI.LaughlinGap.gram_compression_positive_iff line 510
  47. theorem OAI.LaughlinGap.annihilator_collection_bound line 525
  48. theorem OAI.LaughlinGap.quadratic_perturbation_abs_le line 552
  49. theorem OAI.LaughlinGap.quadratic_perturbation_lower_bound line 562
  50. theorem OAI.LaughlinGap.relative_column_perturbation_bound line 570
  51. theorem OAI.LaughlinGap.relative_column_error_tendsto line 591