OAI/NumberTheory/Ostmann/Quadratic/QuadraticMainCoefficients.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.quadraticMainAlpha line 12
2. def OAI.Ostmann.quadraticMainBeta line 16
3. def OAI.Ostmann.quadraticMainGamma line 20
4. theorem OAI.Ostmann.quadratic_euler_coefficient line 23
5. theorem OAI.Ostmann.quadratic_main_coefficient_eq_of_cover line 42

   Source documentation

   Once the finite Euler product contains the small squarefree integers, its coefficient identity applies to the literal cutoffs used in the main terms.

   theorem quadratic_main_coefficient_eq_of_cover {D R K w : ℕ}
       (hD : Squarefree D) (hR : Squarefree R) (hDR : D.Coprime R)
       (hDo : Odd D) (hRo : Odd R)
       (hcover : oddSquarefreeRange K ⊆ (D * R).divisors) (hw : w ≤ K) :
       quadraticMainAlpha D K w = quadraticMainBeta D K w := by
   …

   Mentions: OAI.Ostmann.oddSquarefreeRange, OAI.Ostmann.quadraticMainAlpha, OAI.Ostmann.quadraticMainBeta