OAI/Dynamics/EntropyCounterexample/MapErasure.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem340.ConstructionErasure.inputTerm_eq_zero_of_cutoff line 17
2. lemma OAI.Problem340.ConstructionErasure.baseInput_eq_zero_of_cutoff line 22
3. lemma OAI.Problem340.ConstructionErasure.input_eq_zero_of_cutoff line 27
4. lemma OAI.Problem340.ConstructionErasure.periodicGain_lift_periodic line 32
5. lemma OAI.Problem340.ConstructionErasure.periodicGain_lift_reset line 37
6. theorem OAI.Problem340.ConstructionErasure.rawMap_registers_eventually_zero line 45
7. theorem OAI.Problem340.ConstructionErasure.rawMap_registers_eventually_zero_of_norm_escape line 72
8. lemma OAI.Problem340.ConstructionErasure.clockIncrement_infty line 89
9. theorem OAI.Problem340.ConstructionErasure.rawMap_orbit_infty line 93
10. theorem OAI.Problem340.ConstructionErasure.rawMap_infty_registers_eventually_zero line 112