OAI/Combinatorics/RamseyFive/Decoding/FreshValidation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.FiniteEntropy.eventMass_filter_mono line 10
2. lemma OAI.SharpRamseyFive.FiniteEntropy.eventMass_filter_union line 16
3. lemma OAI.SharpRamseyFive.FiniteEntropy.pair_success_mass line 24
4. def OAI.SharpRamseyFive.ReverseCap.rejected line 48
5. lemma OAI.SharpRamseyFive.ReverseCap.expected_rejected_card line 53
6. lemma OAI.SharpRamseyFive.ReverseCap.capture_partition line 67
7. def OAI.SharpRamseyFive.ReverseCap.validationRows line 79
8. theorem OAI.SharpRamseyFive.ReverseCap.validationRows_mass line 85