OAI/NumberTheory/TwoPoint/Halasz/HalaszTripleEstimate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A complete finite estimate for each grouped triple convolution. The main term, contour tail, and unsmoothing error are all explicit.

  1. lemma OAI.TwoPointCorrelations.halasz_vertical_integral_norm line 18

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszTripleEstimate.lean:18 (same declaration text).

  2. theorem OAI.TwoPointCorrelations.halasz_prime_triple_estimate line 29

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszTripleEstimate.lean:29 (same declaration text).