OAI/Combinatorics/MatchingCount/Algorithm/Guard.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatchingFPRAS.WeightedOptions.draw_law_pos line 9
2. theorem OAI.MatchingFPRAS.Enlargement.intact_partition_identity_even line 27
3. theorem OAI.MatchingFPRAS.Enlargement.frozenPortion_full_even line 59
4. theorem OAI.MatchingFPRAS.Enlargement.observableD_mean_even line 67
5. theorem OAI.MatchingFPRAS.Enlargement.observableD_zero_of_partition_zero line 77
6. lemma OAI.MatchingFPRAS.TableMarking.draw_law_pos line 102
7. lemma OAI.MatchingFPRAS.RationalSource.marking_law_eq line 129
8. theorem OAI.MatchingFPRAS.RationalSource.source_draw_support line 136
9. lemma OAI.MatchingFPRAS.GraphBridge.unpadded_partition line 152
10. def OAI.MatchingFPRAS.Trial.ScaleState.certificateActivity line 172
11. lemma OAI.MatchingFPRAS.Trial.ScaleState.certificateActivity_nonneg line 176
12. lemma OAI.MatchingFPRAS.Trial.ScaleState.certificateActivity_le line 184
13. lemma OAI.MatchingFPRAS.Trial.ScaleState.certificateActivity_partition line 193
14. theorem OAI.MatchingFPRAS.Trial.ScaleState.certificate_zero line 199
15. theorem OAI.MatchingFPRAS.Trial.ScaleState.certificate_mean_lower line 219
16. lemma OAI.MatchingFPRAS.Variation.mean_le_positive_event line 259
17. theorem OAI.MatchingFPRAS.RationalSource.fixedSampler_support line 288