OAI/Analysis/FiniteFactor/CrossedProduct/ScalarCenter.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceOperator_eq_scalar_of_field line 12

   Source documentation

   Constancy of the representing field is equality of the original operators.

   theorem sourceOperator_eq_scalar_of_field (θ : SourceCoordinate → ℝ)
       {A : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
       (hA : A ∈ sourceAlgebra θ) (c : ℂ)
       (hc : ∀ᵐ x ∂sourceBaseMeasure, sourceOperatorField A x =
         c • (1 : SourceFiberHilbert →L[ℂ] SourceFiberHilbert)) :
       A = c • (1 : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate) := by
   …

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

2. theorem OAI.FiniteFactor.sourceCentralCoefficient_constant line 37
3. theorem OAI.FiniteFactor.sourceAlgebra_hasScalarCenter line 46