OAI/Probability/SLE/Angle/AngleLogCosine.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Smooth cosine coordinates in the actual logarithmic Loewner state. These formulas are used to apply the Brownian generator to eigenpolynomials.

  1. def OAI.SLEExactGauge.logInverseNorm line 13
  2. def OAI.SLEExactGauge.logCosine line 16
  3. lemma OAI.SLEExactGauge.logInverseNorm_eq line 19
  4. lemma OAI.SLEExactGauge.logInverseNorm_pos line 26
  5. lemma OAI.SLEExactGauge.logInverseNorm_sq line 29
  6. lemma OAI.SLEExactGauge.logCosine_eq_angle line 36
  7. lemma OAI.SLEExactGauge.logCosine_abs_le_one line 47
  8. lemma OAI.SLEExactGauge.logInverseNorm_spatial line 52
  9. lemma OAI.SLEExactGauge.logCosine_spatial line 59
  10. lemma OAI.SLEExactGauge.logInverseNorm_contDiff line 70
  11. lemma OAI.SLEExactGauge.logCosine_contDiff line 76