RandomizedHaarLift.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Free Haar moments for the actual randomized recovery lifts

theorem OAI.KadisonKastler.freeHaar_mul_constant_right line 19

Source documentation

A constant unitary can be multiplied on the right of a free lift.

theorem freeHaar_mul_constant_right (π : BoundedSequence A →⋆ₐ[ℂ] B)
    (s : unitary (BoundedSequence A))
    (hs : FreeHaarMoments σ (π.comp boundedSequenceConst).range
      (Unitary.map (StarMonoidHom.ofClass π) s)) (U : unitary A) :
    FreeHaarMoments σ (π.comp boundedSequenceConst).range
      (Unitary.map (StarMonoidHom.ofClass π)
        (s * Unitary.map (StarMonoidHom.ofClass (boundedSequenceConst (B := A))) U)) := by
…

Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.boundedSequenceConst

theorem OAI.KadisonKastler.freeHaar_mul_constant_left line 30

Source documentation

A constant unitary can likewise be multiplied on the left.

theorem freeHaar_mul_constant_left (π : BoundedSequence A →⋆ₐ[ℂ] B)
    (s : unitary (BoundedSequence A))
    (hs : FreeHaarMoments σ (π.comp boundedSequenceConst).range
      (Unitary.map (StarMonoidHom.ofClass π) s)) (U : unitary A) :
    FreeHaarMoments σ (π.comp boundedSequenceConst).range
      (Unitary.map (StarMonoidHom.ofClass π)
        (Unitary.map (StarMonoidHom.ofClass (boundedSequenceConst (B := A))) U * s)) := by
…

Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.boundedSequenceConst

def OAI.KadisonKastler.amplificationPhaseUnitary line 44
Source documentation
The diagonal matrix phase is an actual unitary in the amplified algebra.
```
def amplificationPhaseUnitary (E : Generator.MatrixUnitSystem (Fin k) (Algebra M))
    (θ : Fin (n * k) → ZMod q) : unitary (Algebra (matrixVonNeumann (ι := Fin n) M)) :=
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
def OAI.KadisonKastler.randomizedRecoveryLift line 55
Source documentation
The three independent choices used in scalar recovery, as unitary sequences.
```
def randomizedRecoveryLift
    (s : unitary (BoundedSequence (Algebra (matrixVonNeumann (ι := Fin n) M))))
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.randomizedRecoveryLift_free line 66
Source documentation
Every member of the finite recovery family is free from the constant algebra.
```
theorem randomizedRecoveryLift_free
    (π : BoundedSequence (Algebra (matrixVonNeumann (ι := Fin n) M)) →⋆ₐ[ℂ] B)
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.randomizedRecoveryLift_eval line 82
Source documentation
Evaluation of the finite randomized family gives exactly the scalar phase twist of the diagonal-phase unitary used by the row formulas.
```
theorem randomizedRecoveryLift_eval
    (s : unitary (BoundedSequence (Algebra (matrixVonNeumann (ι := Fin n) M))))
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann