OAI/NumberTheory/TwoPoint/Bounds/DilatedWindowScale.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The smooth-divisor truncation is far below the original window length. All surviving quotient windows retain a fixed positive fraction of its logarithmic length.

  1. def OAI.TwoPointCorrelations.dilationCutoff line 16
  2. lemma OAI.TwoPointCorrelations.quotient_log_error_bound line 19
  3. lemma OAI.TwoPointCorrelations.dilationCutoff_bounds line 49
  4. lemma OAI.TwoPointCorrelations.dilation_quotient_log_lower line 65