OAI/Probability/MatroidProphet/Density/Guarded.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatroidProphet.densityEnabled line 9
  2. lemma OAI.MatroidProphet.densityEnabled_extensive line 13
  3. lemma OAI.MatroidProphet.densityEnabled_flat line 20
  4. lemma OAI.MatroidProphet.densityEnabled_mono line 27
  5. lemma OAI.MatroidProphet.densityEnabled_univ line 40
  6. def OAI.MatroidProphet.activation line 44
  7. def OAI.MatroidProphet.guardedPath line 46
  8. def OAI.MatroidProphet.nominalPath line 55
  9. lemma OAI.MatroidProphet.guardedPath_succ line 59
  10. lemma OAI.MatroidProphet.guardedPath_flat line 64
  11. lemma OAI.MatroidProphet.nominalPath_flat line 74
  12. lemma OAI.MatroidProphet.guardedPath_mono line 79
  13. lemma OAI.MatroidProphet.nominalPath_mono line 97
  14. lemma OAI.MatroidProphet.guarded_subset_nominal line 103
  15. lemma OAI.MatroidProphet.nominal_subset_guarded line 108
  16. lemma OAI.MatroidProphet.guarded_subset_next_nominal line 113
  17. lemma OAI.MatroidProphet.guardedPath_nonnegative line 121
  18. lemma OAI.MatroidProphet.nominalPath_nonnegative line 130
  19. lemma OAI.MatroidProphet.guardedPath_early line 135
  20. lemma OAI.MatroidProphet.nominalPath_early line 151
  21. lemma OAI.MatroidProphet.nominalPath_baseline line 159
  22. lemma OAI.MatroidProphet.nominalPath_baseline_gap line 167