OAI/Analysis/FiniteFactor/CrossedProduct/PreparedErgodic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.exists_source_prepared_ergodic line 16

   Source documentation

   The actual source construction now includes proved ergodicity, scalar center, finiteness and the exact separable predual. No minimal-projection or arbitrary invariant-projection conclusion is asserted here.

   theorem exists_source_prepared_ergodic : ∃ θ : SourceCoordinate → ℝ,
       SourceRationalIndependent θ ∧
       (∃ j : ℕ, SourceSecondPhasesFrom θ j) ∧
       SourceOrderedTorusSampling θ ∧
       Ergodic (coordinateRotate θ 1) sourceBaseMeasure ∧
       HasScalarCenter (sourceAlgebra θ) ∧
       IsFiniteAlgebra (sourceAlgebra θ) ∧
       HasSeparablePredual (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.sourceBaseMeasure, OAI.FiniteFactor.HasScalarCenter, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.IsFiniteAlgebra, OAI.FiniteFactor.HasSeparablePredual, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.sourceOperator, OAI.FiniteFactor.sourceLogWeight, OAI.FiniteFactor.sourceLogWeight_nonneg