OAI/Analysis/KadisonSimilarity/Representation/CommonSpectralCommutant.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The represented abelian commutant embeds isometrically in the actual commutant of measurable scalar localizations on a single L² space.

  1. def OAI.KadisonSimilarity.commonScalarRepresentation line 22
  2. theorem OAI.KadisonSimilarity.commonScalarRepresentation_apply line 28
  3. theorem OAI.KadisonSimilarity.commonScalarRepresentation_intertwines line 35
  4. theorem OAI.KadisonSimilarity.commonScalarRepresentation_adjoint_intertwines line 42
  5. theorem OAI.KadisonSimilarity.commonExtension_commutes_representation line 66
  6. theorem OAI.KadisonSimilarity.commonCompression_commutes_representation line 88

    Source documentation

    Compression of a scalar-commuting operator lies in the original represented commutant.

    theorem commonCompression_commutes_representation
    (Q : CommonCyclicHilbert π D →L[ℂ] CommonCyclicHilbert π D)
    (hQ : ∀ a, Q * commonScalarRepresentation π D a =
      commonScalarRepresentation π D a * Q) (a : A) :
    (((cyclicCommonEmbedding π D).toContinuousLinearMap.adjoint.comp Q).comp
      (cyclicCommonEmbedding π D).toContinuousLinearMap) * π a =
    π a * (((cyclicCommonEmbedding π D).toContinuousLinearMap.adjoint.comp Q).comp
      (cyclicCommonEmbedding π D).toContinuousLinearMap) := by
…

    Mentions: OAI.KadisonSimilarity.CommonCyclicHilbert, OAI.KadisonSimilarity.commonScalarRepresentation, OAI.KadisonSimilarity.cyclicCommonEmbedding

  7. theorem OAI.KadisonSimilarity.commonExtension_commutes_continuous line 110
  8. theorem OAI.KadisonSimilarity.commonExtension_commutes_localizations line 120