OAI/Analysis/KadisonKastler/PositiveStateRepresentative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Positive representatives of the faithful vector states used by stability

The positive off-diagonal matrix vector gives a representative in the reference cone. Its partial isometry between the two corners preserves the original algebra action and hence the vector functional.

  1. theorem OAI.KadisonKastler.exists_positive_representative_of_cyclic line 26
  2. theorem OAI.KadisonKastler.TypeIIIFactor.exists_positive_unit_state_representative line 60

    Source documentation

    Only faithful vector states on the type III representation used below are needed; a support isometry first makes the second vector cyclic.

    theorem TypeIIIFactor.exists_positive_unit_state_representative
    [Nontrivial H] (hM : TypeIIIFactor M)
    (Ω : H) (hΩc : DenseRange (algebraVectorMap M Ω))
    (hΩs : Function.Injective (algebraVectorMap M Ω))
    (J : H ≃ₗᵢ⋆[ℂ] H) (ξ : H) (hξ : ‖ξ‖=1)
    (hξs : Function.Injective (algebraVectorMap M ξ)) :
    ∃ η : H, η ∈ canonicalModularPositiveCone J Ω hΩs hΩc ∧
      ‖η‖=1 ∧ Function.Injective (algebraVectorMap M η) ∧
      DenseRange (algebraVectorMap M η) ∧
      vectorFunctional (M := M) η=vectorFunctional ξ := by
…

    Mentions: OAI.KadisonKastler.TypeIIIFactor, OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.canonicalModularPositiveCone