OAI/Probability/SLE/Loewner/RawInverseHolomorphic.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Holomorphicity of every continuous-driver raw inverse follows from interior approximation by actual SLE witnesses. The argument uses the finite Brownian driver tubes, not geometric SLE support.

  1. theorem OAI.SLEExactGauge.raw_inverse_holomorphic_of_witness_approximation line 17
  2. theorem OAI.SLEExactGauge.RegularSLEPresentation.raw_inverse_holomorphic line 30
  3. lemma OAI.SLEExactGauge.Target.inverseFlow_injOn line 49
  4. theorem OAI.SLEExactGauge.RegularSLEPresentation.raw_inverse_deriv_ne_zero line 56