OAI/NumberTheory/TwoPoint/Halasz/HalaszVinogradovTranslation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Translation and dilation preserve the complete Vinogradov system. These are the finite identities used before averaging its solutions.

  1. theorem OAI.TwoPointCorrelations.halasz_vinogradov_translate line 11
  2. theorem OAI.TwoPointCorrelations.halasz_vinogradov_dilate line 34
  3. theorem OAI.TwoPointCorrelations.halasz_vinogradov_affine line 42