OAI/Analysis/IrrationalRotation/Couplings/MixedRadixHybridLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.HybridLaw.tendsto_finiteMeasure_map_of_ae_tendsto line 15
2. theorem OAI.Invariant233.MixedRadix.measurable_hybrid line 41
3. theorem OAI.Invariant233.MixedRadix.tendsto_circleValue_hybrid line 49
4. theorem OAI.Invariant233.MixedRadix.tendsto_circle_hybrid_pair_law line 55
5. theorem OAI.Invariant233.MixedRadix.circleValue_hybrid_eq_add_int_div line 69
6. theorem OAI.Invariant233.MixedRadix.ae_circle_hybrid_pair_graph line 80
7. theorem OAI.Invariant233.MixedRadix.ae_relation_circle_hybrid_pair_law line 99