OAI/NumberTheory/TwoPoint/Walks/CanonicalBinSummation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Sum the actual retained bin correlations, normalized by the exact retained divisor mass. The input functions may differ from bin to bin.

  1. def OAI.TwoPointCorrelations.canonicalRetainedPrefix line 14
  2. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_canonical_bin_sum_uniform line 28
  3. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_canonical_bin_sum line 69