OAI/NumberTheory/TwoPoint/Walks/CanonicalCenteringBins.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Sum the actual partial-centering errors over the logarithmic bins. The interval exponent remains the absolute value 1000.

  1. lemma OAI.TwoPointCorrelations.bin_cutoff_ge line 14
  2. lemma OAI.TwoPointCorrelations.bin_partial_error_sum_bound line 22
  3. theorem OAI.TwoPointCorrelations.quantitative_canonical_centering_bins line 53