OAI/NumberTheory/TwoPoint/Halasz/HalaszFinitePhase.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact Fourier formulas for the finite energies used when the short variables are restricted to one residue class.

  1. def OAI.TwoPointCorrelations.halaszFinitePhase line 12
  2. lemma OAI.TwoPointCorrelations.halasz_finite_phase_continuous line 16
  3. lemma OAI.TwoPointCorrelations.halasz_torus_integrable line 20
  4. theorem OAI.TwoPointCorrelations.halasz_finite_phase_energy line 25
  5. lemma OAI.TwoPointCorrelations.halasz_finite_phase_product line 52
  6. lemma OAI.TwoPointCorrelations.halasz_finite_phase_power line 59
  7. theorem OAI.TwoPointCorrelations.halasz_finite_mixed_moment line 68