OAI/Probability/MatroidProphet/PathStatistics.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatroidProphet.lowerCompetition_congr_test_before line 12
  2. lemma OAI.MatroidProphet.lowerCompetition_ignore_focal line 22
  3. def OAI.MatroidProphet.testRankStatistic line 40
  4. def OAI.MatroidProphet.finalRankStatistic line 46
  5. theorem OAI.MatroidProphet.thinning_nominalRankStatistic line 52
  6. lemma OAI.MatroidProphet.unobservedBirthRegion_eq_nominalLayer line 69
  7. theorem OAI.MatroidProphet.testRankStatistic_le_final_cost line 95
  8. theorem OAI.MatroidProphet.thinning_finalRankStatistic line 123
  9. theorem OAI.MatroidProphet.expected_nominal_to_final line 141