OAI/NumberTheory/TwoPoint/Halasz/HalaszCoefficientBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The triple-convolution coefficients have a logarithm-squared majorant. This bounds the short boundary interval in the Perron unsmoothing step.

  1. lemma OAI.TwoPointCorrelations.halasz_mangoldt_convolution_bound line 14

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszCoefficientBound.lean:14 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.halasz_triple_coefficient_bound line 34

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszCoefficientBound.lean:34 (same declaration text).