QuadraticMainComparison.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The main-term comparison in Heath-Brown's quadratic-sieve recursion

theorem OAI.Ostmann.quadratic_totient_kernel_sum_bound line 12
def OAI.Ostmann.quadraticMainDifference line 39

theorem OAI.Ostmann.quadratic_main_comparison line 45

Source documentation

The actual arithmetic main-term difference is controlled by quadratic energy at the shorter frequency range. All divisor losses are explicit.

theorem quadratic_main_comparison (ε : ℝ) (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ N D K : ℕ, Squarefree D → Odd D → 0 < K →
      ∀ T : ℝ, 0 ≤ T → QuadraticSieveBound (K * D ^ 2) N T → ∀ b : ℕ → ℂ,
      ‖quadraticMainDifference N D K b‖ ≤
        C * ((K * D ^ 2 : ℕ) : ℝ) ^ ε * (N : ℝ) ^ ε * (D : ℝ) ^ ε /
          Real.sqrt (K : ℝ) * T * quadraticSieveEnergy N b := by
…

Mentions: OAI.Ostmann.QuadraticSieveBound, OAI.Ostmann.quadraticMainDifference, OAI.Ostmann.quadraticSieveEnergy