OAI/NumberTheory/TwoPoint/Bounds/FinalCorrelationBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic assembly of the centering, endpoint deletion, and retained spectral estimates at the manuscript's final parameter choice.

  1. lemma OAI.TwoPointCorrelations.quantitative_deletion_small line 11
  2. lemma OAI.TwoPointCorrelations.reciprocal_cutoff_saving line 28
  3. lemma OAI.TwoPointCorrelations.correlation_normalized_bound line 42