OAI/NumberTheory/TwoPoint/Halasz/HalaszGeneralMean.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The ordinary Halász estimate for general normalized multiplicative functions. Only the values at primes enter the pretentious hypothesis.

  1. lemma OAI.TwoPointCorrelations.halasz_complete_distance line 15

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszGeneralMean.lean:15 (same declaration text).

  2. theorem OAI.TwoPointCorrelations.halasz_general_mean_value line 25

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszGeneralMean.lean:25 (same declaration text).