OAI/Dynamics/EntropyCounterexample/PredictionClock.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem340.Construction.predictedClock_zero line 10
  2. theorem OAI.Problem340.Construction.predictedClock_succ line 13
  3. theorem OAI.Problem340.Construction.predictedClock_step_bounds line 18
  4. theorem OAI.Problem340.Construction.predictedClock_monotone line 30
  5. theorem OAI.Problem340.Construction.predictedClock_unit_step line 38
  6. theorem OAI.Problem340.Construction.readoutCoeff_mem_interval line 48
  7. theorem OAI.Problem340.Construction.predictedClock_readout_unique line 53
  8. theorem OAI.Problem340.Construction.predictedClock_readout_single_hit line 65
  9. theorem OAI.Problem340.Construction.prediction_iterate_add_period line 75
  10. theorem OAI.Problem340.Construction.predictedClock_add_period line 90
  11. theorem OAI.Problem340.Construction.increment_eq_one_on_readout_window line 94
  12. theorem OAI.Problem340.Construction.predictedClock_eq_actual_until_readout_end line 101
  13. theorem OAI.Problem340.Construction.readoutCoeff_predictedClock_eq_actual line 128