RecoveryRows.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Concrete rows and coordinate contractions for scalar recovery

A recovery contraction supported on one outer matrix coordinate is exactly an operator from the original algebra in that corner. Its row sandwich is the recovery observable, including the two square-root dimension factors.

theorem OAI.KadisonKastler.coordinate_projection_adjoint line 29
Source documentation
Coordinate evaluation and insertion are adjoints.
```
theorem coordinate_projection_adjoint (a : ι) :
    ((PiLp.proj 2 (fun _ : ι => H) a) : Generator.FiniteHilbert ι H →L[ℂ] H).adjoint =
      Generator.tupleSingle (H := H) a := by
…
```
Mentions: OAI.Generator.FiniteHilbert, OAI.Generator.tupleSingle
theorem OAI.KadisonKastler.matrixOperatorHom_matrixCorner line 44
Source documentation
The represented single-entry matrix is the coordinate insertion/evaluation sandwich of its original-algebra entry.
```
theorem matrixOperatorHom_matrixCorner (M : VonNeumannAlgebra H) (a : ι)
    (x : Algebra M) :
    matrixOperatorHom M (matrixCorner a x) =
      (Generator.tupleSingle a).comp (x.val.comp (PiLp.proj 2 (fun _ : ι => H) a)) := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixOperatorHom, OAI.KadisonKastler.matrixCorner, OAI.Generator.tupleSingle
def OAI.KadisonKastler.coordinateCornerEntry line 63
Source documentation
Extract the original-algebra entry of an operator in the represented matrix algebra. Membership is part of the returned subtype.
```
def coordinateCornerEntry (M : VonNeumannAlgebra H) (a : ι)
    (c : Algebra (matrixVonNeumann (ι := ι) M)) : Algebra M :=
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.norm_coordinateCornerEntry_le line 67
theorem OAI.KadisonKastler.coordinateCornerEntry_reconstruct line 80
Source documentation
Support by a coordinate projection gives exact corner reconstruction.
```
theorem coordinateCornerEntry_reconstruct (M : VonNeumannAlgebra H) (a : ι)
    (c : Algebra (matrixVonNeumann (ι := ι) M))
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
def OAI.KadisonKastler.recoveryCornerContraction line 116
Source documentation
The original-factor contraction obtained from the recovery operator.
```
def recoveryCornerContraction (M : VonNeumannAlgebra H) (a : Fin n)
    (f : Algebra (matrixVonNeumann (ι := Fin n) M)) : Algebra M :=
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.recoveryCornerContraction_norm_le line 120
theorem OAI.KadisonKastler.recoveryCornerContraction_reconstruct line 125
def OAI.KadisonKastler.recoveryForwardRow line 136
Source documentation
The actual forward row of the normalized polynomial.
```
def recoveryForwardRow (M : VonNeumannAlgebra H) (N : ℕ) (a : Fin n)
    (v : unitary (Algebra (matrixVonNeumann (ι := Fin n) M))) :
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
def OAI.KadisonKastler.recoveryBackwardRow line 143
Source documentation
The backward row is formed from the adjoint polynomial.
```
def recoveryBackwardRow (M : VonNeumannAlgebra H) (N : ℕ) (a : Fin n)
    (v : unitary (Algebra (matrixVonNeumann (ι := Fin n) M))) :
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.recoveryBackwardRow_adjoint line 149
theorem OAI.KadisonKastler.recoveryRows_product line 166
Source documentation
The corner contraction and the two normalized rows give precisely the observable whose weak limit is computed by the free-Haar argument.
```
theorem recoveryRows_product (M : VonNeumannAlgebra H) (hn : 0 < n)
    (N : ℕ) (a : Fin n)
    (v : unitary (Algebra (matrixVonNeumann (ι := Fin n) M))) :
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann