OAI/Geometry/NearbyLagrangian/BalancedCoordinates.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Hyperbolic and balanced coordinates for iterated transport.

  1. def OAI.NearbyLagrangian.Transport.hyperbolicCoordinates line 18
  2. lemma OAI.NearbyLagrangian.Transport.hyperbolicCoordinates_form line 29
  3. def OAI.NearbyLagrangian.Tubes.addBalanced line 41
  4. lemma OAI.NearbyLagrangian.Tubes.addBalanced_apply line 45
  5. def OAI.NearbyLagrangian.Tubes.transportIndex line 51
  6. lemma OAI.NearbyLagrangian.Tubes.le_transportIndex line 55
  7. lemma OAI.NearbyLagrangian.Tubes.transportIndex_eq line 60
  8. def OAI.NearbyLagrangian.Tubes.addBalancedFor line 65
  9. def OAI.NearbyLagrangian.Transport.transportCoordinates line 75
  10. lemma OAI.NearbyLagrangian.Transport.iterReference_transportCoordinates line 83
  11. lemma OAI.NearbyLagrangian.Transport.iterReference_transportCoordinates_at line 100