OAI/Probability/MatroidProphet/Maximum/Basic.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatroidProphet.Maximum.firstRule line 14
  2. lemma OAI.MatroidProphet.Maximum.firstRule_decision line 21
  3. lemma OAI.MatroidProphet.Maximum.firstRule_unique line 41
  4. lemma OAI.MatroidProphet.Maximum.firstRule_feasible line 56
  5. lemma OAI.MatroidProphet.Maximum.firstRule_single_qualifier line 75
  6. def OAI.MatroidProphet.Maximum.higher line 98
  7. def OAI.MatroidProphet.Maximum.threshold line 101
  8. def OAI.MatroidProphet.Maximum.maximumRule line 107
  9. lemma OAI.MatroidProphet.Maximum.maximumRule_feasible line 112
  10. lemma OAI.MatroidProphet.Maximum.higher_irrefl line 118
  11. lemma OAI.MatroidProphet.Maximum.higher_trans line 122
  12. lemma OAI.MatroidProphet.Maximum.higher_total line 131
  13. lemma OAI.MatroidProphet.Maximum.threshold_top_two line 143
  14. lemma OAI.MatroidProphet.Maximum.threshold_congr_samples line 167
  15. def OAI.MatroidProphet.Maximum.maximumHidden line 178
  16. lemma OAI.MatroidProphet.Maximum.maximumHidden_feasible line 183
  17. lemma OAI.MatroidProphet.Maximum.maximumHidden_single_qualifier line 200
  18. lemma OAI.MatroidProphet.Maximum.exists_top line 225
  19. lemma OAI.MatroidProphet.Maximum.threshold_only_positive line 253