OAI/Analysis/ModularTheory/WeightedFourierBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The integrable bound for the actual regularized Tomita orbit. This is the dominated-convergence step at compact spectral vectors; the bound comes from the half-graph equation, not from an unbounded exponential multiplier.

  1. lemma OAI.WeakPureInfiniteness.modularShiftedHalfGaussian_norm line 18
  2. lemma OAI.WeakPureInfiniteness.modularTomitaKernel_fourier_norm line 27
  3. lemma OAI.WeakPureInfiniteness.modularTomitaKernel_fourier_continuous line 42
  4. lemma OAI.WeakPureInfiniteness.modularTomitaKernel_weighted_integral_limit line 49