OAI/NumberTheory/TwoPoint/ShortIntervals/MRTLogWindow.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The exact finite logarithmic window and its Fourier multiplier.

  1. def OAI.TwoPointCorrelations.mrtLogWindowAtom line 13
  2. def OAI.TwoPointCorrelations.mrtWindowMultiplier line 16
  3. lemma OAI.TwoPointCorrelations.mrtLogWindowAtom_memLp line 19
  4. lemma OAI.TwoPointCorrelations.mrtLogWindowAtom_integrable line 34
  5. lemma OAI.TwoPointCorrelations.mrt_one_add_imaginary_ne_zero line 37
  6. theorem OAI.TwoPointCorrelations.mrt_log_window_fourier line 42
  7. lemma OAI.TwoPointCorrelations.mrt_log_window_membership line 71
  8. def OAI.TwoPointCorrelations.mrtLogWindow line 85
  9. theorem OAI.TwoPointCorrelations.mrt_log_window_interval line 88