RecoveryRowNormalization.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Exact normalization of the phase-randomized recovery rows

def OAI.KadisonKastler.scalarPhaseUnitary line 20
Source documentation
The scalar root-of-unity phase, as a unitary in any unital complex C-star algebra.
```
def scalarPhaseUnitary (B : Type*) [CStarAlgebra B] (z : ZMod q) : unitary B :=
…
```
theorem OAI.KadisonKastler.scalarPhaseUnitary_coe line 34
theorem OAI.KadisonKastler.scalarPhaseUnitary_mem line 37
def OAI.KadisonKastler.scalarPhaseTwist line 42
Source documentation
Scalar multiplication of a unitary by the chosen finite phase.
```
def scalarPhaseTwist (z : ZMod q) (u : unitary B) : unitary B :=
…
```
theorem OAI.KadisonKastler.scalarPhaseTwist_coe line 46
def OAI.KadisonKastler.scalarPowerCharacter line 52
Source documentation
The characters attached to the first positive powers.
```
def scalarPowerCharacter (q N : ℕ) [NeZero q] (r : Fin N) : AddChar (ZMod q) ℂ :=
…
```
theorem OAI.KadisonKastler.scalarPowerCharacter_apply line 56
theorem OAI.KadisonKastler.scalarPowerCharacter_injective line 59
theorem OAI.KadisonKastler.scalarPowerCharacter_orthogonal line 73
theorem OAI.KadisonKastler.inverseScalarPowerCharacter_orthogonal line 78
theorem OAI.KadisonKastler.inverseScalarPowerCharacter_apply line 84

theorem OAI.KadisonKastler.represented_phase_polynomial line 92

Source documentation

The represented phased polynomial is exactly the finite phase sum.

theorem represented_phase_polynomial (ρ : B →⋆ₐ[ℂ] (K →L[ℂ] K))
    (u : unitary B) (z : ZMod q) (ξ : K) :
    ρ (unitaryHaarPolynomial N (scalarPhaseTwist z u)) ξ =
      (Real.sqrt (N : ℝ))⁻¹ • finitePhaseSum
        (fun r : Fin N => scalarPowerCharacter q N r)
        (fun r => ρ ((u : B) ^ (r.val + 1)) ξ) z := by
…

Mentions: OAI.KadisonKastler.unitaryHaarPolynomial, OAI.KadisonKastler.scalarPhaseTwist, OAI.KadisonKastler.finitePhaseSum, OAI.KadisonKastler.scalarPowerCharacter

theorem OAI.KadisonKastler.represented_adjoint_phase_polynomial line 105

Source documentation

The adjoint polynomial uses the inverse phase characters and the adjoints of the same unitary powers.

theorem represented_adjoint_phase_polynomial (ρ : B →⋆ₐ[ℂ] (K →L[ℂ] K))
    (u : unitary B) (z : ZMod q) (ξ : K) :
    ρ (star (unitaryHaarPolynomial N (scalarPhaseTwist z u))) ξ =
      (Real.sqrt (N : ℝ))⁻¹ • finitePhaseSum
        (fun r : Fin N => ⇑((scalarPowerCharacter q N r)⁻¹ : AddChar (ZMod q) ℂ))
        (fun r => ρ (star ((u : B) ^ (r.val + 1))) ξ) z := by
…

Mentions: OAI.KadisonKastler.unitaryHaarPolynomial, OAI.KadisonKastler.scalarPhaseTwist, OAI.KadisonKastler.finitePhaseSum, OAI.KadisonKastler.scalarPowerCharacter

theorem OAI.KadisonKastler.norm_represented_unitary_power line 118
theorem OAI.KadisonKastler.norm_represented_adjoint_unitary_power line 123
theorem OAI.KadisonKastler.recoveryForwardRow_phase_apply line 131
theorem OAI.KadisonKastler.recoveryBackwardRow_phase_apply line 149
theorem OAI.KadisonKastler.recoveryForwardRows_finiteRMS line 170
Source documentation
The random scalar phase and coordinate row have exact forward RMS norm.
```
theorem recoveryForwardRows_finiteRMS (M : VonNeumannAlgebra H)
    (u : unitary (Algebra (matrixVonNeumann (ι := Fin n) M)))
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.recoveryBackwardRows_finiteRMS line 185
Source documentation
The inverse phases give the identical normalization for backward rows.
```
theorem recoveryBackwardRows_finiteRMS (M : VonNeumannAlgebra H)
    (u : unitary (Algebra (matrixVonNeumann (ι := Fin n) M)))
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann