OAI/Analysis/IrrationalRotation/Sampling/NonresonantPhaseTrials.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductPhases.infinitePi_ae_nonresonant line 10
2. theorem OAI.Invariant233.ProductPhases.exists_ae_requirement_outside_bad line 31
3. theorem OAI.Invariant233.ProductPhases.exists_nonresonant_strict_phase_block line 51
4. theorem OAI.Invariant233.ProductPhases.eventually_exists_nonresonant_strict_phase_block line 78