OAI/NumberTheory/Ostmann/Quadratic/QuadraticMiddleDivisor.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The literal middle-frequency correction in the second Poisson formula

  1. def OAI.Ostmann.quadraticMiddleDivisor line 13
  2. theorem OAI.Ostmann.quadratic_middle_divisor_eq line 22
  3. def OAI.Ostmann.quadraticMiddleWindow line 35
  4. theorem OAI.Ostmann.quadratic_middle_window_eq line 44
  5. theorem OAI.Ostmann.quadratic_middle_divisor_bound line 60
  6. theorem OAI.Ostmann.quadratic_middle_window_bound line 93