OAI/NumberTheory/TwoPoint/Fourier/MinorArcWindowProduct.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

One term of the fourth expansion of a weighted short-window sum.

  1. def OAI.TwoPointCorrelations.minorArcWindowTerm line 13
  2. lemma OAI.TwoPointCorrelations.minor_arc_window_product line 16
  3. lemma OAI.TwoPointCorrelations.minor_arc_window_product_bound line 62
  4. lemma OAI.TwoPointCorrelations.minor_arc_window_product_support line 82