OAI/Dynamics/MultipleMixing/FibreMeasures.lean

GitHub source file

148 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Rokhlin.BorelFibreEnumeration line 15
  2. def OAI.Rokhlin.BorelFibreEnumeration.indexDomain line 26
  3. lemma OAI.Rokhlin.BorelFibreEnumeration.measurable_indexDomain line 28
  4. instance OAI.Rokhlin.BorelFibreEnumeration.(instance at line 33) line 33
  5. def OAI.Rokhlin.BorelFibreEnumeration.point line 35
  6. lemma OAI.Rokhlin.BorelFibreEnumeration.measurable_point line 37
  7. lemma OAI.Rokhlin.BorelFibreEnumeration.injective_point line 43
  8. lemma OAI.Rokhlin.BorelFibreEnumeration.measurableEmbedding_point line 52
  9. def OAI.Rokhlin.BorelFibreEnumeration.indexMeasure line 55
  10. instance OAI.Rokhlin.BorelFibreEnumeration.indexMeasure_sigmaFinite line 58
  11. def OAI.Rokhlin.BorelFibreEnumeration.measure line 64
  12. instance OAI.Rokhlin.BorelFibreEnumeration.measure_sigmaFinite line 65
  13. lemma OAI.Rokhlin.BorelFibreEnumeration.ae_mem line 68
  14. lemma OAI.Rokhlin.BorelFibreEnumeration.lintegral_measure line 72
  15. lemma OAI.Rokhlin.separated_family_enumeration line 100
  16. def OAI.Rokhlin.BorelFibreEnumeration.fibreEquiv line 118
  17. lemma OAI.Rokhlin.BorelFibreEnumeration.sum_sections line 130
  18. lemma OAI.Rokhlin.BorelFibreEnumeration.measurePreserving_fibrewise line 139
  19. lemma OAI.Rokhlin.exactCode_enumeration line 177
  20. def OAI.Rokhlin.exactFibreSlotEquiv line 187
  21. lemma OAI.Rokhlin.exactCounting_slot_preserving line 208
  22. def OAI.Rokhlin.exactSquareSet line 236
  23. lemma OAI.Rokhlin.measurableSet_exactSquareSet line 241
  24. lemma OAI.Rokhlin.exactSquare_unique_cell line 259
  25. lemma OAI.Rokhlin.exactSquare_separated line 272
  26. lemma OAI.Rokhlin.exactSquare_enumeration line 288
  27. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rawExactSquare line 336
  28. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawSquare_row_completion line 340
  29. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawSquare_column_completion line 372
  30. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawSquare_row_bijective line 402
  31. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawSquare_col_bijective line 430
  32. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawCounting_rows_preserving line 458
  33. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawCounting_columns_preserving line 477
  34. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawCounting_coordinate_preserving line 498
  35. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.exists_raw_counting_data line 514
  36. def OAI.Rokhlin.BorelFibreEnumeration.comapBase line 557
  37. lemma OAI.Rokhlin.BorelFibreEnumeration.ae_base line 567
  38. lemma OAI.Rokhlin.BorelFibreEnumeration.comapBase_preserving line 576
  39. lemma OAI.Rokhlin.BorelFibreEnumeration.lintegral_indicator_kernel line 585
  40. lemma OAI.Rokhlin.BorelFibreEnumeration.parameter_conditional line 591
  41. lemma OAI.Rokhlin.ConditionalTransport.with_observation line 650
  42. lemma OAI.Rokhlin.ConditionalTransport.map_observation line 672
  43. lemma OAI.Rokhlin.BorelFibreEnumeration.parameter_conditional_of_fibrewise line 686
  44. def OAI.Rokhlin.Kernel.depMap line 715
  45. instance OAI.Rokhlin.Kernel.depMap_sfinite line 718
  46. lemma OAI.Rokhlin.Kernel.depMap_markov line 723
  47. lemma OAI.Rokhlin.Kernel.depMap_apply line 728
  48. lemma OAI.Rokhlin.Kernel.depMap_comap line 736
  49. lemma OAI.Rokhlin.Kernel.depMap_prod line 746
  50. abbrev OAI.Rokhlin.ArrayObjects.Object.Rolled.RawLabel line 769
  51. abbrev OAI.Rokhlin.ArrayObjects.Object.Rolled.RawLabelTuple line 770
  52. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rawLabelSlot line 772
  53. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_rawLabelSlot line 776
  54. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rawMatchedLabel line 780
  55. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_rawMatchedLabel line 783
  56. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rawLabelTransition line 794
  57. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawLabelTransition_markov line 798
  58. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawCounting_parameter_given_label line 806
  59. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawCounting_label_transition line 838
  60. lemma OAI.Rokhlin.BorelFibreEnumeration.observation_conditional line 870
  61. lemma OAI.Rokhlin.BorelFibreEnumeration.observation_conditional_of_fibrewise line 933
  62. abbrev OAI.Rokhlin.ArrayObjects.Object.Rolled.RawLabelSquare line 962
  63. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rawLabelRow line 963
  64. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_rawLabelRow line 965
  65. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rawLabelColumn line 969
  66. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_rawLabelColumn line 972
  67. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawCounting_parameter_pair_given_row line 977
  68. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawCounting_target_pair_given_row line 1004
  69. lemma OAI.Rokhlin.SigmaFiniteConditional.sigmaFinite_trim line 1075
  70. lemma OAI.Rokhlin.SigmaFiniteConditional.condExp_of_kernel line 1080
  71. lemma OAI.Rokhlin.JoiningOperator.operator_ae_eq_condExp_integrable line 1126
  72. lemma OAI.Rokhlin.JoiningOperator.screened_operator_integrable line 1141
  73. theorem OAI.Rokhlin.JoiningOperator.screened_operator_sigmaFinite line 1163
  74. lemma OAI.Rokhlin.JoiningOperator.product_operator_inner_integrable line 1190
  75. lemma OAI.Rokhlin.JoiningOperator.indicator_integrable line 1251
  76. theorem OAI.Rokhlin.JoiningOperator.product_operator line 1257
  77. lemma OAI.Rokhlin.JoiningOperator.operator_congr line 1295
  78. lemma OAI.Rokhlin.JoiningOperator.square_operator line 1303
  79. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawLabel_cell_commute line 1344
  80. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawCounting_square_operator line 1349
  81. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.ownKernel_tuple_time_preserving line 1382
  82. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rawLabelTime line 1391
  83. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rawLabelTimeInv line 1393
  84. def OAI.Rokhlin.ArrayObjects.Object.Rolled.rawLabelTupleTime line 1395
  85. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_rawLabelTime line 1399
  86. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_rawLabelTimeInv line 1404
  87. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_rawLabelTupleTime line 1409
  88. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.localGraph_time_equiv line 1415
  89. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawCounting_time_preserving line 1444
  90. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawTupleCounting_time_preserving line 1459
  91. lemma OAI.Rokhlin.lp_time_inverse line 1480
  92. def OAI.Rokhlin.aeLpTime line 1487
  93. lemma OAI.Rokhlin.aeLpTime_coe line 1491
  94. lemma OAI.Rokhlin.inverse_measurePreserving line 1497
  95. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.localGraph_code_properties line 1515
  96. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawLabelTime_left_inverse line 1535
  97. lemma OAI.Rokhlin.JoiningOperator.operator_time_conjugate line 1558
  98. lemma OAI.Rokhlin.JoiningOperator.operator_commutes_time line 1566
  99. theorem OAI.Rokhlin.partial_unitary_algebra line 1585
  100. theorem OAI.Rokhlin.partial_unitary_range line 1605
  101. theorem OAI.Rokhlin.partial_unitary_range_adjoint line 1618
  102. theorem OAI.Rokhlin.partial_unitary_norm_on_range line 1634
  103. theorem OAI.Rokhlin.countable_essential_image_of_countable_fibres line 1648
  104. theorem OAI.Rokhlin.deterministic_transition_of_norm_eq line 1673
  105. lemma OAI.Rokhlin.partial_unitary_fixed line 1693
  106. lemma OAI.Rokhlin.partial_unitary_fixed' line 1699
  107. lemma OAI.Rokhlin.partial_unitary_closed_range line 1706
  108. def OAI.Rokhlin.partialUnitary line 1715
  109. def OAI.Rokhlin.commutingRangeUnitary line 1726
  110. lemma OAI.Rokhlin.partialUnitary_commutingRange line 1742
  111. abbrev OAI.Rokhlin.LabelOrbitVector line 1754
  112. def OAI.Rokhlin.labelShiftFirst line 1756
  113. def OAI.Rokhlin.labelShiftSecond line 1764
  114. def OAI.Rokhlin.labelOrbitLP line 1776
  115. def OAI.Rokhlin.labelOrbit line 1777
  116. lemma OAI.Rokhlin.measurable_labelOrbit line 1778
  117. lemma OAI.Rokhlin.labelOrbitLP_first line 1781
  118. lemma OAI.Rokhlin.labelOrbitLP_second line 1787
  119. lemma OAI.Rokhlin.labelOrbit_transition line 1796
  120. lemma OAI.Rokhlin.labelOrbit_time line 1807
  121. lemma OAI.Rokhlin.labelOrbit_zero line 1818
  122. lemma OAI.Rokhlin.exists_positive_memLp_two line 1827
  123. lemma OAI.Rokhlin.JoiningOperator.operator_integral_representative line 1861
  124. lemma OAI.Rokhlin.JoiningOperator.kernel_integrable line 1878
  125. lemma OAI.Rokhlin.JoiningOperator.exists_positive_range_vector line 1888
  126. lemma OAI.Rokhlin.JoiningOperator.deterministic_on_range line 1915
  127. lemma OAI.Rokhlin.JoiningOperator.exists_orbit_vector line 1930
  128. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.parameterLaw_proper line 1962
  129. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.parameter_pair_preserving line 1973
  130. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawCounting_target_parameter_independent line 1998
  131. lemma OAI.Rokhlin.BorelFibreEnumeration.ae_fibre_all line 2045
  132. lemma OAI.Rokhlin.countable_orbit_image line 2073
  133. lemma OAI.Rokhlin.JoiningOperator.partial_unitary_of_squares_aux line 2099
  134. lemma OAI.Rokhlin.JoiningOperator.partial_unitary_of_squares line 2109
  135. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawCounting_partial_unitary line 2138
  136. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rawCounting_exists_orbit line 2148
  137. def OAI.Rokhlin.BorelFibreEnumeration.restrictGraph line 2185
  138. lemma OAI.Rokhlin.BorelFibreEnumeration.restrictGraph_mass line 2196
  139. lemma OAI.Rokhlin.BorelFibreEnumeration.ae_finite_fibres line 2212
  140. lemma OAI.Rokhlin.BorelFibreEnumeration.ae_finite_level line 2235
  141. def OAI.Rokhlin.positiveLevels line 2250
  142. lemma OAI.Rokhlin.positiveLevels_countable line 2253
  143. lemma OAI.Rokhlin.ae_mem_positiveLevels line 2263
  144. lemma OAI.Rokhlin.joining_transport_invariant line 2275
  145. lemma OAI.Rokhlin.positiveLevel_mass_transport line 2286
  146. def OAI.Rokhlin.positiveLevelsEquiv line 2295
  147. lemma OAI.Rokhlin.finite_positive_level_mass line 2313
  148. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.exists_raw_finite_levels line 2352