OAI/Dynamics/MultipleMixing/Joinings.lean

GitHub source file

314 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Rokhlin.JoiningOperator.pull line 21
2. def OAI.Rokhlin.JoiningOperator.operator line 24
3. lemma OAI.Rokhlin.JoiningOperator.pull_norm_le line 27
4. lemma OAI.Rokhlin.JoiningOperator.operator_norm_le line 32
5. lemma OAI.Rokhlin.JoiningOperator.operator_adjoint line 37
6. lemma OAI.Rokhlin.JoiningOperator.pull_adjoint_pull line 40
7. lemma OAI.Rokhlin.JoiningOperator.operator_self line 46
8. lemma OAI.Rokhlin.JoiningOperator.pull_comp line 49
9. lemma OAI.Rokhlin.JoiningOperator.inner_operator line 55
10. lemma OAI.Rokhlin.JoiningOperator.operator_pullback line 67
11. lemma OAI.Rokhlin.JoiningOperator.pull_range line 86
12. lemma OAI.Rokhlin.JoiningOperator.pull_adjoint_projection line 109
13. lemma OAI.Rokhlin.JoiningOperator.operator_ae_eq_condExp line 132
14. lemma OAI.Rokhlin.JoiningOperator.condExp_of_kernel line 151
15. lemma OAI.Rokhlin.JoiningOperator.screened_condExp line 163
16. theorem OAI.Rokhlin.JoiningOperator.screened_operator line 171
17. lemma OAI.Rokhlin.JoiningOperator.operator_comp_right line 193
18. theorem OAI.Rokhlin.JoiningOperator.square_rectangle line 214
19. def OAI.Rokhlin.ArrayObjects.Object.Rolled.tupleUnion line 276
20. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_tupleUnion line 279
21. def OAI.Rokhlin.ArrayObjects.Object.Rolled.tupleSelect line 286
22. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_tupleSelect line 289
23. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.fullGroupedLocality line 294
24. def OAI.Rokhlin.ArrayObjects.Object.Rolled.splitOwnData line 322
25. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_splitOwnData line 325
26. def OAI.Rokhlin.ArrayObjects.Object.Rolled.splitRowKernel line 330
27. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.splitRowKernel_markov line 334
28. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.wholeSplit_field line 337
29. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.splitRowScreen line 356
30. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.splitRowScreen_fibre line 382
31. abbrev OAI.Rokhlin.ArrayObjects.Object.Rolled.squareFibre line 398
32. abbrev OAI.Rokhlin.ArrayObjects.Object.Rolled.cellLaw line 400
33. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.cellMarginal_fibre line 403
34. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_rectangle line 420
35. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rowPairKernel line 479
36. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.rowPairKernel_markov line 482
37. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rowPair_conditional line 485
38. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.parameterEquiv_plane line 507
39. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.columnKernel_eq_posterior line 517
40. def OAI.Rokhlin.ArrayObjects.Object.Rolled.columnGroupKernel line 527
41. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.columnGroupKernel_markov line 531
42. def OAI.Rokhlin.ArrayObjects.Object.Rolled.columnOwnData line 534
43. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_columnOwnData line 537
44. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.columns_group_screen line 540
45. lemma OAI.Rokhlin.JoiningOperator.aestronglyMeasurable_of_inner line 570
46. def OAI.Rokhlin.JoiningOperator.family line 594
47. lemma OAI.Rokhlin.JoiningOperator.family_eq line 599
48. lemma OAI.Rokhlin.JoiningOperator.family_norm_le line 607
49. lemma OAI.Rokhlin.JoiningOperator.family_inner line 616
50. lemma OAI.Rokhlin.JoiningOperator.family_inner_aestronglyMeasurable line 625
51. lemma OAI.Rokhlin.JoiningOperator.family_aestronglyMeasurable line 634
52. lemma OAI.Rokhlin.JoiningOperator.family_eq_of_joint line 643
53. theorem OAI.Rokhlin.JoiningOperator.conditional_square_rectangle line 674
54. def OAI.Rokhlin.JoiningOperator.IsRectangle line 727
55. def OAI.Rokhlin.ArrayObjects.Object.Rolled.columnPairKernel line 735
56. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.columnPairKernel_markov line 738
57. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.columnPairRestrict_planes line 743
58. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.columnPair_conditional line 750
59. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.pair_fst_push line 762
60. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.pair_snd_push line 771
61. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rowEdge line 779
62. def OAI.Rokhlin.ArrayObjects.Object.Rolled.columnEdge line 784
63. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_family_rectangle line 789
64. lemma OAI.Rokhlin.ConditionalFibres.ae_ae line 862
65. lemma OAI.Rokhlin.ConditionalFibres.parameter_fixed line 870
66. lemma OAI.Rokhlin.ConditionalFibres.indep_of_screen line 878
67. lemma OAI.Rokhlin.ConditionalFibres.triple_product line 892
68. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rows_indep_fibre line 911
69. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.columns_indep_fibre line 923
70. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rowRestrict_parents line 936
71. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.cells_indep_rows_fibre line 939
72. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.cells_indep_columns_fibre line 946
73. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.cells_colpair_indep_row_fibre line 954
74. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.cells_rowpair_indep_column_fibre line 963
75. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_product_triples line 973
76. def OAI.Rokhlin.ArrayObjects.Object.Rolled.fibreRowEdge line 1006
77. def OAI.Rokhlin.ArrayObjects.Object.Rolled.fibreColumnEdge line 1010
78. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_fibre_rectangle line 1014
79. lemma OAI.Rokhlin.JoiningOperator.conditional_pair_marginals line 1068
80. lemma OAI.Rokhlin.JoiningOperator.integrable_inner_comp line 1095
81. lemma OAI.Rokhlin.JoiningOperator.family_setIntegral line 1105
82. lemma OAI.Rokhlin.JoiningOperator.ae_eq_zero_of_rectangles line 1139
83. def OAI.Rokhlin.JoiningOperator.weightedTest line 1161
84. lemma OAI.Rokhlin.JoiningOperator.coe_weightedTest line 1165
85. lemma OAI.Rokhlin.JoiningOperator.weightedTest_indicator line 1170
86. lemma OAI.Rokhlin.JoiningOperator.snd_observation line 1193
87. lemma OAI.Rokhlin.JoiningOperator.weighted_inner line 1199
88. lemma OAI.Rokhlin.JoiningOperator.family_inner_integrable line 1220
89. lemma OAI.Rokhlin.JoiningOperator.active_kernel line 1234
90. def OAI.Rokhlin.essentialKernel line 1287
91. theorem OAI.Rokhlin.essentialKernel.ae_annihilate line 1304
92. def OAI.Rokhlin.essentialRange line 1326
93. lemma OAI.Rokhlin.essentialRange.isClosed line 1329
94. instance OAI.Rokhlin.essentialRange.completeSpace line 1332
95. lemma OAI.Rokhlin.essentialRange.ae_range_le line 1335
96. lemma OAI.Rokhlin.essentialRange.le_of_ae_range line 1345
97. lemma OAI.Rokhlin.essentialRange.le_comap_of_ae_comp line 1361
98. lemma OAI.Rokhlin.projection_intertwines line 1375
99. lemma OAI.Rokhlin.projection_commutes_of_invariant line 1389
100. lemma OAI.Rokhlin.JoiningOperator.active_eq_essentialRange line 1408
101. lemma OAI.Rokhlin.JoiningOperator.kernel_measurableSet_eq_const line 1426
102. lemma OAI.Rokhlin.JoiningOperator.stronglyMeasurable_of_inner line 1453
103. lemma OAI.Rokhlin.JoiningOperator.family_good_measurable line 1477
104. lemma OAI.Rokhlin.JoiningOperator.family_inner_stronglyMeasurable line 1489
105. lemma OAI.Rokhlin.JoiningOperator.family_stronglyMeasurable line 1503
106. def OAI.Rokhlin.VectorMeasurable line 1518
107. lemma OAI.Rokhlin.VectorMeasurable.adjoint line 1521
108. lemma OAI.Rokhlin.VectorMeasurable.apply line 1530
109. lemma OAI.Rokhlin.VectorMeasurable.comp line 1538
110. lemma OAI.Rokhlin.VectorMeasurable.comap line 1544
111. lemma OAI.Rokhlin.VectorMeasurable.measurableSet_eq line 1550
112. lemma OAI.Rokhlin.VectorMeasurable.measurableSet_range_le line 1567
113. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.cells_conditional line 1595
114. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.cells_fibre_marginal line 1600
115. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rowPair_fixed_conditional line 1608
116. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.columnPair_own_conditional line 1619
117. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.columnPair_fixed_conditional line 1627
118. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.fibreRowEdge_eq line 1636
119. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.fibreColumnEdge_eq line 1643
120. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.fibreRowEdge_measurable line 1650
121. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.fibreColumnEdge_measurable line 1656
122. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rowPair_fixed_marginals line 1661
123. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.columnPair_fixed_marginals line 1674
124. lemma OAI.Rokhlin.essentialRange.ae_intertwining line 1701
125. lemma OAI.Rokhlin.essentialRange.projection_commutes line 1717
126. lemma OAI.Rokhlin.essentialRange.own_intertwines line 1732
127. lemma OAI.Rokhlin.maps_of_intertwines line 1748
128. lemma OAI.Rokhlin.adjoint_intertwines line 1756
129. lemma OAI.Rokhlin.inf_intertwines line 1764
130. def OAI.Rokhlin.compress line 1787
131. lemma OAI.Rokhlin.compress_adjoint line 1791
132. lemma OAI.Rokhlin.compress_apply line 1798
133. lemma OAI.Rokhlin.compress_onto line 1807
134. lemma OAI.Rokhlin.compressed_total_range line 1816
135. lemma OAI.Rokhlin.rectangle_column_intertwines line 1854
136. lemma OAI.Rokhlin.rectangle_all_intertwines line 1885
137. lemma OAI.Rokhlin.compress_comp line 1932
138. lemma OAI.Rokhlin.VectorMeasurable.compress line 1944
139. instance OAI.Rokhlin.submodule_completeSpace_inf line 1951
140. lemma OAI.Rokhlin.rectangle_active_intersections line 1993
141. lemma OAI.Rokhlin.restricted_rectangle line 2023
142. lemma OAI.Rokhlin.restricted_total_F line 2045
143. lemma OAI.Rokhlin.restricted_total_G line 2056
144. lemma OAI.Rokhlin.restricted_total_K line 2067
145. lemma OAI.Rokhlin.restricted_total_N line 2078
146. lemma OAI.Rokhlin.VectorMeasurable.ae_eq_of_map line 2096
147. lemma OAI.Rokhlin.fixed_squares_of_rectangle line 2116
148. theorem OAI.Rokhlin.restricted_fixed_squares line 2197
149. def OAI.Rokhlin.rectangleSpace₁ line 2238
150. def OAI.Rokhlin.rectangleSpace₂ line 2239
151. def OAI.Rokhlin.rectangleSpace₃ line 2240
152. def OAI.Rokhlin.rectangleSpace₄ line 2241
153. instance OAI.Rokhlin.(instance at line 2243) line 2243
154. instance OAI.Rokhlin.(instance at line 2244) line 2244
155. instance OAI.Rokhlin.(instance at line 2245) line 2245
156. instance OAI.Rokhlin.(instance at line 2246) line 2246
157. def OAI.Rokhlin.rectangleRestrictF line 2248
158. def OAI.Rokhlin.rectangleRestrictG line 2250
159. def OAI.Rokhlin.rectangleRestrictK line 2252
160. def OAI.Rokhlin.rectangleRestrictN line 2254
161. structure OAI.Rokhlin.TriplePartition line 2260
162. lemma OAI.Rokhlin.TriplePartition.properPA line 2273
163. lemma OAI.Rokhlin.TriplePartition.properPB line 2278
164. lemma OAI.Rokhlin.TriplePartition.properAB line 2283
165. lemma OAI.Rokhlin.TriplePartition.properP line 2288
166. lemma OAI.Rokhlin.TriplePartition.properA line 2292
167. lemma OAI.Rokhlin.TriplePartition.properB line 2296
168. lemma OAI.Rokhlin.TriplePartition.card_eq line 2300
169. lemma OAI.Rokhlin.TriplePartition.cardP line 2304
170. lemma OAI.Rokhlin.TriplePartition.cardPA line 2309
171. lemma OAI.Rokhlin.TriplePartition.cardPB line 2313
172. lemma OAI.Rokhlin.MeasurePreserving.triple_swap_right line 2325
173. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_restricted_fixed_squares line 2339
174. lemma OAI.Rokhlin.rectangle_restricted_laws line 2410
175. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_restricted_rectangle line 2440
176. def OAI.Rokhlin.StrongUnitary.code line 2498
177. instance OAI.Rokhlin.StrongUnitary.topology line 2500
178. lemma OAI.Rokhlin.StrongUnitary.code_injective line 2503
179. lemma OAI.Rokhlin.StrongUnitary.code_embedding line 2508
180. instance OAI.Rokhlin.StrongUnitary.t2 line 2511
181. instance OAI.Rokhlin.StrongUnitary.metrizable line 2512
182. instance OAI.Rokhlin.StrongUnitary.secondCountable line 2513
183. instance OAI.Rokhlin.StrongUnitary.measurableSpace line 2515
184. instance OAI.Rokhlin.StrongUnitary.borelSpace line 2516
185. lemma OAI.Rokhlin.StrongUnitary.continuous_eval line 2518
186. lemma OAI.Rokhlin.StrongUnitary.continuous_apply line 2525
187. lemma OAI.Rokhlin.StrongUnitary.continuous_iff line 2528
188. lemma OAI.Rokhlin.StrongUnitary.tendsto_iff line 2535
189. lemma OAI.Rokhlin.StrongUnitary.measurable_iff line 2542
190. lemma OAI.Rokhlin.StrongUnitary.continuous_symm line 2558
191. instance OAI.Rokhlin.StrongUnitary.topologicalGroup line 2571
192. lemma OAI.Rokhlin.unitary_measurable_of_dense line 2585
193. lemma OAI.Rokhlin.HasFixedInjectiveSquares.exists_measurable_polar line 2598
194. structure OAI.Rokhlin.MeasurablePolar line 2659
195. lemma OAI.Rokhlin.HasFixedInjectiveSquares.nonempty_polar line 2665
196. lemma OAI.Rokhlin.MeasurablePolar.rectangle line 2684
197. structure OAI.Rokhlin.MeasurablePolarRectangle line 2712
198. lemma OAI.Rokhlin.exists_measurablePolarRectangle line 2731
199. lemma OAI.Rokhlin.exists_restrictedPolarRectangle line 2764
200. def OAI.Rokhlin.ArrayObjects.Object.Rolled.GroupedPolarData line 2798
201. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_polar_data line 2813
202. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.pairPair_conditional line 2838
203. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.pairPair_fixed_conditional line 2873
204. theorem OAI.Rokhlin.mem_support_map_of_continuous line 2906
205. theorem OAI.Rokhlin.eqOn_support_of_ae_eq line 2917
206. theorem OAI.Rokhlin.eqOn_support_prod_of_ae_eq line 2924
207. def OAI.Rokhlin.translateProbability line 2941
208. theorem OAI.Rokhlin.translateProbability_toMeasure line 2947
209. theorem OAI.Rokhlin.continuous_translateProbability line 2951
210. theorem OAI.Rokhlin.translateProbability_one_right_toMeasure line 2972
211. theorem OAI.Rokhlin.translateProbability_eq_on_support line 2977
212. theorem OAI.Rokhlin.map_mulLeft_inv_eq_of_eq line 2986
213. theorem OAI.Rokhlin.common_abelian_support_of_translated_laws line 2999
214. theorem OAI.Rokhlin.normalized_rectangle_support line 3054
215. theorem OAI.Rokhlin.translated_law_of_rectangle line 3094
216. theorem OAI.Rokhlin.ae_translated_law_of_rectangle line 3114
217. theorem OAI.Rokhlin.ae_translated_law_of_kernel_rectangle line 3127
218. theorem OAI.Rokhlin.normalized_polar_group_from_kernels line 3142
219. lemma OAI.Rokhlin.StrongUnitary.continuous_trans line 3195
220. lemma OAI.Rokhlin.StrongUnitary.support_rectangle line 3201
221. def OAI.Rokhlin.StrongUnitary.normalizeA line 3214
222. def OAI.Rokhlin.StrongUnitary.normalizeB line 3216
223. def OAI.Rokhlin.StrongUnitary.normalizeC line 3217
224. def OAI.Rokhlin.StrongUnitary.normalizeD line 3219
225. lemma OAI.Rokhlin.StrongUnitary.continuous_normalizeA line 3222
226. lemma OAI.Rokhlin.StrongUnitary.continuous_normalizeB line 3228
227. lemma OAI.Rokhlin.StrongUnitary.continuous_normalizeC line 3233
228. lemma OAI.Rokhlin.StrongUnitary.continuous_normalizeD line 3239
229. lemma OAI.Rokhlin.StrongUnitary.normalized_rectangle line 3245
230. lemma OAI.Rokhlin.StrongUnitary.normalized_reference line 3254
231. lemma OAI.Rokhlin.map_pair_fst line 3275
232. lemma OAI.Rokhlin.map_pair_snd line 3279
233. lemma OAI.Rokhlin.kernel_map_pair_fst line 3283
234. lemma OAI.Rokhlin.kernel_map_pair_snd line 3286
235. lemma OAI.Rokhlin.kernel_map_pair_comp line 3290
236. lemma OAI.Rokhlin.StrongUnitary.mapped_normalized_rectangle line 3307
237. lemma OAI.Rokhlin.StrongUnitary.normalized_supports line 3324
238. lemma OAI.Rokhlin.StrongUnitary.polar_normalization line 3343
239. lemma OAI.Rokhlin.ConditionalFibres.law_comp line 3424
240. lemma OAI.Rokhlin.ConditionalFibres.ae_kernel line 3427
241. lemma OAI.Rokhlin.polar_pair_laws line 3453
242. theorem OAI.Rokhlin.isClosed_positive_operators line 3501
243. theorem OAI.Rokhlin.convex_positive_operators line 3514
244. theorem OAI.Rokhlin.positive_compact_integral line 3525
245. theorem OAI.Rokhlin.strict_positive_integral line 3536
246. theorem OAI.Rokhlin.injective_of_strict_positive line 3562
247. def OAI.Rokhlin.conjugateOperator line 3575
248. theorem OAI.Rokhlin.conjugateOperator_apply line 3580
249. theorem OAI.Rokhlin.conjugateOperator_mul line 3584
250. theorem OAI.Rokhlin.conjugateOperator_positive line 3587
251. theorem OAI.Rokhlin.conjugateOperator_compact line 3599
252. theorem OAI.Rokhlin.conjugateOperator_strict_positive line 3604
253. theorem OAI.Rokhlin.averaged_conjugates_commute line 3619
254. theorem OAI.Rokhlin.averaged_positive_compact_injective line 3640
255. def OAI.Rokhlin.quadraticFormCLM line 3661
256. theorem OAI.Rokhlin.quadraticFormCLM_apply line 3665
257. theorem OAI.Rokhlin.weighted_rankOne_quadratic line 3669
258. theorem OAI.Rokhlin.compact_rankOne line 3678
259. theorem OAI.Rokhlin.positive_compact_tsum line 3682
260. theorem OAI.Rokhlin.dense_sequence_inner_ne_zero line 3694
261. theorem OAI.Rokhlin.weighted_rankOne_tsum_strict line 3708
262. def OAI.Rokhlin.compactSeedWeight line 3726
263. theorem OAI.Rokhlin.compactSeedWeight_pos line 3730
264. theorem OAI.Rokhlin.compactSeedWeight_bound line 3735
265. theorem OAI.Rokhlin.exists_positive_compact_strict line 3745
266. theorem OAI.Rokhlin.conjugateOperator_rankOne line 3763
267. theorem OAI.Rokhlin.norm_conjugateOperator line 3771
268. def OAI.Rokhlin.compactSeed line 3775
269. theorem OAI.Rokhlin.compactSeed_summable line 3778
270. theorem OAI.Rokhlin.continuous_conjugate_compactSeed line 3782
271. theorem OAI.Rokhlin.compactSeed_properties line 3801
272. theorem OAI.Rokhlin.exists_invariant_positive_compact line 3811
273. lemma OAI.Rokhlin.symmetric_joint_total line 3832
274. def OAI.Rokhlin.unitaryPart line 3888
275. lemma OAI.Rokhlin.part_commute line 3892
276. lemma OAI.Rokhlin.parts_commute line 3900
277. lemma OAI.Rokhlin.unitary_clm_commute line 3907
278. lemma OAI.Rokhlin.unitary_joint_total line 3912
279. lemma OAI.Rokhlin.orthogonal_total_basis line 3962
280. lemma OAI.Rokhlin.symmetric_joint_basis line 3992
281. lemma OAI.Rokhlin.hilbertBasis_countable line 4015
282. lemma OAI.Rokhlin.unitary_joint_basis line 4041
283. lemma OAI.Rokhlin.eigenvalue_norm_one line 4082
284. lemma OAI.Rokhlin.eigenvalue_mul line 4088
285. def OAI.Rokhlin.eigenCharacter line 4097
286. lemma OAI.Rokhlin.continuous_eigenCharacter line 4111
287. lemma OAI.Rokhlin.subgroup_probability line 4128
288. lemma OAI.Rokhlin.StrongUnitary.polar_spectral line 4167
289. def OAI.Rokhlin.MeasurablePolarRectangle.HasHaarNormalization line 4214
290. lemma OAI.Rokhlin.MeasurablePolarRectangle.haar_normalization line 4229
291. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_haar_normalization line 4262
292. lemma OAI.Rokhlin.JoiningOperator.active_observation_eq line 4302
293. lemma OAI.Rokhlin.JoiningOperator.pair_comap_swap line 4313
294. lemma OAI.Rokhlin.essentialRange.congr_ae line 4327
295. lemma OAI.Rokhlin.JoiningOperator.swapped_marginals line 4341
296. lemma OAI.Rokhlin.JoiningOperator.family_swap line 4350
297. lemma OAI.Rokhlin.JoiningOperator.active_eq_essentialRange_adjoint line 4363
298. lemma OAI.Rokhlin.JoiningOperator.family_active_swap_conditioner line 4383
299. lemma OAI.Rokhlin.JoiningOperator.family_active_adjoint_reverse line 4398
300. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rowActive line 4425
301. def OAI.Rokhlin.ArrayObjects.Object.Rolled.columnActive line 4428
302. def OAI.Rokhlin.ArrayObjects.Object.Rolled.commonActive line 4431
303. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.(instance at line 4434) line 4434
304. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.(instance at line 4436) line 4436
305. instance OAI.Rokhlin.ArrayObjects.Object.Rolled.(instance at line 4438) line 4438
306. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rowActive_swap line 4443
307. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rowActive_adjoint line 4464
308. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.columnActive_swap line 4483
309. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.columnActive_adjoint line 4512
310. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_rectangle_spaces line 4538
311. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_active_intersections line 4575
312. abbrev OAI.Rokhlin.TriplePartition.swapPA line 4634
313. abbrev OAI.Rokhlin.TriplePartition.swapAB line 4646
314. abbrev OAI.Rokhlin.TriplePartition.swapPB line 4658