OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterGlobalTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A uniform prime-tail consequence of the effective all-height character strip, retaining its polynomial modulus cost explicitly.

  1. theorem OAI.TwoPointCorrelations.mrt_character_global_prime_tail line 14