OAI/Probability/SLE/Stochastic/PlanarCutoffStop.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Concrete compact localization stops for planar Brownian motion.

  1. lemma OAI.SLEExactGauge.planarWiener_zero line 14
  2. lemma OAI.SLEExactGauge.planarWiener_adapted line 17
  3. def OAI.SLEExactGauge.planarCutoffHit line 20
  4. def OAI.SLEExactGauge.planarCutoffStop line 23
  5. lemma OAI.SLEExactGauge.planarCutoffHit_stopping line 26
  6. lemma OAI.SLEExactGauge.planarCutoffStop_stopping line 32
  7. lemma OAI.SLEExactGauge.planarCutoffStop_le line 36
  8. lemma OAI.SLEExactGauge.planarCutoffStop_before line 39
  9. lemma OAI.SLEExactGauge.planarCutoffStop_in_support line 45
  10. lemma OAI.SLEExactGauge.planarCutoffStop_ge_of_nonzero line 65