OAI/Analysis/IrrationalRotation/Sampling/MixedRadixHaarLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.MixedRadix.digitLaw_ae_nonterminal line 12
2. theorem OAI.Invariant233.MixedRadix.circleValue_measurePreserving_digitLaw line 17
3. theorem OAI.Invariant233.MixedRadix.map_circleValue_digitLaw line 22
4. theorem OAI.Invariant233.MixedRadix.ae_circleCanonical_circleValue line 27
5. theorem OAI.Invariant233.MixedRadix.map_circleCanonical_volume line 33
6. theorem OAI.Invariant233.MixedRadix.circleCanonical_measurePreserving line 41
7. theorem OAI.Invariant233.MixedRadix.digitLaw_circle_density_transport line 46
8. theorem OAI.Invariant233.MixedRadix.digitLaw_circle_density_transport_ae line 56
9. theorem OAI.Invariant233.MixedRadix.memLp_circleCanonical line 67