OAI/NumberTheory/TwoPoint/ShortIntervals/MRTAdditiveWindows.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Bounded measurable finite interval sums and the squared two-window inequality. These statements allow arbitrary complex coefficients.

  1. lemma OAI.TwoPointCorrelations.mrt_interval_sum_measurable line 13
  2. lemma OAI.TwoPointCorrelations.mrt_interval_sum_norm line 24
  3. lemma OAI.TwoPointCorrelations.mrt_interval_sum_sq_integrableOn line 34
  4. lemma OAI.TwoPointCorrelations.mrt_interval_sum_sq_intervalIntegrable line 45
  5. lemma OAI.TwoPointCorrelations.mrt_interval_sum_sq_split line 53
  6. theorem OAI.TwoPointCorrelations.mrt_interval_sum_averaged_sq line 65