OAI/Combinatorics/BalancedRyser/Probability/FiniteExposureTower.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.ConditionalRestriction.uniformArrayModel line 16
2. theorem OAI.Balanced.ConditionalRestriction.filtered_integral_mul_le line 26
3. theorem OAI.Balanced.ConditionalRestriction.integral_eq_of_eq_on_support line 62