OAI/Analysis/LaughlinGap/SpinWork.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Spin Work.

  1. def OAI.LaughlinGap.Spin.highestFactor line 14
  2. def OAI.LaughlinGap.Spin.highestWeight line 17
  3. def OAI.LaughlinGap.Spin.highestNormalization line 20
  4. def OAI.LaughlinGap.Spin.highestCoefficient line 23
  5. lemma OAI.LaughlinGap.Spin.highestFactor_pos line 27
  6. lemma OAI.LaughlinGap.Spin.highestWeight_nonneg line 35
  7. lemma OAI.LaughlinGap.Spin.highestWeight_zero line 43
  8. lemma OAI.LaughlinGap.Spin.highestNormalization_pos line 46
  9. lemma OAI.LaughlinGap.Spin.highestCoefficient_sq line 51
  10. theorem OAI.LaughlinGap.Spin.highestCoefficient_sum_sq line 58
  11. lemma OAI.LaughlinGap.Spin.highestCoefficient_eq_zero line 64
  12. lemma OAI.LaughlinGap.Spin.highestWeight_step line 68
  13. theorem OAI.LaughlinGap.Spin.highestCoefficient_raising line 82
  14. theorem OAI.LaughlinGap.Spin.highestFactor_tendsto line 98
  15. theorem OAI.LaughlinGap.Spin.highestWeight_tendsto line 119
  16. theorem OAI.LaughlinGap.Spin.highestNormalization_tendsto line 128
  17. theorem OAI.LaughlinGap.Spin.highestCoefficient_tendsto_ratio line 140
  18. lemma OAI.LaughlinGap.Spin.sqrt_nat_pow line 150
  19. def OAI.LaughlinGap.Spin.limitingHighestCoefficient line 156
  20. lemma OAI.LaughlinGap.Spin.highest_ratio_eq line 159
  21. theorem OAI.LaughlinGap.Spin.highestCoefficient_tendsto line 176
  22. lemma OAI.LaughlinGap.Spin.firstAffineRatio_tendsto line 184
  23. lemma OAI.LaughlinGap.Spin.secondAffineRatio_tendsto line 200
  24. lemma OAI.LaughlinGap.Spin.firstSqrtRatio_tendsto line 216
  25. lemma OAI.LaughlinGap.Spin.secondSqrtRatio_tendsto line 228
  26. def OAI.LaughlinGap.Spin.firstLoweringCoefficient line 241
  27. def OAI.LaughlinGap.Spin.secondLoweringCoefficient line 245
  28. lemma OAI.LaughlinGap.Spin.firstLoweringCoefficient_tendsto line 249
  29. lemma OAI.LaughlinGap.Spin.secondLoweringCoefficient_tendsto line 265
  30. def OAI.LaughlinGap.Spin.coupledCoefficient line 286
  31. def OAI.LaughlinGap.Spin.limitingCoupledCoefficient line 293
  32. lemma OAI.LaughlinGap.Spin.coupledCoefficient_eq_zero line 301
  33. lemma OAI.LaughlinGap.Spin.limitingCoupledCoefficient_eq_zero line 308
  34. theorem OAI.LaughlinGap.Spin.coupledCoefficient_tendsto line 316
  35. def OAI.LaughlinGap.Spin.couplingPolynomial line 348
  36. def OAI.LaughlinGap.Spin.monomialWeight line 352
  37. lemma OAI.LaughlinGap.Spin.monomialWeight_pos line 355
  38. lemma OAI.LaughlinGap.Spin.binomial_linear_coeff line 360
  39. lemma OAI.LaughlinGap.Spin.monomialWeight_choose line 369
  40. lemma OAI.LaughlinGap.Spin.highestCoefficient_eq_polynomial line 387
  41. lemma OAI.LaughlinGap.Spin.couplingPolynomial_step line 404
  42. lemma OAI.LaughlinGap.Spin.couplingPolynomial_natDegree_le line 421
  43. lemma OAI.LaughlinGap.Spin.couplingPolynomial_coeff_eq_zero line 435
  44. lemma OAI.LaughlinGap.Spin.monomialWeight_first line 439
  45. lemma OAI.LaughlinGap.Spin.monomialWeight_second line 450
  46. lemma OAI.LaughlinGap.Spin.couplingPolynomial_step_coeff line 462
  47. theorem OAI.LaughlinGap.Spin.limitingCoupledCoefficient_eq_polynomial line 472
  48. theorem OAI.LaughlinGap.Spin.coupledCoefficient_tendsto_polynomial line 503
  49. lemma OAI.LaughlinGap.Spin.ratio_to_total_ratio line 513
  50. theorem OAI.LaughlinGap.Spin.fixed_deficit_coupling_limit line 531