MatrixTraceRetraction.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Trace-preserving ambient retractions onto finite matrix algebras

The minimal cyclic space is based at a diagonal matrix unit applied to the original trace vector. The matrix columns then recover the original trace.

theorem OAI.KadisonKastler.matrixColumn_trace line 26

Source documentation

A matrix-column resolution of the faithful vector trace.

theorem matrixColumn_trace (T : Algebra M) :
    (∑ i, inner ℂ ((E.entry i o).val τ.vector)
      (T.val ((E.entry i o).val τ.vector))) = τ.trace T := by
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.matrixTraceVector_ne_zero line 43
Source documentation
The diagonal trace vector is nonzero by faithfulness.
```
theorem matrixTraceVector_ne_zero : (E.entry o o).val τ.vector ≠ 0 := by
…
```
theorem OAI.KadisonKastler.matrixTraceVector_fixed line 49
Source documentation
The chosen diagonal fixes its own trace vector.
```
theorem matrixTraceVector_fixed :
    (matrixUnitDiagonalProjection (concreteMatrixUnits E) o).val.val
      ((E.entry o o).val τ.vector) = (E.entry o o).val τ.vector := by
…
```
Mentions: OAI.KadisonKastler.matrixUnitDiagonalProjection, OAI.KadisonKastler.concreteMatrixUnits
def OAI.KadisonKastler.matrixTraceRetraction line 57
Source documentation
Ambient compression based at the specified diagonal trace vector.
```
def matrixTraceRetraction : (H →L[ℂ] H) →L[ℂ]
    Algebra (matrixUnitConcreteAlgebra E) :=
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixUnitConcreteAlgebra
theorem OAI.KadisonKastler.matrixTraceRetraction_norm line 68
theorem OAI.KadisonKastler.matrixTraceRetraction_fixed line 71
theorem OAI.KadisonKastler.matrixColumn_mem line 77
Source documentation
Every matrix column belongs to this minimal cyclic space.
```
theorem matrixColumn_mem (i : ι) :
    (E.entry i o).val τ.vector ∈
      typeICyclicSpace (matrixUnitConcreteAlgebra E) ((E.entry o o).val τ.vector) := by
…
```
Mentions: OAI.KadisonKastler.typeICyclicSpace, OAI.KadisonKastler.matrixUnitConcreteAlgebra
theorem OAI.KadisonKastler.matrixTraceRetraction_trace line 91
Source documentation
Compression preserves the original trace on the ambient finite algebra.
```
theorem matrixTraceRetraction_trace (T : Algebra M) :
    τ.trace (coordinateInclusion E.concreteAlgebra_le (matrixTraceRetraction τ E o T.val)) =
      τ.trace T := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixTraceRetraction
theorem OAI.KadisonKastler.matrixTraceRetraction_mul_left line 103
Source documentation
The finite-stage retraction is a left module map over the matrix algebra.
```
theorem matrixTraceRetraction_mul_left
    (a : Algebra (matrixUnitConcreteAlgebra E)) (T : H →L[ℂ] H) :
    matrixTraceRetraction τ E o (a.val * T) = a * matrixTraceRetraction τ E o T :=
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixUnitConcreteAlgebra, OAI.KadisonKastler.matrixTraceRetraction
theorem OAI.KadisonKastler.matrixTraceRetraction_eq_expectation line 109
Source documentation
On the finite ambient algebra this is the trace conditional expectation.
```
theorem matrixTraceRetraction_eq_expectation (T : Algebra M) :
    conditionalExpectation τ (matrixUnitConcreteAlgebra_le E) T =
      coordinateInclusion E.concreteAlgebra_le (matrixTraceRetraction τ E o T.val) := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixUnitConcreteAlgebra_le, OAI.KadisonKastler.matrixTraceRetraction