OAI/Probability/SLE/Gauge/PrescribedTestPast.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The history before each test is taken at the preceding test endpoint. The intervening radius gap is reserved for angular mixing.

  1. def OAI.SLEExactGauge.Target.prescribedTestPastLevel line 12
  2. lemma OAI.SLEExactGauge.Target.prescribedTestPastLevel_nonneg line 17
  3. lemma OAI.SLEExactGauge.Target.prescribedTestPastLevel_succ line 28
  4. lemma OAI.SLEExactGauge.Target.prescribedTestPastLevel_monotone line 35
  5. lemma OAI.SLEExactGauge.Target.prescribedTestPastLevel_gap line 53
  6. lemma OAI.SLEExactGauge.Target.eventually_prescribedTestPastLevel_gap line 72