OAI/NumberTheory/TwoPoint/Bounds/ModifiedShortSums.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The precise MRT input on actual progression windows, uniformly over all multiplicative finite-prime changes of the original nonpretentious factor.

  1. theorem OAI.TwoPointCorrelations.MRTShortExponentialInput.modified_windows line 13