OAI/Analysis/KadisonSimilarity/Representation/SpectralIntertwining.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Both spectral coordinate maps intertwine the continuous scalar action. The identities are proved first on continuous functions and extended by density.

  1. theorem OAI.KadisonSimilarity.VectorSpectralMeasure.cyclicMap_intertwines line 22
  2. theorem OAI.KadisonSimilarity.weightedContinuousVector_mul line 37
  3. theorem OAI.KadisonSimilarity.spectralDensityIsometry_intertwines line 50