ProjectionPositiveConull.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceProjection_positive_common_conull line 12

Source documentation

The strict diagonal conclusion and every previously verified orbit identity hold on one invariant Borel conull set for the original candidate projection.

theorem sourceProjection_positive_common_conull
    (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ) (hr : SourceRationalIndependent θ)
    {p : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
    (hp : p ∈ sourceAlgebra θ) (hproj : IsStarProjection p) (hp0 : p ≠ 0) (hp1 : p ≠ 1)
    (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)) ∧
…