OAI/NumberTheory/TwoPoint/ShortIntervals/MRTWindowAveraging.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Rectangular integration of the finite additive windows. The two-window inequality pays its error once before logarithmic Fourier analysis.

  1. lemma OAI.TwoPointCorrelations.mrt_interval_sum_sq_box line 13
  2. lemma OAI.TwoPointCorrelations.mrt_interval_sum_sq_inner line 21
  3. lemma OAI.TwoPointCorrelations.mrt_interval_sum_sq_swap line 29
  4. theorem OAI.TwoPointCorrelations.mrt_additive_window_rectangular line 36