OAI/Computability/DirectedFeedback/Probability/TraceLaw.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DFVSGames.Foundations.CorrelatedSampling.traceAverage line 13
2. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.traceAverage_const line 17
3. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.traceAverage_mono line 23
4. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.traceAverage_sum line 35
5. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.firstAccepted_law line 47
6. def OAI.DFVSGames.Foundations.CorrelatedSampling.goodFirstIndicator line 93
7. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.goodFirstIndicator_expansion line 98
8. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.goodFirstIndicator_law line 114
9. structure OAI.DFVSGames.Foundations.CorrelatedSampling.ThresholdInterval line 133
10. def OAI.DFVSGames.Foundations.CorrelatedSampling.splitPoint line 138
11. def OAI.DFVSGames.Foundations.CorrelatedSampling.splitLeft line 140
12. def OAI.DFVSGames.Foundations.CorrelatedSampling.splitRight line 143
13. def OAI.DFVSGames.Foundations.CorrelatedSampling.cutAt line 146
14. def OAI.DFVSGames.Foundations.CorrelatedSampling.intervalCDF line 148
15. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.split_cdf line 150
16. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.accepted_interval_mass line 155
17. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.splitLeft_cut line 163
18. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.splitRight_cut line 168
19. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.splitLeft_preserves_cut line 176
20. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.splitRight_preserves_cut line 182
21. def OAI.DFVSGames.Foundations.CorrelatedSampling.splitAll line 188
22. def OAI.DFVSGames.Foundations.CorrelatedSampling.unitThresholdInterval line 192
23. def OAI.DFVSGames.Foundations.CorrelatedSampling.thresholdPartition line 194
24. def OAI.DFVSGames.Foundations.CorrelatedSampling.sumOnIntervals line 198
25. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.sumOn_splitAll line 202
26. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.partition_sum line 212
27. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.partition_total_mass line 221
28. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.partition_cdf line 227
29. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.splitAll_new_cuts line 232
30. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.splitAll_preserves_cuts line 244
31. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.partition_cuts line 258
32. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.sumOnIntervals_congr line 268
33. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.partition_acceptance_mass line 278
34. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.sum_interval_get line 288
35. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.sum_div_const_inline_Rectangle line 298
36. abbrev OAI.DFVSGames.Foundations.CorrelatedSampling.RectangleSeed line 302
37. def OAI.DFVSGames.Foundations.CorrelatedSampling.rectangleWeight line 305
38. def OAI.DFVSGames.Foundations.CorrelatedSampling.rectangleAccept line 309
39. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.rectangleWeight_nonnegative line 313
40. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.rectangleWeight_normalized line 317
41. def OAI.DFVSGames.Foundations.CorrelatedSampling.rectangleDistribution line 328
42. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.rectangle_row_mass line 334
43. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.rectangle_acceptance_mass line 351
44. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.rectangle_label_mass line 361
45. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.min_mem_thresholds line 390
46. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.max_mem_thresholds line 394
47. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.rectangle_union_mass line 398
48. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.rectangle_common_label_mass line 410
49. def OAI.DFVSGames.Foundations.CorrelatedSampling.localSample line 431
50. def OAI.DFVSGames.Foundations.CorrelatedSampling.localDiagonal line 435
51. def OAI.DFVSGames.Foundations.CorrelatedSampling.goodLabel line 440
52. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.common_first_label_lower line 444
53. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.finite_label_diagonal_bound line 473
54. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.rectangle_label_diagonal_bound line 488
55. def OAI.DFVSGames.Foundations.CorrelatedSampling.profileThresholds line 528
56. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.mem_profileThresholds line 533
57. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.distribution_weight_le_one line 538
58. def OAI.DFVSGames.Foundations.CorrelatedSampling.sharedProfileThresholds line 547
59. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.left_mem_sharedProfileThresholds line 551
60. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.right_mem_sharedProfileThresholds line 556
61. abbrev OAI.DFVSGames.Foundations.CorrelatedSampling.SharedProfileSeed line 561
62. def OAI.DFVSGames.Foundations.CorrelatedSampling.sharedProfileLeft line 565
63. def OAI.DFVSGames.Foundations.CorrelatedSampling.sharedProfileRight line 569
64. def OAI.DFVSGames.Foundations.CorrelatedSampling.sharedProfileReject line 573
65. def OAI.DFVSGames.Foundations.CorrelatedSampling.uniformRejectionRate line 578
66. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.uniformRejectionRate_nonnegative line 581
67. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.uniformRejectionRate_lt_one line 590
68. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.sharedProfileReject_nonnegative line 598
69. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.sharedProfile_reject_le_rate line 604
70. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.nonnegative_powers_mono_inline_SharedProfiles line 636
71. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.sharedProfile_label_diagonal_bound line 645
72. theorem OAI.DFVSGames.Foundations.CorrelatedSampling.exists_uniformRejectionRate_pow_lt line 679
73. def OAI.DFVSGames.Foundations.Information.IsProbability line 696
74. def OAI.DFVSGames.Foundations.Information.SupportedBy line 699
75. def OAI.DFVSGames.Foundations.Information.relativeEntropy line 701
76. def OAI.DFVSGames.Foundations.Information.totalVariation line 704
77. def OAI.DFVSGames.Foundations.Information.posterior line 707
78. theorem OAI.DFVSGames.Foundations.Information.posterior_isProbability line 710
79. theorem OAI.DFVSGames.Foundations.Information.posterior_supportedBy line 720
80. theorem OAI.DFVSGames.Foundations.Information.mul_log_div_ge_sub line 725
81. theorem OAI.DFVSGames.Foundations.Information.relativeEntropy_nonneg line 733
82. theorem OAI.DFVSGames.Foundations.Information.posterior_relativeEntropy_le line 745
83. theorem OAI.DFVSGames.Foundations.Information.totalVariation_nonneg line 769
84. theorem OAI.DFVSGames.Foundations.Information.totalVariation_symm line 772
85. theorem OAI.DFVSGames.Foundations.Information.totalVariation_le_one line 775
86. theorem OAI.DFVSGames.Foundations.Information.le_binaryLog_of_le_log line 786
87. theorem OAI.DFVSGames.Foundations.Information.weighted_sum_sq_le line 796