OAI/NumberTheory/Ostmann/Quadratic/QuadraticNegligibleError.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Arbitrary power saving for the complete second-Poisson truncation error

  1. theorem OAI.Ostmann.quadratic_second_error_arbitrary_power line 11