OAI/NumberTheory/TwoPoint/Halasz/HalaszLogConvolution.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact logarithmic identities at the start of Halász's method. The multiplicativity hypothesis here is complete multiplicativity on positive arguments, as supplied by the corrected MRT reduction.

  1. theorem OAI.TwoPointCorrelations.halasz_logarithmic_convolution line 15

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

  2. def OAI.TwoPointCorrelations.halaszDirichletPolynomial line 36

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszLogConvolution.lean:36 (same declaration text).

  3. theorem OAI.TwoPointCorrelations.halaszDirichletPolynomial_hasDerivAt line 39

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszLogConvolution.lean:39 (same declaration text).