OAI/Analysis/KadisonSimilarity/Derivation/CyclicSpectralSum.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The orthogonal cyclic decomposition of a commutative representation, expressed as an actual Hilbert sum of scalar spectral L² spaces.

  1. abbrev OAI.KadisonSimilarity.CyclicSpectralSpace line 23
  2. theorem OAI.KadisonSimilarity.cyclic_spectral_range line 26
  3. def OAI.KadisonSimilarity.cyclicSpectralSummands line 40
  4. theorem OAI.KadisonSimilarity.cyclicSpectral_isHilbertSum line 60
  5. def OAI.KadisonSimilarity.cyclicSpectralEquiv line 75