OAI/Geometry/NearbyLagrangian/CriticalSections.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Smooth nondegenerate critical sections at zero-section endpoints.

  1. theorem OAI.NearbyLagrangian.derivative_zero_on_regular_level line 22
  2. lemma OAI.NearbyLagrangian.Generating.contDiffAt_vertical line 59
  3. theorem OAI.NearbyLagrangian.Generating.vertical_hessian_injective_of_zero_momentum line 64
  4. theorem OAI.NearbyLagrangian.Generating.vertical_hessian_bijective_of_zero_momentum line 93
  5. theorem OAI.NearbyLagrangian.Generating.contDiff_criticalSection_of_zero_momentum line 105
  6. theorem OAI.NearbyLagrangian.Generating.exists_smooth_nondegenerate_criticalSection line 127
  7. lemma OAI.NearbyLagrangian.Transport.phase_zero_momentum line 157
  8. lemma OAI.NearbyLagrangian.Transport.phase_unique_critical line 170
  9. theorem OAI.NearbyLagrangian.Transport.open_zeroSection_endpoint line 196
  10. lemma OAI.NearbyLagrangian.Transport.TameOn.mono line 239
  11. lemma OAI.NearbyLagrangian.Transport.phase_range_restrict line 249
  12. lemma OAI.NearbyLagrangian.Transport.phase_injective_restrict line 260
  13. theorem OAI.NearbyLagrangian.Transport.transported_central_zeroSection_endpoint line 268