OAI/Analysis/FiniteFactor/CrossedProduct/GeneratedAlgebra.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.FiniteFactor.SourceBaseFunction line 15

   Source documentation

   A bounded Borel function on the source cube. Values outside the cube are irrelevant because the representation evaluates rotation representatives.

   structure SourceBaseFunction where
   …

2. def OAI.FiniteFactor.sourcePiSymbol line 22
3. theorem OAI.FiniteFactor.sourcePiSymbol_measurable line 25
4. theorem OAI.FiniteFactor.sourcePiSymbol_bound line 33
5. theorem OAI.FiniteFactor.sourcePiSymbol_memLp line 37
6. def OAI.FiniteFactor.sourcePi line 42
7. theorem OAI.FiniteFactor.sourcePi_apply_ae line 47
8. theorem OAI.FiniteFactor.sourcePi_norm_le line 55
9. def OAI.FiniteFactor.sourceGeneratedVonNeumann line 67

   Source documentation

   Double commutant of a concrete family, including its adjoints.

   def sourceGeneratedVonNeumann {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
       [CompleteSpace H] (S : Set (H →L[ℂ] H)) : VonNeumannAlgebra H where
   …

10. theorem OAI.FiniteFactor.mem_sourceGeneratedVonNeumann line 77
11. def OAI.FiniteFactor.sourceAlgebra line 89

    Source documentation

    The actual generated algebra of the source regular representation. Factor, trace, finiteness and predual properties are separate obligations.

    def sourceAlgebra (θ : SourceCoordinate → ℝ) : VonNeumannAlgebra (SourceHilbert SourceCoordinate) :=
    …

    Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert

12. theorem OAI.FiniteFactor.sourcePi_mem line 92
13. theorem OAI.FiniteFactor.sourceShift_mem line 96
14. def OAI.FiniteFactor.sourceWeightBase line 100
15. theorem OAI.FiniteFactor.sourceMultiplication_eq_pi line 110
16. theorem OAI.FiniteFactor.staged_sourceOperator_mem line 116

    Source documentation

    Actual membership of the already verified staged operator in its generated von Neumann algebra, without an assumed operator-membership hypothesis.

    theorem staged_sourceOperator_mem (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ) :
        sourceOperator θ sourceLogWeight hθ.nonneg sourceLogWeight_nonneg ∈ sourceAlgebra θ := by
    …

    Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.sourceOperator, OAI.FiniteFactor.sourceLogWeight, OAI.FiniteFactor.sourceLogWeight_nonneg, OAI.FiniteFactor.sourceAlgebra