OAI/Dynamics/EntropyCounterexample/MapBoundedOrbit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem340.Construction.rawClockLift_liftedOrbit line 15
2. theorem OAI.Problem340.Construction.periodicReadout_coe_periodic line 24
3. theorem OAI.Problem340.Construction.periodicReadout_coe_eq_zero_near_fifty line 30
4. theorem OAI.Problem340.Construction.readout_eq_sum_smul line 41
5. theorem OAI.Problem340.Construction.raw_clock_tendsto_of_bounded line 51
6. theorem OAI.Problem340.Construction.raw_main_tendsto_zero_of_bounded line 60
7. theorem OAI.Problem340.Construction.concrete_bounded_clock_limits line 92