OAI/Computability/BinPacking/Information/SharedProfiles.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.sum_div_const line 16
2. abbrev OAI.BinPackingGames.Foundations.CorrelatedSampling.RectangleSeed line 20
3. def OAI.BinPackingGames.Foundations.CorrelatedSampling.rectangleWeight line 23
4. def OAI.BinPackingGames.Foundations.CorrelatedSampling.rectangleAccept line 27
5. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.rectangleWeight_nonnegative line 31
6. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.rectangleWeight_normalized line 35
7. def OAI.BinPackingGames.Foundations.CorrelatedSampling.rectangleDistribution line 46
8. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.rectangle_row_mass line 52
9. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.rectangle_acceptance_mass line 69
10. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.rectangle_label_mass line 79
11. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.min_mem_thresholds line 108
12. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.max_mem_thresholds line 112
13. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.rectangle_union_mass line 116
14. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.rectangle_common_label_mass line 128
15. def OAI.BinPackingGames.Foundations.CorrelatedSampling.localSample line 148
16. def OAI.BinPackingGames.Foundations.CorrelatedSampling.localDiagonal line 152
17. def OAI.BinPackingGames.Foundations.CorrelatedSampling.goodLabel line 157
18. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.common_first_label_lower line 161
19. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.finite_label_diagonal_bound line 190
20. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.rectangle_label_diagonal_bound line 204
21. def OAI.BinPackingGames.Foundations.CorrelatedSampling.profileThresholds line 240
22. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.mem_profileThresholds line 245
23. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.distribution_weight_le_one line 250
24. def OAI.BinPackingGames.Foundations.CorrelatedSampling.sharedProfileThresholds line 259
25. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.left_mem_sharedProfileThresholds line 263
26. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.right_mem_sharedProfileThresholds line 268
27. abbrev OAI.BinPackingGames.Foundations.CorrelatedSampling.SharedProfileSeed line 273
28. def OAI.BinPackingGames.Foundations.CorrelatedSampling.sharedProfileLeft line 277
29. def OAI.BinPackingGames.Foundations.CorrelatedSampling.sharedProfileRight line 281
30. def OAI.BinPackingGames.Foundations.CorrelatedSampling.sharedProfileReject line 285
31. def OAI.BinPackingGames.Foundations.CorrelatedSampling.uniformRejectionRate line 290
32. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.uniformRejectionRate_nonnegative line 293
33. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.uniformRejectionRate_lt_one line 302
34. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.sharedProfileReject_nonnegative line 310
35. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.sharedProfile_reject_le_rate line 316
36. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.nonnegative_powers_mono line 348
37. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.sharedProfile_label_diagonal_bound line 357
38. theorem OAI.BinPackingGames.Foundations.CorrelatedSampling.exists_uniformRejectionRate_pow_lt line 391