OAI/NumberTheory/JointDickman/Analysis/LogPhaseFirstDerivative.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A first-derivative bound for short logarithmic phase sums

  1. lemma OAI.JointDickman.log_step_bounds line 9
  2. lemma OAI.JointDickman.log_step_antitone line 24
  3. theorem OAI.JointDickman.positive_log_phase_first_bound line 35

    Source documentation

    Below the first stationary range the sharp logarithmic sum is bounded by the reciprocal frequency, with no length-dependent error.

    theorem positive_log_phase_first_bound {U Z : ℝ} (hU : 1 ≤ U)
    (hZ : 0 < Z) (hZU : Z ≤ U/4) (L R : ℕ)
    (hL : U ≤ (L:ℝ)) (hR : (R:ℝ) ≤ 2*U) :
    ‖∑ n ∈ Icc L R, ExponentialSum.phase (Z*Real.log (n:ℝ))‖ ≤ 8*U/Z := by
…