OAI/Analysis/FiniteFactor/CrossedProduct/NoMinimalProjection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceAlgebra_small_trace_partitions line 14

   Source documentation

   The original algebra has identity partitions of arbitrarily small trace, using equal intervals of its first Haar coordinate.

   theorem sourceAlgebra_small_trace_partitions (θ : SourceCoordinate → ℝ) (ε : ℝ) (hε : 0 < ε) :
       ∃ n : ℕ, ∃ e : Fin n → (sourceAlgebra θ).toStarSubalgebra,
         (∀ j, IsStarProjection (e j : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate)) ∧
         (∑ j, e j) = 1 ∧
         ∀ j, (sourceVacuumFunctional (e j)).re < ε := by
   …

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

2. theorem OAI.FiniteFactor.sourceAlgebra_hasNoMinimalProjection line 40

   Source documentation

   Actual nonzero proper subprojections of every nonzero projection in the original algebra. The support construction is internal to this same algebra.

   theorem sourceAlgebra_hasNoMinimalProjection (θ : SourceCoordinate → ℝ) :
       HasNoMinimalProjection (sourceAlgebra θ) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.HasNoMinimalProjection, OAI.FiniteFactor.sourceAlgebra