QuadraticEulerCancellation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact Euler cancellation of the two quadratic Poisson main terms

This is the finite arithmetic identity in Heath-Brown (1995), §7, Lemma 5. The monomial index records the integer in each character, not a formal degree.

def OAI.Ostmann.quadraticMonomial line 18
theorem OAI.Ostmann.quadraticMonomial_multiplicative line 21
theorem OAI.Ostmann.quadraticMonomial_euler_add line 29
theorem OAI.Ostmann.quadraticMonomial_euler_sub line 44

theorem OAI.Ostmann.quadratic_euler_cancellation line 62

Source documentation

Exact cancellation before imposing the two finite cutoffs.

theorem quadratic_euler_cancellation {D R : ℕ} (hD : Squarefree D) (hR : Squarefree R)
    (hDR : D.Coprime R) :
    (∑ e ∈ D.divisors, single e (ArithmeticFunction.moebius e)) *
        (∑ b ∈ (D * R).divisors, single b (1 : ℤ)) =
      (∑ u ∈ D.divisors, single (u ^ 2) (ArithmeticFunction.moebius u)) *
        (∑ v ∈ R.divisors, single v (1 : ℤ)) := by
…