OAI/Analysis/FiniteFactor/CrossedProduct/InvariantConull.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceTorusRotate_zero line 10
2. theorem OAI.FiniteFactor.sourceTorusRotate_add line 15
3. theorem OAI.FiniteFactor.sourceTorusRotate_preserving line 21
4. theorem OAI.FiniteFactor.exists_source_invariant_conull line 31
5. theorem OAI.FiniteFactor.sourceProjection_common_conull line 58

   Source documentation

   A single invariant Borel conull set for the fixed original projection: finite cocycles, actual projection fields, all covariance entries and all ordered orbit identities hold at every point of the set.

   theorem sourceProjection_common_conull (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ)
       {p : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
       (hp : p ∈ sourceAlgebra θ) (hproj : IsStarProjection p)
       (hinv : (1-p)*sourceOperator θ sourceLogWeight hθ.nonneg sourceLogWeight_nonneg*p = 0) :
       ∃ Q : Set SourceTorus, MeasurableSet Q ∧ (∀ᵐ z ∂sourceTorusHaar, z ∈ Q) ∧
         (∀ z ∈ Q,
           finiteFloorSupport θ (sourceTorusRepresentative z) ∧
           IsStarProjection (sourceTorusOperatorField p z) ∧
           (∀ r k m : ℤ, (sourceTorusOperatorField p (sourceTorusRotate θ r z)
             (lp.single 2 m (1 : ℂ))) k =
             (sourceTorusOperatorField p z (lp.single 2 (m+r) (1 : ℂ))) (k+r)) ∧
           (∀ n : ℕ, (∀ i, sourceTorusRepresentative z i ≤
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceOperator, OAI.FiniteFactor.sourceLogWeight, OAI.FiniteFactor.sourceLogWeight_nonneg, OAI.FiniteFactor.SourceTorus, OAI.FiniteFactor.sourceTorusHaar, OAI.FiniteFactor.finiteFloorSupport, OAI.FiniteFactor.sourceTorusRepresentative, OAI.FiniteFactor.sourceTorusOperatorField, OAI.FiniteFactor.sourceTorusRotate