OAI/NumberTheory/TwoPoint/Halasz/HalaszVinogradovProduct.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Splitting the complete system into long and short tuples, and the diagonal lower bound used to absorb colliding long variables.

  1. def OAI.TwoPointCorrelations.halaszTupleJoin line 14
  2. lemma OAI.TwoPointCorrelations.halasz_join_frequency line 22
  3. theorem OAI.TwoPointCorrelations.halasz_vinogradov_product_count line 30
  4. theorem OAI.TwoPointCorrelations.halasz_vinogradov_diagonal_extension line 54