OAI/NumberTheory/TwoPoint/ShortIntervals/MRTWindowPlancherel.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Plancherel for the actual finite logarithmic windows. The coefficient function is arbitrary; multiplicativity plays no role in this bridge.

  1. lemma OAI.TwoPointCorrelations.mrt_fourier_finsetSum line 12
  2. lemma OAI.TwoPointCorrelations.mrt_fourier_const_mul line 22
  3. def OAI.TwoPointCorrelations.mrtLogDirichlet line 27
  4. lemma OAI.TwoPointCorrelations.mrt_log_window_integrable line 30
  5. lemma OAI.TwoPointCorrelations.mrt_log_window_memLp line 35
  6. theorem OAI.TwoPointCorrelations.mrt_log_window_transform line 40
  7. lemma OAI.TwoPointCorrelations.mrt_log_window_fourier_memLp line 53
  8. theorem OAI.TwoPointCorrelations.mrt_log_window_plancherel line 64