CentralScalarField.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceOperatorField_shift line 12
theorem OAI.FiniteFactor.fiber_commuting_shift_diagonal line 26
Source documentation
Commutation with the bilateral shift makes all diagonal coefficients equal.
```
theorem fiber_commuting_shift_diagonal (A : SourceFiberHilbert →L[ℂ] SourceFiberHilbert)
    (hc : A*fiberShift 1 = fiberShift 1*A) (n : ℤ) :
    A (lp.single 2 n (1 : ℂ)) n = A (lp.single 2 0 (1 : ℂ)) 0 := by
…
```
Mentions: OAI.FiniteFactor.SourceFiberHilbert, OAI.FiniteFactor.fiberShift
def OAI.FiniteFactor.sourceCentralCoefficient line 40
Source documentation
The scalar coefficient is the actual field's 00 entry.
```
def sourceCentralCoefficient
    (A : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate)
    (x : SourceCoordinate → ℝ) : ℂ := sourceOperatorField A x (lp.single 2 0 (1 : ℂ)) 0
```
Mentions: OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceOperatorField
theorem OAI.FiniteFactor.sourceCentralCoefficient_measurable line 44
theorem OAI.FiniteFactor.sourceCentral_scalar_field line 50
Source documentation
Every central element of the original algebra is a scalar field. The scalar may still depend on x; ergodicity is needed to make it constant.
```
theorem sourceCentral_scalar_field (θ : SourceCoordinate → ℝ) (hr : SourceRationalIndependent θ)
    {A : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
    (hA : A ∈ sourceAlgebra θ)
    (hcentral : ∀ B ∈ sourceAlgebra θ, A*B = B*A) :
    ∀ᵐ x ∂sourceBaseMeasure,
      sourceOperatorField A x = sourceCentralCoefficient A x • (1 : SourceFiberHilbert →L[ℂ] SourceFiberHilbert) := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceRationalIndependent, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceBaseMeasure, OAI.FiniteFactor.sourceOperatorField, OAI.FiniteFactor.sourceCentralCoefficient, OAI.FiniteFactor.SourceFiberHilbert
theorem OAI.FiniteFactor.sourceCentralCoefficient_rotation_invariant line 72
Source documentation
Covariance makes the actual scalar field invariant under every integer rotation. No ergodicity hypothesis or constant-value conclusion is inserted.
```
theorem sourceCentralCoefficient_rotation_invariant
    (θ : SourceCoordinate → ℝ) (hr : SourceRationalIndependent θ)
    {A : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
    (hA : A ∈ sourceAlgebra θ)
    (hcentral : ∀ B ∈ sourceAlgebra θ, A*B = B*A) :
    ∀ᵐ x ∂sourceBaseMeasure, ∀ n : ℤ,
      sourceCentralCoefficient A (coordinateRotate θ n x) = sourceCentralCoefficient A x := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceRationalIndependent, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceBaseMeasure, OAI.FiniteFactor.sourceCentralCoefficient, OAI.FiniteFactor.coordinateRotate