OAI/Dynamics/EntropyCounterexample/RegisterErasure.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem340.RegisterErasure.recurring_periodic_window line 11
2. theorem OAI.Problem340.RegisterErasure.recurring_zero_gain line 36
3. theorem OAI.Problem340.RegisterErasure.gain_zero_on_lifted_reset_window line 46
4. theorem OAI.Problem340.RegisterErasure.recurring_zero_periodic_gain line 56
5. theorem OAI.Problem340.RegisterErasure.eventually_zero_of_recurring_reset line 66
6. theorem OAI.Problem340.RegisterErasure.eventually_cutoff_zero_of_norm_escape line 84
7. theorem OAI.Problem340.RegisterErasure.eventually_base_of_recurring_reset line 94
8. theorem OAI.Problem340.RegisterErasure.eventually_all_base_of_recurring_reset line 114
9. theorem OAI.Problem340.RegisterErasure.eventually_registers_erased_of_escape line 131