OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterEuler.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite character Euler product and the real prime sum differ, after taking log norm, by an absolute prime-square error. This reduces the Liouville prime-tail estimate to a genuine Euler-product lower bound.

  1. lemma OAI.TwoPointCorrelations.mrt_local_euler_log_error line 14
  2. def OAI.TwoPointCorrelations.mrtCharacterPrimeEuler line 31
  3. theorem OAI.TwoPointCorrelations.mrt_character_euler_log_error line 35
  4. lemma OAI.TwoPointCorrelations.mrt_character_prime_sum_ge_of_euler_log line 75