OAI/Dynamics/MultipleMixing/HilbertCodes.lean

GitHub source file

186 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Rokhlin.timeMap line 20

    Also declared: ComparatorChallenges/Rokhlin.lean:12 (same declaration text).

  2. def OAI.Rokhlin.IsMixing line 23

    Also declared: ComparatorChallenges/Rokhlin.lean:15 (same declaration text).

  3. def OAI.Rokhlin.layoutTime line 28

    Also declared: ComparatorChallenges/Rokhlin.lean:20 (same declaration text).

  4. def OAI.Rokhlin.MixingOfOrder line 31

    Also declared: ComparatorChallenges/Rokhlin.lean:23 (same declaration text).

  5. theorem OAI.Rokhlin.rectangle_square_identities line 48
  6. def OAI.Rokhlin.HasEssentialTotalRange line 93
  7. theorem OAI.Rokhlin.HasEssentialTotalRange.cancel_left line 97
  8. theorem OAI.Rokhlin.essentially_constant_of_intertwining line 111
  9. theorem OAI.Rokhlin.HasEssentialTotalRange.eq_zero_of_adjoint_ae_eq_zero line 138
  10. theorem OAI.Rokhlin.fixed_source_square_injective line 149
  11. theorem OAI.Rokhlin.essentially_constant_right_of_intertwining line 167
  12. theorem OAI.Rokhlin.fixed_ends_of_product_intertwining line 193
  13. theorem OAI.Rokhlin.denseRange_iff_adjoint_injective line 214
  14. theorem OAI.Rokhlin.exists_unitary_of_selfAdjoint_square line 221
  15. def OAI.Rokhlin.operatorAbs line 238
  16. theorem OAI.Rokhlin.operatorAbs_nonneg line 241
  17. theorem OAI.Rokhlin.operatorAbs_sq line 244
  18. theorem OAI.Rokhlin.operatorAbs_injective line 249
  19. theorem OAI.Rokhlin.exists_unitary_polar line 257
  20. def OAI.Rokhlin.intertwinerAlgebra line 271
  21. instance OAI.Rokhlin.intertwinerAlgebra_isClosed line 294
  22. theorem OAI.Rokhlin.sqrt_intertwines line 302
  23. theorem OAI.Rokhlin.eq_of_comp_eq_of_denseRange line 324
  24. theorem OAI.Rokhlin.operatorAbs_denseRange line 331
  25. theorem OAI.Rokhlin.polar_rectangle line 337
  26. def OAI.Rokhlin.HasFixedInjectiveSquares line 397
  27. theorem OAI.Rokhlin.hasFixedInjectiveSquares_of_fixed line 403
  28. theorem OAI.Rokhlin.fixed_squares_of_product_identities line 416
  29. lemma OAI.Rokhlin.timeMap_zero line 470
  30. lemma OAI.Rokhlin.timeMap_add line 472
  31. lemma OAI.Rokhlin.timeMap_nat line 474
  32. lemma OAI.Rokhlin.timeMap_neg_nat line 476
  33. lemma OAI.Rokhlin.timeMap_preserving line 479
  34. lemma OAI.Rokhlin.timeMap_measurable line 484
  35. lemma OAI.Rokhlin.timeMap_comm line 488
  36. lemma OAI.Rokhlin.timeMap_inv_apply line 492
  37. lemma OAI.Rokhlin.reverse_tail_pairing_along line 504
  38. lemma OAI.Rokhlin.integral_tail_replacement line 526
  39. def OAI.Rokhlin.hilbertTestAlgebra line 569
  40. lemma OAI.Rokhlin.hilbertTestAlgebra_algebra line 571
  41. lemma OAI.Rokhlin.hilbertTestAlgebra_countable line 574
  42. lemma OAI.Rokhlin.hilbertTestAlgebra_generates line 577
  43. lemma OAI.Rokhlin.hilbertTestAlgebra_measurable line 580
  44. lemma OAI.Rokhlin.hilbertTestAlgebra_dense line 584
  45. abbrev OAI.Rokhlin.HilbertTestKey line 623
  46. instance OAI.Rokhlin.(instance at line 626) line 626
  47. def OAI.Rokhlin.hilbertTestFunction line 630
  48. lemma OAI.Rokhlin.hilbertTestFunction_measurable line 634
  49. def OAI.Rokhlin.hilbertTestVector line 644
  50. lemma OAI.Rokhlin.hilbertTestVector_append line 648
  51. lemma OAI.Rokhlin.rationalComplex_dense line 652
  52. lemma OAI.Rokhlin.hilbertTestVector_dense line 662
  53. def OAI.Rokhlin.IsDistanceCode line 708
  54. lemma OAI.Rokhlin.distance_isCode line 714
  55. lemma OAI.Rokhlin.IsDistanceCode.exists_eq line 724
  56. lemma OAI.Rokhlin.distance_code_injective line 752
  57. lemma OAI.Rokhlin.isDistanceCode_iff line 760
  58. lemma OAI.Rokhlin.measurableSet_distanceCode line 773
  59. lemma OAI.Rokhlin.hilbertTestVector_coe line 796
  60. def OAI.Rokhlin.hilbertTestKeys line 815
  61. lemma OAI.Rokhlin.hilbertTestKeys_surjective line 816
  62. def OAI.Rokhlin.hilbertTests line 819
  63. lemma OAI.Rokhlin.hilbertTests_dense line 821
  64. lemma OAI.Rokhlin.hilbertTestVector_dist line 834
  65. lemma OAI.Rokhlin.hilbertTests_dist_measurable line 854
  66. def OAI.Rokhlin.HilbertCode line 873
  67. instance OAI.Rokhlin.(instance at line 876) line 876
  68. instance OAI.Rokhlin.(instance at line 877) line 877
  69. def OAI.Rokhlin.HilbertCode.base line 883
  70. def OAI.Rokhlin.HilbertCode.code line 884
  71. lemma OAI.Rokhlin.HilbertCode.measurable_base line 885
  72. lemma OAI.Rokhlin.HilbertCode.measurable_code line 886
  73. def OAI.Rokhlin.HilbertCode.decode line 889
  74. lemma OAI.Rokhlin.HilbertCode.decode_dist line 890
  75. def OAI.Rokhlin.HilbertCode.encode line 893
  76. lemma OAI.Rokhlin.HilbertCode.decode_encode line 895
  77. lemma OAI.Rokhlin.HilbertCode.encode_decode line 900
  78. def OAI.Rokhlin.HilbertCode.approxIndex line 906
  79. lemma OAI.Rokhlin.HilbertCode.approxIndex_spec line 907
  80. lemma OAI.Rokhlin.HilbertCode.measurable_approxIndex line 912
  81. def OAI.Rokhlin.HilbertCode.approximant line 917
  82. lemma OAI.Rokhlin.HilbertCode.measurable_approximant line 920
  83. def OAI.Rokhlin.HilbertCode.representative line 925
  84. lemma OAI.Rokhlin.HilbertCode.measurable_representative line 927
  85. lemma OAI.Rokhlin.HilbertCode.representative_eq_decode line 930
  86. lemma OAI.Rokhlin.lp_dist_of_representatives line 972
  87. def OAI.Rokhlin.HilbertCode.distance line 988
  88. lemma OAI.Rokhlin.HilbertCode.distance_encode line 992
  89. lemma OAI.Rokhlin.HilbertCode.measurable_distance line 999
  90. lemma OAI.Rokhlin.measurable_hilbert_encode line 1014
  91. def OAI.Rokhlin.RayCanonical line 1042
  92. lemma OAI.Rokhlin.exists_inner_ne_zero_of_dense line 1046
  93. lemma OAI.Rokhlin.exists_rayCanonical line 1054
  94. lemma OAI.Rokhlin.rayCanonical_unique line 1078
  95. lemma OAI.Rokhlin.borel_injective_cover_branches line 1120
  96. def OAI.Rokhlin.HilbertCode.coefficient line 1143
  97. lemma OAI.Rokhlin.HilbertCode.coefficient_eq line 1146
  98. lemma OAI.Rokhlin.HilbertCode.measurable_coefficient line 1156
  99. def OAI.Rokhlin.HilbertCode.IsCanonical line 1164
  100. lemma OAI.Rokhlin.HilbertCode.measurableSet_isCanonical line 1166
  101. def OAI.Rokhlin.HilbertCode.IsUnimodular line 1176
  102. lemma OAI.Rokhlin.HilbertCode.measurableSet_isUnimodular line 1179
  103. lemma OAI.Rokhlin.HilbertCode.norm_decode_eq_one line 1185
  104. lemma OAI.Rokhlin.HilbertCode.distance_le_codes line 1192
  105. theorem OAI.Rokhlin.exact_mean_dichotomy line 1217
  106. theorem OAI.Rokhlin.exact_tuple_mean_equations line 1253
  107. theorem OAI.Rokhlin.ae_eq_mean_of_norm_mean_eq_one line 1280
  108. theorem OAI.Rokhlin.exact_tuple_dichotomy line 1288
  109. theorem OAI.Rokhlin.exact_quotient_dichotomy line 1302
  110. lemma OAI.Rokhlin.HilbertCode.inner_decode line 1354
  111. lemma OAI.Rokhlin.HilbertCode.eq_of_decode_smul line 1370
  112. lemma OAI.Rokhlin.HilbertCode.distance_ge_one_of_orthogonal line 1391
  113. lemma OAI.Rokhlin.HilbertCode.ae_norm_representative_comp line 1418
  114. lemma OAI.Rokhlin.HilbertCode.ae_norm_prod_representative line 1426
  115. lemma OAI.Rokhlin.HilbertCode.code_tuple_quotient line 1432
  116. lemma OAI.Rokhlin.HilbertCode.exact_codes_dichotomy line 1459
  117. lemma OAI.Rokhlin.HilbertCode.separated_branches line 1500
  118. def OAI.Rokhlin.exactCodeMean line 1540
  119. lemma OAI.Rokhlin.measurable_exactCodeMean line 1544
  120. def OAI.Rokhlin.exactCodeSet line 1557
  121. lemma OAI.Rokhlin.measurableSet_exactCodeSet line 1564
  122. abbrev OAI.Rokhlin.ExactCodeTuple line 1584
  123. lemma OAI.Rokhlin.exactCodeTuple_branches line 1586
  124. lemma OAI.Rokhlin.measurable_branch_sections line 1620
  125. lemma OAI.Rokhlin.measurableSet_branched_relation line 1645
  126. abbrev OAI.Rokhlin.RationalSpanKey line 1671
  127. def OAI.Rokhlin.rationalSpanTest line 1672
  128. lemma OAI.Rokhlin.rationalSpanTest_append line 1675
  129. lemma OAI.Rokhlin.closure_rationalSpanTest line 1679
  130. def OAI.Rokhlin.HilbertCode.atBase line 1722
  131. lemma OAI.Rokhlin.HilbertCode.encode_atBase line 1723
  132. def OAI.Rokhlin.MeasurableSection line 1729
  133. lemma OAI.Rokhlin.MeasurableSection.zero line 1732
  134. lemma OAI.Rokhlin.MeasurableSection.add line 1737
  135. lemma OAI.Rokhlin.MeasurableSection.smul line 1755
  136. lemma OAI.Rokhlin.MeasurableSection.rationalSpanTest line 1770
  137. lemma OAI.Rokhlin.measurableSet_section_mem_span line 1777
  138. lemma OAI.Rokhlin.exactCode_sections line 1809
  139. lemma OAI.Rokhlin.measurableSet_exactCodeSlot line 1841
  140. lemma OAI.Rokhlin.circle_memLp line 1869
  141. def OAI.Rokhlin.circleLp line 1874
  142. lemma OAI.Rokhlin.circleLp_coe line 1877
  143. lemma OAI.Rokhlin.circleLp_congr line 1880
  144. lemma OAI.Rokhlin.circleLp_norm line 1886
  145. lemma OAI.Rokhlin.circleLp_ne_zero line 1894
  146. lemma OAI.Rokhlin.circleLp_inner line 1900
  147. lemma OAI.Rokhlin.circleLp_phase line 1910
  148. lemma OAI.Rokhlin.normalized_exact_codes line 1930
  149. def OAI.Rokhlin.circleOfValue line 1984
  150. lemma OAI.Rokhlin.circleOfValue_coe line 1990
  151. lemma OAI.Rokhlin.measurable_circleOfValue line 1994
  152. def OAI.Rokhlin.HilbertCode.circleRep line 2006
  153. lemma OAI.Rokhlin.HilbertCode.circleRep_coe line 2007
  154. lemma OAI.Rokhlin.HilbertCode.measurable_circleRep line 2011
  155. lemma OAI.Rokhlin.HilbertCode.measurable_circleRep_fixed line 2013
  156. lemma OAI.Rokhlin.HilbertCode.circleRep_ae line 2018
  157. lemma OAI.Rokhlin.HilbertCode.circleLp_circleRep line 2021
  158. lemma OAI.Rokhlin.exactCode_circle_tuple line 2029
  159. abbrev OAI.Rokhlin.HilbertCode.UnitCode line 2062
  160. lemma OAI.Rokhlin.HilbertCode.unitCode_exists_coefficient line 2064
  161. def OAI.Rokhlin.HilbertCode.firstCoefficient line 2069
  162. lemma OAI.Rokhlin.HilbertCode.measurable_firstCoefficient line 2070
  163. def OAI.Rokhlin.HilbertCode.unitPhase line 2074
  164. lemma OAI.Rokhlin.HilbertCode.measurable_unitPhase line 2076
  165. lemma OAI.Rokhlin.HilbertCode.unitPhase_norm line 2083
  166. lemma OAI.Rokhlin.HilbertCode.unitPhase_canonical line 2088
  167. def OAI.Rokhlin.HilbertCode.normalizeUnit line 2103
  168. lemma OAI.Rokhlin.HilbertCode.normalizeUnit_base line 2105
  169. lemma OAI.Rokhlin.HilbertCode.normalizeUnit_canonical line 2106
  170. lemma OAI.Rokhlin.HilbertCode.normalizeUnit_representative line 2111
  171. lemma OAI.Rokhlin.HilbertCode.normalizeUnit_unimodular line 2122
  172. lemma OAI.Rokhlin.HilbertCode.measurable_normalizeUnit line 2126
  173. def OAI.Rokhlin.HilbertCode.transportRaw line 2137
  174. lemma OAI.Rokhlin.HilbertCode.transportRaw_base line 2141
  175. lemma OAI.Rokhlin.HilbertCode.transportRaw_representative line 2144
  176. lemma OAI.Rokhlin.HilbertCode.transportRaw_unimodular line 2153
  177. lemma OAI.Rokhlin.HilbertCode.measurable_circleRep_comp line 2158
  178. lemma OAI.Rokhlin.HilbertCode.measurable_transportRaw line 2166
  179. def OAI.Rokhlin.HilbertCode.transport line 2178
  180. lemma OAI.Rokhlin.HilbertCode.transport_base line 2181
  181. lemma OAI.Rokhlin.HilbertCode.transport_canonical line 2183
  182. lemma OAI.Rokhlin.HilbertCode.transport_unimodular line 2185
  183. lemma OAI.Rokhlin.HilbertCode.measurable_transport line 2187
  184. lemma OAI.Rokhlin.HilbertCode.transport_representative line 2191
  185. lemma OAI.Rokhlin.HilbertCode.transport_inverse line 2204
  186. lemma OAI.Rokhlin.exactCode_transport line 2233