OAI/Combinatorics/BalancedRyser/Selection/CensoredDrift.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Balanced.abs_condExp_sub_le_indicatorline 18 - theorem
OAI.Balanced.abs_condExp_sub_le_of_censor_probabilityline 39 - theorem
OAI.Balanced.abs_condExp_censored_sub_leline 50 - theorem
OAI.Balanced.condExp_censored_le_addline 63