OAI/NumberTheory/JointDickman/Analysis/MellinProfileBlock.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.mellin_sum_Icc_split line 10
2. lemma OAI.JointDickman.mellin_profile_crossing_bound line 22
3. lemma OAI.JointDickman.mellin_profile_block_bound line 52
4. theorem OAI.JointDickman.mellin_profile_block_uniform line 118

   Source documentation

   A fixed polynomial frequency range has a positive power saving for all the scaled profile blocks, uniformly in the profile's maximum.

   theorem mellin_profile_block_uniform (B : ℝ) (hB : 1/2 ≤ B) :
       ∃ A δ : ℝ, 0 < A ∧ 0 < δ ∧ δ ≤ 1 ∧
         ∀ᶠ U : ℝ in atTop, ∀ (N t : ℝ) (L R : ℤ), 1 ≤ N →
           U^(1/2:ℝ) ≤ |t/(2*Real.pi)| → |t/(2*Real.pi)| ≤ U^B →
           U ≤ (L:ℝ) → (R:ℝ) ≤ 2*U →
           ‖∑ n ∈ Icc L R, mellinSieveFunction N t n‖ ≤ A*N^(1-δ) := by
   …

   Mentions: OAI.JointDickman.mellinSieveFunction

5. theorem OAI.JointDickman.mellin_dilated_profile_block_uniform line 140