OAI/Probability/MatroidProphet/CandidateFilter.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatroidProphet.MainAlgorithm.candidateSet line 11
  2. def OAI.MatroidProphet.MainAlgorithm.candidateLabels line 16
  3. lemma OAI.MatroidProphet.MainAlgorithm.candidateSet_eq_candidateLabels line 19
  4. lemma OAI.MatroidProphet.MainAlgorithm.candidate_congr_observed line 22
  5. lemma OAI.MatroidProphet.MainAlgorithm.candidateSet_eq_filter line 33
  6. lemma OAI.MatroidProphet.MainAlgorithm.sum_candidateLabels line 51
  7. def OAI.MatroidProphet.MainAlgorithm.positiveGreedy line 62
  8. lemma OAI.MatroidProphet.MainAlgorithm.positiveGreedy_indep line 66
  9. lemma OAI.MatroidProphet.MainAlgorithm.positiveGreedy_survivors_subset line 72
  10. lemma OAI.MatroidProphet.MainAlgorithm.sum_positiveGreedy line 83
  11. theorem OAI.MatroidProphet.MainAlgorithm.expectation_positiveGreedy_survivors line 93
  12. theorem OAI.MatroidProphet.MainAlgorithm.expectation_candidateLabels_le_optimum line 104
  13. lemma OAI.MatroidProphet.MainAlgorithm.candidate_observed_hidden line 122
  14. lemma OAI.MatroidProphet.MainAlgorithm.positiveGreedy_survivors_indep line 133
  15. lemma OAI.MatroidProphet.MainAlgorithm.candidate_not_mem_closure_empty line 138
  16. lemma OAI.MatroidProphet.MainAlgorithm.candidate_singleton_indep line 144