OAI/NumberTheory/TwoPoint/Fourier/MinorArcRamareWindow.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact change of variables from the Ramaré coefficient to the finite bilinear short-window sum.

  1. def OAI.TwoPointCorrelations.minorArcRamareCofactor line 14
  2. lemma OAI.TwoPointCorrelations.minor_arc_ramare_cofactor_bound line 17
  3. lemma OAI.TwoPointCorrelations.minor_arc_bilinear_zero_cofactor line 26
  4. lemma OAI.TwoPointCorrelations.minor_arc_divisibility_window line 38
  5. lemma OAI.TwoPointCorrelations.minor_arc_window_weighted_sum line 63
  6. lemma OAI.TwoPointCorrelations.minor_arc_window_interval_eq_of_cutoff line 83
  7. lemma OAI.TwoPointCorrelations.minor_arc_bilinear_cutoff_eq line 89
  8. lemma OAI.TwoPointCorrelations.minor_arc_ramare_short_eq line 104
  9. lemma OAI.TwoPointCorrelations.minor_arc_ramare_short_eq_bounded line 136