MellinSieveUniform.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform divisor-kernel errors on polynomial frequency ranges

lemma OAI.JointDickman.mellin_integer_dyadic_scale line 8
lemma OAI.JointDickman.mellin_integer_frequency_scale line 19

theorem OAI.JointDickman.mellinSieve_integer_scale_uniform line 41

Source documentation

A uniform divisor estimate up to q over a polynomial frequency range, with explicit level-dependent error.

theorem mellinSieve_integer_scale_uniform (B : ℝ) (hB : 1 ≤ B) :
    ∃ A δ V : ℝ, 0 < A ∧ 0 < δ ∧ δ ≤ 1 ∧
      ∀ (q d : ℕ), 16 ≤ q → 0 < d → d ≤ q → V ≤ (q:ℝ)^9 →
      ∀ (N t : ℝ), (q:ℝ)^10 ≤ N → N ≤ (q:ℝ)^11 → |t| ≤ (q:ℝ)^B →
      ‖mellinSieveDiscreteKernel (q^12) d N t-mellinSieveMainKernel N t/(d:ℂ)‖ ≤
        6*(q:ℝ)^9 + (Nat.log 2 (q^3)+1:ℕ)*A*N^(1-δ) := by
…

Mentions: OAI.JointDickman.mellinSieveDiscreteKernel, OAI.JointDickman.mellinSieveMainKernel