TracialFreeCompression.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The free-compression norm bound in the faithful tracial representation. The hypotheses describe only the elementary reduced-word coordinates; their zero block, creation bound, and the small-corner norm bound are conclusions.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.norm_narrow_compression_of_reduced_words line 28

Source documentation

The faithful tracial norm and the elementary creation action give the order-u bound used for the narrow spectral arc.

theorem norm_narrow_compression_of_reduced_words
    (hfaithful : Function.Injective G.vector) (hτ : G.trace 1 = 1)
    (W : H ≃ₗᵢ[ℂ] HilbertTensor (G.baseSpace A) F)
    (hhead : ∀ (a : A) x, W (G.left (a : P) x) =
      tensorHeadAction (G.baseRepresentation A a) (W x))
    (Q : F →L[ℂ] F) (hQ : Q.adjoint = Q) (hQsq : Q * Q = Q) (hQnorm : ‖Q‖ ≤ 1)
    (J : K →ₗᵢ[ℂ] HilbertTensor (G.baseSpace A) F)
    (C : HilbertTensor (centeredSubspace (G.baseVector Z 1)) K →ₗᵢ[ℂ]
      HilbertTensor (G.baseSpace A) F)
    (hcomplement : J.toContinuousLinearMap.comp J.toContinuousLinearMap.adjoint =
      1 - firstLetterProjection (G.baseVector A 1) Q)
    (e : A) (he : IsStarProjection (e : P))
…

Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.tensorHeadAction, OAI.KadisonSimilarity.centeredSubspace, OAI.KadisonSimilarity.firstLetterProjection