OAI/Dynamics/MultipleMixing/Saturation.lean

GitHub source file

141 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Rokhlin.SequentialLimit.step line 23
2. instance OAI.Rokhlin.SequentialLimit.step_markov line 26
3. def OAI.Rokhlin.SequentialLimit.transition line 30
4. instance OAI.Rokhlin.SequentialLimit.transition_markov line 33
5. def OAI.Rokhlin.SequentialLimit.law line 37
6. instance OAI.Rokhlin.SequentialLimit.law_probability line 39
7. lemma OAI.Rokhlin.SequentialLimit.hasCondDistrib_step line 43
8. lemma OAI.Rokhlin.SequentialLimit.map_zero line 51
9. lemma OAI.Rokhlin.SequentialLimit.map_eval line 66
10. lemma OAI.Rokhlin.SequentialLimit.map_pair line 76
11. lemma OAI.Rokhlin.SequentialLimit.ae_compatible line 83
12. lemma OAI.Rokhlin.SequentialLimit.ae_all_compatible line 89
13. theorem OAI.Rokhlin.SequentialLimit.exists_law line 92
14. def OAI.Rokhlin.SequentialLimit.bond line 104
15. lemma OAI.Rokhlin.SequentialLimit.bond_self line 107
16. lemma OAI.Rokhlin.SequentialLimit.bond_succ line 110
17. lemma OAI.Rokhlin.SequentialLimit.measurable_bond line 116
18. lemma OAI.Rokhlin.SequentialLimit.bond_apply_of_compatible line 123
19. lemma OAI.Rokhlin.SequentialLimit.map_restrict_of_compatible line 130
20. theorem OAI.Rokhlin.SequentialLimit.unique_of_compatible line 143
21. theorem OAI.Rokhlin.SequentialLimit.map_coordinatewise line 175
22. abbrev OAI.Rokhlin.InverseSystems.Path line 211
23. def OAI.Rokhlin.InverseSystems.eval line 214
24. lemma OAI.Rokhlin.InverseSystems.measurable_eval line 216
25. lemma OAI.Rokhlin.InverseSystems.measurableSet_path line 224
26. lemma OAI.Rokhlin.InverseSystems.standardBorel_path line 229
27. def OAI.Rokhlin.InverseSystems.law line 235
28. lemma OAI.Rokhlin.InverseSystems.law_probability line 239
29. lemma OAI.Rokhlin.InverseSystems.map_val_law line 245
30. lemma OAI.Rokhlin.InverseSystems.map_eval_law line 251
31. lemma OAI.Rokhlin.InverseSystems.nonempty_path line 257
32. lemma OAI.Rokhlin.InverseSystems.unique line 263
33. def OAI.Rokhlin.InverseSystems.map line 282
34. lemma OAI.Rokhlin.InverseSystems.measurable_map line 287
35. lemma OAI.Rokhlin.InverseSystems.eval_map line 293
36. lemma OAI.Rokhlin.InverseSystems.map_law line 299
37. def OAI.Rokhlin.InverseSystems.time line 314
38. lemma OAI.Rokhlin.InverseSystems.time_preserving line 327
39. def OAI.Rokhlin.InverseSystems.arrayBond line 338
40. def OAI.Rokhlin.InverseSystems.transpose line 340
41. lemma OAI.Rokhlin.InverseSystems.transpose_eval line 351
42. lemma OAI.Rokhlin.InverseSystems.array_unique line 359
43. def OAI.Rokhlin.InverseSystems.arrayLaw line 374
44. lemma OAI.Rokhlin.InverseSystems.arrayLaw_probability line 378
45. lemma OAI.Rokhlin.InverseSystems.arrayLaw_map_eval line 384
46. lemma OAI.Rokhlin.InverseSystems.array_pi_unique line 399
47. structure OAI.Rokhlin.ArrayObjects.Object.Tower line 427
48. abbrev OAI.Rokhlin.ArrayObjects.Object.Tower.yBond line 434
49. abbrev OAI.Rokhlin.ArrayObjects.Object.Tower.uBond line 435
50. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.measurable_yBond line 437
51. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.measurable_uBond line 438
52. abbrev OAI.Rokhlin.ArrayObjects.Object.Tower.stateSpace line 440
53. abbrev OAI.Rokhlin.ArrayObjects.Object.Tower.parameterSpace line 447
54. def OAI.Rokhlin.ArrayObjects.Object.Tower.timeState line 454
55. def OAI.Rokhlin.ArrayObjects.Object.Tower.timeParameter line 458
56. abbrev OAI.Rokhlin.ArrayObjects.Object.Tower.proj line 462
57. abbrev OAI.Rokhlin.ArrayObjects.Object.Tower.pproj line 463
58. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.measurable_proj line 465
59. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.measurable_pproj line 466
60. def OAI.Rokhlin.ArrayObjects.Object.Tower.x line 468
61. def OAI.Rokhlin.ArrayObjects.Object.Tower.par line 470
62. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.measurable_x line 475
63. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.measurable_par line 478
64. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.time_x line 482
65. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.time_par line 486
66. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.x_stage line 492
67. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.par_stage line 502
68. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.array_coherent line 504
69. def OAI.Rokhlin.ArrayObjects.Object.Tower.arrayLaw line 508
70. instance OAI.Rokhlin.ArrayObjects.Object.Tower.arrayLaw_probability line 511
71. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.array_marginal line 515
72. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.array_over_base line 520
73. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.array_invariant line 526
74. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.array_consistent line 540
75. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.array_proper line 552
76. def OAI.Rokhlin.ArrayObjects.Object.Tower.localLaw line 572
77. instance OAI.Rokhlin.ArrayObjects.Object.Tower.localLaw_probability line 575
78. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.localLaw_marginal line 578
79. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.local_indep_stage line 585
80. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.parameter_comap line 600
81. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.parameter_comap_mono line 610
82. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.local_independent line 621
83. theorem OAI.Rokhlin.ConditionalLimits.product_identity line 647
84. lemma OAI.Rokhlin.ConditionalProducts.kernel_ae_eq_of_boxes line 681
85. lemma OAI.Rokhlin.ConditionalProducts.condDistrib_product_of_indicator line 711
86. lemma OAI.Rokhlin.ConditionalPullback.indicator line 738
87. lemma OAI.Rokhlin.ArrayObjects.Object.indicator_product line 760
88. lemma OAI.Rokhlin.InverseSystems.comap_array_path line 803
89. lemma OAI.Rokhlin.InverseSystems.comap_array_path_mono line 814
90. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.stage_indicator_product line 836
91. def OAI.Rokhlin.ArrayObjects.Object.Tower.parameterFiltration line 869
92. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.parameterFiltration_iSup line 876
93. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.proj_bond line 882
94. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.indicator_box line 887
95. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.limit_indicator_product line 898
96. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.conditional_observation line 955
97. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.parameter_plane_preserving line 994
98. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.conditional line 1006
99. def OAI.Rokhlin.ArrayObjects.Object.Tower.limit line 1057
100. def OAI.Rokhlin.ArrayObjects.Object.Tower.projection line 1077
101. structure OAI.Rokhlin.ArrayObjects.Object.Test line 1096
102. def OAI.Rokhlin.ArrayObjects.Object.Test.pull line 1104
103. def OAI.Rokhlin.ArrayObjects.Object.Test.energy line 1107
104. lemma OAI.Rokhlin.ArrayObjects.Object.Test.energy_pull_le line 1109
105. lemma OAI.Rokhlin.ArrayObjects.Object.Test.energy_mono line 1113
106. lemma OAI.Rokhlin.ArrayObjects.Object.Test.pull_comp line 1116
107. lemma OAI.Rokhlin.ArrayObjects.Object.Test.exists_near_max line 1121
108. lemma OAI.Rokhlin.eq_of_finite_stage_Lp line 1142
109. lemma OAI.Rokhlin.ArrayObjects.Object.Extension.ext line 1196
110. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.projection_step line 1202
111. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.projection_fields_mono line 1208
112. lemma OAI.Rokhlin.ArrayObjects.Object.Tower.projection_fields_generate line 1214
113. def OAI.Rokhlin.ArrayObjects.Object.Saturating.origin line 1228
114. def OAI.Rokhlin.ArrayObjects.Object.Saturating.testIndex line 1229
115. lemma OAI.Rokhlin.ArrayObjects.Object.Saturating.origin_le line 1230
116. lemma OAI.Rokhlin.ArrayObjects.Object.Saturating.origin_pair line 1232
117. lemma OAI.Rokhlin.ArrayObjects.Object.Saturating.testIndex_pair line 1234
118. instance OAI.Rokhlin.ArrayObjects.Object.Saturating.(instance at line 1237) line 1237
119. def OAI.Rokhlin.ArrayObjects.Object.Saturating.keys line 1238
120. lemma OAI.Rokhlin.ArrayObjects.Object.Saturating.keys_surjective line 1240
121. def OAI.Rokhlin.ArrayObjects.Object.Saturating.dense line 1243
122. lemma OAI.Rokhlin.ArrayObjects.Object.Saturating.dense_range line 1245
123. def OAI.Rokhlin.ArrayObjects.Object.Saturating.listed line 1248
124. lemma OAI.Rokhlin.ArrayObjects.Object.Saturating.listed_key line 1252
125. structure OAI.Rokhlin.ArrayObjects.Object.Saturating.Bank line 1258
126. def OAI.Rokhlin.ArrayObjects.Object.Saturating.Bank.seed line 1263
127. def OAI.Rokhlin.ArrayObjects.Object.Saturating.Bank.focus line 1266
128. def OAI.Rokhlin.ArrayObjects.Object.Saturating.Bank.nextObj line 1269
129. def OAI.Rokhlin.ArrayObjects.Object.Saturating.Bank.nextMap line 1272
130. lemma OAI.Rokhlin.ArrayObjects.Object.Saturating.Bank.near line 1275
131. def OAI.Rokhlin.ArrayObjects.Object.Saturating.Bank.next line 1280
132. def OAI.Rokhlin.ArrayObjects.Object.Saturating.sequence line 1285
133. abbrev OAI.Rokhlin.ArrayObjects.Object.Saturating.tower line 1289
134. lemma OAI.Rokhlin.ArrayObjects.Object.Saturating.tests_birth line 1293
135. lemma OAI.Rokhlin.ArrayObjects.Object.Saturating.tests_transport line 1299
136. lemma OAI.Rokhlin.ArrayObjects.Object.Saturating.tests_limit line 1304
137. lemma OAI.Rokhlin.ArrayObjects.Object.Saturating.listed_maximal line 1312
138. lemma OAI.Rokhlin.ArrayObjects.Object.Saturating.listed_project_eq line 1341
139. lemma OAI.Rokhlin.ArrayObjects.Object.Saturating.finite_stage_project_eq line 1350
140. lemma OAI.Rokhlin.ArrayObjects.Object.Saturating.tower_saturated line 1365
141. theorem OAI.Rokhlin.ArrayObjects.Object.Saturating.exists_saturated_extension line 1380