OAI/Dynamics/MultipleMixing/Arrays.lean

GitHub source file

276 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Rokhlin.ArrayObjects.StandardSpace line 17
2. instance OAI.Rokhlin.ArrayObjects.(instance at line 23) line 23
3. instance OAI.Rokhlin.ArrayObjects.(instance at line 24) line 24
4. instance OAI.Rokhlin.ArrayObjects.(instance at line 25) line 25
5. instance OAI.Rokhlin.ArrayObjects.(instance at line 26) line 26
6. abbrev OAI.Rokhlin.ArrayObjects.Index line 28
7. abbrev OAI.Rokhlin.ArrayObjects.Arr line 29
8. def OAI.Rokhlin.ArrayObjects.amap line 31
9. def OAI.Rokhlin.ArrayObjects.plane line 34
10. def OAI.Rokhlin.ArrayObjects.planes line 37
11. def OAI.Rokhlin.ArrayObjects.zeroEquiv line 41
12. lemma OAI.Rokhlin.ArrayObjects.measurable_amap line 49
13. lemma OAI.Rokhlin.ArrayObjects.measurable_plane line 54
14. lemma OAI.Rokhlin.ArrayObjects.measurable_planes line 58
15. lemma OAI.Rokhlin.ArrayObjects.amap_id line 62
16. lemma OAI.Rokhlin.ArrayObjects.amap_comp line 63
17. lemma OAI.Rokhlin.ArrayObjects.plane_amap line 65
18. structure OAI.Rokhlin.ArrayObjects.InitialLaws line 71
19. structure OAI.Rokhlin.ArrayObjects.Object line 82
20. def OAI.Rokhlin.ArrayObjects.Object.localLaw line 114
21. instance OAI.Rokhlin.ArrayObjects.Object.(instance at line 116) line 116
22. def OAI.Rokhlin.ArrayObjects.Object.parameter line 120
23. instance OAI.Rokhlin.ArrayObjects.Object.(instance at line 121) line 121
24. structure OAI.Rokhlin.ArrayObjects.Object.Extension line 124
25. def OAI.Rokhlin.ArrayObjects.Object.Extension.refl line 137
26. def OAI.Rokhlin.ArrayObjects.Object.Extension.comp line 148
27. lemma OAI.Rokhlin.ArrayObjects.Object.Extension.measurePreserving line 165
28. lemma OAI.Rokhlin.ArrayObjects.Object.Extension.localLaw_map line 169
29. lemma OAI.Rokhlin.ArrayObjects.Object.Extension.parameter_map line 176
30. lemma OAI.Rokhlin.ArrayObjects.condDistrib_condition_const line 186
31. def OAI.Rokhlin.ArrayObjects.trivialSpace line 196
32. def OAI.Rokhlin.ArrayObjects.initialObject line 204
33. theorem OAI.Rokhlin.Saturation.projection_difference_inner line 257
34. theorem OAI.Rokhlin.Saturation.projection_norm_difference line 271
35. theorem OAI.Rokhlin.Saturation.projection_eq_of_norm_eq line 283
36. theorem OAI.Rokhlin.Saturation.projection_norm_mono line 293
37. inductive OAI.Rokhlin.ArrayObjects.DataKind line 306
38. abbrev OAI.Rokhlin.ArrayObjects.Object.data line 317
39. lemma OAI.Rokhlin.ArrayObjects.Object.data_le line 326
40. lemma OAI.Rokhlin.ArrayObjects.Object.Extension.data_comap_le line 338
41. def OAI.Rokhlin.ArrayObjects.Object.Extension.pull line 369
42. lemma OAI.Rokhlin.ArrayObjects.Object.Extension.pull_comp line 373
43. lemma OAI.Rokhlin.ArrayObjects.Object.Extension.pull_data_mem line 377
44. def OAI.Rokhlin.ArrayObjects.Object.project line 397
45. lemma OAI.Rokhlin.ArrayObjects.Object.project_norm_le line 403
46. lemma OAI.Rokhlin.ArrayObjects.Object.Extension.project_norm_mono line 410
47. lemma OAI.Rokhlin.ArrayObjects.Object.Extension.project_eq_of_norm_le line 421
48. def OAI.Rokhlin.ArrayObjects.Object.IsSaturated line 436
49. lemma OAI.Rokhlin.KernelTests.ae_eq_of_evaluations line 447
50. lemma OAI.Rokhlin.KernelTests.hasCondDistrib_of_indicators line 457
51. lemma OAI.Rokhlin.ArrayObjects.Object.project_ae_eq_condExp line 483
52. lemma OAI.Rokhlin.ArrayObjects.Object.IsSaturated.condExp line 491
53. lemma OAI.Rokhlin.ArrayObjects.Object.IsSaturated.indicator line 507
54. lemma OAI.Rokhlin.ArrayObjects.Object.IsSaturated.hasCondDistrib line 541
55. def OAI.Rokhlin.ArrayObjects.roll line 573
56. lemma OAI.Rokhlin.ArrayObjects.roll_amap line 586
57. lemma OAI.Rokhlin.ArrayObjects.select_roll line 590
58. lemma OAI.Rokhlin.ArrayObjects.plane_roll line 595
59. lemma OAI.Rokhlin.ArrayObjects.planes_roll line 602
60. abbrev OAI.Rokhlin.ArrayObjects.Object.Rolled.State line 614
61. abbrev OAI.Rokhlin.ArrayObjects.Object.Rolled.Parameter line 620
62. def OAI.Rokhlin.ArrayObjects.Object.Rolled.timeState line 626
63. def OAI.Rokhlin.ArrayObjects.Object.Rolled.timeParameter line 629
64. def OAI.Rokhlin.ArrayObjects.Object.Rolled.parameter line 633
65. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_parameter line 636
66. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.time_parameter line 640
67. def OAI.Rokhlin.ArrayObjects.Object.Rolled.law line 647
68. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.law_probability line 649
69. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.invariant line 652
70. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.select_law line 660
71. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.over_base line 666
72. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.consistent line 671
73. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.proper line 677
74. def OAI.Rokhlin.FiniteKernel.pi line 698
75. theorem OAI.Rokhlin.FiniteKernel.pi_apply line 708
76. instance OAI.Rokhlin.FiniteKernel.(instance at line 711) line 711
77. theorem OAI.Rokhlin.FiniteKernel.pi_box line 714
78. theorem OAI.Rokhlin.FiniteKernel.map_pi line 718
79. def OAI.Rokhlin.FiniteKernel.zipEquiv line 729
80. theorem OAI.Rokhlin.FiniteKernel.compProd_pi line 743
81. theorem OAI.Rokhlin.FiniteKernel.pi_compProd line 765
82. theorem OAI.Rokhlin.ConditionalScreens.chain line 799
83. theorem OAI.Rokhlin.ConditionalScreens.compProd_prodMkRight line 813
84. theorem OAI.Rokhlin.ConditionalScreens.screening line 820
85. def OAI.Rokhlin.ConditionalReveal.insertTuple line 840
86. theorem OAI.Rokhlin.ConditionalReveal.measurable_insertTuple line 844
87. theorem OAI.Rokhlin.ConditionalReveal.map_insertTuple line 853
88. def OAI.Rokhlin.ConditionalReveal.splitTuple line 894
89. theorem OAI.Rokhlin.ConditionalReveal.measurable_splitTuple line 898
90. theorem OAI.Rokhlin.ConditionalReveal.split_insertTuple line 904
91. theorem OAI.Rokhlin.ConditionalReveal.map_splitTuple line 913
92. theorem OAI.Rokhlin.ConditionalReveal.probability_eq_of_subsingleton line 921
93. theorem OAI.Rokhlin.ConditionalReveal.finite_reveal line 933
94. theorem OAI.Rokhlin.ConditionalTransport.pullback line 988
95. theorem OAI.Rokhlin.ConditionalTransport.recondition line 999
96. theorem OAI.Rokhlin.ConditionalTransport.comap_le_of_factor line 1018
97. theorem OAI.Rokhlin.ConditionalTransport.of_indep line 1024
98. theorem OAI.Rokhlin.ConditionalTransport.indep_of_const line 1031
99. theorem OAI.Rokhlin.ConditionalReveal.independent_image line 1044
100. lemma OAI.Rokhlin.ConditionalTransport.map_indep line 1084
101. def OAI.Rokhlin.ArrayObjects.Object.ownKernel line 1097
102. instance OAI.Rokhlin.ArrayObjects.Object.ownKernel_markov line 1099
103. lemma OAI.Rokhlin.ArrayObjects.Object.ownKernel_conditional line 1103
104. lemma OAI.Rokhlin.ArrayObjects.Object.planes_conditional line 1108
105. lemma OAI.Rokhlin.ArrayObjects.Object.ownKernel_zero_image line 1116
106. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.local_independent line 1136
107. lemma OAI.Rokhlin.ArrayObjects.cons_snoc line 1177
108. abbrev OAI.Rokhlin.ArrayObjects.Object.Rolled.Outside line 1187
109. abbrev OAI.Rokhlin.ArrayObjects.Object.Rolled.RawData line 1193
110. abbrev OAI.Rokhlin.ArrayObjects.Object.Rolled.RevealData line 1196
111. abbrev OAI.Rokhlin.ArrayObjects.Object.Rolled.RollData line 1199
112. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rawData line 1202
113. def OAI.Rokhlin.ArrayObjects.Object.Rolled.missingRow line 1205
114. def OAI.Rokhlin.ArrayObjects.Object.Rolled.revealData line 1208
115. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rollData line 1211
116. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_rawData line 1215
117. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_missingRow line 1218
118. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_revealData line 1222
119. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_rollData line 1227
120. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rollToReveal line 1231
121. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_rollToReveal line 1237
122. def OAI.Rokhlin.ArrayObjects.Object.Rolled.revealToRoll line 1242
123. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_revealToRoll line 1249
124. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rollToReveal_observation line 1263
125. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.revealToRoll_observation line 1278
126. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.comap_reveal_eq_rollData line 1299
127. abbrev OAI.Rokhlin.ArrayObjects.Object.Rolled.OldData line 1308
128. def OAI.Rokhlin.ArrayObjects.Object.Rolled.oldData line 1311
129. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_oldData line 1314
130. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rowData line 1317
131. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_rowData line 1320
132. def OAI.Rokhlin.ArrayObjects.Object.Rolled.selectData line 1325
133. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_selectData line 1328
134. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.selectData_observation line 1334
135. def OAI.Rokhlin.ArrayObjects.Object.Rolled.IsConditional line 1352
136. def OAI.Rokhlin.ArrayObjects.Object.Rolled.makeObject line 1360
137. def OAI.Rokhlin.ArrayObjects.Object.Rolled.extension line 1381
138. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rowKernel line 1394
139. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.rowKernel_markov line 1397
140. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.parent_reveal line 1401
141. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.parent_joint line 1442
142. def OAI.Rokhlin.LocalConditioning.observe line 1467
143. instance OAI.Rokhlin.LocalConditioning.(instance at line 1471) line 1471
144. theorem OAI.Rokhlin.LocalConditioning.observe_apply line 1475
145. theorem OAI.Rokhlin.LocalConditioning.deterministic line 1488
146. theorem OAI.Rokhlin.LocalConditioning.hasCondDistrib_observe line 1496
147. theorem OAI.Rokhlin.LocalConditioning.observe_pi line 1506
148. theorem OAI.Rokhlin.LocalConditioning.compProd_comap line 1517
149. theorem OAI.Rokhlin.LocalConditioning.observe_comap line 1525
150. theorem OAI.Rokhlin.LocalConditioning.disintegrate_pi line 1533
151. theorem OAI.Rokhlin.LocalConditioning.hasCondDistrib_update line 1544
152. theorem OAI.Rokhlin.LocalConditioning.hasCondDistrib_local_update line 1563
153. theorem OAI.Rokhlin.LocalConditioning.hasCondDistrib_posterior line 1592
154. theorem OAI.Rokhlin.LocalConditioning.local_conditioning line 1603
155. def OAI.Rokhlin.ArrayObjects.Object.Rolled.parameterEquiv line 1641
156. def OAI.Rokhlin.ArrayObjects.Object.Rolled.parents line 1658
157. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_parents line 1660
158. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.parameterEquiv_observation line 1663
159. def OAI.Rokhlin.ArrayObjects.Object.Rolled.posterior line 1672
160. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.posterior_markov line 1676
161. def OAI.Rokhlin.ArrayObjects.Object.Rolled.ownPosterior line 1680
162. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.ownPosterior_markov line 1684
163. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.roll_symm_preserving line 1689
164. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.ownPosterior_conditional line 1695
165. abbrev OAI.Rokhlin.ArrayObjects.Object.Rolled.ParentOutside line 1720
166. abbrev OAI.Rokhlin.ArrayObjects.Object.Rolled.ScreenData line 1722
167. def OAI.Rokhlin.ArrayObjects.Object.Rolled.parentOutside line 1725
168. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_parentOutside line 1728
169. def OAI.Rokhlin.ArrayObjects.Object.Rolled.parentRow line 1733
170. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_parentRow line 1736
171. def OAI.Rokhlin.ArrayObjects.Object.Rolled.parentsKernel line 1741
172. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.parentsKernel_markov line 1746
173. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.parentsKernel_comap line 1752
174. def OAI.Rokhlin.ArrayObjects.Object.Rolled.screenData line 1759
175. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_screenData line 1763
176. def OAI.Rokhlin.ArrayObjects.Object.Rolled.screenKernel line 1769
177. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.screenKernel_markov line 1774
178. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.screen_conditional line 1779
179. def OAI.Rokhlin.ArrayObjects.Object.Rolled.screenEquiv line 1797
180. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.screenEquiv_observation line 1841
181. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.screen_plane_parameters line 1856
182. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.screenKernel_roll line 1868
183. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.outside_conditional line 1888
184. lemma OAI.Rokhlin.FiniteKernel.measure_pi_precomp line 1919
185. lemma OAI.Rokhlin.FiniteKernel.pi_precomp line 1931
186. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.proper_conditional line 1945
187. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.parameter_plane_preserving line 1967
188. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.conditional_step line 1977
189. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.isConditional line 1994
190. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.insert_proper line 2005
191. def OAI.Rokhlin.ArrayObjects.Object.Rolled.object line 2012
192. def OAI.Rokhlin.ArrayObjects.Object.Rolled.objectExtension line 2016
193. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.row_reveal line 2022
194. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.rows_conditional line 2062
195. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.single_cell_locality line 2082
196. lemma OAI.Rokhlin.ConditionalReveal.comap_union_reveal line 2095
197. theorem OAI.Rokhlin.ConditionalReveal.finite_reveal_with_parents line 2116
198. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_single_missing line 2143
199. theorem OAI.Rokhlin.ConditionalScreens.reverse_screen line 2170
200. theorem OAI.Rokhlin.FiniteKernel.independent_observation line 2205
201. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.outside_row_screen line 2235
202. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.plane_first_last line 2284
203. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.columns_given_row line 2293
204. lemma OAI.Rokhlin.FiniteKernel.map_eval line 2333
205. lemma OAI.Rokhlin.ArrayObjects.Object.plane_conditional line 2347
206. def OAI.Rokhlin.ArrayObjects.Object.parameterLaw line 2362
207. instance OAI.Rokhlin.ArrayObjects.Object.parameterLaw_probability line 2365
208. def OAI.Rokhlin.ArrayObjects.Object.parameterCoordinateKernel line 2370
209. instance OAI.Rokhlin.ArrayObjects.Object.parameterCoordinateKernel_markov line 2374
210. lemma OAI.Rokhlin.ArrayObjects.Object.column_parameter_given_cell line 2381
211. lemma OAI.Rokhlin.ArrayObjects.Object.shared_parameter_kernel line 2402
212. theorem OAI.Rokhlin.ConditionalTransport.pushforward line 2423
213. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.columns_parameter_given_row line 2441
214. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.parameter_geometry_outside line 2481
215. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.parameter_geometry line 2492
216. theorem OAI.Rokhlin.ConditionalScreens.joint_of_screen line 2518
217. lemma OAI.Rokhlin.ArrayObjects.Object.parameterLaw_consistent line 2543
218. theorem OAI.Rokhlin.ArrayObjects.Object.diagonal_parameter_product line 2552
219. theorem OAI.Rokhlin.FiniteKernel.pi_split line 2585
220. theorem OAI.Rokhlin.ConditionalReveal.disjoint_families line 2622
221. theorem OAI.Rokhlin.ConditionalScreens.screened_marginal line 2641
222. abbrev OAI.Rokhlin.ArrayObjects.Object.Rolled.ParentData line 2664
223. def OAI.Rokhlin.ArrayObjects.Object.Rolled.parentData line 2667
224. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_parentData line 2670
225. def OAI.Rokhlin.ArrayObjects.Object.Rolled.columnKernel line 2674
226. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.columnKernel_markov line 2679
227. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.columns_with_parents line 2686
228. def OAI.Rokhlin.ArrayObjects.Object.Rolled.cells line 2729
229. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_cells line 2732
230. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rowRestrict line 2735
231. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_rowRestrict line 2738
232. def OAI.Rokhlin.ArrayObjects.Object.Rolled.columnRestrict line 2744
233. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_columnRestrict line 2747
234. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.columnRestrict_planes line 2754
235. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rowFamilyKernel line 2759
236. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.rowFamilyKernel_markov line 2763
237. def OAI.Rokhlin.ArrayObjects.Object.Rolled.groupMarginal line 2766
238. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.groupMarginal_markov line 2769
239. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.group_marginal_with_parents line 2773
240. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.group_intermediate_marginal line 2786
241. abbrev OAI.Rokhlin.ArrayObjects.Object.Rolled.GroupData line 2811
242. abbrev OAI.Rokhlin.ArrayObjects.Object.Rolled.WholeGroupData line 2813
243. def OAI.Rokhlin.ArrayObjects.Object.Rolled.groupData line 2816
244. def OAI.Rokhlin.ArrayObjects.Object.Rolled.wholeGroupData line 2818
245. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_groupData line 2821
246. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_wholeGroupData line 2825
247. def OAI.Rokhlin.ArrayObjects.Object.Rolled.groupSelect line 2829
248. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_groupSelect line 2832
249. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.groupSelect_observation line 2836
250. def OAI.Rokhlin.ArrayObjects.Object.Rolled.revealParent line 2843
251. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_revealParent line 2845
252. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.revealParent_observation line 2849
253. def OAI.Rokhlin.ArrayObjects.Object.Rolled.revealSelect line 2856
254. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_revealSelect line 2861
255. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.revealSelect_observation line 2866
256. def OAI.Rokhlin.ArrayObjects.Object.Rolled.groupLastData line 2878
257. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_groupLastData line 2883
258. def OAI.Rokhlin.ArrayObjects.Object.Rolled.groupLastKernel line 2891
259. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.groupLastKernel_markov line 2896
260. def OAI.Rokhlin.ArrayObjects.Object.Rolled.wholeLastSelect line 2901
261. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_wholeLastSelect line 2906
262. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_missing_after_retain line 2910
263. lemma OAI.Rokhlin.ConditionalScreens.compProd_comap line 2950
264. theorem OAI.Rokhlin.ConditionalScreens.canonical_screen line 2959
265. def OAI.Rokhlin.ArrayObjects.Object.Rolled.joinOutput line 2977
266. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_joinOutput line 2981
267. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.joinOutput_observation line 2987
268. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_cell_locality line 2996
269. lemma OAI.Rokhlin.conditional_kernel_equivariant line 3046
270. def OAI.Rokhlin.ArrayObjects.amapEquiv line 3075
271. lemma OAI.Rokhlin.ArrayObjects.Object.parameterLaw_invariant line 3087
272. lemma OAI.Rokhlin.ArrayObjects.Object.ownKernel_time_equivariant line 3098
273. lemma OAI.Rokhlin.ArrayObjects.Object.ownKernel_time_preserving line 3107
274. lemma OAI.Rokhlin.ConditionalFibres.chain line 3125
275. theorem OAI.Rokhlin.ConditionalFibres.disintegrate line 3140
276. theorem OAI.Rokhlin.ConditionalFibres.marginal line 3157