OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrincipalCorrection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The principal character differs from zeta by the Euler factors at primes dividing its modulus. Their total logarithmic derivative has norm at most log(q), uniformly on Re(s)>=1.

  1. def OAI.TwoPointCorrelations.mrtPrincipalEulerFactor line 15
  2. lemma OAI.TwoPointCorrelations.mrt_principal_factor_cpow_norm line 18
  3. lemma OAI.TwoPointCorrelations.mrt_principal_factor_norm_ge line 26
  4. lemma OAI.TwoPointCorrelations.mrt_principal_factor_ne_zero line 36
  5. lemma OAI.TwoPointCorrelations.mrt_principal_factor_hasDeriv line 43
  6. lemma OAI.TwoPointCorrelations.mrt_principal_factor_logderiv_norm line 50
  7. lemma OAI.TwoPointCorrelations.mrt_prime_factor_log_sum line 70
  8. theorem OAI.TwoPointCorrelations.mrt_principal_logderiv line 82
  9. theorem OAI.TwoPointCorrelations.mrt_principal_logderiv_error line 107