OAI/Probability/SLE/Loewner/CanonicalInverseHolomorphic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Holomorphicity of the raw inverse under the canonical Wiener law. Clipping the endpoint inside the half-plane makes differentiability a Borel condition on a continuous function space.

  1. def OAI.SLEExactGauge.upperClip line 21
  2. lemma OAI.SLEExactGauge.continuous_upperClip line 23
  3. lemma OAI.SLEExactGauge.upperClip_eq line 30
  4. def OAI.SLEExactGauge.clippedRawInverse line 35
  5. lemma OAI.SLEExactGauge.measurable_clippedRawInverse line 42
  6. lemma OAI.SLEExactGauge.clippedRawInverse_eventuallyEq line 53
  7. lemma OAI.SLEExactGauge.ae_canonical_inverse_holomorphic line 63