Covariance.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceCommutantRotation_basis line 9
theorem OAI.FiniteFactor.sourceMatrixEntry_covariance line 23
Source documentation
Matrix form of H(sigma^r x) = S^(-r) H(x) S^r, for the original regular representation and every integer power of the base rotation.
```
theorem sourceMatrixEntry_covariance (θ : SourceCoordinate → ℝ)
    {H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
    (hH : H ∈ sourceAlgebra θ) (r n : ℤ) :
    ∀ᵐ x ∂sourceBaseMeasure, ∀ k : ℤ,
      sourceMatrixEntry H k n (coordinateRotate θ r x) =
        sourceMatrixEntry H (k+r) (n+r) x := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceBaseMeasure, OAI.FiniteFactor.sourceMatrixEntry, OAI.FiniteFactor.coordinateRotate
theorem OAI.FiniteFactor.sourceMatrixEntry_covariance_all line 42
Source documentation
All countably many covariance identities hold on one conull base set.
```
theorem sourceMatrixEntry_covariance_all (θ : SourceCoordinate → ℝ)
    {H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
    (hH : H ∈ sourceAlgebra θ) :
    ∀ᵐ x ∂sourceBaseMeasure, ∀ r n k : ℤ,
      sourceMatrixEntry H k n (coordinateRotate θ r x) =
        sourceMatrixEntry H (k+r) (n+r) x := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceBaseMeasure, OAI.FiniteFactor.sourceMatrixEntry, OAI.FiniteFactor.coordinateRotate
theorem OAI.FiniteFactor.sourceMatrixEntry_pi line 54
Source documentation
Matrix entries of the actual multiplication generators.
```
theorem sourceMatrixEntry_pi (θ : SourceCoordinate → ℝ) (g : SourceBaseFunction) (n : ℤ) :
    ∀ᵐ x ∂sourceBaseMeasure, ∀ k : ℤ,
      sourceMatrixEntry (sourcePi θ g) k n x =
        if k = n then g.toFun (coordinateRotate θ n x) else 0 := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceBaseFunction, OAI.FiniteFactor.sourceBaseMeasure, OAI.FiniteFactor.sourceMatrixEntry, OAI.FiniteFactor.sourcePi, OAI.FiniteFactor.coordinateRotate
theorem OAI.FiniteFactor.sourceMatrixEntry_shift line 65
Source documentation
Matrix entries of the original fiber shift.
```
theorem sourceMatrixEntry_shift (n : ℤ) :
    ∀ᵐ x ∂sourceBaseMeasure, ∀ k : ℤ,
      sourceMatrixEntry (sourceShift SourceCoordinate) k n x =
        if k = n+1 then 1 else 0 := by
…
```
Mentions: OAI.FiniteFactor.sourceBaseMeasure, OAI.FiniteFactor.sourceMatrixEntry, OAI.FiniteFactor.sourceShift, OAI.FiniteFactor.SourceCoordinate