RecoveryRandomizedFamily.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The actual randomized recovery family

The diagonal phase, scalar phase, and outer coordinate are the three finite choices used in the recovery argument. Their rows have exact normalization, the corner operators are contractions in the original algebra, and the row product converges to a scalar with real part at least one half.

def OAI.KadisonKastler.randomizedRecoveryFamily line 25
Source documentation
The finite unitary family before the final coordinate-row choice.
```
def randomizedRecoveryFamily
    (s : unitary (BoundedSequence (Algebra (matrixVonNeumann (ι := Fin n) M))))
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.randomizedRecoveryFamily_forward_finiteRMS line 34
Source documentation
The exact forward RMS normalization holds at every sequence coordinate.
```
theorem randomizedRecoveryFamily_forward_finiteRMS
    (s : unitary (BoundedSequence (Algebra (matrixVonNeumann (ι := Fin n) M))))
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.randomizedRecoveryFamily_backward_finiteRMS line 48
Source documentation
The same exact normalization holds for the backward rows.
```
theorem randomizedRecoveryFamily_backward_finiteRMS
    (s : unitary (BoundedSequence (Algebra (matrixVonNeumann (ι := Fin n) M))))
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.randomizedRecoveryFamily_contractions_norm_le line 62
Source documentation
The extracted operators stay inside the unit ball of the original factor.
```
theorem randomizedRecoveryFamily_contractions_norm_le
    (s : unitary (BoundedSequence (Algebra (matrixVonNeumann (ι := Fin n) M))))
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.TraceQuotientMap.exists_randomizedRecoveryFamily_weak_scalar line 77
Source documentation
Free Haar moments for the starting lift suffice for the scalar weak limit of this specific randomized family; every phase twist is proved free.
```
theorem TraceQuotientMap.exists_randomizedRecoveryFamily_weak_scalar
    (D : TraceQuotientMap (matrixVonNeumannTrace (ι := Fin n) M τ) σ ω)
…
```
Mentions: OAI.KadisonKastler.TraceQuotientMap, OAI.KadisonKastler.matrixVonNeumannTrace