ScalarCommutant.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.sourceScalar line 10
Source documentation
Scalar base multiplication, independent of the fiber coordinate.
```
def sourceScalar (g : SourceBaseFunction) :
    SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate :=
…
```
Mentions: OAI.FiniteFactor.SourceBaseFunction, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.SourceCoordinate
theorem OAI.FiniteFactor.sourceScalar_star line 14
theorem OAI.FiniteFactor.sourceShift_apply_ae line 18
theorem OAI.FiniteFactor.sourceScalar_shift_commute line 23
theorem OAI.FiniteFactor.sourceScalar_mem_generator_commutant line 47
Source documentation
The scalar multipliers commute with the generators and their adjoints.
```
theorem sourceScalar_mem_generator_commutant (θ : SourceCoordinate → ℝ)
    (g : SourceBaseFunction) :
    sourceScalar g ∈ StarSubalgebra.centralizer ℂ
      ({sourceShift SourceCoordinate} ∪ Set.range (sourcePi θ)) := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceBaseFunction, OAI.FiniteFactor.sourceScalar, OAI.FiniteFactor.sourceShift, OAI.FiniteFactor.sourcePi
theorem OAI.FiniteFactor.sourceAlgebra_commutes_scalar line 65
Source documentation
The commutation holds for every element of the actual double commutant.
```
theorem sourceAlgebra_commutes_scalar (θ : SourceCoordinate → ℝ)
    {H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
    (hH : H ∈ sourceAlgebra θ) (g : SourceBaseFunction) :
    sourceScalar g * H = H * sourceScalar g := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.SourceBaseFunction, OAI.FiniteFactor.sourceScalar