OAI/Analysis/FiniteFactor/CrossedProduct/FreeRotation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteFactor.sourceFirstCoordinate line 11
  2. theorem OAI.FiniteFactor.SourceRationalIndependent.mul_ne_integer line 14
  3. theorem OAI.FiniteFactor.SourceRationalIndependent.rotation_free line 24

    Source documentation

    Every nonzero integer rotation has no fixed point, using one source coordinate. This is pointwise freeness, not merely an almost-everywhere claim.

    theorem SourceRationalIndependent.rotation_free {θ : SourceCoordinate → ℝ}
    (hθ : SourceRationalIndependent θ) (k : ℤ) (hk : k ≠ 0) (x : SourceCoordinate → ℝ) :
    coordinateRotate θ k x ≠ x := by
…

    Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceRationalIndependent, OAI.FiniteFactor.coordinateRotate

  4. theorem OAI.FiniteFactor.exists_source_free_base line 36