OAI/Analysis/FiniteFactor/CrossedProduct/Rotation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceCircleRepresentative line 11
2. theorem OAI.FiniteFactor.sourceCircleRepresentative_measurable line 14
3. theorem OAI.FiniteFactor.sourceCircleRepresentative_coe line 17
4. theorem OAI.FiniteFactor.sourceCircle_mk_preserving line 25
5. theorem OAI.FiniteFactor.sourceCircleRepresentative_preserving line 30
6. theorem OAI.FiniteFactor.unitInterval_rotate_preserving line 42

   Source documentation

   Translation modulo one preserves the exact real representative measure.

   theorem unitInterval_rotate_preserving (a : ℝ) :
       MeasurePreserving (fun x : ℝ => Int.fract (x+a)) unitIntervalMeasure unitIntervalMeasure := by
   …

   Mentions: OAI.FiniteFactor.unitIntervalMeasure

7. theorem OAI.FiniteFactor.coordinateRotate_preserving line 53

   Source documentation

   All integer iterates of the countable source rotation preserve its actual infinite product measure. This is not an assumed action property.

   theorem coordinateRotate_preserving {ι : Type*} (θ : ι → ℝ) (k : ℤ) :
       MeasurePreserving (coordinateRotate θ k)
         (Measure.infinitePi (fun _ : ι => unitIntervalMeasure))
         (Measure.infinitePi (fun _ : ι => unitIntervalMeasure)) := by
   …

   Mentions: OAI.FiniteFactor.coordinateRotate, OAI.FiniteFactor.unitIntervalMeasure