OAI/Probability/SLE/Geometry/DiskRecentering.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The elementary disk automorphism needed to compare derivatives on the quarter disk.

  1. def OAI.SLEExactGauge.diskRecenter line 14
  2. lemma OAI.SLEExactGauge.diskRecenter_den_ne line 16
  3. lemma OAI.SLEExactGauge.diskRecenter_det line 24
  4. lemma OAI.SLEExactGauge.diskRecenter_maps line 30
  5. lemma OAI.SLEExactGauge.diskRecenter_injOn line 48
  6. lemma OAI.SLEExactGauge.diskRecenter_hasDerivAt line 60
  7. lemma OAI.SLEExactGauge.diskRecenter_differentiable line 66
  8. lemma OAI.SLEExactGauge.diskRecenter_zero line 71
  9. lemma OAI.SLEExactGauge.diskRecenter_neg line 72
  10. lemma OAI.SLEExactGauge.diskRecenter_deriv_zero line 74
  11. lemma OAI.SLEExactGauge.diskRecenter_deriv_neg line 80