OAI/Probability/SLE/Angle/AngleRecurrenceCoefficients.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The coefficients needed for the monic three-term recurrence, including a uniform positive lower bound for its squared-norm ratio.

  1. lemma OAI.SLEExactGauge.angleEigenPolynomial_penultimate line 12
  2. lemma OAI.SLEExactGauge.angleEigenPolynomial_second_coeff line 18
  3. def OAI.SLEExactGauge.angleRecurrenceCoefficient line 31
  4. lemma OAI.SLEExactGauge.angleRecurrenceCoefficient_zero line 34
  5. lemma OAI.SLEExactGauge.angleRecurrenceCoefficient_sub line 45
  6. lemma OAI.SLEExactGauge.angleRecurrenceCoefficient_lower line 57
  7. lemma OAI.SLEExactGauge.angleRecurrenceCoefficient_pos line 67