OAI/Analysis/ModularTheory/TomitaOrbit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Removing the compact spectral cutoff from the Gaussian orbit formula. The orbit integral is a bounded operator on the actual Hilbert space, so its identity on the dense compact spectral vectors determines it everywhere.

  1. def OAI.WeakPureInfiniteness.modularTomitaFrequencyKernel line 18
  2. lemma OAI.WeakPureInfiniteness.modularTomitaFrequencyKernel_integrable line 21
  3. def OAI.WeakPureInfiniteness.modularTomitaOrbitOperator line 30
  4. lemma OAI.WeakPureInfiniteness.modularTomitaOrbitOperator_fourier line 51
  5. lemma OAI.WeakPureInfiniteness.modularTomitaOrbitOperator_eq line 66
  6. lemma OAI.WeakPureInfiniteness.modularTomitaKernel_fourier_all line 85
  7. lemma OAI.WeakPureInfiniteness.modularTomitaKernel_fourier_limit_all line 93
  8. lemma OAI.WeakPureInfiniteness.modularTomitaKernel_fourier_norm_all line 100