OAI/Probability/SLE/Gauge/BatchRadiusGaps.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The exact radius prescription leaves a full test interval and the subsequent mixing gap between consecutive tests and before cleanup.

  1. lemma OAI.SLEExactGauge.Target.entryPosition_lt_cleanup line 12
  2. lemma OAI.SLEExactGauge.Target.entryRadius_gap_of_position_lt line 48
  3. lemma OAI.SLEExactGauge.Target.entryRadius_cleanup_gap line 63