OAI/Analysis/KadisonKastler/MatrixProjectionCuts.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Projection cuts of a concrete full matrix diagonal

  1. def OAI.KadisonKastler.matrixDiagonalCut line 20

    Source documentation

    The projection onto a finite subset of the matrix diagonal.

    def matrixDiagonalCut (E : MatrixUnitSystem ι (Algebra M)) (s : Finset ι) :
    AlgebraProjection M :=
…

    Mentions: OAI.KadisonKastler.Algebra

  2. theorem OAI.KadisonKastler.matrixDiagonalCut_mul_entry line 30
  3. theorem OAI.KadisonKastler.matrixDiagonalCut_le line 35
  4. theorem OAI.KadisonKastler.matrixDiagonalCut_univ line 43
  5. theorem OAI.KadisonKastler.matrixDiagonalCut_mem line 46
  6. theorem OAI.KadisonKastler.matrixDiagonalCut_trace line 51

    Source documentation

    Equal diagonal traces give the exact trace of every cut.

    theorem matrixDiagonalCut_trace (τ : TracialRepresentation M)
    (E : MatrixUnitSystem ι (Algebra M)) (c : ℂ)
    (hc : ∀ i, τ.trace (E.entry i i) = c) (s : Finset ι) :
    τ.trace (matrixDiagonalCut E s).val = (s.card : ℂ) * c := by
…

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