OAI/Analysis/FiniteFactor/OrbitSampling/CompactTorus.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FiniteFactor.SourceSamplingTorus line 12
2. instance OAI.FiniteFactor.sourceSamplingTorus_compact line 14
3. instance OAI.FiniteFactor.sourceSamplingTorus_borel line 16
4. def OAI.FiniteFactor.sourceSamplingTorusMap line 18
5. theorem OAI.FiniteFactor.sourceSamplingTorusMap_continuous line 21
6. def OAI.FiniteFactor.sourceSamplingUntrimmedTorus line 27
7. def OAI.FiniteFactor.sourceSamplingLambdaTorus line 31
8. theorem OAI.FiniteFactor.sourceSamplingUntrimmed_torus_event line 34