OAI/Geometry/NearbyLagrangian/CylinderEquations.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Ambient radial trapping and uniqueness of central cylinder curves.

  1. theorem OAI.NearbyLagrangian.Transport.hamiltonian_equation_of_open_chart line 20
  2. theorem OAI.NearbyLagrangian.RadialExtension.ambient_hamiltonian_radial_trapping line 79
  3. theorem OAI.NearbyLagrangian.RadialExtension.central_radial_curve_unique line 121