OAI/Analysis/FiniteFactor/CrossedProduct/VacuumSeparating.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceVacuum_separating line 10

   Source documentation

   The actual constant e_0 vector separates the source double commutant.

   theorem sourceVacuum_separating (θ : SourceCoordinate → ℝ)
       {H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
       (hH : H ∈ sourceAlgebra θ) (hv : H sourceVacuum = 0) : H = 0 := by
   …

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

2. theorem OAI.FiniteFactor.sourceVacuumFunctional_square_eq_zero_iff line 37

   Source documentation

   Faithfulness on squares of the actual normal vacuum functional.

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

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