OAI/NumberTheory/JointDickman/Analysis/MovingCharacterBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.roughTruncation_rankin_full line 13
2. theorem OAI.JointDickman.roughCharacterSum_exponential line 31

   Source documentation

   Every fixed logarithmic saving survives the convolution, at the cost of a fixed power of the cutoff logarithm and an explicit Rankin error.

   theorem roughCharacterSum_exponential
       (hSW : PublishedInputs.SquarefreeCharacterEstimateInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput) {z : ℝ}
       (hz : z = 1 / 4 ∨ z = 1 / 2) {D : ℝ} (hD : 0 ≤ D) :
       ∃ K : ℝ, 0 ≤ K ∧ ∀ (P : ℕ) (Y : ℝ),
         2 ≤ P → 1 ≤ Real.log P → 9 ≤ Y → 16 ≤ Real.log Y →
         ∀ (q : ℕ) [NeZero q], (q : ℝ) ≤ (Real.log Y / 2) ^ (200 : ℝ) →
         ∀ χ : DirichletCharacter ℂ q, χ ≠ 1 →
         ‖roughCharacterSum χ (Nat.primesLE P) z Y‖ ≤
           Y * K * ((Real.log Y) ^ (-D) * (Real.log P) ^ (Real.exp 1 + 1) +
             (Real.log P) ^ (Real.exp 1) * Real.exp (-(Real.log Y / (8 * Real.log P)))) := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.SquarefreeCharacterEstimateInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.roughCharacterSum