OAI/NumberTheory/TwoPoint/ShortIntervals/MRTLogPartition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual logarithmic prime-polynomial family in the finite first-small partition. Index r corresponds to prime band r+1.

  1. def OAI.TwoPointCorrelations.mrtLogFamilyBins line 14
  2. def OAI.TwoPointCorrelations.mrtLogFamilyPolynomial line 18
  3. def OAI.TwoPointCorrelations.mrtLogFamilyThreshold line 22
  4. def OAI.TwoPointCorrelations.mrtFirstLogClass line 26
  5. lemma OAI.TwoPointCorrelations.mrt_first_log_class_zero line 31
  6. lemma OAI.TwoPointCorrelations.mrt_first_log_class_succ_subset line 41
  7. theorem OAI.TwoPointCorrelations.mrt_log_partition_integral line 56