OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPlancherel.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Agreement of the classical integral Fourier transform with the library L² transform, in the integrable case needed for finite windows.

  1. theorem OAI.TwoPointCorrelations.mrt_fourier_toL2 line 13
  2. lemma OAI.TwoPointCorrelations.mrt_toL2_norm_sq line 37
  3. theorem OAI.TwoPointCorrelations.mrt_plancherel line 44