IsometricTransfer.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Transfer through an isometric row

This is the operator calculation in the properly infinite case of prop:factor-representations. The row/column derivation estimates must still be provided before applying this lemma to a properly infinite von Neumann algebra.

theorem OAI.KadisonSimilarity.isometric_commutator_identity line 24

Source documentation

Solving the three-term commutator expansion by compressing with an isometry.

theorem isometric_commutator_identity (Y : H →L[ℂ] H) (A X : K →L[ℂ] K)
    (V : K →L[ℂ] H) (hV : V.adjoint.comp V = ContinuousLinearMap.id ℂ K) :
    commutator A X =
      V.adjoint.comp ((commutator Y (V.comp (X.comp V.adjoint))).comp V) -
      V.adjoint.comp ((Y.comp V - V.comp A).comp X) -
      X.comp ((A.comp V.adjoint - V.adjoint.comp Y).comp V) := by
…

Mentions: OAI.KadisonSimilarity.commutator

theorem OAI.KadisonSimilarity.norm_commutator_le_isometric_transfer line 35

Source documentation

The coefficient 1+2c in the properly infinite factor estimate.

theorem norm_commutator_le_isometric_transfer (Y : H →L[ℂ] H)
    (A X : K →L[ℂ] K) (V : K →L[ℂ] H)
    (hV : V.adjoint.comp V = ContinuousLinearMap.id ℂ K)
    {δ c : ℝ} (hδ : 0 ≤ δ) (hc : 0 ≤ c)
    (hscalar : ‖commutator Y (V.comp (X.comp V.adjoint))‖ ≤
      δ * ‖V.comp (X.comp V.adjoint)‖)
    (hrow : ‖Y.comp V - V.comp A‖ ≤ c * δ)
    (hcol : ‖A.comp V.adjoint - V.adjoint.comp Y‖ ≤ c * δ) :
    ‖commutator A X‖ ≤ (1 + 2 * c) * δ * ‖X‖ := by
…

Mentions: OAI.KadisonSimilarity.commutator