OAI/Analysis/LaughlinFock/OscillatorLimit.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Oscillator Limit.

  1. def OAI.LaughlinFock.monomialWeight line 15
  2. def OAI.LaughlinFock.monomialCoefficient line 18
  3. theorem OAI.LaughlinFock.monomialWeight_left line 21
  4. theorem OAI.LaughlinFock.monomialWeight_right line 27
  5. theorem OAI.LaughlinFock.monomialCoefficient_linear line 40
  6. def OAI.LaughlinFock.couplingPolynomial line 73
  7. def OAI.LaughlinFock.polynomialCouplingCoefficient line 76
  8. theorem OAI.LaughlinFock.couplingPolynomial_degree line 80
  9. theorem OAI.LaughlinFock.polynomialCouplingCoefficient_zero line 96
  10. theorem OAI.LaughlinFock.couplingPolynomial_succ line 101
  11. theorem OAI.LaughlinFock.coefficient_scale_succ line 108
  12. theorem OAI.LaughlinFock.polynomialCouplingCoefficient_succ line 114
  13. theorem OAI.LaughlinFock.coeff_linear_pow line 125
  14. theorem OAI.LaughlinFock.sqrt_nat_pow line 130
  15. theorem OAI.LaughlinFock.binomial_monomialWeight line 138
  16. theorem OAI.LaughlinFock.polynomialCouplingCoefficient_top line 156
  17. theorem OAI.LaughlinFock.oscillatorCoefficient_eq_polynomial line 174
  18. theorem OAI.LaughlinFock.coupledCoefficient_polynomial_limit line 186