PreparedPairState.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The common vector functional centralizes the shared algebra

Matching left and right vector actions, including their adjoints, gives the centralizer identity directly by the Hilbert-space adjoint formula. The source's common conjugation supplies these matches on unitaries; the four-unitary span then gives every element of the common algebra.

theorem OAI.KadisonKastler.vector_functional_commutes_of_right_vector line 23

Source documentation

Matching a left operator and its adjoint on the vector with one commutant operator proves the vector-functional centralizer identity.

theorem vector_functional_commutes_of_right_vector
    (N : VonNeumannAlgebra H) (Ω : H) (r s : H →L[ℂ] H)
    (hs : s ∈ N.commutant)
    (hvector : r Ω = s Ω) (hstar : (star r) Ω = (star s) Ω)
    (x : Algebra N) :
    inner ℂ Ω ((r * x.val) Ω) = inner ℂ Ω ((x.val * r) Ω) := by
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.vector_functional_centralizes_of_right_unitaries line 45

Source documentation

It suffices to identify the right vector actions on unitaries of the common algebra: these unitaries span every element.

theorem vector_functional_centralizes_of_right_unitaries
    (R N : VonNeumannAlgebra H) (hRN : R ≤ N) (Ω : H)
    (hright : ∀ u : unitary (Algebra R), ∃ s ∈ N.commutant,
      (u : Algebra R).val Ω = s Ω ∧
      (star (u : Algebra R)).val Ω = (star s) Ω)
    (r : Algebra R) (x : Algebra N) :
    inner ℂ Ω ((r.val * x.val) Ω) = inner ℂ Ω ((x.val * r.val) Ω) := by
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.vector_functional_centralizes_of_conjugate_right line 74

Source documentation

The actual conjugate right algebra and central-vector relation in the prepared-pair construction imply that the vector functional on N centralizes R.

theorem vector_functional_centralizes_of_conjugate_right
    (R N : VonNeumannAlgebra H) (hRN : R ≤ N)
    (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J) (Ω : H)
    (hright : ∀ r : Algebra R, conjugationOperator J r.val ∈ N.commutant)
    (hcentral : ∀ r : Algebra R,
      r.val Ω = conjugationOperator J (star r).val Ω)
    (r : Algebra R) (x : Algebra N) :
    inner ℂ Ω ((r.val * x.val) Ω) = inner ℂ Ω ((x.val * r.val) Ω) := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.conjugationOperator