OAI/Probability/SLE/Geometry/CenteredFutureSlit.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Centering at the proved driving value makes every future segment an ordinary simple attached slit, to which the existing normalized chart theorem applies.

  1. def OAI.SLEExactGauge.centeredFutureArc line 15
  2. lemma OAI.SLEExactGauge.centeredFutureArc_zero line 22
  3. lemma OAI.SLEExactGauge.centeredFutureArc_injective line 29
  4. lemma OAI.SLEExactGauge.centeredFutureArc_upper line 36
  5. def OAI.SLEExactGauge.futureSlitChart line 46