OAI/Analysis/IrrationalRotation/Couplings/CircleCouplingOrder.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Invariant233.UniformQuantization.quantize_mono_on_unit line 12
2. lemma OAI.Invariant233.UniformQuantization.quantize_val_eq_floor line 24
3. lemma OAI.Invariant233.CircleDigitCoupling.rawLaw_ae_ordered line 36
4. lemma OAI.Invariant233.CircleCoupling.coordinateLaw_ae_ordered line 51
5. lemma OAI.Invariant233.CircleCoupling.coordinateLaw_ae_endpoint_unit line 66
6. lemma OAI.Invariant233.CircleCoupling.ae_digits_ordered line 87
7. lemma OAI.Invariant233.CircleCoupling.ae_coordinates_ordered line 101
8. lemma OAI.Invariant233.CircleCoupling.ae_raw_endpoints_unit line 111
9. lemma OAI.Invariant233.CircleCoupling.ae_coordinate_raw_error line 119