OAI/Probability/SLE/Gauge/GaugeEntrySmallness.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

All radii in a late prescribed batch are uniformly small. Hence every marked point above a fixed height has a uniformly long initial radius clock.

  1. lemma OAI.SLEExactGauge.Target.entryRadius_le_batch_exp line 15
  2. lemma OAI.SLEExactGauge.Target.radii_uniformly_small line 24
  3. lemma OAI.SLEExactGauge.Target.uniform_marked_radius_gap line 38