OAI/NumberTheory/Ostmann/Arithmetic/MovingDiagonalErrorBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The retained comparison errors in the full diagonal estimate

  1. theorem OAI.Ostmann.moving_diagonal_four_term_bound line 11
  2. theorem OAI.Ostmann.eventual_moving_comparison_error line 19
  3. theorem OAI.Ostmann.moving_diagonal_reserve line 31