ProductStateIrreducible.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Local independent swaps force scalar relative commutant

theorem OAI.KadisonKastler.LocalProductSwaps.local_factorization line 19

Source documentation

Factorization of the vector state against every local observable.

theorem local_factorization (hΩ : ‖Ω‖ = 1) (x : H →L[ℂ] H) (hx : x ∈ D)
    (hcomm : ∀ u : unitary (H →L[ℂ] H), (u : H →L[ℂ] H) ∈ D →
      ProductStateCentralizes D Ω u → (u : H →L[ℂ] H) * x = x * u)
    (k : ℕ) (a : L.localAlgebra k) :
    productVectorState Ω ((a : H →L[ℂ] H) * x) =
      productVectorState Ω a * productVectorState Ω x := by
…

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

theorem OAI.KadisonKastler.LocalProductSwaps.scalar_of_commutes line 81
Source documentation
The relative commutant of the full vector-state centralizer is scalar. The argument uses only finite-site independence, dense local vectors, and separation by the product vector.
```
theorem scalar_of_commutes (hΩ : ‖Ω‖ = 1)
    (hsep : Function.Injective (algebraVectorMap D Ω))
    (x : H →L[ℂ] H) (hx : x ∈ D)
    (hcomm : ∀ u : unitary (H →L[ℂ] H), (u : H →L[ℂ] H) ∈ D →
      ProductStateCentralizes D Ω u → (u : H →L[ℂ] H) * x = x * u) :
    x = productVectorState Ω x • (1 : H →L[ℂ] H) := by
…
```
Mentions: OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.ProductStateCentralizes, OAI.KadisonKastler.productVectorState

theorem OAI.KadisonKastler.LocalProductSwaps.relative_commutant_scalar line 113

Source documentation

Set-theoretic form of the relative-commutant assertion, usable before bundling the state centralizer as a von Neumann subalgebra.

theorem relative_commutant_scalar (hΩ : ‖Ω‖ = 1)
    (hsep : Function.Injective (algebraVectorMap D Ω))
    (x : H →L[ℂ] H) (hx : x ∈ D)
    (hcomm : x ∈ Set.centralizer
      {u : H →L[ℂ] H | u ∈ D ∧ ProductStateCentralizes D Ω u}) :
    ∃ z : ℂ, x = z • (1 : H →L[ℂ] H) := by
…

Mentions: OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.ProductStateCentralizes