OAI/NumberTheory/TwoPoint/ShortIntervals/MRTLogClassData.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Literal logarithmic prime polynomials and their small/large frequency sets. These sets supply the hypotheses of the general cofactor estimates.

  1. def OAI.TwoPointCorrelations.mrtLogPrimePolynomial line 16
  2. def OAI.TwoPointCorrelations.mrtLogSmallSet line 21
  3. def OAI.TwoPointCorrelations.mrtLogLargeSet line 26
  4. lemma OAI.TwoPointCorrelations.mrt_log_prime_polynomial_continuous line 31
  5. lemma OAI.TwoPointCorrelations.mrt_log_small_set_measurable line 35
  6. lemma OAI.TwoPointCorrelations.mrt_log_large_set_measurable line 47
  7. lemma OAI.TwoPointCorrelations.mrt_log_bin_lower_gt_one line 59
  8. lemma OAI.TwoPointCorrelations.mrt_log_bin_prime_data line 69