OAI/Probability/MatroidProphet/GroupPayoff.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatroidProphet.MainAlgorithm.trueGroup_eq_candidate_filter line 12
2. def OAI.MatroidProphet.MainAlgorithm.higherTrueGroups line 20
3. lemma OAI.MatroidProphet.MainAlgorithm.trueZ_eq_listedRankStatistic line 24
4. lemma OAI.MatroidProphet.MainAlgorithm.mainMean_trueZ line 33
5. theorem OAI.MatroidProphet.MainAlgorithm.mainMean_trueZ_lower line 48
6. lemma OAI.MatroidProphet.MainAlgorithm.true_expected_nominal_to_final line 57
7. lemma OAI.MatroidProphet.MainAlgorithm.trueGroup_eq_of_H_eq line 108
8. lemma OAI.MatroidProphet.MainAlgorithm.higherTrueGroups_eq_of_H_eq line 113
9. lemma OAI.MatroidProphet.MainAlgorithm.mainMean_resample_test line 118
10. theorem OAI.MatroidProphet.MainAlgorithm.mainMean_nominal_to_final line 131
11. theorem OAI.MatroidProphet.MainAlgorithm.true_group_payoff line 158