AmplificationWordUnits.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The unitary words used by coefficient and row estimates

def OAI.KadisonKastler.phaseWordBase line 15
Source documentation
The base word after the independent diagonal phase.
```
def phaseWordBase (E : Generator.MatrixUnitSystem (Fin k) (Algebra M))
    (v : unitary (Algebra (matrixVonNeumann (ι := Fin n) M)))
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
def OAI.KadisonKastler.positivePhaseWordUnitary line 21
Source documentation
Positive word with its last free-unitary factor removed.
```
def positivePhaseWordUnitary (E : Generator.MatrixUnitSystem (Fin k) (Algebra M))
    (v : unitary (Algebra (matrixVonNeumann (ι := Fin n) M)))
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
def OAI.KadisonKastler.negativePhaseWordUnitary line 28
Source documentation
Negative word, already a full adjoint power.
```
def negativePhaseWordUnitary (E : Generator.MatrixUnitSystem (Fin k) (Algebra M))
    (v : unitary (Algebra (matrixVonNeumann (ι := Fin n) M)))
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.positivePhaseWordUnitary_coe line 34
theorem OAI.KadisonKastler.negativePhaseWordUnitary_coe line 44
theorem OAI.KadisonKastler.positivePhaseWordUnitary_mul line 55
Source documentation
Appending the removed factor recovers the exact power used in the row.
```
theorem positivePhaseWordUnitary_mul
    (E : Generator.MatrixUnitSystem (Fin k) (Algebra M))
    (v : unitary (Algebra (matrixVonNeumann (ι := Fin n) M)))
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann