OAI/NumberTheory/TwoPoint/Halasz/HalaszVinogradovOrthogonality.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Fourier orthogonality for the complete Vinogradov system, with normalised Haar measure on its coefficient torus.

  1. def OAI.TwoPointCorrelations.halaszVinogradovHaar line 17
  2. instance OAI.TwoPointCorrelations.(instance at line 20) line 20
  3. def OAI.TwoPointCorrelations.halaszVinogradovCharacter line 24
  4. lemma OAI.TwoPointCorrelations.halasz_vinogradov_fourier_integral line 28
  5. theorem OAI.TwoPointCorrelations.halasz_vinogradov_character_integral line 38
  6. lemma OAI.TwoPointCorrelations.halasz_vinogradov_character_add line 57
  7. lemma OAI.TwoPointCorrelations.halasz_vinogradov_character_neg line 63
  8. lemma OAI.TwoPointCorrelations.halasz_vinogradov_character_continuous line 68
  9. lemma OAI.TwoPointCorrelations.halasz_vinogradov_character_integrable line 73
  10. lemma OAI.TwoPointCorrelations.halasz_vinogradov_character_inner line 78