MatrixOrbitSampleLaw.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Finite laws of the actual matrix-orbit samples

This converts the complex four-variable matrix-average identities to real moment identities for a single product-valued sample. It supplies the diagonal and the two off-diagonal inputs to the independent-sample fourth-moment estimate.

abbrev OAI.KadisonKastler.MatrixOrbitIndex line 24
Source documentation
The actual finite sample space for one left and one right unitary.
```
abbrev MatrixOrbitIndex (d : ℕ) := SignedPermutation (Fin d) × SignedPermutation (Fin d)
```
Mentions: OAI.KadisonKastler.SignedPermutation
def OAI.KadisonKastler.matrixOrbitSample line 27
Source documentation
An operator sampled from the finite two-sided matrix orbit.
```
def matrixOrbitSample {d : ℕ}
    (E : Generator.MatrixUnitSystem (Fin d) (H →L[ℂ] H))
    (x : H →L[ℂ] H) (g : MatrixOrbitIndex d) : H →L[ℂ] H :=
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.MatrixOrbitIndex
theorem OAI.KadisonKastler.complex_expect_eq_average line 33
theorem OAI.KadisonKastler.re_average line 38
theorem OAI.KadisonKastler.expect_prod line 43
theorem OAI.KadisonKastler.state_conj line 48
Distinct definitions of this name: OAI/Analysis/KadisonKastler/MatrixGraphMomentBounds.lean:55 (different declaration text). Qualify references as OAI.KadisonKastler.state_conj@path.

theorem OAI.KadisonKastler.matrixOrbit_diagonal_fourth line 63

Source documentation

The fourth moment of a single orbit sample is unchanged by its two unitaries, since the right unitary belongs to the state's centralizer.

theorem matrixOrbit_diagonal_fourth
    (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) (g : MatrixOrbitIndex d) :
    realVectorState Ω ((star (matrixOrbitSample E x g) * matrixOrbitSample E x g) ^ 2) =
      realVectorState Ω ((star x * x) ^ 2) := by
…

Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.MatrixOrbitIndex, OAI.KadisonKastler.realVectorState, OAI.KadisonKastler.matrixOrbitSample

theorem OAI.KadisonKastler.matrixOrbit_first_pairing_expect line 86

Source documentation

The first off-diagonal moment is the actual first independent-copy matrix pairing, expressed as a real number.

theorem matrixOrbit_first_pairing_expect
    (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) :
    (𝔼 g : MatrixOrbitIndex d, 𝔼 h : MatrixOrbitIndex d,
      realVectorState Ω ((star (matrixOrbitSample E x g) * matrixOrbitSample E x g) *
        (star (matrixOrbitSample E x h) * matrixOrbitSample E x h))) =
      realVectorState Ω ((star x * x) * matrixUnitAverage E (star x * x)) := by
…

Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.MatrixOrbitIndex, OAI.KadisonKastler.realVectorState, OAI.KadisonKastler.matrixOrbitSample, OAI.KadisonKastler.matrixUnitAverage

theorem OAI.KadisonKastler.matrixOrbit_third_pairing_expect line 115

Source documentation

The positive mixed pairing similarly becomes one averaged left square between x* and x.

theorem matrixOrbit_third_pairing_expect
    (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) :
    (𝔼 g : MatrixOrbitIndex d, 𝔼 h : MatrixOrbitIndex d,
      realVectorState Ω ((star (matrixOrbitSample E x g) * matrixOrbitSample E x h) *
        (star (matrixOrbitSample E x h) * matrixOrbitSample E x g))) =
      realVectorState Ω (star x * matrixUnitAverage E (x * star x) * x) := by
…

Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.MatrixOrbitIndex, OAI.KadisonKastler.realVectorState, OAI.KadisonKastler.matrixOrbitSample, OAI.KadisonKastler.matrixUnitAverage