OAI/NumberTheory/TwoPoint/ShortIntervals/MRTRieszEstimate.lean
3 declarations, 0 contain sorry, 0 declared as axioms
The sparse-prime Riesz kernel estimate, with no upper restriction on the prime cutoff. Far tails are charged to the pole term.
- lemma
OAI.TwoPointCorrelations.mrt_riesz_finite_shift_simpleline 16 - theorem
OAI.TwoPointCorrelations.MRTWeakHurwitzGrowthInput.riesz_sparse_kernelline 45 - theorem
OAI.TwoPointCorrelations.MRTWeakHurwitzGrowthInput.prime_sparseline 159