OAI/Dynamics/EntropyCounterexample/MapOrbitLift.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem340.Construction.liftIco_coe_of_periodic line 12
  2. theorem OAI.Problem340.Construction.clockIncrement_coe line 19
  3. theorem OAI.Problem340.Construction.clockIncrement_mem_Icc line 23
  4. def OAI.Problem340.Construction.rawClockLift line 31
  5. theorem OAI.Problem340.Construction.rawClockLift_zero line 34
  6. theorem OAI.Problem340.Construction.coe_rawClockLift line 38
  7. theorem OAI.Problem340.Construction.rawClockLift_succ line 43
  8. theorem OAI.Problem340.Construction.monotone_rawClockLift line 53
  9. theorem OAI.Problem340.Construction.rawClockLift_step_bounds line 59
  10. theorem OAI.Problem340.Construction.exists_rawClockLift line 66
  11. theorem OAI.Problem340.Construction.coe_rawClockLift_sub_period line 78
  12. theorem OAI.Problem340.Construction.rawClockLift_sub_period_succ line 86
  13. theorem OAI.Problem340.Construction.input_at_passage_clock line 98
  14. theorem OAI.Problem340.Construction.periodicReadout_at_passage_clock line 108
  15. theorem OAI.Problem340.Construction.periodicGain_at_passage_clock line 118
  16. theorem OAI.Problem340.Construction.main_update_at_passage_clock line 127
  17. theorem OAI.Problem340.Construction.register_update_at_passage_clock line 139