OAI/Probability/SLE/Loewner/InitialSlitFuture.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The physical future of an initial simple slit, with an exact real offset parameter and no choice of conformal chart.

  1. def OAI.SLEExactGauge.slitFutureParameter line 14
  2. lemma OAI.SLEExactGauge.slitFutureParameter_continuous line 17
  3. lemma OAI.SLEExactGauge.slitFutureParameter_zero line 21
  4. lemma OAI.SLEExactGauge.slitFutureParameter_coe line 25
  5. lemma OAI.SLEExactGauge.slitFuturePoint_mem_domain line 31
  6. lemma OAI.SLEExactGauge.slit_tip_not_mem_domain line 45