OAI/NumberTheory/Ostmann/Quadratic/QuadraticRoughBound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticRoughBound line 13
2. theorem OAI.Ostmann.QuadraticRoughBound.mono_constant line 16
3. theorem OAI.Ostmann.quadraticRoughEnergy_restrict line 21
4. theorem OAI.Ostmann.QuadraticRoughBound.mono_second line 33
5. theorem OAI.Ostmann.quadratic_rough_divisibility line 39
6. def OAI.Ostmann.quadraticRoughGcdMoment line 52
7. theorem OAI.Ostmann.quadratic_gcd_kernel_remove line 57
8. theorem OAI.Ostmann.quadratic_rough_gcd_moment_divisors line 70

   Source documentation

   Removing the gcd and then the coprimality condition only introduces actual rough moments of divisor-restricted coefficients.

   theorem quadratic_rough_gcd_moment_divisors {M N K D : ℕ}
       (hD : Squarefree D) (ho : Odd D) (v : ℕ → ℂ) :
       ‖quadraticRoughGcdMoment M N K D v‖ ≤
         ∑ d ∈ Finset.Icc 1 (N / D), quadraticRoughEnergy M (N / D) K
           (fun n => if d ∣ n then quadraticDivisibilityCoeff D v n else 0) := by
   …

   Mentions: OAI.Ostmann.quadraticRoughGcdMoment, OAI.Ostmann.quadraticRoughEnergy, OAI.Ostmann.quadraticDivisibilityCoeff