OAI/NumberTheory/TwoPoint/Halasz/HalaszTriplePrefix.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Identify a grouped piece of the adaptive double convolution with the actual coefficients to which narrow Perron inversion is applied.

  1. lemma OAI.TwoPointCorrelations.halasz_convolution_prefix line 14

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

  2. lemma OAI.TwoPointCorrelations.halasz_finite_convolution_prefix line 22

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

  3. lemma OAI.TwoPointCorrelations.halasz_prime_smooth_prefix line 32

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszTriplePrefix.lean:32 (same declaration text).

  4. theorem OAI.TwoPointCorrelations.halasz_grouped_triple_prefix line 54

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszTriplePrefix.lean:54 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.halasz_smooth_oneBounded line 70

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszTriplePrefix.lean:70 (same declaration text).