MatrixProjectionInterpolation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Bracketing a finite-factor projection by consecutive matrix cuts

theorem OAI.KadisonKastler.exists_projection_between_matrix_cuts line 20

Source documentation

A single unused diagonal slot absorbs the trace remainder between two consecutive cuts. The conjugating unitary is in the original finite factor.

theorem exists_projection_between_matrix_cuts (τ : TracialRepresentation M)
    (hfactor : ∀ c : Algebra M, (∀ a : Algebra M, a * c = c * a) →
      ∃ z : ℂ, c = z • (1 : Algebra M))
    (hdiff : ∀ p : Algebra M, IsStarProjection p → p ≠ 0 →
      ∃ q : Algebra M, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p * q = q ∧ q * p = q)
    (E : MatrixUnitSystem ι (Algebra M)) (p : AlgebraProjection M)
    (s : Finset ι) (j : ι) (hj : j ∉ s)
    (hlo : (τ.trace (matrixDiagonalCut E s).val).re ≤ (τ.trace p.val).re)
    (hhi : (τ.trace p.val).re ≤ (τ.trace (matrixDiagonalCut E s).val).re +
      (τ.trace (E.entry j j)).re) :
    ∃ (r : AlgebraProjection M) (u : unitary (Algebra M)),
      matrixDiagonalCut E s ≤ r ∧ r ≤ matrixDiagonalCut E (insert j s) ∧
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixDiagonalCut