OAI/Probability/SLE/Loewner/FutureSlitDomain.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact transport of the later slit complement to the centered future slit complement.

  1. lemma OAI.SLEExactGauge.initialInverseChart_mem_domain line 13
  2. lemma OAI.SLEExactGauge.centeredFutureArc_range_iff line 28
  3. lemma OAI.SLEExactGauge.initialForward_centered_mem_domain_iff line 40
  4. theorem OAI.SLEExactGauge.initialForward_centered_bijOn line 57