OAI/Geometry/NearbyLagrangian/FiberJets.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Triangular regular systems and fiber jet coordinates.

  1. def OAI.NearbyLagrangian.Transport.triangularSystem line 23
  2. def OAI.NearbyLagrangian.Transport.triangularDerivative line 27
  3. lemma OAI.NearbyLagrangian.Transport.hasFDerivAt_triangularSystem line 35
  4. theorem OAI.NearbyLagrangian.Transport.triangularDerivative_surjective line 48
  5. theorem OAI.NearbyLagrangian.Transport.regular_triangularSystem line 72
  6. def OAI.NearbyLagrangian.Transport.supportedCoordinates line 83
  7. def OAI.NearbyLagrangian.Transport.fiberJetCoordinates line 106
  8. def OAI.NearbyLagrangian.Transport.fiberDifferential line 115
  9. lemma OAI.NearbyLagrangian.Transport.fiberDifferential_congr line 120
  10. lemma OAI.NearbyLagrangian.Transport.fiberJetCoordinates_apply line 125
  11. lemma OAI.NearbyLagrangian.Transport.fiberJetCoordinates_fiberDifferential line 134
  12. def OAI.NearbyLagrangian.Transport.totalPhase line 158
  13. def OAI.NearbyLagrangian.Transport.mixedDisplacement line 162
  14. lemma OAI.NearbyLagrangian.Transport.innerSL_mixedDisplacement line 165