OAI/Analysis/KadisonSimilarity/Representation/CanonicalGeneratedOperators.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Operator transfer to the constructed generated algebra. These results use the exact factor embeddings of the canonical model.

  1. def OAI.KadisonSimilarity.canonicalGeneratedOperator line 18
  2. theorem OAI.KadisonSimilarity.canonicalGeneratedOperator_commutes line 21
  3. theorem OAI.KadisonSimilarity.canonicalGeneratedOperator_traceCornerBound line 41
  4. theorem OAI.KadisonSimilarity.norm_commutator_le_canonicalGeneratedOperator line 59

    Source documentation

    Recovery in the constructed generated model has no density or generated-algebra hypothesis left to supply.

    theorem norm_commutator_le_canonicalGeneratedOperator
    (T : τA.GNS →L[ℂ] τA.GNS) (S : τ.GNS →L[ℂ] τ.GNS)
    (hT : (gnsTracialHomIsometry τA τ φ hφ).toContinuousLinearMap.adjoint.comp
      (S.comp (gnsTracialHomIsometry τA τ φ hφ).toContinuousLinearMap) = T)
    (a : A) :
    ‖commutator T (τA.gnsStarAlgHom a)‖ ≤
      ‖(canonicalGeneratedGeometry τ htr φ ψ).baseOperator
        (canonicalGeneratedFirst τ htr φ ψ).range
        (commutator (canonicalGeneratedOperator τ htr φ ψ S)
          ((canonicalGeneratedGeometry τ htr φ ψ).left
            (canonicalGeneratedFirst τ htr φ ψ a)))‖ :=
…

    Mentions: OAI.KadisonSimilarity.gnsTracialHomIsometry, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.canonicalGeneratedGeometry, OAI.KadisonSimilarity.canonicalGeneratedFirst, OAI.KadisonSimilarity.canonicalGeneratedOperator