OAI/Computability/MinUncut/Games/Basic.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.CorrelatedSampling.firstAccepted line 8
2. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.first_union_common line 13
3. def OAI.MinUncutGames.Foundations.CorrelatedSampling.thresholdSample line 36
4. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.thresholdSample_agreement line 40
5. def OAI.MinUncutGames.Foundations.CorrelatedSampling.totalVariation line 59
6. def OAI.MinUncutGames.Foundations.CorrelatedSampling.overlapMass line 61
7. def OAI.MinUncutGames.Foundations.CorrelatedSampling.unionMass line 63
8. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.totalVariation_nonneg line 65
9. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.overlapMass_nonneg line 69
10. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.min_abs_identity line 73
11. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.max_abs_identity line 80
12. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.overlapMass_eq line 87
13. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.unionMass_eq line 95
14. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.totalVariation_le_one line 103
15. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.overlap_union_ratio line 110
16. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.overlap_union_ratio_lower_bound line 116
17. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.first_union_disagreement_upper_bound line 125
18. def OAI.MinUncutGames.Foundations.CorrelatedSampling.eventMass line 132
19. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.eventMass_nonneg line 135
20. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.eventMass_complement line 141
21. def OAI.MinUncutGames.Foundations.CorrelatedSampling.geometricMass line 153
22. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.geometricMass_nonneg line 157
23. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.geometricMass_identity line 163
24. def OAI.MinUncutGames.Foundations.CorrelatedSampling.firstHitWeight line 174
25. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.firstHitWeight_nonneg line 182
26. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.firstHitWeight_none line 196
27. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.firstHitWeight_some line 202
28. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.firstHitWeight_normalized line 212
29. def OAI.MinUncutGames.Foundations.CorrelatedSampling.goodFirstMass line 225
30. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.goodFirstMass_eq line 228
31. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.goodFirstMass_exact line 239
32. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.commonMass_le_acceptMass line 255
33. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.goodFirstMass_lower_bound line 262
34. def OAI.MinUncutGames.Foundations.CorrelatedSampling.traceAverage line 275
35. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.traceAverage_const line 279
36. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.traceAverage_mono line 285
37. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.traceAverage_sum line 297
38. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.firstAccepted_law line 309
39. def OAI.MinUncutGames.Foundations.CorrelatedSampling.goodFirstIndicator line 355
40. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.goodFirstIndicator_expansion line 360
41. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.goodFirstIndicator_law line 376
42. structure OAI.MinUncutGames.Foundations.CorrelatedSampling.ThresholdInterval line 390
43. def OAI.MinUncutGames.Foundations.CorrelatedSampling.splitPoint line 395
44. def OAI.MinUncutGames.Foundations.CorrelatedSampling.splitLeft line 397
45. def OAI.MinUncutGames.Foundations.CorrelatedSampling.splitRight line 400
46. def OAI.MinUncutGames.Foundations.CorrelatedSampling.cutAt line 403
47. def OAI.MinUncutGames.Foundations.CorrelatedSampling.intervalCDF line 405
48. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.split_cdf line 407
49. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.accepted_interval_mass line 412
50. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.splitLeft_cut line 420
51. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.splitRight_cut line 425
52. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.splitLeft_preserves_cut line 433
53. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.splitRight_preserves_cut line 439
54. def OAI.MinUncutGames.Foundations.CorrelatedSampling.splitAll line 445
55. def OAI.MinUncutGames.Foundations.CorrelatedSampling.unitThresholdInterval line 449
56. def OAI.MinUncutGames.Foundations.CorrelatedSampling.thresholdPartition line 451
57. def OAI.MinUncutGames.Foundations.CorrelatedSampling.sumOnIntervals line 455
58. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.sumOn_splitAll line 459
59. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.partition_sum line 469
60. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.partition_total_mass line 478
61. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.partition_cdf line 484
62. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.splitAll_new_cuts line 489
63. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.splitAll_preserves_cuts line 501
64. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.partition_cuts line 515
65. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.sumOnIntervals_congr line 525
66. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.partition_acceptance_mass line 535
67. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.sum_interval_get line 545
68. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.sum_div_const line 554
69. abbrev OAI.MinUncutGames.Foundations.CorrelatedSampling.RectangleSeed line 558
70. def OAI.MinUncutGames.Foundations.CorrelatedSampling.rectangleWeight line 561
71. def OAI.MinUncutGames.Foundations.CorrelatedSampling.rectangleAccept line 565
72. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.rectangleWeight_nonnegative line 569
73. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.rectangleWeight_normalized line 573
74. def OAI.MinUncutGames.Foundations.CorrelatedSampling.rectangleDistribution line 584
75. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.rectangle_row_mass line 590
76. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.rectangle_acceptance_mass line 607
77. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.rectangle_label_mass line 617
78. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.min_mem_thresholds line 646
79. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.max_mem_thresholds line 650
80. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.rectangle_union_mass line 654
81. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.rectangle_common_label_mass line 666