OAI/Analysis/KadisonSimilarity/Derivation/CyclicCommutativeModel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Scalar spectral coordinates for one cyclic subspace of a commutative representation. These are the components of the central Hilbert model.

  1. def OAI.KadisonSimilarity.commutativeSpectralCalculus line 20
  2. def OAI.KadisonSimilarity.commutativeVectorMeasure line 24
  3. instance OAI.KadisonSimilarity.commutativeVectorMeasure_finite line 28
  4. instance OAI.KadisonSimilarity.commutativeVectorMeasure_regular line 32
  5. def OAI.KadisonSimilarity.commutativeCyclicIsometry line 36
  6. theorem OAI.KadisonSimilarity.commutativeCyclicIsometry_gelfand line 40
  7. theorem OAI.KadisonSimilarity.commutativeCyclicIsometry_range line 51