OAI/NumberTheory/TwoPoint/Halasz/HalaszFiniteHolder.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The two finite Hölder steps used in the double mean-value argument.

  1. lemma OAI.TwoPointCorrelations.halasz_finite_weighted_power line 11
  2. theorem OAI.TwoPointCorrelations.halasz_finite_weighted_holder line 29
  3. lemma OAI.TwoPointCorrelations.halasz_complex_sum_power line 46