OAI/NumberTheory/TwoPoint/Bounds/RoughCutoffAverage.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual two-cutoff rough correlation is a finite Fourier average of the already bounded rough correlations. Both original-factor choices are supported, with every cutoff parameter uniform after the long threshold.

  1. def OAI.TwoPointCorrelations.roughPairCoefficient line 15
  2. lemma OAI.TwoPointCorrelations.weightedRoughShiftAverage_eq_pairSum line 19
  3. def OAI.TwoPointCorrelations.cutoffRoughAverage line 42
  4. lemma OAI.TwoPointCorrelations.cutoffRoughAverage_fourier line 49
  5. theorem OAI.TwoPointCorrelations.norm_cutoffRoughAverage_le line 62
  6. theorem OAI.TwoPointCorrelations.qualitative_cutoff_rough_shifts line 87
  7. theorem OAI.TwoPointCorrelations.qualitative_cutoff_rough_shifts_right line 117