OAI/NumberTheory/TwoPoint/Bounds/LogSavingScale.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Convert the fixed prime-count saving into the final logarithmic power, retaining a single exponent for all affine coefficients.

  1. lemma OAI.TwoPointCorrelations.primeSupplyCount_log_saving line 10
  2. lemma OAI.TwoPointCorrelations.log_saving_exponent_pos line 26