MatrixRetractionTransport.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Transporting finite matrix retractions through an ambient extension

Only the finite matrix images are inverted. The ambient map is required to agree with the represented algebra and to be contractive; no continuity in the weak operator topology is assumed for it.

theorem OAI.KadisonKastler.mem_mapped_matrix_concrete line 29
Source documentation
Membership in a finite matrix image is preserved by the given algebra isomorphism.
```
theorem mem_mapped_matrix_concrete (a : Algebra M) :
    (e a).val ∈ (E.map e.toStarAlgHom).concreteAlgebra ↔ a.val ∈ E.concreteAlgebra := by
…
```
Mentions: OAI.KadisonKastler.Algebra
def OAI.KadisonKastler.matrixTransferEquiv line 43
Source documentation
The given isomorphism restricted to the concrete finite matrix images.
```
def matrixTransferEquiv :
    Algebra (matrixUnitConcreteAlgebra E) ≃⋆ₐ[ℂ]
      Algebra (matrixUnitConcreteAlgebra (E.map e.toStarAlgHom)) where
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixUnitConcreteAlgebra
theorem OAI.KadisonKastler.matrixTransferEquiv_inclusion line 81
def OAI.KadisonKastler.transferredMatrixRetraction line 94
Source documentation
A finite-stage retraction on the original ambient operators.
```
def transferredMatrixRetraction (o : ι) :
    (H →L[ℂ] H) →L[ℂ] Algebra (matrixUnitConcreteAlgebra E) := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixUnitConcreteAlgebra
theorem OAI.KadisonKastler.transferredMatrixRetraction_norm line 111

theorem OAI.KadisonKastler.transferredMatrixRetraction_expectation line 127

Source documentation

On the original algebra the transported retraction is the trace expectation.

theorem transferredMatrixRetraction_expectation (o : ι)
    (hRa : ∀ a : Algebra M, R a.val = (e a).val) (a : Algebra M) :
    e (coordinateInclusion (matrixUnitConcreteAlgebra_le E)
      (transferredMatrixRetraction E e τ R hR o a.val)) =
    conditionalExpectation τ (matrixUnitConcreteAlgebra_le (E.map e.toStarAlgHom)) (e a) := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixUnitConcreteAlgebra_le, OAI.KadisonKastler.transferredMatrixRetraction