OAI/Geometry/Arnold/Rotation.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArnoldCounterexample.Quadric.rotation line 11

    Source documentation

    Two simultaneous identical planar rotations.

    def rotation (c s : ℝ) (z : CV) : CV :=
…

    Mentions: OAI.ArnoldCounterexample.CV

  2. lemma OAI.ArnoldCounterexample.Quadric.rotation_quadricPolynomial line 15
  3. lemma OAI.ArnoldCounterexample.Quadric.rotation_normSquared line 21
  4. lemma OAI.ArnoldCounterexample.Quadric.rotation_inverse line 29
  5. lemma OAI.ArnoldCounterexample.Quadric.rotation_phase line 40
  6. lemma OAI.ArnoldCounterexample.Quadric.rotation_start line 45
  7. lemma OAI.ArnoldCounterexample.Quadric.rotation_finish line 49
  8. lemma OAI.ArnoldCounterexample.Quadric.contDiff_ofReal line 53
  9. lemma OAI.ArnoldCounterexample.Quadric.contDiff_re line 56
  10. lemma OAI.ArnoldCounterexample.Quadric.contDiff_im line 59
  11. def OAI.ArnoldCounterexample.Quadric.rotationPath line 62
  12. lemma OAI.ArnoldCounterexample.Quadric.rotationPath_smooth line 65
  13. lemma OAI.ArnoldCounterexample.Quadric.rotationPath_preserves line 71
  14. lemma OAI.ArnoldCounterexample.Quadric.rotationPath_inverse line 78
  15. lemma OAI.ArnoldCounterexample.Quadric.rotationPath_start line 83
  16. lemma OAI.ArnoldCounterexample.Quadric.rotationPath_finish line 86
  17. lemma OAI.ArnoldCounterexample.Quadric.rotationPath_phase line 89
  18. def OAI.ArnoldCounterexample.Quadric.rotationGenerator line 97

    Source documentation

    The ambient vector field generating the prescribed rotations.

    def rotationGenerator (z : CV) : CV :=
…

    Mentions: OAI.ArnoldCounterexample.CV

  19. def OAI.ArnoldCounterexample.Quadric.rotationHamiltonian line 102

    Source documentation

    Minus alpha(Z), exactly the sign convention i_X omega = dH.

    def rotationHamiltonian (z : CV) : ℝ :=
…

    Mentions: OAI.ArnoldCounterexample.CV

  20. lemma OAI.ArnoldCounterexample.Quadric.rotationHamiltonian_smooth line 106
  21. lemma OAI.ArnoldCounterexample.Quadric.rotationHamiltonian_smul line 110
  22. def OAI.ArnoldCounterexample.Quadric.realCoord line 116
  23. def OAI.ArnoldCounterexample.Quadric.imagCoord line 119
  24. lemma OAI.ArnoldCounterexample.Quadric.realCoord_apply line 122
  25. lemma OAI.ArnoldCounterexample.Quadric.imagCoord_apply line 123
  26. def OAI.ArnoldCounterexample.Quadric.rotationHamiltonianDiff line 125
  27. lemma OAI.ArnoldCounterexample.Quadric.rotationHamiltonian_hasFDerivAt line 131
  28. lemma OAI.ArnoldCounterexample.Quadric.rotationHamiltonian_equation line 139
  29. lemma OAI.ArnoldCounterexample.Quadric.horizontal_finrank_real line 146
  30. lemma OAI.ArnoldCounterexample.Quadric.rotationPath_hasDerivAt line 154
  31. def OAI.ArnoldCounterexample.Quadric.involutionHamiltonianPath line 178

    Source documentation

    A complete explicit Hamiltonian witness for the actual quadric involution. No flow existence, moment-map theorem, or descent theorem is assumed.

    def involutionHamiltonianPath : HamiltonianPath involution where
…

    Mentions: OAI.ArnoldCounterexample.HamiltonianPath, OAI.ArnoldCounterexample.Quadric.involution

  32. theorem OAI.ArnoldCounterexample.Quadric.involution_isHamiltonian line 204

    Source documentation

    The explicit involution is Hamiltonian for the fixed Fubini--Study normalization.

    theorem involution_isHamiltonian : IsHamiltonian involution :=
…

    Mentions: OAI.ArnoldCounterexample.IsHamiltonian, OAI.ArnoldCounterexample.Quadric.involution