OAI/Analysis/IrrationalRotation/Sampling/StrictPhaseTrials.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductPhases.strictPhaseGoodCount_ae_eq line 12
2. theorem OAI.Invariant233.ProductPhases.strictLargePhaseFailure_ae_eq line 34
3. theorem OAI.Invariant233.ProductPhases.not_mem_strictLargePhaseFailure_iff line 59
4. theorem OAI.Invariant233.ProductPhases.uniformProduct_measure_strictLargePhaseFailure_le line 70
5. theorem OAI.Invariant233.ProductPhases.intervalProduct_ae_strict_bounds line 99
6. theorem OAI.Invariant233.ProductPhases.exists_strict_phase_block line 124
7. theorem OAI.Invariant233.ProductPhases.eventually_strictLargePhaseCondition line 163
8. theorem OAI.Invariant233.ProductPhases.isOpen_strictLargePhaseCondition line 188
9. theorem OAI.Invariant233.ProductPhases.eventually_exists_strict_phase_block line 195