OAI/Combinatorics/RamseyFive/Entropy/HistoryCylinder.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.FiniteEntropy.eventMass_independent_product line 16
2. lemma OAI.SharpRamseyFive.FiniteEntropy.conditionOn_independent_product line 26
3. def OAI.SharpRamseyFive.FiniteEntropy.indexValueHistory line 40
4. lemma OAI.SharpRamseyFive.FiniteEntropy.history_rectangle line 44
5. theorem OAI.SharpRamseyFive.FiniteEntropy.history_factorization line 58
6. lemma OAI.SharpRamseyFive.FiniteEntropy.map_independent_pair line 72
7. def OAI.SharpRamseyFive.FiniteEntropy.uniformType line 94
8. lemma OAI.SharpRamseyFive.FiniteEntropy.uniformType_mass line 97
9. lemma OAI.SharpRamseyFive.FiniteEntropy.uniformType_event_pos line 101
10. lemma OAI.SharpRamseyFive.FiniteEntropy.conditionOn_uniformType line 107
11. lemma OAI.SharpRamseyFive.FiniteEntropy.map_uniformType line 119
12. lemma OAI.SharpRamseyFive.FiniteEntropy.map_uniformType_subtype line 127
13. instance OAI.SharpRamseyFive.PermutationCylinder.cylinderNonempty line 157
14. def OAI.SharpRamseyFive.PermutationCylinder.drawLaw line 160
15. lemma OAI.SharpRamseyFive.PermutationCylinder.drawLaw_available line 163
16. lemma OAI.SharpRamseyFive.PermutationCylinder.drawLaw_exposed line 169
17. theorem OAI.SharpRamseyFive.PermutationCylinder.drawLaw_exact line 182
18. lemma OAI.SharpRamseyFive.FiniteEntropy.map_uniformOn line 195
19. def OAI.SharpRamseyFive.PermutationCylinder.rankPrefix line 212
20. def OAI.SharpRamseyFive.PermutationCylinder.cylinderSet line 214
21. lemma OAI.SharpRamseyFive.PermutationCylinder.mem_cylinderSet line 217
22. lemma OAI.SharpRamseyFive.PermutationCylinder.cylinderSet_nonempty line 222
23. def OAI.SharpRamseyFive.PermutationCylinder.cylinderSetEquiv line 226
24. lemma OAI.SharpRamseyFive.PermutationCylinder.card_cylinderSet line 230
25. def OAI.SharpRamseyFive.PermutationCylinder.filterNextEquiv line 235
26. theorem OAI.SharpRamseyFive.PermutationCylinder.posterior_draw line 245