OAI/Probability/SLE/Gauge/PrescribedBatchClock.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The chronological repeated entries, followed by their cleanup level, give a nondecreasing discrete clock for the adapted test calculation.

  1. def OAI.SLEExactGauge.Target.prescribedBatchLevel line 12
  2. lemma OAI.SLEExactGauge.Target.entryPhysicalLevel_mono_position line 17
  3. lemma OAI.SLEExactGauge.Target.prescribedBatchLevel_monotone line 30
  4. lemma OAI.SLEExactGauge.Target.prescribedBatchLevel_test_end_le_next line 49
  5. lemma OAI.SLEExactGauge.Target.prescribedBatchLevel_test_end_le_cleanup line 67