OAI/NumberTheory/Ostmann/Quadratic/QuadraticRoughGcdDescent.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.quadratic_divisor_coefficient_weight line 13
2. theorem OAI.Ostmann.quadratic_rough_gcd_shorter line 29
3. theorem OAI.Ostmann.quadratic_rough_energy_gcd line 46
4. theorem OAI.Ostmann.quadratic_rough_gcd_moment_zero line 55
5. theorem OAI.Ostmann.quadratic_rough_gcd_descent line 62

   Source documentation

   Heath-Brown's large-gcd descent, with the original small-gcd moments left literal. The shorter range is the integer quotient N/D₀.

   theorem quadratic_rough_gcd_descent {M N K D₀ : ℕ} {T : ℝ}
       (hD₀ : 0 < D₀) (hT : 0 ≤ T) (h : QuadraticRoughBound M (N / D₀) K T)
       (v : ℕ → ℂ) :
       quadraticRoughEnergy M N K v ≤
         (∑ D ∈ (Finset.Icc 1 N).filter (fun D => D ≤ D₀),
           ‖quadraticRoughGcdMoment M N K D v‖) + T * quadraticDivisorMoment N v := by
   …

   Mentions: OAI.Ostmann.QuadraticRoughBound, OAI.Ostmann.quadraticRoughEnergy, OAI.Ostmann.quadraticRoughGcdMoment, OAI.Ostmann.quadraticDivisorMoment