OAI/NumberTheory/TwoPoint/ShortIntervals/MRTLiouvilleLSeries.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Reduction of the Liouville distance estimate to a uniform lower bound for a Dirichlet L-value ratio.

  1. def OAI.TwoPointCorrelations.mrtPrimePowerCutoff line 14
  2. lemma OAI.TwoPointCorrelations.mrt_sievePrimesUpTo_floor line 17
  3. lemma OAI.TwoPointCorrelations.mrt_prime_power_tail_cutoff line 22
  4. theorem OAI.TwoPointCorrelations.mrt_prime_power_cutoff_eventually line 27
  5. theorem OAI.TwoPointCorrelations.mrt_character_power_tail_LSeries_ratio line 55
  6. theorem OAI.TwoPointCorrelations.mrt_liouville_distance_from_LSeries_ratio line 69
  7. theorem OAI.TwoPointCorrelations.mrt_liouville_short_of_LSeries_ratio line 95