OAI/Dynamics/MultipleMixing/OrbitCancellation.lean

GitHub source file

113 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Rokhlin.localProjectiveGroup line 17
  2. lemma OAI.Rokhlin.localProjectiveGroup_eq line 21
  3. def OAI.Rokhlin.localCodeEquivSlot line 37
  4. def OAI.Rokhlin.localCodeEquivGroup line 43
  5. lemma OAI.Rokhlin.localCodeEquivGroup_val line 51
  6. def OAI.Rokhlin.localProjectiveMatching line 57
  7. lemma OAI.Rokhlin.localProjectiveGroup_map line 79
  8. def OAI.Rokhlin.localProjectiveTransport line 94
  9. lemma OAI.Rokhlin.localProjectiveTransport_val line 98
  10. lemma OAI.Rokhlin.localProjectiveMatching_code line 109
  11. def OAI.Rokhlin.localGroupCode line 138
  12. lemma OAI.Rokhlin.localGroupCode_equiv line 142
  13. def OAI.Rokhlin.localGroupBlock line 152
  14. lemma OAI.Rokhlin.localGroupBlock_equiv line 155
  15. lemma OAI.Rokhlin.localProjectiveTransport_block line 162
  16. lemma OAI.Rokhlin.localProjectiveMatching_block line 183
  17. def OAI.Rokhlin.measurableCircleTime line 214
  18. lemma OAI.Rokhlin.measurableCircleTime_phase line 221
  19. def OAI.Rokhlin.projectiveTime line 231
  20. lemma OAI.Rokhlin.projectiveTime_apply line 235
  21. lemma OAI.Rokhlin.HilbertCode.projective_transport line 243
  22. lemma OAI.Rokhlin.exists_block_preserving_trivialization line 269
  23. lemma OAI.Rokhlin.exists_good_block_preserving_trivialization line 286
  24. lemma OAI.Rokhlin.exists_block_automorphism line 300
  25. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.localGraph_group_equiv line 333
  26. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.localGraph_matching_blocks line 350
  27. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.localGraph_time_blocks line 368
  28. lemma OAI.Rokhlin.localGroup_countable line 419
  29. lemma OAI.Rokhlin.localGroupBlock_symm line 431
  30. lemma OAI.Rokhlin.localGroupBlock_finite line 440
  31. lemma OAI.Rokhlin.localGroupBlock_nonempty line 459
  32. lemma OAI.Rokhlin.localBlock_card_le line 482
  33. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.exists_raw_finite_blocks line 535
  34. def OAI.Rokhlin.ArrayObjects.Object.Rolled.slotExact line 591
  35. def OAI.Rokhlin.ArrayObjects.Object.Rolled.slotExactSpan line 597
  36. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.slotExactSpan_closed line 600
  37. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.slotExactSpan_le_active line 603
  38. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.oneColumn_single_row line 618
  39. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.fullExact_subset_slot_row line 625
  40. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.transport_pair line 640
  41. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.slot_pair_on_square line 651
  42. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.slot_conditional_pairs line 672
  43. theorem OAI.Rokhlin.ArrayObjects.Object.Rolled.slot_conditional_exactness line 695
  44. def OAI.Rokhlin.ArrayObjects.Object.Rolled.unpadCell line 711
  45. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.measurable_unpadCell line 714
  46. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.unpad_pad line 717
  47. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.pad_unpad line 719
  48. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.slotExactSpan_le_codeSpan line 725
  49. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.codeSpan_le_slotExactSpan line 747
  50. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.slotExactSpan_eq_codeSpan line 768
  51. lemma OAI.Rokhlin.measurableSet_code_tests line 787
  52. lemma OAI.Rokhlin.code_tests_iff_range line 800
  53. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.slot_global_exactness line 816
  54. def OAI.Rokhlin.projectiveRep line 880
  55. lemma OAI.Rokhlin.projectiveRep_class line 883
  56. lemma OAI.Rokhlin.projectiveRep_one line 892
  57. def OAI.Rokhlin.projectiveCharacter line 894
  58. lemma OAI.Rokhlin.projectiveCharacter_measurable line 896
  59. lemma OAI.Rokhlin.projectiveCharacter_mul line 900
  60. lemma OAI.Rokhlin.projectiveCharacters_of_zero_mean line 914
  61. def OAI.Rokhlin.absoluteCoefficient line 933
  62. lemma OAI.Rokhlin.measurable_absoluteCoefficient line 936
  63. lemma OAI.Rokhlin.absoluteCoefficient_nonneg line 949
  64. lemma OAI.Rokhlin.absoluteCoefficient_le line 952
  65. lemma OAI.Rokhlin.norm_integral_mul_conj_of_phase line 961
  66. lemma OAI.Rokhlin.absoluteCoefficient_projective line 970
  67. lemma OAI.Rokhlin.absoluteCoefficient_encode_smul line 983
  68. lemma OAI.Rokhlin.inner_circle_toLp line 1003
  69. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.raw_exact_coefficient_zero line 1023
  70. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.slotExact_coefficient_zero line 1038
  71. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.slotActive_orthogonal_of_coefficients_zero line 1075
  72. lemma OAI.Rokhlin.JoiningOperator.correlation_zero_of_orthogonal line 1105
  73. lemma OAI.Rokhlin.ConditionalFibres.integral_integral_of_bound line 1128
  74. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.slot_product_zero line 1146
  75. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.raw_correlation_forces_coefficient line 1185
  76. def OAI.Rokhlin.BorelFibreEnumeration.sumFibreEquiv line 1228
  77. def OAI.Rokhlin.BorelFibreEnumeration.fibreSum line 1237
  78. lemma OAI.Rokhlin.BorelFibreEnumeration.measurable_fibreSum line 1240
  79. lemma OAI.Rokhlin.BorelFibreEnumeration.fibreSum_eq_tsum line 1247
  80. lemma OAI.Rokhlin.BorelFibreEnumeration.fibreSum_eq_finite_sum line 1252
  81. lemma OAI.Rokhlin.BorelFibreEnumeration.fibreSum_nonneg line 1259
  82. lemma OAI.Rokhlin.BorelFibreEnumeration.fibreSum_eq_zero_iff line 1267
  83. lemma OAI.Rokhlin.BorelFibreEnumeration.fibreSum_eq_sum_equiv line 1273
  84. lemma OAI.Rokhlin.BorelFibreEnumeration.fibreSum_transport line 1279
  85. def OAI.Rokhlin.BorelFibreEnumeration.restrictLevel line 1287
  86. lemma OAI.Rokhlin.BorelFibreEnumeration.fibreSum_le_card_mul line 1305
  87. lemma OAI.Rokhlin.BorelFibreEnumeration.exists_positive_block line 1313
  88. structure OAI.Rokhlin.ArrayObjects.Object.Rolled.PositiveRawBlock line 1360
  89. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.exists_positive_raw_block line 1394
  90. def OAI.Rokhlin.fibreLevelEquiv line 1429
  91. lemma OAI.Rokhlin.fibreLevelSum_transport line 1451
  92. def OAI.Rokhlin.movingFibreSum line 1469
  93. lemma OAI.Rokhlin.measurable_movingFibreSum line 1472
  94. lemma OAI.Rokhlin.movingFibreSum_step line 1477
  95. lemma OAI.Rokhlin.movingFibreSum_iterate line 1490
  96. lemma OAI.Rokhlin.movingFibreSum_integral line 1502
  97. lemma OAI.Rokhlin.movingFibreSum_bound line 1515
  98. lemma OAI.Rokhlin.absoluteCoefficient_transport line 1532
  99. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.raw_moving_sum_step line 1569
  100. lemma OAI.Rokhlin.block_iterate line 1603
  101. def OAI.Rokhlin.movingBlockCodeEquiv line 1609
  102. lemma OAI.Rokhlin.movingBlock_sum line 1624
  103. lemma OAI.Rokhlin.exactCircleTuples_mean_zero line 1643
  104. lemma OAI.Rokhlin.exactProjectiveSlot_mean_zero line 1682
  105. lemma OAI.Rokhlin.localProjectiveCharacters line 1711
  106. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.localGraph_projectiveCharacters line 1744
  107. lemma OAI.Rokhlin.ProjectiveCharacters.reindex line 1764
  108. lemma OAI.Rokhlin.finite_block_cancellation line 1793
  109. lemma OAI.Rokhlin.constant_integral_zero_of_bounded_cesaro line 1806
  110. lemma OAI.Rokhlin.local_moving_cancellation line 1879
  111. lemma OAI.Rokhlin.ArrayObjects.Object.selected_time_iterate line 1931
  112. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.raw_correlation_zero line 1974
  113. lemma OAI.Rokhlin.ArrayObjects.Object.Rolled.saturated_correlation_zero line 2038