OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterEulerTail.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Absolute truncation of the character Euler product at sigma=1+1/log X. Together with the horizontal shift this identifies the finite prime sum with the logarithm of the actual L-series, up to an absolute error.

  1. lemma OAI.TwoPointCorrelations.mrt_character_shifted_norm line 15
  2. lemma OAI.TwoPointCorrelations.mrt_character_shifted_log_sum line 30
  3. lemma OAI.TwoPointCorrelations.mrt_character_shifted_log_local line 46
  4. lemma OAI.TwoPointCorrelations.mrt_character_shifted_finite_tail line 69
  5. theorem OAI.TwoPointCorrelations.mrt_character_LSeries_truncation line 106
  6. theorem OAI.TwoPointCorrelations.mrt_character_euler_LSeries_comparison line 123
  7. theorem OAI.TwoPointCorrelations.mrt_character_prime_tail_LSeries_ratio line 136