OrbitNormalization.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceCocycle_orbit_ratio line 12
theorem OAI.FiniteFactor.sourceTorusRepresentative_rotate line 19
theorem OAI.FiniteFactor.fiber_rotated_invariant line 32
Source documentation
Covariance and invariance give the rotated range inclusion after removing the shift. This is an identity of bounded operators, not a range assumption.
```
theorem fiber_rotated_invariant
    (A B W : SourceFiberHilbert →L[ℂ] SourceFiberHilbert) (n : ℤ)
    (hc : fiberShift (-n) * A = B * fiberShift (-n))
    (hi : (1-A)*W*A = 0) :
    (1-B)*(fiberShift (-n)*W)*A = 0 := by
…
```
Mentions: OAI.FiniteFactor.SourceFiberHilbert, OAI.FiniteFactor.fiberShift

theorem OAI.FiniteFactor.sourceCappedRatio_orbit_diagonal line 47

Source documentation

On ordered actual orbit pairs, the capped diagonal is exactly the normalized weighted shift power.

theorem sourceCappedRatio_orbit_diagonal
    (θ : SourceCoordinate → ℝ) (z : SourceTorus) (n : ℕ)
    (hx : finiteFloorSupport θ (sourceTorusRepresentative z))
    (hord : ∀ i, sourceTorusRepresentative z i ≤
      sourceTorusRepresentative (sourceTorusRotate θ n z) i)
    (W : SourceFiberHilbert →L[ℂ] SourceFiberHilbert)
    (hW : ∀ (v : SourceFiberHilbert) (k : ℤ), W v k =
      (sourceCocycle θ sourceLogWeight n
        (coordinateRotate θ (k-(n : ℤ)) (sourceTorusRepresentative z)) : ℂ) * v (k-(n : ℤ))) :
    fiberDiagonal (sourceCappedRatio θ (z,sourceTorusRotate θ n z))
      (sourceCappedRatio_norm θ (z,sourceTorusRotate θ n z)) =
    (sourceCocycle θ sourceLogWeight n (sourceTorusRepresentative z) : ℂ)⁻¹ •
…

Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceTorus, OAI.FiniteFactor.finiteFloorSupport, OAI.FiniteFactor.sourceTorusRepresentative, OAI.FiniteFactor.sourceTorusRotate, OAI.FiniteFactor.SourceFiberHilbert, OAI.FiniteFactor.sourceCocycle, OAI.FiniteFactor.sourceLogWeight, OAI.FiniteFactor.coordinateRotate, OAI.FiniteFactor.fiberDiagonal, OAI.FiniteFactor.sourceCappedRatio, OAI.FiniteFactor.sourceCappedRatio_norm