MatrixStateMoments.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Mixed vector-state moments of finite matrix orbits

These are the two independent-copy pairings used in graph flattening. The finite signed-permutation averages are actual matrix averages, and only the common vector-state centralizer identity is used. In particular none of the state calculations presupposes a tracial ambient state.

def OAI.KadisonKastler.operatorVectorState line 24
Source documentation
The ambient vector functional, without an algebra-membership wrapper.
```
def operatorVectorState (Ω : H) : (H →L[ℂ] H) →ₗ[ℂ] ℂ where
…
```
theorem OAI.KadisonKastler.operatorVectorState_apply line 30
theorem OAI.KadisonKastler.average_linear line 33
theorem OAI.KadisonKastler.average_sandwich line 40
theorem OAI.KadisonKastler.state_unitaryConj line 46

theorem OAI.KadisonKastler.matrixState_two_orbit_average line 60

Source documentation

The first pairing of two independently conjugated copies is exactly one matrix average, paired against the unaveraged first element.

theorem matrixState_two_orbit_average
    (M : VonNeumannAlgebra H) (Ω : H) {d : ℕ}
    (E : Generator.MatrixUnitSystem (Fin d) (H →L[ℂ] H))
    (hEM : E.algebra ≤ M.toStarSubalgebra)
    (hcentral : ∀ a ∈ E.algebra, ∀ x ∈ M,
      inner ℂ Ω ((a * x) Ω) = inner ℂ Ω ((x * a) Ω))
    (a b : H →L[ℂ] H) (ha : a ∈ M) (hb : b ∈ M) :
    finiteAverage (fun g : SignedPermutation (Fin d) =>
      finiteAverage (fun h : SignedPermutation (Fin d) =>
        operatorVectorState Ω
          (unitaryConj (matrixUnitSignedRepresentation E g) a *
            unitaryConj (matrixUnitSignedRepresentation E h) b))) =
…

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

theorem OAI.KadisonKastler.matrixState_relative_orbit_average line 112

Source documentation

Averaging a relative pair of independently sampled matrix unitaries also gives the ordinary matrix average.

theorem matrixState_relative_orbit_average
    (Ω : H) {d : ℕ}
    (E : Generator.MatrixUnitSystem (Fin d) (H →L[ℂ] H))
    (a b c : H →L[ℂ] H) :
    finiteAverage (fun g : SignedPermutation (Fin d) =>
      finiteAverage (fun h : SignedPermutation (Fin d) =>
        operatorVectorState Ω (a *
          unitaryConj (star (matrixUnitSignedRepresentation E g))
            (unitaryConj (matrixUnitSignedRepresentation E h) b) * c))) =
      operatorVectorState Ω (a * matrixUnitAverage E b * c) := by
…

theorem OAI.KadisonKastler.matrixState_two_orbit_tendsto line 153

Source documentation

The first independent-copy pairing tends to the product of the two vector-state values.

theorem matrixState_two_orbit_tendsto
    (M : VonNeumannAlgebra H) (Ω : H) (hΩ : ‖Ω‖ = 1)
    (d : ℕ → ℕ) (E : ∀ n, Generator.MatrixUnitSystem (Fin (d n)) (H →L[ℂ] H))
    (hmono : Monotone (fun n => (E n).algebra))
    (hEM : ∀ n, (E n).algebra ≤ M.toStarSubalgebra)
    (hirr : ∀ T ∈ M, (∀ n a, a ∈ (E n).algebra → a * T = T * a) →
      ∃ z : ℂ, T = z • (1 : H →L[ℂ] H))
    (hcentral : ∀ n a, a ∈ (E n).algebra → ∀ x ∈ M,
      inner ℂ Ω ((a * x) Ω) = inner ℂ Ω ((x * a) Ω))
    (a b : H →L[ℂ] H) (ha : a ∈ M) (hb : b ∈ M) :
    Tendsto (fun n => finiteAverage (fun g : SignedPermutation (Fin (d n)) =>
      finiteAverage (fun h : SignedPermutation (Fin (d n)) =>
…

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

theorem OAI.KadisonKastler.matrixState_relative_orbit_tendsto line 178

Source documentation

The nested relative-conjugation pairing tends to the scalar state value of the averaged element times the state of the sandwich.

theorem matrixState_relative_orbit_tendsto
    (M : VonNeumannAlgebra H) (Ω : H) (hΩ : ‖Ω‖ = 1)
    (d : ℕ → ℕ) (E : ∀ n, Generator.MatrixUnitSystem (Fin (d n)) (H →L[ℂ] H))
    (hmono : Monotone (fun n => (E n).algebra))
    (hEM : ∀ n, (E n).algebra ≤ M.toStarSubalgebra)
    (hirr : ∀ T ∈ M, (∀ n a, a ∈ (E n).algebra → a * T = T * a) →
      ∃ z : ℂ, T = z • (1 : H →L[ℂ] H))
    (hcentral : ∀ n a, a ∈ (E n).algebra → ∀ x ∈ M,
      inner ℂ Ω ((a * x) Ω) = inner ℂ Ω ((x * a) Ω))
    (a b c : H →L[ℂ] H) (hb : b ∈ M) :
    Tendsto (fun n => finiteAverage (fun g : SignedPermutation (Fin (d n)) =>
      finiteAverage (fun h : SignedPermutation (Fin (d n)) =>
…

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

theorem OAI.KadisonKastler.operatorVectorState_square_re_le line 203
Source documentation
The crossed fourth-moment pairing is controlled by the two positive pairings. This is the vector-state version, with no trace assumption.
```
theorem operatorVectorState_square_re_le (Ω : H) (a : H →L[ℂ] H) :
    2 * (operatorVectorState Ω (a ^ 2)).re ≤
      ‖a Ω‖ ^ 2 + ‖(star a) Ω‖ ^ 2 := by
…
```
Mentions: OAI.KadisonKastler.operatorVectorState