OAI/Analysis/FiniteFactor/CrossedProduct/Trace.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceVacuumFunctional_tracial line 9

   Source documentation

   Traciality of the actual, previously constructed normal vacuum functional.

   theorem sourceVacuumFunctional_tracial (θ : SourceCoordinate → ℝ)
       {A B : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
       (hA : A ∈ sourceAlgebra θ) (hB : B ∈ sourceAlgebra θ) :
       sourceVacuumFunctional (A * B) = sourceVacuumFunctional (B * A) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceVacuumFunctional

2. theorem OAI.FiniteFactor.sourceVacuumFunctional_square_commute line 23

   Source documentation

   Equality of the two square expectations is derived from traciality.

   theorem sourceVacuumFunctional_square_commute (θ : SourceCoordinate → ℝ)
       {H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
       (hH : H ∈ sourceAlgebra θ) :
       sourceVacuumFunctional (star H * H) = sourceVacuumFunctional (H * star H) :=
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceVacuumFunctional