OAI/Analysis/KadisonKastler/ModularPacketCoefficient.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integrated vector-state coefficients of modular Fourier packets

  1. theorem OAI.KadisonKastler.integrable_regular_vector_coefficient line 16
  2. theorem OAI.KadisonKastler.integral_regular_vector_coefficient line 22
  3. theorem OAI.KadisonKastler.ModularSpectralResolution.fourierPacket_coefficient line 35
  4. theorem OAI.KadisonKastler.ModularSpectralResolution.fourierPacket_coefficient_re line 48