OAI/Analysis/IrrationalRotation/Product/IndependentMissBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.measure_many_independent_events_le line 10
2. theorem OAI.Invariant233.measure_exists_many_independent_events_le line 49
3. theorem OAI.Invariant233.exists_many_misses_of_few_successes line 77
4. theorem OAI.Invariant233.measure_exists_few_successes_le line 92