OAI/Probability/SLE/Angle/AngleEigenPolynomials.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Monic polynomial eigenfunctions for the centered cosine generator. The coefficients are solved downwards in degree, with no choice of an auxiliary stochastic process or additional published input.

  1. def OAI.SLEExactGauge.angleEigenCoefficient line 13
  2. lemma OAI.SLEExactGauge.angleEigenCoefficient_top line 21
  3. lemma OAI.SLEExactGauge.angleEigenCoefficient_above line 24
  4. lemma OAI.SLEExactGauge.angleEigenCoefficient_recurrence line 28
  5. def OAI.SLEExactGauge.angleEigenPolynomial line 43
  6. lemma OAI.SLEExactGauge.angleEigenPolynomial_coeff line 46
  7. lemma OAI.SLEExactGauge.angleEigenPolynomial_natDegree_le line 53
  8. lemma OAI.SLEExactGauge.angleEigenPolynomial_monic line 59
  9. lemma OAI.SLEExactGauge.angleEigenPolynomial_natDegree line 63
  10. lemma OAI.SLEExactGauge.angleEigenPolynomial_eigen line 69