OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterSmallHeight.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A concrete low-height range in the original Liouville prime tail. Only nonprincipal characters are covered here.

  1. lemma OAI.TwoPointCorrelations.mrt_prime_power_cutoff_log_lower line 15
  2. lemma OAI.TwoPointCorrelations.mrt_character_small_height_bound line 39
  3. lemma OAI.TwoPointCorrelations.mrt_character_small_height_cost line 58
  4. theorem OAI.TwoPointCorrelations.mrt_liouville_nonprincipal_small_height line 98