OAI/Dynamics/StandardMap/ShapeCore.lean
12 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.StandardMapEntropy.slowCoreline 11 - lemma
OAI.StandardMapEntropy.isClosed_slowCoreline 12 - lemma
OAI.StandardMapEntropy.unit_Iic_localline 13 - lemma
OAI.StandardMapEntropy.unit_Ici_localline 19 - lemma
OAI.StandardMapEntropy.nonaffine_has_nonlocalline 25 - lemma
OAI.StandardMapEntropy.slowCore_nonemptyline 32 - lemma
OAI.StandardMapEntropy.slowCore_ordConnectedline 35 - lemma
OAI.StandardMapEntropy.slowCore_local_speedline 45 - lemma
OAI.StandardMapEntropy.slow_affine_prefixline 52 - lemma
OAI.StandardMapEntropy.slow_affine_suffixline 64 - lemma
OAI.StandardMapEntropy.slowCore_secant_sortedline 76 - lemma
OAI.StandardMapEntropy.slowCore_secantline 123