OAI/Dynamics/MultipleMixing/Tensors.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Rokhlin.memLp_tensor line 16
  2. def OAI.Rokhlin.tensorLp line 26
  3. lemma OAI.Rokhlin.coe_tensorLp line 30
  4. lemma OAI.Rokhlin.tensorLp_inner line 34
  5. lemma OAI.Rokhlin.tensorLp_norm line 43
  6. lemma OAI.Rokhlin.tensorLp_add_left line 52
  7. lemma OAI.Rokhlin.tensorLp_smul_left line 64
  8. lemma OAI.Rokhlin.tensorLp_add_right line 76
  9. lemma OAI.Rokhlin.tensorLp_smul_right line 88
  10. def OAI.Rokhlin.JoiningOperator.contraction line 111
  11. lemma OAI.Rokhlin.JoiningOperator.contraction_norm_le line 116
  12. lemma OAI.Rokhlin.JoiningOperator.contraction_inner line 125
  13. lemma OAI.Rokhlin.JoiningOperator.contraction_integrand line 138
  14. lemma OAI.Rokhlin.JoiningOperator.family_weight_integrable line 152
  15. lemma OAI.Rokhlin.JoiningOperator.contraction_integral line 164
  16. lemma OAI.Rokhlin.JoiningOperator.contraction_projection line 196
  17. lemma OAI.Rokhlin.tensorLp_indicator line 220
  18. lemma OAI.Rokhlin.dense_tensorLp line 238
  19. lemma OAI.Rokhlin.closure_tensor_image line 265
  20. lemma OAI.Rokhlin.restricted_contractions_span line 289
  21. lemma OAI.Rokhlin.JoiningOperator.contraction_swap line 331
  22. lemma OAI.Rokhlin.JoiningOperator.contraction_projection_both line 344
  23. lemma OAI.Rokhlin.JoiningOperator.active_eq_essentialRange_product line 365
  24. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.commonActive_swapColumns line 392
  25. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.commonActive_swapRows line 399
  26. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_first_row_edge line 406
  27. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_second_row_edge line 422
  28. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_row_contraction_projection line 437
  29. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_first_column_edge line 472
  30. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_second_column_edge line 488
  31. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_column_contraction_projection line 503
  32. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.rowActive_eq_range line 549
  33. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.columnActive_eq_range line 569
  34. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_row_contractions_span line 589
  35. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_column_contractions_span line 608
  36. lemma OAI.Rokhlin.JoiningOperator.contraction_coefficient line 644
  37. lemma OAI.Rokhlin.JoiningOperator.tensor_pull line 685
  38. lemma OAI.Rokhlin.JoiningOperator.contraction_pull line 696
  39. lemma OAI.Rokhlin.JoiningOperator.contraction_mem_screen line 706
  40. lemma OAI.Rokhlin.measure_eq_graph_of_ratio line 735
  41. def OAI.Rokhlin.ratioKernel line 751
  42. lemma OAI.Rokhlin.ratioKernel_apply line 754
  43. instance OAI.Rokhlin.ratioKernel_markov line 764
  44. lemma OAI.Rokhlin.hasCondDistrib_ratio line 772
  45. lemma OAI.Rokhlin.JoiningOperator.mem_field_of_eq_comp line 799
  46. lemma OAI.Rokhlin.JoiningOperator.common_space_le_screen line 809
  47. lemma OAI.Rokhlin.JoiningOperator.common_space_le_ratio line 833
  48. lemma OAI.Rokhlin.JoiningOperator.contraction_mem_operatorField line 872
  49. lemma OAI.Rokhlin.JoiningOperator.common_space_le_operatorField line 891
  50. lemma OAI.Rokhlin.MeasurablePolar.fixed_factor line 926
  51. lemma OAI.Rokhlin.JoiningOperator.common_space_le_polarField line 959
  52. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_polar_a_field line 988
  53. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.grouped_polar_b_field line 1037
  54. lemma OAI.Rokhlin.lpMeas_comap_congr line 1094
  55. lemma OAI.Rokhlin.lpMeas_comap_mono line 1111
  56. lemma OAI.Rokhlin.comap_eq_of_measurable_leftInverse line 1123
  57. lemma OAI.Rokhlin.StrongUnitary.comap_normalizeA line 1142
  58. lemma OAI.Rokhlin.StrongUnitary.comap_normalizeB line 1157
  59. lemma OAI.Rokhlin.StrongUnitary.measurable_of_eigenvalues line 1181
  60. lemma OAI.Rokhlin.StrongUnitary.measurable_iff_eigenCoords line 1205
  61. lemma OAI.Rokhlin.StrongUnitary.comap_eigenCoords line 1228
  62. def OAI.Rokhlin.StrongUnitary.subgroupVersion line 1246
  63. lemma OAI.Rokhlin.StrongUnitary.measurable_subgroupVersion line 1251
  64. lemma OAI.Rokhlin.StrongUnitary.subgroupVersion_coe line 1257
  65. def OAI.Rokhlin.StrongUnitary.spectralCoords line 1260
  66. lemma OAI.Rokhlin.StrongUnitary.measurable_spectralCoords line 1264
  67. lemma OAI.Rokhlin.StrongUnitary.spectralCoords_mul_inv line 1270
  68. lemma OAI.Rokhlin.StrongUnitary.lpMeas_spectralCoords line 1280
  69. lemma OAI.Rokhlin.exists_const_of_ae_prod_eq line 1298
  70. lemma OAI.Rokhlin.measurable_conull_subset line 1310
  71. lemma OAI.Rokhlin.exists_measurable_common_unitary line 1322
  72. lemma OAI.Rokhlin.StrongUnitary.rectangle_ratio_eq line 1356
  73. lemma OAI.Rokhlin.StrongUnitary.measurable_corner_ratio line 1366
  74. lemma OAI.Rokhlin.ConditionalFibres.ae_of_ae_kernel line 1413
  75. lemma OAI.Rokhlin.StrongUnitary.spectral_corner line 1433
  76. lemma OAI.Rokhlin.MeasurablePolarRectangle.torus_coordinates line 1527
  77. def OAI.Rokhlin.characterAlgebra line 1619
  78. lemma OAI.Rokhlin.characterAlgebra_span line 1638
  79. lemma OAI.Rokhlin.dense_character_span line 1644
  80. def OAI.Rokhlin.torusWordCircle line 1664
  81. def OAI.Rokhlin.circleMapComplex line 1667
  82. def OAI.Rokhlin.torusWord line 1672
  83. lemma OAI.Rokhlin.torusWord_star line 1675
  84. lemma OAI.Rokhlin.torusWord_of line 1681
  85. lemma OAI.Rokhlin.torusWord_dense line 1687
  86. lemma OAI.Rokhlin.dense_span_image line 1697
  87. lemma OAI.Rokhlin.dense_span_continuous_toLp line 1715
  88. lemma OAI.Rokhlin.torusWord_L2_dense line 1729
  89. lemma OAI.Rokhlin.torusWordCircle_of line 1737
  90. lemma OAI.Rokhlin.torusWordCircle_mul line 1742
  91. lemma OAI.Rokhlin.torusWordCircle_one line 1754
  92. lemma OAI.Rokhlin.torusWordCircle_inv line 1760
  93. def OAI.Rokhlin.torusCharacter line 1766
  94. lemma OAI.Rokhlin.torusWord_ratio line 1771
  95. lemma OAI.Rokhlin.torusWord_norm line 1778