OAI/NumberTheory/Ostmann/Quadratic/QuadraticMainSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The genuine support of the difference of quadratic Poisson main terms

  1. theorem OAI.Ostmann.quadraticMainAlpha_witness line 12
  2. theorem OAI.Ostmann.quadraticMainBeta_witness line 22
  3. theorem OAI.Ostmann.quadraticMainAlpha_support line 33
  4. theorem OAI.Ostmann.quadraticMainBeta_support line 49
  5. theorem OAI.Ostmann.quadraticMainGamma_support line 67

    Source documentation

    The difference is supported precisely in the required upper interval; its square part divides the original gcd, with no dependence on the character.

    theorem quadraticMainGamma_support {D K w : ℕ} (hD : Squarefree D) (hDo : Odd D)
    (h : quadraticMainGamma D K w ≠ 0) :
    K < w ∧ w ≤ K * D ^ 2 ∧ Odd w ∧ quadraticSquarePart w ∣ D := by
…

    Mentions: OAI.Ostmann.quadraticMainGamma, OAI.Ostmann.quadraticSquarePart