OAI/NumberTheory/TwoPoint/ShortIntervals/MRTLiouvillePrimitive.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

On the actual Liouville prime tail, every prime is larger than the allowed character modulus. Passing to the primitive character therefore leaves the prime sum exactly unchanged.

  1. lemma OAI.TwoPointCorrelations.mrt_primitive_character_twist line 14
  2. lemma OAI.TwoPointCorrelations.mrt_liouville_tail_above_modulus line 25
  3. theorem OAI.TwoPointCorrelations.mrt_liouville_tail_primitive line 38
  4. theorem OAI.TwoPointCorrelations.mrt_liouville_short_of_primitive_prime_tail line 48