OAI/NumberTheory/TwoPoint/Bounds/DilatedRoughBins.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual real bins for the direct dilation estimates, retaining their single Euler cost for subsequent averaging over padding divisors.

  1. theorem OAI.TwoPointCorrelations.qualitative_dilated_rough_shifts_real_bins line 14
  2. theorem OAI.TwoPointCorrelations.qualitative_dilated_rough_shifts_real_bins_right line 50