OAI/Dynamics/MultipleMixing/Foundations.lean

GitHub source file

121 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Rokhlin.ProjectiveCharacters line 12
  2. theorem OAI.Rokhlin.ProjectiveCharacters.integrable line 27
  3. theorem OAI.Rokhlin.ProjectiveCharacters.conjugate line 32
  4. theorem OAI.Rokhlin.ProjectiveCharacters.finset_prod line 46
  5. theorem OAI.Rokhlin.ProjectiveCharacters.integral_finset_prod_eq_zero line 70
  6. theorem OAI.Rokhlin.ProjectiveCharacters.orthogonal line 79
  7. theorem OAI.Rokhlin.ProjectiveCharacters.integrable_finset_prod line 93
  8. theorem OAI.Rokhlin.ProjectiveCharacters.weighted_finset_prod line 98
  9. def OAI.Rokhlin.Dissociated line 107
  10. theorem OAI.Rokhlin.ProjectiveCharacters.integral_signed_linear_prod_eq_zero line 117
  11. theorem OAI.Rokhlin.ProjectiveCharacters.integral_real_prod_eq_zero line 151
  12. theorem OAI.Rokhlin.ProjectiveCharacters.integral_affine_real_prod line 176
  13. theorem OAI.Rokhlin.ProjectiveCharacters.dissociated_exponential_bound line 204
  14. def OAI.Rokhlin.shannonEntropy line 269
  15. theorem OAI.Rokhlin.probability_le_one line 277
  16. theorem OAI.Rokhlin.entropy_term_nonneg line 281
  17. theorem OAI.Rokhlin.shannonEntropy_nonneg line 286
  18. theorem OAI.Rokhlin.unlikely_mass_bound line 289
  19. theorem OAI.Rokhlin.likely_card_bound line 309
  20. theorem OAI.Rokhlin.exponential_tail_bound line 327
  21. theorem OAI.Rokhlin.randomized_tail_bound line 341
  22. theorem OAI.Rokhlin.integral_le_threshold_add_tail line 385
  23. theorem OAI.Rokhlin.dissociated_tail_bound line 414
  24. def OAI.Rokhlin.entropyWord line 434
  25. def OAI.Rokhlin.wordEntropy line 437
  26. theorem OAI.Rokhlin.randomized_dissociated_tail line 449
  27. theorem OAI.Rokhlin.exists_aligning_phase line 486
  28. theorem OAI.Rokhlin.dissociated_correlation_mean_bound line 500
  29. theorem OAI.Rokhlin.entropy_cancellation line 557
  30. theorem OAI.Rokhlin.shannonEntropy_map_le line 598
  31. theorem OAI.Rokhlin.randomEntropy_comp_le line 630
  32. theorem OAI.Rokhlin.wordEntropy_nonneg line 646
  33. theorem OAI.Rokhlin.wordEntropy_progression_le line 654
  34. theorem OAI.Rokhlin.zero_entropy_progression line 664
  35. theorem OAI.Rokhlin.isClosed_mixing_right line 706
  36. theorem OAI.Rokhlin.isClosed_mixing_left line 721
  37. def OAI.Rokhlin.probabilityOne line 742
  38. theorem OAI.Rokhlin.mixing_L2 line 745
  39. theorem OAI.Rokhlin.inner_probabilityOne line 799
  40. theorem OAI.Rokhlin.mixing_integral_coupling line 812
  41. def OAI.Rokhlin.cesaro line 851
  42. theorem OAI.Rokhlin.norm_cesaro_le line 857
  43. theorem OAI.Rokhlin.norm_cesaro_le_bound line 862
  44. theorem OAI.Rokhlin.norm_cesaro_shift_sub_le line 872
  45. theorem OAI.Rokhlin.cesaro_shift_sub_tendsto_zero line 903
  46. theorem OAI.Rokhlin.cesaro_finset_sum line 910
  47. theorem OAI.Rokhlin.cesaro_smul line 915
  48. theorem OAI.Rokhlin.cesaro_sub line 921
  49. theorem OAI.Rokhlin.cesaro_smoothing_sub_tendsto_zero line 925
  50. theorem OAI.Rokhlin.cesaro_mono line 941
  51. theorem OAI.Rokhlin.cesaro_le_bound line 945
  52. theorem OAI.Rokhlin.norm_cesaro_sq_le line 953
  53. theorem OAI.Rokhlin.norm_finite_mean_sq line 974
  54. theorem OAI.Rokhlin.norm_smoothed_cesaro_sq_le line 983
  55. def OAI.Rokhlin.LagCesaroBound line 994
  56. theorem OAI.Rokhlin.shifted_lag_cesaro_bound line 998
  57. theorem OAI.Rokhlin.pair_cesaro_bound line 1015
  58. theorem OAI.Rokhlin.van_der_corput line 1031
  59. def OAI.Rokhlin.DifferencePolynomial line 1118
  60. theorem OAI.Rokhlin.DifferencePolynomial.const line 1125
  61. theorem OAI.Rokhlin.DifferencePolynomial.add line 1132
  62. theorem OAI.Rokhlin.DifferencePolynomial.shift line 1146
  63. theorem OAI.Rokhlin.DifferencePolynomial.sum line 1157
  64. theorem OAI.Rokhlin.DifferencePolynomial.succ line 1168
  65. theorem OAI.Rokhlin.DifferencePolynomial.mono line 1178
  66. theorem OAI.Rokhlin.DifferencePolynomial.of_forward_difference line 1184
  67. theorem OAI.Rokhlin.DifferencePolynomial.choose_nsmul line 1202
  68. theorem OAI.Rokhlin.DifferencePolynomial.binomial line 1213
  69. theorem OAI.Rokhlin.norm_toLp_le_bound line 1224
  70. theorem OAI.Rokhlin.ProjectiveCharacters.mul_conj line 1240
  71. theorem OAI.Rokhlin.ProjectiveCharacters.norm_integral_conj_le_one line 1252
  72. theorem OAI.Rokhlin.l2_real_inner_eq_re_inner line 1259
  73. theorem OAI.Rokhlin.phased_memLp line 1275
  74. theorem OAI.Rokhlin.phased_lag_norm line 1290
  75. theorem OAI.Rokhlin.polynomial_cancellation line 1318
  76. theorem OAI.Rokhlin.binomial_cancellation line 1439
  77. theorem OAI.Rokhlin.monic_mahlerMeasure_eq_one line 1460
  78. theorem OAI.Rokhlin.integer_polynomial_dvd_cyclotomic_power line 1470
  79. theorem OAI.Rokhlin.quasiUnipotent_of_integer_annihilator line 1520
  80. lemma OAI.Rokhlin.charpoly_dual line 1534
  81. lemma OAI.Rokhlin.map_mem_torsion line 1550
  82. lemma OAI.Rokhlin.torsion_map_equiv line 1559
  83. def OAI.Rokhlin.torsionQuotEquiv line 1568
  84. lemma OAI.Rokhlin.torsionQuotEquiv_mk line 1572
  85. def OAI.Rokhlin.torsionRestrictEquiv line 1576
  86. lemma OAI.Rokhlin.torsionRestrictEquiv_pow line 1585
  87. lemma OAI.Rokhlin.torsion_period line 1594
  88. lemma OAI.Rokhlin.eigenfunctional_generator_ne_zero line 1618
  89. theorem OAI.Rokhlin.lattice_orbit_alternative line 1647
  90. lemma OAI.Rokhlin.nilpotent_pow_sub_one line 1707
  91. lemma OAI.Rokhlin.linear_semiconj_pow line 1715
  92. lemma OAI.Rokhlin.torsionQuotEquiv_zpow_mk line 1726
  93. lemma OAI.Rokhlin.torsionQuot_cyclic line 1738
  94. theorem OAI.Rokhlin.quasiUnipotent_of_torsionQuot line 1752
  95. theorem OAI.Rokhlin.fg_cyclic_orbit_alternative line 1791
  96. def OAI.Rokhlin.cyclicOrbit line 1810
  97. def OAI.Rokhlin.initialOrbit line 1813
  98. lemma OAI.Rokhlin.mem_initialOrbit line 1816
  99. theorem OAI.Rokhlin.cyclicOrbit_fg_of_boundary line 1820
  100. theorem OAI.Rokhlin.cyclicOrbit_fg_of_relation line 1870
  101. lemma OAI.Rokhlin.cyclicOrbit_shift line 1899
  102. theorem OAI.Rokhlin.cyclicOrbit_fg_of_signed_relation line 1913
  103. theorem OAI.Rokhlin.dissociated_of_geometric_functional line 1961
  104. theorem OAI.Rokhlin.dissociated_progressions_of_eigenfunctional line 2004
  105. theorem OAI.Rokhlin.differencePolynomial_of_nilpotent_difference line 2029
  106. theorem OAI.Rokhlin.polynomial_progressions_of_nilpotent line 2052
  107. lemma OAI.Rokhlin.cyclicOrbit_zpow_mem line 2066
  108. lemma OAI.Rokhlin.cyclicOrbit_apply_mem line 2077
  109. lemma OAI.Rokhlin.cyclicOrbit_symm_apply_mem line 2080
  110. def OAI.Rokhlin.cyclicOrbitEquiv line 2083
  111. lemma OAI.Rokhlin.cyclicOrbitEquiv_zpow_coe line 2091
  112. lemma OAI.Rokhlin.cyclicOrbitEquiv_pow_coe line 2102
  113. def OAI.Rokhlin.cyclicGenerator line 2106
  114. lemma OAI.Rokhlin.cyclicGenerator_spans line 2109
  115. lemma OAI.Rokhlin.Dissociated.of_injective_map line 2120
  116. theorem OAI.Rokhlin.orbit_alternatives line 2132
  117. theorem OAI.Rokhlin.cesaro_zero_of_progressions line 2168
  118. theorem OAI.Rokhlin.DifferencePolynomial.map line 2191
  119. theorem OAI.Rokhlin.wordEntropy_comp line 2201
  120. theorem OAI.Rokhlin.orbit_cancellation_unit line 2217
  121. theorem OAI.Rokhlin.orbit_cancellation line 2285