OAI/Analysis/KadisonSimilarity/Similarity/KirchbergScalarDerivation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Kirchberg's scalar commutator bound for an exponential similarity of a star representation. This is the estimate before equation (2), p. 61.

  1. theorem OAI.KadisonSimilarity.star_kirchbergPath_one line 16
  2. theorem OAI.KadisonSimilarity.kirchberg_commutator_bound line 22

    Source documentation

    A bound for the positive endpoint also bounds the negative endpoint, because the source representation preserves adjoints.

    theorem kirchberg_commutator_bound (σ : A →⋆ₐ[ℂ] B) (t : B)
    (ht : IsSelfAdjoint t) {M : ℝ} (hM : 0 < M)
    (hπ : ∀ a : A, ‖kirchbergPath t (σ a) 1‖ ≤ M * ‖a‖) (a : A) :
    ‖t * σ a - σ a * t‖ ≤ (M + 1) * ‖a‖ := by
…

    Mentions: OAI.KadisonSimilarity.kirchbergPath