OAI/NumberTheory/JointDickman/Analysis/CharacterLogPhase.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.imaginary_power_as_log_phase line 11
2. theorem OAI.JointDickman.character_log_phase_uniform line 25

   Source documentation

   A character contributes at most the finite Fourier expansion factor q. The power saving is uniform in the character.

   theorem character_log_phase_uniform (B : ℝ) (hB : 1/2 ≤ B) :
       ∃ A δ : ℝ, 0 < A ∧ 0 < δ ∧
         ∀ᶠ U : ℝ in atTop, ∀ (q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q)
           (t : ℝ) (L R : ℤ),
           U^(1/2:ℝ) ≤ |t/(2*Real.pi)| → |t/(2*Real.pi)| ≤ U^B →
           U ≤ (L:ℝ) → (R:ℝ) ≤ 2*U →
           ‖∑ n ∈ Finset.Icc L R, χ (n:ZMod q)*(n:ℂ)^(-((t:ℂ)*I))‖ ≤
             (q:ℝ)*A*U^(1-δ) := by
   …