OAI/Analysis/KadisonSimilarity/Similarity/PaulsenDischarge.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative similarity from the proved completely bounded factorization

The entrywise C-star matrix norm agrees with the concrete matrix operator norm. Applying the proved factorization and then removing its kernel gives Paulsen's quantitative similarity conclusion on the original Hilbert space.

  1. theorem OAI.KadisonSimilarity.completeBound_entrywise line 19
  2. theorem OAI.KadisonSimilarity.paulsenSimilarityInput line 27

    Source documentation

    Paulsen's quantitative similarity bound, including the zero Hilbert space.

    theorem paulsenSimilarityInput (π : BoundedUnitalHom A H) : PaulsenSimilarityInput π := by
…

    Mentions: OAI.KadisonSimilarity.BoundedUnitalHom, OAI.KadisonSimilarity.PaulsenSimilarityInput