OAI/Combinatorics/BalancedRyser/Probability/BoundedDriftCore.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Balanced.condExp_exp_le_of_abs_le line 17
2. lemma OAI.Balanced.subGaussian_add_of_bounded_difference line 57
3. lemma OAI.Balanced.subGaussian_sum_of_bounded_differences line 108
4. lemma OAI.Balanced.measure_abs_ge_le_of_subGaussian line 131