OAI/Analysis/ModularTheory/FourierOrbit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual vector-valued Fourier transform of a compact spectral orbit. The frequency shift and the factor 2π are explicit, connecting the spectral Gaussian calculation to the regular representation used for the core.

  1. lemma OAI.BoundedRecovery.integrable_spectral_orbit line 16
  2. lemma OAI.BoundedRecovery.fourier_spectral_orbit line 23
  3. lemma OAI.BoundedRecovery.fourier_gaussian_spectral_orbit line 42