OAI/Dynamics/EntropyCounterexample/MapGlobalEscape.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem340.Construction.exists_period_representative line 15
2. theorem OAI.Problem340.Construction.rawOrbit_main_square_of_no_readout line 22
3. theorem OAI.Problem340.Construction.rawOrbit_norm_square_of_no_readout line 41
4. theorem OAI.Problem340.Construction.rawOrbit_norm_tendsto_atTop_of_passage_bounds line 54
5. theorem OAI.Problem340.Construction.rawOrbit_main_tendsto_infty_of_norm line 74
6. theorem OAI.Problem340.Construction.rawOrbit_norm_tendsto_atTop_of_complete_passages line 81
7. theorem OAI.Problem340.Construction.rawOrbit_main_tendsto_infty_of_complete_passages line 100