WeightedShiftField.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceMatrixEntry_sourceOperator_pow line 11
theorem OAI.FiniteFactor.sourceOperatorField_sourceOperator_pow line 31
Source documentation
The field of each power of the original quasinilpotent operator acts by its verified source cocycle, simultaneously on every l2 vector.
```
theorem sourceOperatorField_sourceOperator_pow (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ)
    (q : ℕ) :
    ∀ᵐ x ∂sourceBaseMeasure, ∀ (v : SourceFiberHilbert) (k : ℤ),
      (sourceOperatorField
        (sourceOperator θ sourceLogWeight hθ.nonneg sourceLogWeight_nonneg ^ q) x v) k =
        (sourceCocycle θ sourceLogWeight q (coordinateRotate θ (k - (q : ℤ)) x) : ℂ) *
          v (k - (q : ℤ)) := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.sourceBaseMeasure, OAI.FiniteFactor.SourceFiberHilbert, OAI.FiniteFactor.sourceOperatorField, OAI.FiniteFactor.sourceOperator, OAI.FiniteFactor.sourceLogWeight, OAI.FiniteFactor.sourceLogWeight_nonneg, OAI.FiniteFactor.sourceCocycle, OAI.FiniteFactor.coordinateRotate
theorem OAI.FiniteFactor.sourceOperatorField_covariance line 59
Source documentation
Covariance for the actual field's matrix, with all integer indices on one conull set. This is the coordinate form of conjugation by the fiber shift.
```
theorem sourceOperatorField_covariance (θ : SourceCoordinate → ℝ)
    {H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate}
    (hH : H ∈ sourceAlgebra θ) :
    ∀ᵐ x ∂sourceBaseMeasure, ∀ r n k : ℤ,
      (sourceOperatorField H (coordinateRotate θ r x) (lp.single 2 n (1 : ℂ))) k =
        (sourceOperatorField H x (lp.single 2 (n+r) (1 : ℂ))) (k+r) := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceAlgebra, OAI.FiniteFactor.sourceBaseMeasure, OAI.FiniteFactor.sourceOperatorField, OAI.FiniteFactor.coordinateRotate