OAI/NumberTheory/TwoPoint/Bounds/WeightedCenteredWord.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Keep the nonnegative weight inside the expectation when it is independent of tuple residues.

  1. theorem OAI.TwoPointCorrelations.uniform_weighted_centered_word_majorant line 13