OAI/NumberTheory/JointDickman/Analysis/LogPhaseSharpBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Sharp dyadic logarithmic sums in the first two derivative ranges

  1. lemma OAI.JointDickman.log_phase_sum_neg line 11
  2. lemma OAI.JointDickman.log_phase_sum_trivial line 16
  3. lemma OAI.JointDickman.log_phase_second_bound line 26
  4. theorem OAI.JointDickman.log_phase_sharp_bound line 73

    Source documentation

    Uniform sharp-interval estimate. The square-root term is used only above the first derivative range.

    theorem log_phase_sharp_bound {U : ℝ} (hU : 1 ≤ U) (Z : ℝ) (L R : ℕ)
    (hL : U ≤ (L:ℝ)) (hR : (R:ℝ) ≤ 2*U) :
    ‖∑ n ∈ Icc L R, ExponentialSum.phase (Z*Real.log (n:ℝ))‖ ≤
      2000*(U/(1+|Z|)+Real.sqrt |Z|) := by
…