OAI/Analysis/KadisonSimilarity/Similarity/ArvesonDischarge.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The Arveson commutant-distance identity follows from the sharp implementation theorem for completely bounded derivations.

  1. theorem OAI.KadisonSimilarity.twice_distance_le_of_complete_bound line 21
  2. theorem OAI.KadisonSimilarity.arvesonDistanceFormula line 43

    Source documentation

    The precise CSSW (2010), Equation (2.1), specialization is proved.

    theorem arvesonDistanceFormula (M : VonNeumannAlgebra H) (T : H →L[ℂ] H) :
    ArvesonDistanceFormula M T := by
…

    Mentions: OAI.KadisonSimilarity.ArvesonDistanceFormula