OAI/Dynamics/EntropyCounterexample/ClockDynamics.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem340.ClockDynamics.bounded_clock_limit line 10
  2. theorem OAI.Problem340.ClockDynamics.bounded_clock_limit_barrier line 21
  3. theorem OAI.Problem340.ClockDynamics.bounded_clock_limit_lattice line 32
  4. theorem OAI.Problem340.ClockDynamics.monotone_of_nonneg_increments line 43
  5. theorem OAI.Problem340.ClockDynamics.barrier_trapping line 49
  6. theorem OAI.Problem340.ClockDynamics.exists_first_crossing line 59
  7. theorem OAI.Problem340.ClockDynamics.single_visit_short_interval line 81
  8. theorem OAI.Problem340.ClockDynamics.squaring_tendsto_zero line 93
  9. theorem OAI.Problem340.ClockDynamics.eventually_squaring_tendsto_zero line 105
  10. theorem OAI.Problem340.ClockDynamics.eventually_small_of_bounded_clock line 118
  11. theorem OAI.Problem340.ClockDynamics.bounded_clock_eventually_squaring_tendsto_zero line 128
  12. theorem OAI.Problem340.ClockDynamics.preparation_norm_gt_half line 139
  13. theorem OAI.Problem340.ClockDynamics.exists_crossing_after line 161
  14. theorem OAI.Problem340.ClockDynamics.exists_later_periodic_reset line 175
  15. theorem OAI.Problem340.ClockDynamics.eventually_zero_after_periodic_reset line 185