OAI/Probability/SLE/Angle/AnglePolynomialGenerator.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The cosine-coordinate generator in the actual logarithmic radius clock. Its polynomial eigenvalues retain the paper's time normalization.

  1. def OAI.SLEExactGauge.anglePolynomialGenerator line 12
  2. def OAI.SLEExactGauge.anglePolynomialEigenvalue line 15
  3. lemma OAI.SLEExactGauge.anglePolynomialGenerator_add line 18
  4. lemma OAI.SLEExactGauge.anglePolynomialGenerator_C_mul line 24
  5. lemma OAI.SLEExactGauge.anglePolynomialGenerator_one line 29
  6. lemma OAI.SLEExactGauge.anglePolynomialGenerator_X line 32
  7. lemma OAI.SLEExactGauge.anglePolynomialGenerator_X_pow_add_two line 39
  8. lemma OAI.SLEExactGauge.anglePolynomialEigenvalue_strictMono line 50
  9. lemma OAI.SLEExactGauge.anglePolynomialEigenvalue_clock line 60