OAI/Analysis/FiniteFactor/CrossedProduct/FieldAlgebra.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceFiberVector_basis line 10
2. theorem OAI.FiniteFactor.sourceOperatorField_mul line 21
3. theorem OAI.FiniteFactor.sourceOperatorField_one line 42
4. theorem OAI.FiniteFactor.fiberOperator_star_entry line 58
5. theorem OAI.FiniteFactor.sourceOperatorField_star line 67
6. theorem OAI.FiniteFactor.sourceOperatorField_zero line 83
7. theorem OAI.FiniteFactor.sourceOperatorField_sub line 88
8. theorem OAI.FiniteFactor.sourceOperatorField_projection line 109

   Source documentation

   Every projection in the source algebra yields an actual measurable orthogonal-projection field.

   theorem sourceOperatorField_projection (θ : SourceCoordinate → ℝ)
       {p : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
       (hp : p ∈ sourceAlgebra θ) (hproj : IsStarProjection p) :
       ∀ᵐ x ∂sourceBaseMeasure, IsStarProjection (sourceOperatorField p x) := by
   …

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

9. theorem OAI.FiniteFactor.sourceOperatorField_invariant line 122

   Source documentation

   The original invariant-projection equation holds fiberwise for the actual operator and projection fields.

   theorem sourceOperatorField_invariant (θ : SourceCoordinate → ℝ)
       {p T : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
       (hp : p ∈ sourceAlgebra θ) (hT : T ∈ sourceAlgebra θ)
       (hinv : (1-p)*T*p = 0) :
       ∀ᵐ x ∂sourceBaseMeasure,
         (1-sourceOperatorField p x)*sourceOperatorField T x*sourceOperatorField p x = 0 := by
   …

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

10. theorem OAI.FiniteFactor.sourceVacuumFunctional_fieldIntegral line 136

    Source documentation

    The normal trace already proved is exactly the field-integral formula.

    theorem sourceVacuumFunctional_fieldIntegral (θ : SourceCoordinate → ℝ)
        {H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
        (hH : H ∈ sourceAlgebra θ) :
        sourceVacuumFunctional H = ∫ x,
          (sourceOperatorField H x (lp.single 2 0 (1 : ℂ))) 0 ∂sourceBaseMeasure := by
    …

    Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceVacuumFunctional, OAI.FiniteFactor.sourceOperatorField, OAI.FiniteFactor.sourceBaseMeasure