OAI/Geometry/SurfaceImmersion/Primitive/UniformPrimitiveRemainder.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One finite loss and one coefficient profile control all metric components of the actual periodic primitive, before the slow map is selected.

  1. theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.uniform_primitive_remainder line 14