OAI/Probability/SLE/Multipoint/MultipointLogAngular.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Identification of the smooth logarithmic monomials with the angular factors, in actual capacity-two coordinates.

  1. def OAI.SLEExactGauge.Multipoint.logPoint line 14
  2. def OAI.SLEExactGauge.Multipoint.logAngle line 17
  3. def OAI.SLEExactGauge.Multipoint.logVelocity line 19
  4. lemma OAI.SLEExactGauge.Multipoint.logPoint_re line 22
  5. lemma OAI.SLEExactGauge.Multipoint.logPoint_im line 25
  6. lemma OAI.SLEExactGauge.Multipoint.logPoint_norm_sq line 30
  7. lemma OAI.SLEExactGauge.Multipoint.logPoint_norm_pos line 38
  8. lemma OAI.SLEExactGauge.Multipoint.logAngle_sin_pos line 46
  9. lemma OAI.SLEExactGauge.Multipoint.logAngle_sin_sq line 51
  10. lemma OAI.SLEExactGauge.Multipoint.logAngle_log_sin line 58
  11. lemma OAI.SLEExactGauge.Multipoint.logFactor_eq_angular line 69
  12. lemma OAI.SLEExactGauge.Multipoint.logVelocity_pos line 78
  13. lemma OAI.SLEExactGauge.Multipoint.logFactor_spatial_eq_angular line 81
  14. lemma OAI.SLEExactGauge.Multipoint.sineGenerator_relative line 94
  15. theorem OAI.SLEExactGauge.Multipoint.logFactor_generator_eq_angular line 103