OAI/Probability/SLE/Stochastic/PlanarSamplingLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Passing finite-grid conditional sampling to bounded stopping times for compact smooth planar harmonic tests.

  1. lemma OAI.SLEExactGauge.planar_compensated_grid_tendsto line 14
  2. theorem OAI.SLEExactGauge.planar_compact_optional_between line 74