OAI/NumberTheory/TwoPoint/Bounds/DilatedWindowParameters.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform parameter bounds for the exact smooth-divisor MRT reduction.

  1. lemma OAI.TwoPointCorrelations.dilation_quotient_log_upper line 12
  2. lemma OAI.TwoPointCorrelations.dilation_cutoff_error_bounds line 33
  3. structure OAI.TwoPointCorrelations.DilationWindowParameters line 63
  4. theorem OAI.TwoPointCorrelations.eventually_dilationWindowParameters line 76