OAI/Analysis/FiniteFactor/CrossedProduct/TorusRotation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceTorusRotationStep line 10
2. theorem OAI.FiniteFactor.sourceTorusRotationStep_preserving line 13
3. theorem OAI.FiniteFactor.sourceCharacter_translate line 21
4. theorem OAI.FiniteFactor.sourceCharacter_nonresonant line 28

   Source documentation

   Rational independence rules out every nonconstant character eigenvalue 1.

   theorem sourceCharacter_nonresonant (θ : SourceCoordinate → ℝ)
       (hr : SourceRationalIndependent θ) (v : SourceCoordinate →₀ ℤ) (hv : v ≠ 0) :
       sourceCharacter v (sourceTorusQuotient θ) ≠ 1 := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceRationalIndependent, OAI.FiniteFactor.sourceCharacter, OAI.FiniteFactor.sourceTorusQuotient

5. theorem OAI.FiniteFactor.sourceCharacterL2_rotation line 49