OAI/Probability/SLE/Angle/AngleEigenDifferential.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The polynomial eigenfunctions satisfy the actual centered angular generator equation, with time measured by logarithmic conformal radius.

  1. def OAI.SLEExactGauge.anglePolynomialTest line 12
  2. lemma OAI.SLEExactGauge.anglePolynomialTest_hasDerivAt line 14
  3. lemma OAI.SLEExactGauge.anglePolynomialTest_deriv line 21
  4. lemma OAI.SLEExactGauge.anglePolynomialTest_second line 26
  5. lemma OAI.SLEExactGauge.anglePolynomialTest_generator line 39
  6. lemma OAI.SLEExactGauge.angleEigenPolynomial_differential line 51