OAI/NumberTheory/TwoPoint/Bounds/GoodWeightedDifferenceSum.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Average the good-word forest estimate while retaining the exact padding normalization.

  1. theorem OAI.TwoPointCorrelations.good_weighted_difference_sum line 13