OAI/Geometry/SurfaceImmersion/Primitive/GeometricControlledVelocity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Construct the actual four-dimensional velocity with exact mean and metric, from its smooth geometric frame.

  1. lemma OAI.ClosedSurfaceR4.VelocityFrame.scaled_coordinates_reconstruct line 15
  2. theorem OAI.ClosedSurfaceR4.VelocityFrame.geometric_controlled_velocity line 26