OAI/Analysis/KadisonKastler/ModularLocalizedPackets.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Fourier packets localized by the modular spectral cuts

The already constructed Fourier gauge identity transports bounded scalar frequency windows to short modular spectral intervals, fiber by fiber. The norm identity gives the total weight of the resulting vector states.

  1. def OAI.KadisonKastler.ModularSpectralResolution.fourierPacket line 29
  2. theorem OAI.KadisonKastler.ModularSpectralResolution.norm_fourierPacket line 32
  3. theorem OAI.KadisonKastler.ModularSpectralResolution.fourierPacket_cut line 36
  4. theorem OAI.KadisonKastler.ModularSpectralResolution.fourierPacket_lower_support line 65
  5. theorem OAI.KadisonKastler.ModularSpectralResolution.fourierPacket_upper_support line 74
  6. theorem OAI.KadisonKastler.ModularSpectralResolution.fourierPacket_mass line 86