OAI/Probability/SLE/Geometry/HarmonicStopSamples.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Ordered samples between compact domain stops retain their full stopped past. The resulting finite maximal bound controls all mesh observations.

  1. def OAI.SLEExactGauge.orderedStopFiltration line 14
  2. theorem OAI.SLEExactGauge.planar_local_harmonic_sampled_martingale line 23
  3. theorem OAI.SLEExactGauge.harmonic_clipped_grid_maximal line 62