OAI/Probability/SLE/Angle/AngleEigenOrthogonality.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Symmetry under the paper's stationary angular weight, and orthogonality of the actual centered-generator polynomial eigenfunctions.

  1. lemma OAI.SLEExactGauge.anglePolynomialWronskian_hasDerivAt line 13
  2. lemma OAI.SLEExactGauge.anglePolynomialGenerator_symmetric line 26
  3. lemma OAI.SLEExactGauge.angleEigenPolynomial_orthogonal line 58