MatrixOrbitPairings.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Fourth-moment pairings of actual two-sided matrix orbits

The sampled elements are u*x*v*. Their first and third sign-pairing terms reduce exactly to the independent matrix averages in MatrixStateMoments; the reductions use the vector-state centralizer, not a trace identity for arbitrary elements.

def OAI.KadisonKastler.unitaryDoubleOrbit line 23
Source documentation
One actual sample of the two-sided unitary orbit.
```
def unitaryDoubleOrbit (x : H →L[ℂ] H)
    (u v : unitary (H →L[ℂ] H)) : H →L[ℂ] H :=
…
```
theorem OAI.KadisonKastler.unitaryDoubleOrbit_star_mul_self line 28
Source documentation
The left orbit unitary cancels from the right square.
```
theorem unitaryDoubleOrbit_star_mul_self (x : H →L[ℂ] H)
    (u v : unitary (H →L[ℂ] H)) :
    star (unitaryDoubleOrbit x u v) * unitaryDoubleOrbit x u v =
      unitaryConj v (star x * x) := by
…
```
Mentions: OAI.KadisonKastler.unitaryDoubleOrbit, OAI.KadisonKastler.unitaryConj

theorem OAI.KadisonKastler.unitaryDoubleOrbit_mixed_square line 40

Source documentation

The mixed positive square exposes the relative left conjugation.

theorem unitaryDoubleOrbit_mixed_square (x : H →L[ℂ] H)
    (u v u' v' : unitary (H →L[ℂ] H)) :
    (star (unitaryDoubleOrbit x u v) * unitaryDoubleOrbit x u' v') *
        (star (unitaryDoubleOrbit x u' v') * unitaryDoubleOrbit x u v) =
      unitaryConj v (star x * unitaryConj (star u)
        (unitaryConj u' (x * star x)) * x) := by
…

Mentions: OAI.KadisonKastler.unitaryDoubleOrbit, OAI.KadisonKastler.unitaryConj

theorem OAI.KadisonKastler.state_conjugation line 55

theorem OAI.KadisonKastler.vectorState_unitaryDoubleOrbit_mixed_square line 69

Source documentation

Removing the right conjugation from the vector state identifies the third pairing for two actual orbit samples.

theorem vectorState_unitaryDoubleOrbit_mixed_square
    (M : VonNeumannAlgebra H) (Ω : H) (x : H →L[ℂ] H) (hx : x ∈ M)
    (u v u' v' : unitary (H →L[ℂ] H))
    (hu : (u : H →L[ℂ] H) ∈ M) (hv : (v : H →L[ℂ] H) ∈ M)
    (hu' : (u' : H →L[ℂ] H) ∈ M)
    (hc : ∀ z ∈ M, inner ℂ Ω (((v : H →L[ℂ] H) * z) Ω) =
      inner ℂ Ω ((z * (v : H →L[ℂ] H)) Ω)) :
    operatorVectorState Ω
      ((star (unitaryDoubleOrbit x u v) * unitaryDoubleOrbit x u' v') *
        (star (unitaryDoubleOrbit x u' v') * unitaryDoubleOrbit x u v)) =
      operatorVectorState Ω (star x * unitaryConj (star u)
        (unitaryConj u' (x * star x)) * x) := by
…

Mentions: OAI.KadisonKastler.operatorVectorState, OAI.KadisonKastler.unitaryDoubleOrbit, OAI.KadisonKastler.unitaryConj

theorem OAI.KadisonKastler.matrixOrbit_first_pairing_average line 96

Source documentation

Averaging the first pairing over the four independent matrix samples is precisely the first scalar expression of MatrixStateMoments.

theorem matrixOrbit_first_pairing_average
    (M : VonNeumannAlgebra H) (Ω : H) {d : ℕ}
    (E : Generator.MatrixUnitSystem (Fin d) (H →L[ℂ] H))
    (hEM : E.algebra ≤ M.toStarSubalgebra)
    (hc : ∀ a ∈ E.algebra, ∀ z ∈ M,
      inner ℂ Ω ((a * z) Ω) = inner ℂ Ω ((z * a) Ω))
    (x : H →L[ℂ] H) (hx : x ∈ M) :
    finiteAverage (fun i : SignedPermutation (Fin d) =>
      finiteAverage (fun j : SignedPermutation (Fin d) =>
        finiteAverage (fun k : SignedPermutation (Fin d) =>
          finiteAverage (fun l : SignedPermutation (Fin d) =>
            operatorVectorState Ω
…

Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.finiteAverage, OAI.KadisonKastler.SignedPermutation, OAI.KadisonKastler.operatorVectorState

theorem OAI.KadisonKastler.matrixOrbit_third_pairing_average line 124

Source documentation

Averaging the third pairing over four independent matrix samples reduces to the relative left-unitary average sandwiched by x* and x.

theorem matrixOrbit_third_pairing_average
    (M : VonNeumannAlgebra H) (Ω : H) {d : ℕ}
    (E : Generator.MatrixUnitSystem (Fin d) (H →L[ℂ] H))
    (hEM : E.algebra ≤ M.toStarSubalgebra)
    (hc : ∀ a ∈ E.algebra, ∀ z ∈ M,
      inner ℂ Ω ((a * z) Ω) = inner ℂ Ω ((z * a) Ω))
    (x : H →L[ℂ] H) (hx : x ∈ M) :
    finiteAverage (fun i : SignedPermutation (Fin d) =>
      finiteAverage (fun j : SignedPermutation (Fin d) =>
        finiteAverage (fun k : SignedPermutation (Fin d) =>
          finiteAverage (fun l : SignedPermutation (Fin d) =>
            operatorVectorState Ω
…

Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.finiteAverage, OAI.KadisonKastler.SignedPermutation, OAI.KadisonKastler.operatorVectorState