OAI/Probability/MatroidProphet/FiniteBits.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatroidProphet.bitsWeight line 17
  2. def OAI.MatroidProphet.bitsExpectation line 20
  3. lemma OAI.MatroidProphet.bitsWeight_nonneg line 24
  4. lemma OAI.MatroidProphet.bitsWeight_insert_no line 32
  5. lemma OAI.MatroidProphet.bitsWeight_insert_yes line 38
  6. lemma OAI.MatroidProphet.bitsExpectation_insert line 48
  7. lemma OAI.MatroidProphet.bitsExpectation_empty line 65
  8. lemma OAI.MatroidProphet.bitsExpectation_one line 69
  9. lemma OAI.MatroidProphet.bitsExpectation_mono line 78
  10. lemma OAI.MatroidProphet.bitsExpectation_congr line 85
  11. lemma OAI.MatroidProphet.bitsExpectation_add line 92
  12. lemma OAI.MatroidProphet.bitsExpectation_const line 97
  13. lemma OAI.MatroidProphet.bitsExpectation_nonneg line 103
  14. def OAI.MatroidProphet.bitsFailure line 110
  15. lemma OAI.MatroidProphet.bitsFailure_nonneg line 114
  16. lemma OAI.MatroidProphet.bitsFailure_le_one line 121
  17. lemma OAI.MatroidProphet.bitsFailure_forced_antitone line 129
  18. lemma OAI.MatroidProphet.bitsFailure_certifies line 140
  19. lemma OAI.MatroidProphet.bitsFailure_insert line 149
  20. lemma OAI.MatroidProphet.bitsFailure_split line 160
  21. lemma OAI.MatroidProphet.bitsFailure_antitone line 167