OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterLogDerivative.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Real-sigma integration of the logarithmic derivative. The real logarithm of the norm is differentiated through normSq, so no branch choice for the complex logarithm is needed.

  1. lemma OAI.TwoPointCorrelations.mrt_hasDerivAt_log_norm line 17
  2. lemma OAI.TwoPointCorrelations.mrt_log_norm_sigma_bound line 41
  3. lemma OAI.TwoPointCorrelations.mrt_log_norm_sigma_upper line 55
  4. lemma OAI.TwoPointCorrelations.mrt_character_LSeries_real_deriv line 73
  5. theorem OAI.TwoPointCorrelations.mrt_character_LSeries_sigma_ratio line 85
  6. theorem OAI.TwoPointCorrelations.mrt_character_LSeries_sigma_lower line 131

    Source documentation

    The one-sided version is compatible with the principal-character pole: only an upper bound for the real logarithmic derivative is used.

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