OAI/Dynamics/EntropyCounterexample/ClockOrbit.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Problem340.Clock.LiftedOrbit line 11
  2. lemma OAI.Problem340.Clock.LiftedOrbit.monotone line 21
  3. lemma OAI.Problem340.Clock.LiftedOrbit.increments_le_one line 27
  4. lemma OAI.Problem340.Clock.LiftedOrbit.barrier_le_difference line 31
  5. theorem OAI.Problem340.Clock.LiftedOrbit.bounded_limit line 35
  6. theorem OAI.Problem340.Clock.LiftedOrbit.bounded_circle_limit line 42
  7. lemma OAI.Problem340.Clock.LiftedOrbit.cutoff_le_difference line 57
  8. theorem OAI.Problem340.Clock.LiftedOrbit.cutoff_tendsto_zero line 63
  9. theorem OAI.Problem340.Clock.LiftedOrbit.eventually_observation_zero line 68
  10. theorem OAI.Problem340.Clock.LiftedOrbit.eventually_norm_lt line 82
  11. theorem OAI.Problem340.Clock.LiftedOrbit.main_tendsto_zero line 92
  12. theorem OAI.Problem340.Clock.LiftedOrbit.main_tendsto_zero_of_readouts line 101
  13. theorem OAI.Problem340.Clock.LiftedOrbit.bounded_or_tendsto_atTop line 117
  14. theorem OAI.Problem340.Clock.LiftedOrbit.avoids_invariant_fast_set line 123
  15. theorem OAI.Problem340.Clock.LiftedOrbit.onePoint_main_tendsto_zero_of_readouts line 140