OAI/Geometry/NearbyLagrangian/RadialTrapping.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Compact radial Hamiltonian extensions and central trapping.

  1. def OAI.NearbyLagrangian.RadialExtension.cutoffHamiltonian line 18
  2. lemma OAI.NearbyLagrangian.RadialExtension.mdifferentiableAt_cutoffHamiltonian line 22
  3. lemma OAI.NearbyLagrangian.RadialExtension.cutoffHamiltonian_radial_derivative line 31
  4. theorem OAI.NearbyLagrangian.RadialExtension.cutoffHamiltonian_radial_equations line 56
  5. lemma OAI.NearbyLagrangian.RadialExtension.norm_curve_le line 90
  6. lemma OAI.NearbyLagrangian.RadialExtension.curve_constant line 100
  7. lemma OAI.NearbyLagrangian.RadialExtension.gradient_plateau line 107
  8. theorem OAI.NearbyLagrangian.RadialExtension.radial_trapping line 114
  9. theorem OAI.NearbyLagrangian.RadialExtension.radial_trapping_central line 143
  10. lemma OAI.NearbyLagrangian.RadialExtension.radialCurve_hasDerivWithinAt line 176
  11. theorem OAI.NearbyLagrangian.RadialExtension.hamiltonian_radial_trapping line 191
  12. lemma OAI.NearbyLagrangian.RadialExtension.cutoffHamiltonian_plateau_derivative line 245
  13. theorem OAI.NearbyLagrangian.RadialExtension.central_product_hamiltonian_curve line 262