OAI/Geometry/Arnold/Hamiltonian.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArnoldCounterexample.Quadric.rotationLinear line 15

    Source documentation

    The ambient real-linear rotation, not merely its quotient action.

    def rotationLinear (c s : ℝ) : CV →L[ℝ] CV :=
…

    Mentions: OAI.ArnoldCounterexample.CV

  2. lemma OAI.ArnoldCounterexample.Quadric.rotationLinear_apply line 27
  3. def OAI.ArnoldCounterexample.Quadric.pathLinear line 29
  4. lemma OAI.ArnoldCounterexample.Quadric.pathLinear_apply line 30
  5. lemma OAI.ArnoldCounterexample.Quadric.rotation_symplectic line 32
  6. lemma OAI.ArnoldCounterexample.Quadric.rotationPath_symplectic line 39
  7. lemma OAI.ArnoldCounterexample.Quadric.rotationPath_pullback line 43
  8. lemma OAI.ArnoldCounterexample.Quadric.rotationPath_comp_hasDerivAt line 49
  9. def OAI.ArnoldCounterexample.Construction.forward line 71
  10. def OAI.ArnoldCounterexample.Construction.backward line 72
  11. def OAI.ArnoldCounterexample.Construction.hamiltonian line 73
  12. lemma OAI.ArnoldCounterexample.Construction.forward_smooth line 75
  13. lemma OAI.ArnoldCounterexample.Construction.backward_smooth line 76
  14. lemma OAI.ArnoldCounterexample.Construction.hamiltonian_smooth line 78
  15. lemma OAI.ArnoldCounterexample.Construction.forward_preserves line 83
  16. lemma OAI.ArnoldCounterexample.Construction.backward_preserves line 85
  17. lemma OAI.ArnoldCounterexample.Construction.forward_phase line 87
  18. lemma OAI.ArnoldCounterexample.Construction.backward_phase line 90
  19. lemma OAI.ArnoldCounterexample.Construction.hamiltonian_phase line 93
  20. lemma OAI.ArnoldCounterexample.Construction.backward_forward_full line 97
  21. lemma OAI.ArnoldCounterexample.Construction.forward_backward_full line 99
  22. lemma OAI.ArnoldCounterexample.Construction.forward_start line 102
  23. def OAI.ArnoldCounterexample.Construction.mainEquiv line 104
  24. lemma OAI.ArnoldCounterexample.Construction.mainEquiv_project line 109
  25. lemma OAI.ArnoldCounterexample.Construction.forward_equation line 114
  26. def OAI.ArnoldCounterexample.Construction.mainHamiltonianPath line 142

    Source documentation

    A complete smooth Hamiltonian path on the actual normalized Fubini--Study quadric.

    def mainHamiltonianPath : HamiltonianPath mainEquiv where
…

    Mentions: OAI.ArnoldCounterexample.HamiltonianPath, OAI.ArnoldCounterexample.Construction.mainEquiv

  27. lemma OAI.ArnoldCounterexample.Construction.main_isHamiltonian line 160