OAI/Analysis/FiniteFactor/CrossedProduct/InvariantProjection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceInvariantProjection_trivial line 14

   Source documentation

   The source probability contradiction for the original operator and original algebra. All event, convolution and error estimates are proved from this p's actual projection and invariance identities.

   theorem sourceInvariantProjection_trivial
       (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ) (hr : SourceRationalIndependent θ)
       (hs : SourceOrderedTorusSampling θ) (hphase : ∃ J, SourceSecondPhasesFrom θ J)
       {p : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
       (hp : p ∈ sourceAlgebra θ) (hproj : IsStarProjection p)
       (hinv : (1-p)*sourceOperator θ sourceLogWeight hθ.nonneg sourceLogWeight_nonneg*p = 0) :
       p = 0 ∨ p = 1 := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.SourceRationalIndependent, OAI.FiniteFactor.SourceOrderedTorusSampling, OAI.FiniteFactor.SourceSecondPhasesFrom, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceOperator, OAI.FiniteFactor.sourceLogWeight, OAI.FiniteFactor.sourceLogWeight_nonneg