OAI/NumberTheory/Ostmann/Quadratic/QuadraticSecondMomentError.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The full second-Poisson remainder on the original dyadic coefficient block

  1. theorem OAI.Ostmann.quadratic_gcd_remainder_support_bound line 12
  2. theorem OAI.Ostmann.quadratic_pair_dyadic_kernel line 37
  3. def OAI.Ostmann.quadraticSecondMomentError line 67
  4. theorem OAI.Ostmann.quadratic_second_moment_error line 72
  5. theorem OAI.Ostmann.quadratic_polynomial_error_power_choice line 112
  6. theorem OAI.Ostmann.quadratic_second_moment_arbitrary_power line 131