OAI/Probability/SLE/Loewner/InitialReflectedForward.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The normalized initial forward maps continued across the real axis away from the attached slit. These are the same maps on the upper side.

  1. def OAI.SLEExactGauge.initialReflectedChart line 15
  2. def OAI.SLEExactGauge.initialReflectedForward line 22
  3. lemma OAI.SLEExactGauge.reflected_initial_subset line 27
  4. lemma OAI.SLEExactGauge.initialReflectedForward_eq line 34
  5. lemma OAI.SLEExactGauge.initialReflectedForward_differentiable line 45
  6. lemma OAI.SLEExactGauge.real_not_reflected_arc line 57
  7. lemma OAI.SLEExactGauge.initialReflectedForward_real line 76
  8. lemma OAI.SLEExactGauge.initialReflectedForward_uniform_bound line 90