OAI/NumberTheory/TwoPoint/Halasz/HalaszDoubleHolder.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The two Hölder steps in Ford's double mean-value argument (Lemma 5.1), with the full complete-system frequency on both sides.

  1. theorem OAI.TwoPointCorrelations.halasz_double_holder line 13