OAI/NumberTheory/TwoPoint/Bounds/DilatedRoughRight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The same dilated rough-shift estimate when the original second factor is uniformly nonpretentious.

  1. theorem OAI.TwoPointCorrelations.qualitative_dilated_rough_shifts_right line 14