OAI/NumberTheory/TwoPoint/ShortIntervals/MRTSparseContourScale.lean
2 declarations, 0 contain sorry, 0 declared as axioms
Numerical compatibility of the narrower sparse-prime contour with the weak VK strip, uniformly over its full finite height.
- lemma
OAI.TwoPointCorrelations.mrt_sparse_contour_heightline 13 - lemma
OAI.TwoPointCorrelations.mrt_sparse_contour_budgetline 23