OAI/Probability/SLE/Loewner/MappedFutureRange.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The mapped future arc has exactly the expected physical segment as its interior range.

  1. lemma OAI.SLEExactGauge.point_after_prefix_mem_domain line 13
  2. lemma OAI.SLEExactGauge.mappedFutureArc_segment line 21
  3. theorem OAI.SLEExactGauge.mappedFutureArc_range_upper line 31
  4. theorem OAI.SLEExactGauge.initialForward_avoids_future_iff line 55