OAI/NumberTheory/Ostmann/Quadratic/QuadraticEulerCover.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A finite Euler product covering the original small squarefree indices

  1. def OAI.Ostmann.quadraticEulerPrimes line 11
  2. def OAI.Ostmann.quadraticEulerCover line 14
  3. theorem OAI.Ostmann.prime_product_squarefree line 17
  4. theorem OAI.Ostmann.quadraticEulerCover_squarefree line 33
  5. theorem OAI.Ostmann.quadraticEulerCover_odd line 39
  6. theorem OAI.Ostmann.quadraticEulerCover_coprime line 53
  7. theorem OAI.Ostmann.quadraticEulerCover_covers line 60
  8. theorem OAI.Ostmann.quadratic_main_coefficient_eq line 88

    Source documentation

    The literal alpha and beta coefficients agree at every index below the cutoff. There is no auxiliary covering hypothesis.

    theorem quadratic_main_coefficient_eq {D K w : ℕ} (hD : Squarefree D)
    (hDo : Odd D) (hw : w ≤ K) : quadraticMainAlpha D K w = quadraticMainBeta D K w :=
…

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

  9. theorem OAI.Ostmann.quadratic_main_gamma_zero line 94