OAI/NumberTheory/JointDickman/Analysis/CharacterConvolution.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.characterTwist line 12
2. theorem OAI.JointDickman.characterTwist_apply line 16
3. theorem OAI.JointDickman.characterTwist_mul line 20
4. def OAI.JointDickman.roughCharacterSum line 32
5. def OAI.JointDickman.characterConvolutionTail line 36
6. theorem OAI.JointDickman.roughCharacterSum_split line 41
7. theorem OAI.JointDickman.squarefreeCharacterSum_norm_le line 59
8. theorem OAI.JointDickman.characterConvolutionTail_rankin line 77

   Source documentation

   Twisting cannot enlarge the Rankin remainder.

   theorem characterConvolutionTail_rankin {q : ℕ} [NeZero q]
       (χ : DirichletCharacter ℂ q) (E : Finset ℕ) {z ε : ℝ}
       (hz : 0 ≤ z) (hz1 : z ≤ 1) (hε : 0 ≤ ε) (N V : ℕ) (hV : 0 < V) :
       ‖characterConvolutionTail χ E z N V‖ ≤
         ((N : ℝ) / (V : ℝ) ^ ε) *
           ∑ v ∈ Ioc V N, |smoothCorrection E z v| / (v : ℝ) ^ (1 - ε) := by
   …

   Mentions: OAI.JointDickman.characterConvolutionTail, OAI.JointDickman.smoothCorrection