OAI/Combinatorics/SharpRamsey/Reciprocal/AuxiliaryLevels.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SharpLogRamsey.Selection.entropy_le_cross line 13
2. lemma OAI.SharpLogRamsey.Selection.geometric_subprob line 27
3. theorem OAI.SharpLogRamsey.Selection.integer_entropy line 36
4. def OAI.SharpLogRamsey.Selection.massLevel line 69
5. lemma OAI.SharpLogRamsey.Selection.massLevel_mean line 71
6. abbrev OAI.SharpLogRamsey.Selection.Levels line 84
7. def OAI.SharpLogRamsey.Selection.levelIndex line 86
8. lemma OAI.SharpLogRamsey.Selection.level_entropy line 89
9. lemma OAI.SharpLogRamsey.Selection.same_level_weight line 98
10. def OAI.SharpLogRamsey.Selection.Law.onEvent line 114
11. lemma OAI.SharpLogRamsey.Selection.Law.onEvent_mean line 121
12. theorem OAI.SharpLogRamsey.Selection.support_average line 127
13. theorem OAI.SharpLogRamsey.Selection.partition_entropy line 171
14. theorem OAI.SharpLogRamsey.Selection.partition_loss line 210
15. def OAI.SharpLogRamsey.Selection.levelSet line 225
16. lemma OAI.SharpLogRamsey.Selection.levelSet_mass line 228
17. lemma OAI.SharpLogRamsey.Selection.levelSet_charge line 238
18. lemma OAI.SharpLogRamsey.Selection.bad_level_charge line 251
19. lemma OAI.SharpLogRamsey.Selection.good_level_charge line 274
20. lemma OAI.SharpLogRamsey.Selection.Law.mass_ext line 284
21. lemma OAI.SharpLogRamsey.Selection.Law.map_comp line 290
22. lemma OAI.SharpLogRamsey.Selection.Law.map_prod_marginals line 294
23. lemma OAI.SharpLogRamsey.Selection.endpoint_levels_entropy line 304
24. def OAI.SharpLogRamsey.Selection.levelLoss line 312
25. lemma OAI.SharpLogRamsey.Selection.levelLoss_nonneg line 315
26. lemma OAI.SharpLogRamsey.Selection.levelLoss_size line 323
27. lemma OAI.SharpLogRamsey.Selection.level_bad_total line 335
28. def OAI.SharpLogRamsey.Selection.retainedLevels line 352
29. lemma OAI.SharpLogRamsey.Selection.retained_mass line 356
30. theorem OAI.SharpLogRamsey.Selection.auxiliary_supports line 403