OAI/Analysis/IrrationalRotation/Sampling/MixedRadixNonterminal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.infinitePi_eventually_mem_null line 14
2. theorem OAI.Invariant233.MixedRadix.uniformDigit_singleton line 50
3. theorem OAI.Invariant233.MixedRadix.ae_nonterminal_uniformDigits line 54
4. theorem OAI.Invariant233.MixedRadix.ae_nonterminal_of_absolutelyContinuous line 75
5. theorem OAI.Invariant233.MixedRadix.ae_floor_coordinate_recovers_digit line 82
6. theorem OAI.Invariant233.MixedRadix.ae_ofDigits_mem_Ico line 89