OAI/Analysis/FiniteFactor/CrossedProduct/Transport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceTransportIndex line 10

   Source documentation

   Combined integer base rotation and fiber translation.

   def sourceTransportIndex (θ : SourceCoordinate → ℝ) (n m : ℤ)
       (z : (SourceCoordinate → ℝ) × ℤ) : (SourceCoordinate → ℝ) × ℤ :=
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate

2. theorem OAI.FiniteFactor.sourceTransportIndex_preserving line 14
3. def OAI.FiniteFactor.sourceTransport line 27
4. theorem OAI.FiniteFactor.sourceTransport_apply_ae line 32
5. theorem OAI.FiniteFactor.sourceTransport_mul line 38
6. theorem OAI.FiniteFactor.sourceHilbert_cube line 52
7. theorem OAI.FiniteFactor.sourceTransport_zero line 65
8. theorem OAI.FiniteFactor.sourceTransport_star line 78