OAI/Dynamics/StandardMap/CocycleAlgebra.lean
16 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.StandardMapEntropy.transferProduct_concatline 11 - lemma
OAI.StandardMapEntropy.torusSegmentCoefficient_shiftline 18 - lemma
OAI.StandardMapEntropy.torusSegmentTransfer_concatline 25 - lemma
OAI.StandardMapEntropy.torusSegmentTransfer_shiftline 30 - lemma
OAI.StandardMapEntropy.torusIter_neg_swapline 39 - def
OAI.StandardMapEntropy.planeSwapline 48 - lemma
OAI.StandardMapEntropy.planeSwap_reline 55 - lemma
OAI.StandardMapEntropy.planeSwap_imline 56 - lemma
OAI.StandardMapEntropy.planeSwap_involline 57 - lemma
OAI.StandardMapEntropy.norm_planeSwapline 58 - lemma
OAI.StandardMapEntropy.norm_comp_planeSwapline 62 - lemma
OAI.StandardMapEntropy.norm_planeSwap_compline 71 - lemma
OAI.StandardMapEntropy.planeSwap_transferStepline 79 - lemma
OAI.StandardMapEntropy.torus_backward_pair_coordinateline 81 - lemma
OAI.StandardMapEntropy.torusSegmentTransfer_reverse_identityline 85 - lemma
OAI.StandardMapEntropy.torusSegmentTransfer_reverse_normline 114