OAI/NumberTheory/TwoPoint/ShortIntervals/MRTWindowMultiplier.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic-window multiplier has square-integrable quadratic decay. These bounds keep the actual finite window width.

  1. lemma OAI.TwoPointCorrelations.mrtWindowMultiplier_continuous line 13
  2. lemma OAI.TwoPointCorrelations.mrt_window_multiplier_sq line 20
  3. lemma OAI.TwoPointCorrelations.mrt_log_window_atom_fourier_norm line 32
  4. lemma OAI.TwoPointCorrelations.mrt_log_window_atom_fourier_memLp line 41