OAI/NumberTheory/Ostmann/Quadratic/QuadraticSmallGcdTransform.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.quadratic_rough_gcd_pair_sum line 12
2. theorem OAI.Ostmann.quadratic_rough_gcd_transform line 37
3. theorem OAI.Ostmann.quadratic_small_gcd_ne_diagonal line 49

   Source documentation

   Small gcds cannot contain a diagonal pair in the actual dyadic support.

   theorem quadratic_small_gcd_ne_diagonal {R D : ℕ} (hDR : D < R)
       (v : ℕ → ℂ) (hsupp : ∀ n ∈ oddSquarefreeRange (2 * R), n < R → v n = 0)
       {z : ℕ × ℕ} (hz : z ∈ quadraticGcdPairs (2 * R) D) (hv : v z.1 ≠ 0) :
       z.1 ≠ z.2 := by
   …

   Mentions: OAI.Ostmann.oddSquarefreeRange, OAI.Ostmann.quadraticGcdPairs

4. def OAI.Ostmann.quadraticGcdMomentCorrections line 61
5. def OAI.Ostmann.quadraticGcdMomentError line 69
6. theorem OAI.Ostmann.quadratic_small_gcd_moment_decomposition line 78