PositiveSimilarity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Paulsen's attained complete bound can be realized by a positive similarity. Kirchberg takes its self-adjoint logarithm.

theorem OAI.KadisonSimilarity.positive_similarity_of_similarity line 18

theorem OAI.KadisonSimilarity.exists_positive_similarity_completeNorm line 50

Source documentation

The positive similarity has condition number exactly the complete norm.

theorem exists_positive_similarity_completeNorm (π : BoundedUnitalHom A H)
    (hπ : IsCompletelyBounded π.1) :
    ∃ S : (H →L[ℂ] H)ˣ, 0 ≤ (S : H →L[ℂ] H) ∧
      ‖(S : H →L[ℂ] H)‖ * ‖(↑S⁻¹ : H →L[ℂ] H)‖ = completeNorm π.1 ∧
      ∀ a, (S : H →L[ℂ] H) * π.1 (star a) * (↑S⁻¹ : H →L[ℂ] H) =
        star ((S : H →L[ℂ] H) * π.1 a * (↑S⁻¹ : H →L[ℂ] H)) := by
…

Mentions: OAI.KadisonSimilarity.BoundedUnitalHom, OAI.KadisonSimilarity.IsCompletelyBounded, OAI.KadisonSimilarity.completeNorm