OAI/Analysis/FiniteFactor/CrossedProduct/ProjectionDiagonal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceProjection_zero_of_diagonal_zero line 13

   Source documentation

   Faithfulness turns a zero diagonal almost everywhere into the zero projection.

   theorem sourceProjection_zero_of_diagonal_zero (θ : SourceCoordinate → ℝ)
       {p : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
       (hp : p ∈ sourceAlgebra θ) (hproj : IsStarProjection p)
       (hz : sourceCentralCoefficient p =ᵐ[sourceBaseMeasure] fun _ => 0) : p = 0 := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceCentralCoefficient, OAI.FiniteFactor.sourceBaseMeasure

2. theorem OAI.FiniteFactor.sourceProjection_one_of_diagonal_one line 22
3. theorem OAI.FiniteFactor.sourceProjection_diagonal_rotation_implications line 38

   Source documentation

   The diagonal's zero event is backwards invariant and its one event forwards invariant. Both implications follow from the original invariant operator.

   theorem sourceProjection_diagonal_rotation_implications
       (θ : 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) :
       ∀ᵐ x ∂sourceBaseMeasure,
         (sourceCentralCoefficient p (coordinateRotate θ 1 x) = 0 → sourceCentralCoefficient p x = 0) ∧
         (sourceCentralCoefficient p x = 1 → sourceCentralCoefficient p (coordinateRotate θ 1 x) = 1) := by
   …

   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.sourceBaseMeasure, OAI.FiniteFactor.sourceCentralCoefficient, OAI.FiniteFactor.coordinateRotate

4. theorem OAI.FiniteFactor.sourceProjection_strict_diagonal line 77