OAI/Combinatorics/RamseyFive/Entropy/ProductHistory.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.FiniteEntropy.piRectangle line 13
2. lemma OAI.SharpRamseyFive.FiniteEntropy.eventMass_piRectangle line 16
3. lemma OAI.SharpRamseyFive.FiniteEntropy.conditionOn_piRectangle line 30
4. lemma OAI.SharpRamseyFive.FiniteEntropy.map_piLaw line 42
5. lemma OAI.SharpRamseyFive.FiniteEntropy.uniformType_pi line 55
6. theorem OAI.SharpRamseyFive.PermutationCylinder.blocks_posterior line 70
7. theorem OAI.SharpRamseyFive.PermutationCylinder.blocks_fresh_law line 84
8. lemma OAI.SharpRamseyFive.FiniteEntropy.piLaw_update_balance line 107
9. theorem OAI.SharpRamseyFive.FiniteEntropy.independent_selected_identity line 123