OAI/Analysis/IrrationalRotation/Sampling/StrictPhaseStability.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductPhases.threshold_fiber_countable line 12
2. theorem OAI.Invariant233.ProductPhases.ae_threshold_ne line 21
3. theorem OAI.Invariant233.ProductPhases.threshold_Ioo_ae_eq_Icc line 26
4. theorem OAI.Invariant233.ProductPhases.uniform_angle_strict_threshold_miss_le line 39
5. theorem OAI.Invariant233.ProductPhases.continuousAt_threshold_of_mem_Ioo line 58
6. theorem OAI.Invariant233.ProductPhases.eventually_threshold_mem_Ioo line 70
7. theorem OAI.Invariant233.ProductPhases.eventually_finite_phase_tests line 75