OAI/Probability/MatroidSecretary/Density/Comparison.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatroidProphet.DensityComparison.unionExpansion line 13
2. theorem OAI.MatroidProphet.DensityComparison.unionExpansion_eq line 17
3. def OAI.MatroidProphet.DensityComparison.guardedBirth line 30
4. theorem OAI.MatroidProphet.DensityComparison.guardedBirth_eq line 36
5. lemma OAI.MatroidProphet.densityExpansion_eq_chosen line 45
6. lemma OAI.MatroidProphet.nominalBirth_eq_find line 50