OAI/NumberTheory/JointDickman/Analysis/MellinSieveScale.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Polynomial cutoffs for the explicit Mellin divisor error

  1. lemma OAI.JointDickman.mellinSieve_grid_error_coarse line 8
  2. theorem OAI.JointDickman.mellinSieve_integer_scale_low line 40

    Source documentation

    One fixed set of integer powers gives a common low-frequency range for all profiles between the tenth and eleventh powers.

    theorem mellinSieve_integer_scale_low (q d : ℕ) (hq : 2 ≤ q) (hd : 0 < d) (hdq : d ≤ q)
    {N t : ℝ} (hNlo : (q:ℝ)^10 ≤ N) (hNhi : N ≤ (q:ℝ)^11)
    (ht : |t| ≤ (q:ℝ)^7) :
    ‖mellinSieveDiscreteKernel (q^12) d N t-mellinSieveMainKernel N t/(d:ℂ)‖ ≤
      6*(q:ℝ)^9 := by
…

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