OAI/Analysis/Laughlin/Polynomial/OscillatorPolynomial.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Laughlin.Spin.sqrtFactorial line 10
  2. def OAI.Laughlin.Spin.monomialNormFactor line 11
  3. def OAI.Laughlin.Spin.couplingPolynomial line 13
  4. def OAI.Laughlin.Spin.couplingPolynomialCoefficient line 16
  5. theorem OAI.Laughlin.Spin.sqrtFactorial_pos line 20
  6. theorem OAI.Laughlin.Spin.sqrtFactorial_succ line 24
  7. theorem OAI.Laughlin.Spin.sqrt_choose_factorial line 30
  8. theorem OAI.Laughlin.Spin.couplingPolynomial_base_coeff line 45
  9. theorem OAI.Laughlin.Spin.couplingPolynomial_base_normalized line 54
  10. theorem OAI.Laughlin.Spin.couplingPolynomial_succ_coeff line 69
  11. theorem OAI.Laughlin.Spin.couplingPolynomial_coeff_off line 83