OAI/Geometry/NearbyLagrangian/VerticalChanges.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Linear changes of fiber coordinates and restored tube endpoints.

  1. def OAI.NearbyLagrangian.Transport.verticalChange line 20
  2. lemma OAI.NearbyLagrangian.Transport.verticalChange_fderiv line 22
  3. lemma OAI.NearbyLagrangian.Transport.verticalChange_base line 27
  4. lemma OAI.NearbyLagrangian.Transport.verticalChange_vertical line 34
  5. lemma OAI.NearbyLagrangian.Transport.verticalChange_critical_iff line 42
  6. theorem OAI.NearbyLagrangian.Transport.TameOn.verticalChange line 54
  7. lemma OAI.NearbyLagrangian.Transport.verticalChange_hessian line 112
  8. lemma OAI.NearbyLagrangian.Transport.verticalChange_hessian_bijective line 130
  9. def OAI.NearbyLagrangian.Tubes.tubeCoe line 147
  10. theorem OAI.NearbyLagrangian.Tubes.lift_tube_homotopy line 150
  11. theorem OAI.NearbyLagrangian.Tubes.StablyNonNull.of_homotopic line 176
  12. theorem OAI.NearbyLagrangian.Transport.exists_restored_tube_endpoint line 192