OAI/NumberTheory/TwoPoint/Halasz/HalaszCrossMoment.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Fourier counting with two different collections of tuples, applied to a prescribed repeated coordinate.

  1. def OAI.TwoPointCorrelations.halaszCrossCount line 12
  2. theorem OAI.TwoPointCorrelations.halasz_cross_integral line 16
  3. theorem OAI.TwoPointCorrelations.halasz_cross_count_bound line 32
  4. def OAI.TwoPointCorrelations.halaszRepeatedFrequency line 43
  5. def OAI.TwoPointCorrelations.halaszRepeatedCount line 46
  6. lemma OAI.TwoPointCorrelations.halasz_repeated_phase line 50
  7. theorem OAI.TwoPointCorrelations.halasz_repeated_count_bound line 68