OAI/NumberTheory/TwoPoint/Halasz/HalaszLogMean.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Recover an ordinary mean from its logarithmically weighted sum. The absolute error is at most N for a one-bounded sequence.

  1. lemma OAI.TwoPointCorrelations.halasz_sum_log_factorial line 13

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszLogMean.lean:13 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.halasz_sum_log_gap line 22

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszLogMean.lean:22 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.halasz_logarithmic_sum_error line 31

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszLogMean.lean:31 (same declaration text).

  4. theorem OAI.TwoPointCorrelations.halasz_logarithmic_mean_bound line 55

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszLogMean.lean:55 (same declaration text).