OAI/NumberTheory/TwoPoint/Bounds/WeightedDivisorWord.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Convert the full residue-weighted divisor word to its exact centered form.

  1. theorem OAI.TwoPointCorrelations.uniform_weighted_divisor_word_average line 13