CommonConull.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceProjection_biased_common_conull line 11

Source documentation

One invariant Borel conull set for the original projection works for every actual biased law, with strict positivity and the full uncapped pair identity.

theorem sourceProjection_biased_common_conull
    (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ) (hr : SourceRationalIndependent θ)
    (hs : SourceOrderedTorusSampling θ)
    {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 =
…