OAI/Analysis/KadisonKastler/RegularActionPackets.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Spectral action on the packets of an invariant vector

  1. theorem OAI.KadisonKastler.fourier_regularTensorVector line 16
  2. theorem OAI.KadisonKastler.regularFrequencyPacket_eq_tensor line 21
  3. theorem OAI.KadisonKastler.regularConstantHom_frequencyPacket line 28
  4. theorem OAI.KadisonKastler.regularScalarMultiplier_tensor line 36
  5. theorem OAI.KadisonKastler.regularGauge_frequencyPacket_fixed line 53
  6. theorem OAI.KadisonKastler.regularGauge_star_frequencyPacket_fixed line 65
  7. theorem OAI.KadisonKastler.regularActionMultiplier_packet line 77