OAI/Probability/SLE/Angle/AnglePolynomialCoefficients.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact triangular coefficient relation for the cosine generator. This is the recurrence used to construct its polynomial eigenfunctions.

  1. lemma OAI.SLEExactGauge.anglePolynomialGenerator_coeff line 12
  2. lemma OAI.SLEExactGauge.anglePolynomial_eigen_iff_coeff line 32