OAI/Combinatorics/RamseyFive/Entropy/ConditionalSampling.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.FiniteEntropy.mean_by_fibers line 15
2. lemma OAI.SharpRamseyFive.FiniteEntropy.mean_comm line 25
3. def OAI.SharpRamseyFive.FiniteEntropy.coveredPositions line 35
4. lemma OAI.SharpRamseyFive.FiniteEntropy.mem_coveredPositions line 39
5. lemma OAI.SharpRamseyFive.FiniteEntropy.omitted_card_eq line 44
6. theorem OAI.SharpRamseyFive.FiniteEntropy.conditional_omissions line 52
7. theorem OAI.SharpRamseyFive.FiniteEntropy.conditional_extraction line 85
8. theorem OAI.SharpRamseyFive.FiniteEntropy.preRound_ready_omissions line 104