OAI/Probability/MatroidProphet/Residual/Tail.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatroidProphet.residualDelta_nonneg line 9
2. lemma OAI.MatroidProphet.bitsExpectation_residualBad_delta line 11
3. lemma OAI.MatroidProphet.capturedResidual_le line 26
4. lemma OAI.MatroidProphet.tripleMask_residual_error_le line 43