OAI/Probability/SLE/Stochastic/PlanarHarmonicSampling.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Conditional harmonic sampling on the actual compact domain stops.

  1. theorem OAI.SLEExactGauge.planar_local_harmonic_optional_between line 14
  2. def OAI.SLEExactGauge.SmoothDomainExhaustion.stopFiltration line 44
  3. lemma OAI.SLEExactGauge.SmoothDomainExhaustion.harmonic_stopped_adapted line 50
  4. theorem OAI.SLEExactGauge.SmoothDomainExhaustion.harmonic_stopped_martingale line 65
  5. theorem OAI.SLEExactGauge.SmoothDomainExhaustion.harmonic_stopped_converges line 84