OAI/Combinatorics/EditApproximation/Geometry/GroupSmallConstants.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The prescribed small parameters satisfy the group and online error inequalities.

  1. theorem OAI.EditApproximation.group_online_range_small line 9
  2. theorem OAI.EditApproximation.group_online_eta_range line 23
  3. theorem OAI.EditApproximation.group_rounded_error_small line 32