QuadraticGcdMainGrowth.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The genuine main-term cancellation under the current sieve exponent

theorem OAI.Ostmann.quadratic_gcd_main_growth line 13

theorem OAI.Ostmann.quadratic_gcd_main_exponent line 50

Source documentation

Only the fourth power of the common divisor is needed for exponents at most two; the shortened matrix parameter remains the actual integer K D².

theorem quadratic_gcd_main_exponent {ξ : ℝ} (hξ : ξ ≤ 2)
    {K D : ℕ} (hK : 0 < K) (hD : 0 < D) (N : ℝ) (hN : 0 ≤ N) :
    (((K * D ^ 2 : ℕ) : ℝ) ^ ξ + N) ≤
      (D : ℝ) ^ 4 * ((K : ℝ) ^ ξ + N) := by
…