OAI/Analysis/FiniteFactor/CrossedProduct/PreparedFinite.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.exists_source_prepared_finite line 14

   Source documentation

   One actual finite tracial source algebra, with the sampled rotation and nonzero quasinilpotent operator. Scalar center, no minimal projections, separable predual and the invariant-projection conclusion remain separate.

   theorem exists_source_prepared_finite : ∃ θ : SourceCoordinate → ℝ,
       SourceRationalIndependent θ ∧
       (∃ j : ℕ, SourceSecondPhasesFrom θ j) ∧
       SourceOrderedTorusSampling θ ∧
       (∀ k : ℤ, MeasurePreserving (coordinateRotate θ k) sourceSamplingHaar sourceSamplingHaar) ∧
       (∀ k : ℤ, k ≠ 0 → ∀ x, coordinateRotate θ k x ≠ x) ∧
       IsFiniteAlgebra (sourceAlgebra θ) ∧
       Nonempty (TracialRepresentation (sourceAlgebra θ)) ∧
       ∃ hθ : SourceAngles θ,
         let T := sourceOperator θ sourceLogWeight hθ.nonneg sourceLogWeight_nonneg
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceRationalIndependent, OAI.FiniteFactor.SourceSecondPhasesFrom, OAI.FiniteFactor.SourceOrderedTorusSampling, OAI.FiniteFactor.coordinateRotate, OAI.FiniteFactor.sourceSamplingHaar, OAI.FiniteFactor.IsFiniteAlgebra, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.TracialRepresentation, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.sourceOperator, OAI.FiniteFactor.sourceLogWeight, OAI.FiniteFactor.sourceLogWeight_nonneg