OAI/Combinatorics/BalancedRyser/Probability/DriftUnionBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Balanced.measureReal_le_of_ae_imp line 15
2. theorem OAI.Balanced.upper_tail_of_accumulated_drift_bound line 19
3. theorem OAI.Balanced.lower_tail_of_accumulated_drift_bound line 34
4. theorem OAI.Balanced.abs_tail_of_accumulated_drift_bound line 50
5. theorem OAI.Balanced.simultaneous_upper_tail_of_drift_bound line 68
6. theorem OAI.Balanced.simultaneous_abs_tail_of_drift_bound line 99