OAI/Probability/SLE/Geometry/HarmonicExitLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bounded harmonic observables have actual left limits at every finite domain exit, simultaneously on the original planar Wiener space.

  1. theorem OAI.SLEExactGauge.SmoothDomainExhaustion.harmonic_exit_limit line 17