OAI/NumberTheory/TwoPointCorrelations/HalaszDoubleConvolution.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Apply the prime convolution a second time, retaining the varying denominator log(N/p). This is the adaptive triple sum in the short proof of Halasz's theorem.

  1. def OAI.TwoPointCorrelations.halaszDoubleConvolution line 15

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszDoubleConvolution.lean:15 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.halasz_divisor_cutoff line 20

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszDoubleConvolution.lean:20 (same declaration text).

  3. theorem OAI.TwoPointCorrelations.halasz_double_convolution_error line 35

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszDoubleConvolution.lean:35 (same declaration text).