OAI/Probability/SLE/Stochastic/PlanarDomainStops.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A nested sequence of actual stopping times exhausts each finite exit of a continuous planar Wiener path from an open domain.

  1. def OAI.SLEExactGauge.SmoothDomainExhaustion.stop line 17
  2. lemma OAI.SLEExactGauge.SmoothDomainExhaustion.stop_stopping line 19
  3. lemma OAI.SLEExactGauge.SmoothDomainExhaustion.stop_le line 23
  4. lemma OAI.SLEExactGauge.SmoothDomainExhaustion.stop_mem_support line 26
  5. lemma OAI.SLEExactGauge.SmoothDomainExhaustion.stop_mem_domain line 30
  6. lemma OAI.SLEExactGauge.SmoothDomainExhaustion.stop_monotone line 34
  7. lemma OAI.SLEExactGauge.SmoothDomainExhaustion.eventually_le_stop line 48
  8. lemma OAI.SLEExactGauge.SmoothDomainExhaustion.stop_tendsto_finite_exit line 60