OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterPrimeDerivative.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic derivative of an arbitrary Dirichlet L-series is its prime logarithmic series up to an absolute higher-prime-power correction. The correction is bounded uniformly as the real part tends to one.

  1. def OAI.TwoPointCorrelations.mrtCharacterPrimeLogTerm line 14
  2. def OAI.TwoPointCorrelations.mrtCharacterPrimePowerCoefficient line 18
  3. lemma OAI.TwoPointCorrelations.mrt_character_prime_power_term_bound line 22
  4. lemma OAI.TwoPointCorrelations.mrt_character_prime_power_summable line 40
  5. lemma OAI.TwoPointCorrelations.mrt_character_prime_power_LSeries_bound line 46
  6. lemma OAI.TwoPointCorrelations.mrt_character_mangoldt_term_split line 53
  7. lemma OAI.TwoPointCorrelations.mrt_character_prime_log_summable line 67
  8. theorem OAI.TwoPointCorrelations.mrt_character_logDerivative_prime_series line 79
  9. theorem OAI.TwoPointCorrelations.mrt_character_logDerivative_prime_error line 93
  10. theorem OAI.TwoPointCorrelations.mrt_character_logDerivative_real_prime_error line 100
  11. lemma OAI.TwoPointCorrelations.mrt_character_logDerivative_upper_of_prime_lower line 109
  12. theorem OAI.TwoPointCorrelations.mrt_character_LSeries_sigma_lower_of_prime_sum line 119

    Source documentation

    A lower bound on the smoothed prime logarithmic series throughout the sigma segment suffices for the character L-value ratio. All prime-power terms cost just one absolute constant.

    theorem mrt_character_LSeries_sigma_lower_of_prime_sum {q : ℕ}
    (χ : DirichletCharacter ℂ q) (hq : 0<q) (t : ℝ)
    {Y X : ℕ} (hY : 1≤Real.log (Y:ℝ)) (hYX : Y≤X)
    {K : ℝ} (hK : 0≤K)
    (hprime : ∀ σ ∈ Set.Ioo (1+1/Real.log (X:ℝ)) (1+1/Real.log (Y:ℝ)),
      -(K*Real.log (Y:ℝ))≤
        (∑' n : ℕ, mrtCharacterPrimeLogTerm χ ((σ:ℂ)-(t:ℂ)*Complex.I) n).re) :
    -K-halaszPrimePowerConstant≤
      Real.log ‖L ↗χ (1+(1/Real.log (X:ℝ):ℝ)-(t:ℂ)*Complex.I)‖-
      Real.log ‖L ↗χ (1+(1/Real.log (Y:ℝ):ℝ)-(t:ℂ)*Complex.I)‖ := by
…

    Mentions: OAI.TwoPointCorrelations.mrtCharacterPrimeLogTerm, OAI.TwoPointCorrelations.halaszPrimePowerConstant