OAI/Analysis/IrrationalRotation/Sampling/MixedRadixLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Invariant233.MixedRadix.digitLaw_isProbability line 15
2. theorem OAI.Invariant233.MixedRadix.measurable_prefix_sum line 20
3. theorem OAI.Invariant233.MixedRadix.tendsto_prefix_sum line 27
4. theorem OAI.Invariant233.MixedRadix.tendsto_quantized_prefix line 31
5. theorem OAI.Invariant233.MixedRadix.map_prefixRank_uniform line 49
6. theorem OAI.Invariant233.MixedRadix.prefix_sum_eq_normalized_rank line 66
7. theorem OAI.Invariant233.MixedRadix.map_prefix_sum_eq_quantized line 82
8. theorem OAI.Invariant233.MixedRadix.map_ofDigits_eq_volume line 110