OAI/Analysis/KadisonKastler/TracialMatrixBracketAverage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.exists_scalar_average_of_tracial_matrix_bracket line 20

   Source documentation

   Two matrix cuts with close real traces give a finite inner average of the intervening projection close to the lower scalar trace.

   theorem exists_scalar_average_of_tracial_matrix_bracket (τ : TracialRepresentation M)
       {n : ℕ} [Nonempty (Fin n)] (E : MatrixUnitSystem (Fin n) (H →L[ℂ] H))
       (hE : E.algebra ≤ M.toStarSubalgebra)
       (p q r : AlgebraProjection M) (hq : q.val.val ∈ E.algebra) (hr : r.val.val ∈ E.algebra)
       (α β : ℝ) (hαβ : α ≤ β)
       (hqt : τ.trace q.val = (α : ℂ)) (hrt : τ.trace r.val = (β : ℂ))
       (hqp : q.val.val ≤ p.val.val) (hpr : p.val.val ≤ r.val.val) :
       ∃ A : FiniteInnerAverage M, ‖A.apply p.val.val - (α : ℂ) • (1 : H →L[ℂ] H)‖ ≤ β - α := by
   …

   Mentions: OAI.KadisonKastler.FiniteInnerAverage