OAI/Probability/SLE/Gauge/ActualDenseWindow.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Repeated actual dense tests on the retained scale window. All tests are evaluated under one later finite centered law.

  1. def OAI.SLEExactGauge.actualDenseScaleTest line 19
  2. def OAI.SLEExactGauge.actualDenseWindowFailure line 27
  3. lemma OAI.SLEExactGauge.coverLogLevel_next_gap line 32
  4. theorem OAI.SLEExactGauge.actual_dense_window_failure_bound line 40
  5. theorem OAI.SLEExactGauge.actual_dense_window_failure_measurable_at_end line 100