OAI/Dynamics/StandardMap/CancellationVector.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StandardMapEntropy.torus_reverse_operator line 11
2. lemma OAI.StandardMapEntropy.small_vector_of_cancellation line 19
3. lemma OAI.StandardMapEntropy.torus_cancellation_vector line 35
4. def OAI.StandardMapEntropy.torusSmallEndpoints line 60
5. lemma OAI.StandardMapEntropy.torusSegmentTransfer_first line 64
6. lemma OAI.StandardMapEntropy.torusStep_swap_prev line 74
7. lemma OAI.StandardMapEntropy.torusPotential_bound line 76
8. lemma OAI.StandardMapEntropy.max_unit_coordinate line 79
9. lemma OAI.StandardMapEntropy.normalized_endpoint_norm line 85
10. lemma OAI.StandardMapEntropy.torus_small_normalize line 92