OAI/NumberTheory/JointDickman/Analysis/CharacterContourBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.characterContourSeries_small_power line 9
2. theorem OAI.JointDickman.characterContourSeries_rectangle_bound line 40

   Source documentation

   On a fixed-height rectangle the bound depends on the height and modulus only.

   theorem characterContourSeries_rectangle_bound {z η : ℝ}
       (hz : 0 ≤ z) (hz1 : z ≤ 1) (hη : 0 < η) (hη1 : η ≤ 1/4) :
       ∃ C : ℝ, 0 < C ∧ ∀ (q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q),
         χ ≠ 1 → ∀ (f : ℂ → ℂ) (T : ℝ), 0 ≤ T → ∀ s : ℂ,
         1-η/2 ≤ s.re → s.re ≤ 2 → |s.im| ≤ T →
         Complex.exp (f s) = χ.LFunction s →
         ‖characterContourSeries χ z f s‖ ≤ C * (((q:ℝ)+2)*(T+2))^η := by
   …

   Mentions: OAI.JointDickman.characterContourSeries