MatrixStateRetraction.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

State-preserving finite matrix retractions

Only the finite matrix algebra lies in the vector-state centralizer. The ambient algebra need not carry a trace. Compression to a minimal matrix column and the column resolution preserve the original state.

theorem OAI.KadisonKastler.matrixStateVector_ne_zero line 28
theorem OAI.KadisonKastler.matrixStateVector_fixed line 33
def OAI.KadisonKastler.matrixStateRetraction line 41
Source documentation
A minimal matrix column gives a concrete contractive retraction.
```
def matrixStateRetraction : (H →L[ℂ] H) →L[ℂ]
    Algebra (matrixUnitConcreteAlgebra E) :=
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixUnitConcreteAlgebra
theorem OAI.KadisonKastler.matrixStateRetraction_norm line 52
theorem OAI.KadisonKastler.matrixStateRetraction_fixed line 55
theorem OAI.KadisonKastler.matrixStateColumn_mem line 60

theorem OAI.KadisonKastler.matrixColumn_state line 74

Source documentation

Centrality of the matrix units is enough for the matrix-column identity.

theorem matrixColumn_state
    (hcentral : ∀ i j (x : Algebra M),
      inner ℂ Ω ((E.entry i j * x).val Ω) =
        inner ℂ Ω ((x * E.entry i j).val Ω)) (T : Algebra M) :
    (∑ i, inner ℂ ((E.entry i o).val Ω) (T.val ((E.entry i o).val Ω))) =
      inner ℂ Ω (T.val Ω) := by
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.matrixStateRetraction_state line 94

Source documentation

The retraction preserves the ambient vector state on its centralizer domain.

theorem matrixStateRetraction_state
    (hcentral : ∀ i j (x : Algebra M),
      inner ℂ Ω ((E.entry i j * x).val Ω) =
        inner ℂ Ω ((x * E.entry i j).val Ω)) (T : Algebra M) :
    inner ℂ Ω ((matrixStateRetraction Ω hsep E o T.val).val Ω) =
      inner ℂ Ω (T.val Ω) := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixStateRetraction

theorem OAI.KadisonKastler.matrixStateRetraction_mul_left line 111
theorem OAI.KadisonKastler.matrixStateRetraction_star line 116
theorem OAI.KadisonKastler.matrixStateRetraction_mul_right line 124