OAI/Dynamics/StandardMap/PlaneTransfer.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StandardMapEntropy.norm_smul_add_smul_sq line 11
2. lemma OAI.StandardMapEntropy.dot_quarterTurn_right line 16
3. lemma OAI.StandardMapEntropy.wedge_quarterTurn_left line 18
4. lemma OAI.StandardMapEntropy.dot_comm line 20
5. lemma OAI.StandardMapEntropy.PlaneAreaPreserving.norm_map_sq line 21
6. lemma OAI.StandardMapEntropy.PlaneAreaPreserving.norm_lower line 37
7. lemma OAI.StandardMapEntropy.PlaneAreaPreserving.norm_inverse line 54
8. lemma OAI.StandardMapEntropy.PlaneAreaPreserving.comp line 64
9. lemma OAI.StandardMapEntropy.PlaneAreaPreserving.norm_le_product line 68
10. lemma OAI.StandardMapEntropy.expanded_projection_bound line 73
11. lemma OAI.StandardMapEntropy.two_singular_upper line 80
12. lemma OAI.StandardMapEntropy.PlaneAreaPreserving.small_two_endpoints line 94