ProductStateCentralizer.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The centralizer of an infinite product state is irreducible

The proof uses only dense local vectors and state-preserving local swaps which move a local observable to an independent set of sites. These are the finite-site properties of the two-ratio tensor product in section 6.

def OAI.KadisonKastler.productVectorState line 20
Source documentation
The ambient vector functional, without any trace assumption.
```
def productVectorState (Ω : H) (T : H →L[ℂ] H) : ℂ := inner ℂ Ω (T Ω)
…
```
theorem OAI.KadisonKastler.norm_productVectorState_le line 23
def OAI.KadisonKastler.ProductStateCentralizes line 31
Source documentation
The state centralizer identity used by a finite-site swap.
```
def ProductStateCentralizes (D : VonNeumannAlgebra H) (Ω : H) (u : H →L[ℂ] H) : Prop :=
…
```

theorem OAI.KadisonKastler.productVectorState_swap line 36

Source documentation

State centralization and commutation with x allow a local observable to be moved by the swap while leaving its pairing with x unchanged.

theorem productVectorState_swap (D : VonNeumannAlgebra H) (Ω : H)
    (u : unitary (H →L[ℂ] H)) (hu : (u : H →L[ℂ] H) ∈ D)
    (hcentral : ProductStateCentralizes D Ω u)
    (a x : H →L[ℂ] H) (ha : a ∈ D) (hx : x ∈ D)
    (hcomm : (u : H →L[ℂ] H) * x = x * u) :
    productVectorState Ω (unitaryConj u a * x) = productVectorState Ω (a * x) := by
…

Mentions: OAI.KadisonKastler.ProductStateCentralizes, OAI.KadisonKastler.productVectorState, OAI.KadisonKastler.unitaryConj

theorem OAI.KadisonKastler.productVectorState_mul_error line 56

Source documentation

A vector-functional error only sees the vector error in the right factor.

theorem productVectorState_mul_error (Ω : H) (hΩ : ‖Ω‖ = 1)
    (a x y : H →L[ℂ] H) :
    ‖productVectorState Ω (a * x) - productVectorState Ω (a * y)‖ ≤
      ‖a‖ * ‖(x - y) Ω‖ := by
…

Mentions: OAI.KadisonKastler.productVectorState

structure OAI.KadisonKastler.LocalProductSwaps line 70
Source documentation
The two finite-site properties sufficient for the product-state argument. No centralizer irreducibility or core-type conclusion is a field here.
```
structure LocalProductSwaps (D : VonNeumannAlgebra H) (Ω : H) where
…
```