OAI/Probability/SLE/Loewner/MappedFutureArc.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Each finite future subarc becomes a continuous attached arc in the current half-plane chart. Its initial value is the proved driving limit.

  1. lemma OAI.SLEExactGauge.initialForwardChart_continuousAt line 15
  2. def OAI.SLEExactGauge.mappedFutureRaw line 25
  3. lemma OAI.SLEExactGauge.future_scaled_offset line 31
  4. lemma OAI.SLEExactGauge.mappedFutureRaw_continuousAt line 40
  5. lemma OAI.SLEExactGauge.mappedFutureRaw_tendsto line 55
  6. def OAI.SLEExactGauge.mappedFutureArc line 73
  7. lemma OAI.SLEExactGauge.mappedFutureArc_zero line 83
  8. lemma OAI.SLEExactGauge.mappedFutureArc_upper line 91