OAI/Analysis/ModularTheory/SpectralShift.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Translation of the modular spectral variable. It preserves the actual nondegenerate calculus and supplies Gaussian convergence at every frequency needed by the Fourier-orbit formula.

  1. def OAI.BoundedRecovery.spectralTranslation line 15
  2. lemma OAI.BoundedRecovery.spectralTranslation_apply line 25
  3. lemma OAI.BoundedRecovery.spectralTranslation_cancel line 28
  4. lemma OAI.BoundedRecovery.spectralTranslation_compact line 33
  5. def OAI.BoundedRecovery.RealSpectralCalculus.shift line 50
  6. lemma OAI.BoundedRecovery.RealSpectralCalculus.shiftedGaussian_strong line 57
  7. def OAI.WeakPureInfiniteness.modularShiftedHalfGaussian line 69
  8. lemma OAI.WeakPureInfiniteness.modularShiftedHalfGaussian_apply line 72
  9. lemma OAI.WeakPureInfiniteness.modularShiftedHalfGaussian_resolvent line 82
  10. lemma OAI.WeakPureInfiniteness.modularShiftedHalfGaussian_halfGraph line 99
  11. lemma OAI.WeakPureInfiniteness.modularShiftedHalfGaussian_strong line 105