OAI/NumberTheory/Ostmann/Quadratic/QuadraticPairKernel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The primitive kernel of a pair of odd squarefree denominators

Writing d = gcd n₁ n₂, the product character has squarefree kernel (n₁/d)(n₂/d) and the remaining factor is precisely the coprimality mask modulo d. This is the arithmetic decomposition in Heath-Brown (1995), §3.

  1. def OAI.Ostmann.quadraticPairKernel line 14
  2. theorem OAI.Ostmann.quadraticPairKernel_factor line 17
  3. theorem OAI.Ostmann.quadraticPairKernel_squarefree line 26
  4. theorem OAI.Ostmann.quadraticPairKernel_odd line 34
  5. theorem OAI.Ostmann.quadraticPairKernel_coprime_gcd line 39
  6. theorem OAI.Ostmann.quadraticPairKernel_eq_one_iff line 49
  7. theorem OAI.Ostmann.jacobi_pair_kernel line 67