OAI/Analysis/KadisonKastler/CoreTraceFrequencyVector.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The bounded-frequency vector for the core trace

The scalar weight is exp(pi (s-1)) on (0,1], in the Fourier convention exp(-2 pi i t s). The corresponding vector has explicit L2 bounds and frequency support.

  1. def OAI.KadisonKastler.coreTraceFrequencyFunction line 17
  2. theorem OAI.KadisonKastler.coreTraceFrequencyFunction_memLp line 20
  3. def OAI.KadisonKastler.coreTraceFrequencyScalar line 36
  4. theorem OAI.KadisonKastler.coreTraceFrequencyScalar_apply_ae line 39
  5. theorem OAI.KadisonKastler.coreTraceFrequencyScalar_norm_le_one line 43
  6. theorem OAI.KadisonKastler.coreTraceFrequencyScalar_norm_lower line 59
  7. theorem OAI.KadisonKastler.coreTraceFrequencyScalar_norm_pos line 78
  8. theorem OAI.KadisonKastler.coreTraceFrequencyScalar_fixed line 81
  9. def OAI.KadisonKastler.coreTraceFrequencyVector line 96
  10. theorem OAI.KadisonKastler.coreTraceFrequencyVector_fixed line 99
  11. theorem OAI.KadisonKastler.coreTraceFrequencyVector_norm_le line 103
  12. theorem OAI.KadisonKastler.coreTraceFrequencyVector_ne_zero line 108