OAI/NumberTheory/TwoPoint/Bounds/QuantitativeRoughBins.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The quantitative rough-shift estimate on the actual logarithmic bins, retaining the absolute long-interval exponent 1000.

  1. theorem OAI.TwoPointCorrelations.quantitative_rough_real_bin line 14