OAI/NumberTheory/TwoPoint/ShortIntervals/MRTNoSmallEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

No-small-class energy, including the complete extra-band extraction error, under the sparse-prime estimate and the cofactor pointwise bound.

  1. theorem OAI.TwoPointCorrelations.mrt_no_small_energy_sharp line 13
  2. lemma OAI.TwoPointCorrelations.mrt_sharp_log_error_le line 87

    Source documentation

    Monotonicity in the additional-band error bound.

    lemma mrt_sharp_log_error_le {L : ℝ} (hL : 1 ≤ L) :
    Real.log L/L^(1/80:ℝ) ≤ Real.log L/L^(1/100:ℝ) := by
…
  3. theorem OAI.TwoPointCorrelations.mrt_no_small_energy line 93