OAI/NumberTheory/Ostmann/Quadratic/QuadraticOriginalMainTerms.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The two original Poisson main terms and their proved comparison

The common real factor (sqrt M / 2 times the fixed smoothing integral) is omitted from both terms. All character, totient and gcd factors are retained.

  1. def OAI.Ostmann.quadraticFirstMain line 15
  2. def OAI.Ostmann.quadraticSecondMain line 23
  3. theorem OAI.Ostmann.quadratic_original_main_difference line 30
  4. theorem OAI.Ostmann.quadratic_original_main_comparison line 71