OAI/Probability/MatroidProphet/Residual/Probability.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatroidProphet.bitsExpectation_contains line 12
2. lemma OAI.MatroidProphet.bitsExpectation_mul_const line 65
3. lemma OAI.MatroidProphet.bitsExpectation_contains_le_half_pow line 72
4. def OAI.MatroidProphet.residualBad line 79
5. def OAI.MatroidProphet.residualBadIndicator line 82
6. lemma OAI.MatroidProphet.residualBad_indicator_le line 86
7. lemma OAI.MatroidProphet.bitsExpectation_residualBad_le line 99