OAI/Probability/SLE/Angle/TargetDiskRadius.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The prescribed disk chart has the angle-independent initial conformal radius needed for the centered moment bounds.

  1. lemma OAI.SLEExactGauge.Target.diskMap_hasDerivAt line 14
  2. lemma OAI.SLEExactGauge.Target.diskMap_differentiableOn line 24
  3. lemma OAI.SLEExactGauge.Target.diskMap_injOn line 29
  4. lemma OAI.SLEExactGauge.Target.diskMap_deriv_norm line 35
  5. lemma OAI.SLEExactGauge.Target.diskMap_initial_radius line 42
  6. theorem OAI.SLEExactGauge.Target.initialRadius_disk line 54
  7. lemma OAI.SLEExactGauge.Target.initialRadius_zero line 59
  8. lemma OAI.SLEExactGauge.Target.initialRadius_pos line 64