OAI/Analysis/IrrationalRotation/Sampling/LargePhaseAssembly.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductPhases.not_mem_largePhaseFailure_iff line 18
2. theorem OAI.Invariant233.ProductPhases.measure_largePhaseFailure_le line 29
3. theorem OAI.Invariant233.ProductPhases.iIndepSet_phaseMiss_infinitePi line 90
4. theorem OAI.Invariant233.ProductPhases.infinitePi_phaseMiss_eq line 107
5. theorem OAI.Invariant233.ProductPhases.ae_largePhaseCondition_of_miss_bounds line 120
6. theorem OAI.Invariant233.ProductPhases.uniformProduct_ae_largePhaseCondition line 155
7. theorem OAI.Invariant233.ProductPhases.exists_summable_independent_largePhases line 183
8. theorem OAI.Invariant233.ProductPhases.smallPhaseCondition_of_bounds line 196
9. theorem OAI.Invariant233.ProductPhases.uniformProduct_ae_phaseRanges line 206
10. theorem OAI.Invariant233.ProductPhases.exists_summable_independent_phaseRanges line 232