OAI/Dynamics/StandardMap/DoublingPointwise.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.StandardMapEntropy.wingDefectline 11 - def
OAI.StandardMapEntropy.cancellationLossline 13 - lemma
OAI.StandardMapEntropy.wingDefect_nonnegline 15 - lemma
OAI.StandardMapEntropy.cancellationLoss_boundsline 20 - lemma
OAI.StandardMapEntropy.torusCancellation_iff_distanceline 30 - lemma
OAI.StandardMapEntropy.large_loss_implies_cancellationline 47 - lemma
OAI.StandardMapEntropy.cancellationLoss_pointwise_boundline 79