OAI/Geometry/NearbyLagrangian/FiniteTransport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite composition and complete tame Hamiltonian transport.

  1. def OAI.NearbyLagrangian.Transport.preparedComposite line 18
  2. theorem OAI.NearbyLagrangian.Transport.finite_tame_transport line 27
  3. theorem OAI.NearbyLagrangian.Transport.phaseGenerate_injective_of_conjugacy line 59
  4. lemma OAI.NearbyLagrangian.Transport.flat_hamiltonian_evolution_endpoint line 80
  5. lemma OAI.NearbyLagrangian.Transport.preparedComposite_evolution line 105
  6. theorem OAI.NearbyLagrangian.Transport.tame_hamiltonian_transport line 122
  7. theorem OAI.NearbyLagrangian.Transport.tame_hamiltonian_transport_endpoint line 142