MatrixProductStateSwap.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Product moments put finite block swaps in the state centralizer

The finite calculation needs only the three-block product formula and equal moments on the two blocks being exchanged. Strong density then extends the resulting identities from local matrix algebras to their generated von Neumann algebra.

theorem OAI.KadisonKastler.unitary_conjugation_mul line 28

theorem OAI.KadisonKastler.matrix_functional_invariant_of_entries line 38

Source documentation

Equality on the matrix-unit coefficients implies equality on the whole finite matrix algebra.

theorem matrix_functional_invariant_of_entries
    (E : MatrixUnitSystem ι A) (φ : A →ₗ[ℂ] ℂ) (u : unitary A)
    (hφ : ∀ i j, φ ((u : A) * E.entry i j * star (u : A)) = φ (E.entry i j))
    (x : A) (hx : x ∈ E.algebra) :
    φ ((u : A) * x * star (u : A)) = φ x := by
…

theorem OAI.KadisonKastler.finiteMatrixBlockSwap_product_invariant line 49

Source documentation

Three-block product moments are invariant under swapping the two equal-state blocks, with an arbitrary finite complement left in place.

theorem finiteMatrixBlockSwap_product_invariant
    (E : MatrixUnitSystem (ι × ι) A) (C : MatrixUnitSystem κ A)
    (hEC : ∀ i j k l, Commute (E.entry i j) (C.entry k l))
    (φ : A →ₗ[ℂ] ℂ) (α : ι → ι → ℂ) (β : κ → κ → ℂ)
    (hφ : ∀ i j k l r s,
      φ (E.entry (i, j) (k, l) * C.entry r s) = α i k * α j l * β r s)
    (x : A) (hx : x ∈ (E.product C hEC).algebra) :
    φ ((finiteMatrixBlockSwap E : A) * x * star (finiteMatrixBlockSwap E : A)) = φ x := by
…

Mentions: OAI.KadisonKastler.finiteMatrixBlockSwap

theorem OAI.KadisonKastler.finiteMatrixBlockSwap_product_centralizes line 75

Source documentation

Product moments imply centralization on the finite joint algebra.

theorem finiteMatrixBlockSwap_product_centralizes
    (E : MatrixUnitSystem (ι × ι) A) (C : MatrixUnitSystem κ A)
    (hEC : ∀ i j k l, Commute (E.entry i j) (C.entry k l))
    (φ : A →ₗ[ℂ] ℂ) (α : ι → ι → ℂ) (β : κ → κ → ℂ)
    (hφ : ∀ i j k l r s,
      φ (E.entry (i, j) (k, l) * C.entry r s) = α i k * α j l * β r s)
    (x : A) (hx : x ∈ (E.product C hEC).algebra) :
    φ ((finiteMatrixBlockSwap E : A) * x) = φ (x * finiteMatrixBlockSwap E) := by
…

Mentions: OAI.KadisonKastler.finiteMatrixBlockSwap

theorem OAI.KadisonKastler.finiteMatrixBlockSwap_conjugate_left_entry line 93

Source documentation

In the product of two commuting copies, the block swap carries each left matrix unit to the corresponding right matrix unit.

theorem finiteMatrixBlockSwap_conjugate_left_entry
    (E F : MatrixUnitSystem ι A)
    (hEF : ∀ i j k l, Commute (E.entry i j) (F.entry k l)) (i j : ι) :
    (finiteMatrixBlockSwap (E.product F hEF) : A) * E.entry i j *
      star (finiteMatrixBlockSwap (E.product F hEF) : A) = F.entry i j := by
…

Mentions: OAI.KadisonKastler.finiteMatrixBlockSwap

theorem OAI.KadisonKastler.finiteMatrixBlockSwap_conjugate_left_hom line 102

theorem OAI.KadisonKastler.finiteMatrixBlockSwap_independent line 113

Source documentation

Independence of the remote block on matrix units implies the desired factorization for every observable in the original finite block.

theorem finiteMatrixBlockSwap_independent
    (E F : MatrixUnitSystem ι A)
    (hEF : ∀ i j k l, Commute (E.entry i j) (F.entry k l))
    (φ : A →ₗ[ℂ] ℂ) (b : A)
    (hfar : ∀ i j, φ (F.entry i j * b) = φ (E.entry i j) * φ b)
    (a : A) (ha : a ∈ E.algebra) :
    φ (((finiteMatrixBlockSwap (E.product F hEF) : A) * a *
      star (finiteMatrixBlockSwap (E.product F hEF) : A)) * b) = φ a * φ b := by
…

Mentions: OAI.KadisonKastler.finiteMatrixBlockSwap

def OAI.KadisonKastler.productVectorLinear line 135
Source documentation
The linear vector functional used by the finite product calculation.
```
def productVectorLinear (Ω : H) : (H →L[ℂ] H) →ₗ[ℂ] ℂ where
…
```
theorem OAI.KadisonKastler.productStateCentralizes_generated line 142
Source documentation
Centralization on a dense star algebra extends to its actual bicommutant. This uses the proved unbounded strong-density theorem.
```
theorem productStateCentralizes_generated
    (S : StarSubalgebra ℂ (H →L[ℂ] H)) (Ω : H) (u : H →L[ℂ] H)
    (hS : ∀ x ∈ S, productVectorState Ω (u * x) = productVectorState Ω (x * u)) :
    ProductStateCentralizes (generatedVonNeumannAlgebra S) Ω u := by
…
```
Mentions: OAI.KadisonKastler.productVectorState, OAI.KadisonKastler.ProductStateCentralizes, OAI.KadisonKastler.generatedVonNeumannAlgebra
theorem OAI.KadisonKastler.productStateCentralizes_of_local line 167
Source documentation
Stage-by-stage finite centralization supplies centralization on the von Neumann algebra generated by the increasing local algebras.
```
theorem productStateCentralizes_of_local
    (S : ℕ → StarSubalgebra ℂ (H →L[ℂ] H)) (hmono : Monotone S)
    (Ω : H) (u : H →L[ℂ] H)
    (hS : ∀ n x, x ∈ S n → productVectorState Ω (u * x) = productVectorState Ω (x * u)) :
    ProductStateCentralizes (generatedVonNeumannAlgebra (⨆ n, S n)) Ω u := by
…
```
Mentions: OAI.KadisonKastler.productVectorState, OAI.KadisonKastler.ProductStateCentralizes, OAI.KadisonKastler.generatedVonNeumannAlgebra