OAI/Probability/SLE/Stochastic/PlanarHolomorphicTests.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Bounded holomorphic observables on the physical planar domain give the two real harmonic tests used for conformal exit limits.

  1. def OAI.SLEExactGauge.planarTranslatedDomain line 15
  2. lemma OAI.SLEExactGauge.planarTranslatedDomain_open line 18
  3. lemma OAI.SLEExactGauge.holomorphic_planar_components line 22
  4. theorem OAI.SLEExactGauge.holomorphic_stopped_converges line 53