CentralDiagonal.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.sourceFirstMultiplier line 11
theorem OAI.FiniteFactor.sourceFirstMultiplier_distinct line 20
theorem OAI.FiniteFactor.sourceOperatorField_pi_action line 37
Source documentation
The field of pi(g) has its actual diagonal action on every vector.
```
theorem sourceOperatorField_pi_action (θ : SourceCoordinate → ℝ) (g : SourceBaseFunction) :
    ∀ᵐ x ∂sourceBaseMeasure, ∀ (v : SourceFiberHilbert) (k : ℤ),
      sourceOperatorField (sourcePi θ g) x v k = g.toFun (coordinateRotate θ k x) * v k := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceBaseFunction, OAI.FiniteFactor.sourceBaseMeasure, OAI.FiniteFactor.SourceFiberHilbert, OAI.FiniteFactor.sourceOperatorField, OAI.FiniteFactor.sourcePi, OAI.FiniteFactor.coordinateRotate

theorem OAI.FiniteFactor.sourceOperatorField_commute line 54

Source documentation

Commutation in the source algebra passes to the actual fields.

theorem sourceOperatorField_commute (θ : SourceCoordinate → ℝ)
    {A B : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
    (hA : A ∈ sourceAlgebra θ) (hB : B ∈ sourceAlgebra θ) (hAB : A*B = B*A) :
    ∀ᵐ x ∂sourceBaseMeasure, sourceOperatorField A x * sourceOperatorField B x =
      sourceOperatorField B x * sourceOperatorField A x := by
…

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

theorem OAI.FiniteFactor.fiber_commuting_diagonal_entry line 64

Source documentation

Distinct diagonal eigenvalues force every off-diagonal matrix coefficient of a commuting bounded operator to vanish.

theorem fiber_commuting_diagonal_entry
    (A G : SourceFiberHilbert →L[ℂ] SourceFiberHilbert) (d : ℤ → ℂ)
    (hG : ∀ v k, G v k = d k * v k) (hAG : A*G = G*A)
    (n k : ℤ) (hd : d n ≠ d k) : A (lp.single 2 n (1 : ℂ)) k = 0 := by
…

Mentions: OAI.FiniteFactor.SourceFiberHilbert

theorem OAI.FiniteFactor.sourceCentral_offDiagonal_zero line 84