OAI/Geometry/RCD/Coordinates/FrameVelocityDefect.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative scalar velocity recovery from dense residual tests

  1. theorem OAI.RegularPointCoordinates.velocity_defect_of_dense_residual_bounds line 12
  2. theorem OAI.RegularPointCoordinates.scalar_velocity_abs_error line 25