OAI/NumberTheory/TwoPoint/Halasz/HalaszTorusBessel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite Fourier Bessel inequality on the coefficient torus, for the localized kernel in the double mean-value estimate.

  1. def OAI.TwoPointCorrelations.halaszCharacterL2 line 14
  2. lemma OAI.TwoPointCorrelations.halasz_character_l2_coe line 19
  3. lemma OAI.TwoPointCorrelations.halasz_character_l2_inner line 25
  4. theorem OAI.TwoPointCorrelations.halasz_torus_bessel line 39