OAI/NumberTheory/JointDickman/Analysis/CharacterDyadicSum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.character_cpow_split line 11
2. lemma OAI.JointDickman.rpow_weight_dyadic_bound line 21
3. theorem OAI.JointDickman.character_dyadic_sum_uniform line 34

   Source documentation

   The logarithmic phase estimate survives the full Dirichlet-series weight, with a decaying bound for each dyadic interval.

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