OAI/Dynamics/EntropyCounterexample/GlobalEscape.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Problem340.GlobalEscape.tendsto_coe_infty_of_normline 11 - lemma
OAI.Problem340.GlobalEscape.period_le_of_readoutline 20 - theorem
OAI.Problem340.GlobalEscape.square_le_after_passageline 28 - theorem
OAI.Problem340.GlobalEscape.tendsto_atTop_of_passage_boundsline 58 - theorem
OAI.Problem340.GlobalEscape.tendsto_atTop_of_complete_passagesline 73