OAI/NumberTheory/TwoPoint/Walks/CanonicalPartialWindows.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual logarithmic bins and bounded padding provide the window and length hypotheses in the quantitative partial-centering estimate.

  1. lemma OAI.TwoPointCorrelations.partial_bin_window line 15
  2. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_partial_extracted_windows line 41