OAI/Dynamics/StandardMap/PlaneGeometry.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.wedge line 11

    Also declared: ComparatorChallenges/StandardMapComponents.lean:47 (same declaration text), ComparatorChallenges/StandardMapLyapunov.lean:83 (same declaration text).

  2. def OAI.StandardMapEntropy.dot line 12
  3. def OAI.StandardMapEntropy.quarterTurn line 13
  4. lemma OAI.StandardMapEntropy.norm_quarterTurn line 14
  5. lemma OAI.StandardMapEntropy.dot_self line 15
  6. lemma OAI.StandardMapEntropy.wedge_quarterTurn line 17
  7. lemma OAI.StandardMapEntropy.dot_quarterTurn line 19
  8. lemma OAI.StandardMapEntropy.dot_wedge_sq line 22
  9. lemma OAI.StandardMapEntropy.norm_add_smul_sq line 25
  10. lemma OAI.StandardMapEntropy.unit_expansion line 30
  11. lemma OAI.StandardMapEntropy.abs_dot_le_norm_mul line 39
  12. lemma OAI.StandardMapEntropy.abs_wedge_le_norm_mul line 44
  13. lemma OAI.StandardMapEntropy.wedge_add_left line 48
  14. lemma OAI.StandardMapEntropy.wedge_smul_left line 50
  15. lemma OAI.StandardMapEntropy.wedge_add_right line 52
  16. lemma OAI.StandardMapEntropy.wedge_smul_right line 54
  17. lemma OAI.StandardMapEntropy.wedge_refl line 56
  18. lemma OAI.StandardMapEntropy.wedge_swap line 57
  19. lemma OAI.StandardMapEntropy.wedge_sine_triangle line 58
  20. lemma OAI.StandardMapEntropy.exists_unit_opNorm line 72
  21. lemma OAI.StandardMapEntropy.linear_term_of_quadratic_nonpos line 87
  22. lemma OAI.StandardMapEntropy.orthogonal_image_of_max line 94
  23. def OAI.StandardMapEntropy.PlaneAreaPreserving line 105
  24. lemma OAI.StandardMapEntropy.PlaneAreaPreserving.singular_pair line 106