OAI/Probability/MatroidProphet/ExitNumerics.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatroidProphet.hazardBandBound line 9
2. def OAI.MatroidProphet.hazardTailPotential line 12
3. lemma OAI.MatroidProphet.hazardTailPotential_nonneg line 15
4. lemma OAI.MatroidProphet.hazardTailPotential_step line 21
5. lemma OAI.MatroidProphet.hazardBandBound_sum line 29
6. lemma OAI.MatroidProphet.hazardTailPotential_twelve line 40
7. theorem OAI.MatroidProphet.hazardBandBound_sum_lt_half line 48
8. theorem OAI.MatroidProphet.squared_exit_mass line 55
9. theorem OAI.MatroidProphet.exit_band_bound line 77
10. lemma OAI.MatroidProphet.hazardBandBound_eq_certificate_bound line 98