OAI/MathematicalPhysics/CriticalSK/GaussianConcentration.lean

GitHub source file

170 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CriticalSK.(instance at line 42) line 42
2. lemma OAI.CriticalSK.chiSquare_mgf line 46
3. lemma OAI.CriticalSK.chiSquare_exp_integrable line 55
4. lemma OAI.CriticalSK.chiSquare_mgf_exp line 61
5. lemma OAI.CriticalSK.chiSquare_chernoff_value line 71
6. lemma OAI.CriticalSK.chiSquare_upper_tail line 83
7. lemma OAI.CriticalSK.chiSquare_lower_tail line 95
8. lemma OAI.CriticalSK.chi_entropy_lower line 106
9. lemma OAI.CriticalSK.chiSquare_nonneg line 112
10. lemma OAI.CriticalSK.chiSquare_eq_zero_iff line 115
11. lemma OAI.CriticalSK.chiSquare_zero_measure line 126
12. lemma OAI.CriticalSK.chi_radius_algebra line 133
13. lemma OAI.CriticalSK.chi_upper_tail line 145
14. lemma OAI.CriticalSK.chi_lower_tail line 175
15. lemma OAI.CriticalSK.chi_tail line 218
16. def OAI.CriticalSK.chi line 233
17. lemma OAI.CriticalSK.chi_measurable line 235
18. lemma OAI.CriticalSK.chi_sq line 239
19. lemma OAI.CriticalSK.chiSquare_integrable line 242
20. lemma OAI.CriticalSK.chi_integrable line 247
21. lemma OAI.CriticalSK.chi_memLp_two line 254
22. lemma OAI.CriticalSK.chi_center_integrable_sq line 258
23. lemma OAI.CriticalSK.chi_mean_square_error line 263
24. lemma OAI.CriticalSK.gaussian_integral_square line 287
25. lemma OAI.CriticalSK.chiSquare_mean line 292
26. lemma OAI.CriticalSK.chi_mean_nonneg line 308
27. lemma OAI.CriticalSK.chi_mean_upper line 311
28. lemma OAI.CriticalSK.chi_mean_bias line 317
29. lemma OAI.CriticalSK.chi_square_deviation_tail line 337
30. lemma OAI.CriticalSK.chi_square_deviation_exp_integrable line 348
31. lemma OAI.CriticalSK.chi_square_deviation_exp_bound line 366
32. lemma OAI.CriticalSK.exp_quadratic_remainder line 420
33. lemma OAI.CriticalSK.exp_quadratic_domination line 430
34. lemma OAI.CriticalSK.one_add_linear_mul_exp_le line 451
35. lemma OAI.CriticalSK.centered_mgf_from_exp_square line 463
36. lemma OAI.CriticalSK.integrable_exp_of_exp_square line 490
37. lemma OAI.CriticalSK.chi_bias_le_two line 502
38. lemma OAI.CriticalSK.chi_center_square_exp_pointwise line 511
39. lemma OAI.CriticalSK.chi_center_square_exp_integrable line 523
40. lemma OAI.CriticalSK.chi_center_square_exp_bound line 534
41. theorem OAI.CriticalSK.chi_centered_subGaussian line 550
42. def OAI.CriticalSK.chiRowDim line 570
43. abbrev OAI.CriticalSK.ChiRows line 572
44. def OAI.CriticalSK.chiRowLaw line 574
45. instance OAI.CriticalSK.(instance at line 577) line 577
46. def OAI.CriticalSK.centeredChiRow line 581
47. lemma OAI.CriticalSK.centeredChiRow_measurable line 584
48. lemma OAI.CriticalSK.centeredChiRows_independent line 587
49. lemma OAI.CriticalSK.centeredChiRow_subGaussian line 590
50. lemma OAI.CriticalSK.centeredChiRow_mean line 603
51. def OAI.CriticalSK.scaledChiRow line 616
52. lemma OAI.CriticalSK.scaledChiRow_subGaussian line 619
53. lemma OAI.CriticalSK.scaledChiRows_independent line 634
54. lemma OAI.CriticalSK.scaledChiRow_measurable line 638
55. lemma OAI.CriticalSK.scaledChiRow_mean line 641
56. def OAI.CriticalSK.diagonalMarginal line 645
57. instance OAI.CriticalSK.(instance at line 648) line 648
58. def OAI.CriticalSK.diagonalLaw line 651
59. instance OAI.CriticalSK.(instance at line 654) line 654
60. lemma OAI.CriticalSK.gaussian_id_subGaussian line 658
61. lemma OAI.CriticalSK.diagonalRows_subGaussian line 663
62. lemma OAI.CriticalSK.diagonalRows_independent line 672
63. lemma OAI.CriticalSK.diagonalRows_mean line 676
64. lemma OAI.CriticalSK.independent_product_submartingale line 686
65. lemma OAI.CriticalSK.exp_partial_sum_submartingale line 721
66. lemma OAI.CriticalSK.partial_sum_maximal_exponential line 754
67. lemma OAI.CriticalSK.partial_sum_maximal_tail line 794
68. lemma OAI.CriticalSK.partial_sum_abs_maximal_tail line 810
69. lemma OAI.CriticalSK.block_prefix_tail line 834
70. def OAI.CriticalSK.blockThreshold line 845
71. lemma OAI.CriticalSK.blockThreshold_sq line 848
72. lemma OAI.CriticalSK.block_prefix_dyadic_tail line 854
73. lemma OAI.CriticalSK.geometric_half_sum_le_two line 874
74. lemma OAI.CriticalSK.finite_scale_shell_union_bound line 883
75. def OAI.CriticalSK.blockShell line 926
76. lemma OAI.CriticalSK.blockShell_card line 930
77. lemma OAI.CriticalSK.blockShell_covers line 949
78. lemma OAI.CriticalSK.blockShell_lower line 966
79. def OAI.CriticalSK.multiscaleBad line 971
80. lemma OAI.CriticalSK.multiscaleBad_measurable line 977
81. lemma OAI.CriticalSK.multiscaleBad_probability line 999
82. lemma OAI.CriticalSK.good_multiscale_prefix line 1013
83. lemma OAI.CriticalSK.good_multiscale_prefix_all line 1027
84. lemma OAI.CriticalSK.block_summation_by_parts line 1039
85. lemma OAI.CriticalSK.block_zero_sum_bound line 1050
86. lemma OAI.CriticalSK.block_prefix_weight_bound line 1069
87. instance OAI.CriticalSK.(instance at line 1114) line 1114
88. instance OAI.CriticalSK.(instance at line 1118) line 1118
89. instance OAI.CriticalSK.(instance at line 1122) line 1122
90. instance OAI.CriticalSK.(instance at line 1125) line 1125
91. instance OAI.CriticalSK.(instance at line 1129) line 1129
92. instance OAI.CriticalSK.(instance at line 1133) line 1133
93. instance OAI.CriticalSK.(instance at line 1137) line 1137
94. instance OAI.CriticalSK.(instance at line 1140) line 1140
95. instance OAI.CriticalSK.(instance at line 1144) line 1144
96. instance OAI.CriticalSK.(instance at line 1148) line 1148
97. instance OAI.CriticalSK.(instance at line 1152) line 1152
98. instance OAI.CriticalSK.(instance at line 1155) line 1155
99. instance OAI.CriticalSK.(instance at line 1159) line 1159
100. instance OAI.CriticalSK.(instance at line 1163) line 1163
101. instance OAI.CriticalSK.(instance at line 1167) line 1167
102. instance OAI.CriticalSK.(instance at line 1170) line 1170
103. instance OAI.CriticalSK.(instance at line 1174) line 1174
104. instance OAI.CriticalSK.(instance at line 1178) line 1178
105. instance OAI.CriticalSK.(instance at line 1182) line 1182
106. instance OAI.CriticalSK.(instance at line 1185) line 1185
107. instance OAI.CriticalSK.(instance at line 1189) line 1189
108. instance OAI.CriticalSK.(instance at line 1193) line 1193
109. instance OAI.CriticalSK.(instance at line 1197) line 1197
110. instance OAI.CriticalSK.(instance at line 1200) line 1200
111. instance OAI.CriticalSK.(instance at line 1204) line 1204
112. instance OAI.CriticalSK.(instance at line 1208) line 1208
113. instance OAI.CriticalSK.(instance at line 1212) line 1212
114. instance OAI.CriticalSK.(instance at line 1215) line 1215
115. instance OAI.CriticalSK.(instance at line 1219) line 1219
116. instance OAI.CriticalSK.(instance at line 1223) line 1223
117. instance OAI.CriticalSK.(instance at line 1227) line 1227
118. instance OAI.CriticalSK.(instance at line 1230) line 1230
119. instance OAI.CriticalSK.(instance at line 1234) line 1234
120. instance OAI.CriticalSK.(instance at line 1238) line 1238
121. instance OAI.CriticalSK.(instance at line 1242) line 1242
122. instance OAI.CriticalSK.(instance at line 1245) line 1245
123. instance OAI.CriticalSK.(instance at line 1249) line 1249
124. instance OAI.CriticalSK.(instance at line 1253) line 1253
125. instance OAI.CriticalSK.(instance at line 1257) line 1257
126. instance OAI.CriticalSK.(instance at line 1260) line 1260
127. instance OAI.CriticalSK.(instance at line 1264) line 1264
128. instance OAI.CriticalSK.(instance at line 1268) line 1268
129. instance OAI.CriticalSK.(instance at line 1272) line 1272
130. instance OAI.CriticalSK.(instance at line 1275) line 1275
131. instance OAI.CriticalSK.(instance at line 1279) line 1279
132. instance OAI.CriticalSK.(instance at line 1283) line 1283
133. instance OAI.CriticalSK.(instance at line 1287) line 1287
134. instance OAI.CriticalSK.(instance at line 1290) line 1290
135. instance OAI.CriticalSK.(instance at line 1294) line 1294
136. instance OAI.CriticalSK.(instance at line 1298) line 1298
137. instance OAI.CriticalSK.(instance at line 1302) line 1302
138. instance OAI.CriticalSK.(instance at line 1305) line 1305
139. instance OAI.CriticalSK.(instance at line 1309) line 1309
140. instance OAI.CriticalSK.(instance at line 1313) line 1313
141. instance OAI.CriticalSK.(instance at line 1317) line 1317
142. instance OAI.CriticalSK.(instance at line 1320) line 1320
143. instance OAI.CriticalSK.(instance at line 1324) line 1324
144. instance OAI.CriticalSK.(instance at line 1328) line 1328
145. instance OAI.CriticalSK.(instance at line 1332) line 1332
146. instance OAI.CriticalSK.(instance at line 1335) line 1335
147. instance OAI.CriticalSK.(instance at line 1339) line 1339
148. instance OAI.CriticalSK.(instance at line 1343) line 1343
149. instance OAI.CriticalSK.(instance at line 1347) line 1347
150. instance OAI.CriticalSK.(instance at line 1350) line 1350
151. instance OAI.CriticalSK.(instance at line 1354) line 1354
152. instance OAI.CriticalSK.(instance at line 1358) line 1358
153. instance OAI.CriticalSK.(instance at line 1362) line 1362
154. instance OAI.CriticalSK.(instance at line 1365) line 1365
155. instance OAI.CriticalSK.(instance at line 1369) line 1369
156. instance OAI.CriticalSK.(instance at line 1373) line 1373
157. instance OAI.CriticalSK.(instance at line 1377) line 1377
158. instance OAI.CriticalSK.(instance at line 1380) line 1380
159. instance OAI.CriticalSK.(instance at line 1384) line 1384
160. instance OAI.CriticalSK.(instance at line 1388) line 1388
161. instance OAI.CriticalSK.(instance at line 1392) line 1392
162. instance OAI.CriticalSK.(instance at line 1395) line 1395
163. instance OAI.CriticalSK.(instance at line 1399) line 1399
164. instance OAI.CriticalSK.(instance at line 1403) line 1403
165. instance OAI.CriticalSK.(instance at line 1407) line 1407
166. instance OAI.CriticalSK.(instance at line 1410) line 1410
167. instance OAI.CriticalSK.(instance at line 1414) line 1414
168. instance OAI.CriticalSK.(instance at line 1418) line 1418
169. instance OAI.CriticalSK.(instance at line 1422) line 1422
170. instance OAI.CriticalSK.(instance at line 1425) line 1425