OAI/Dynamics/MultipleMixing/Entropy.lean

GitHub source file

112 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Rokhlin.shannonEntropy_eq_negMulLog line 14
  2. def OAI.Rokhlin.rowEntropy line 17
  3. lemma OAI.Rokhlin.rowEntropy_zero line 20
  4. lemma OAI.Rokhlin.zero_row line 23
  5. lemma OAI.Rokhlin.rowEntropy_normalize line 26
  6. lemma OAI.Rokhlin.rowEntropy_sum_le line 46
  7. def OAI.Rokhlin.conditionalShannon line 89
  8. lemma OAI.Rokhlin.shannon_chain_rule line 91
  9. lemma OAI.Rokhlin.conditionalShannon_refine line 98
  10. def OAI.Rokhlin.randomEntropy line 115
  11. def OAI.Rokhlin.randomConditionalEntropy line 117
  12. lemma OAI.Rokhlin.sum_joint_mass line 121
  13. lemma OAI.Rokhlin.randomEntropy_pair line 134
  14. lemma OAI.Rokhlin.randomEntropy_nonneg line 140
  15. lemma OAI.Rokhlin.randomConditionalEntropy_nonneg line 145
  16. lemma OAI.Rokhlin.randomConditionalEntropy_le line 152
  17. lemma OAI.Rokhlin.randomConditionalEntropy_refine line 171
  18. lemma OAI.Rokhlin.randomEntropy_prod_le line 183
  19. lemma OAI.Rokhlin.randomEntropy_recode line 188
  20. lemma OAI.Rokhlin.continuous_shannonEntropy line 203
  21. lemma OAI.Rokhlin.randomEntropy_congr_ae line 208
  22. lemma OAI.Rokhlin.randomEntropy_measurePreserving line 219
  23. lemma OAI.Rokhlin.atom_mass_disagreement line 228
  24. lemma OAI.Rokhlin.randomEntropy_tendsto_of_disagreement line 238
  25. lemma OAI.Rokhlin.randomEntropy_self_pair line 248
  26. lemma OAI.Rokhlin.randomConditionalEntropy_self line 254
  27. lemma OAI.Rokhlin.randomConditionalEntropy_tendsto_self line 260
  28. lemma OAI.Rokhlin.randomEntropy_mutual_factor line 293
  29. lemma OAI.Rokhlin.randomEntropy_pair_factor line 302
  30. lemma OAI.Rokhlin.randomConditionalEntropy_condition_redundant line 307
  31. lemma OAI.Rokhlin.randomConditionalEntropy_condition_comp line 321
  32. lemma OAI.Rokhlin.randomConditionalEntropy_measurable_factor line 329
  33. lemma OAI.Rokhlin.randomConditionalEntropy_measurePreserving line 337
  34. lemma OAI.Rokhlin.randomConditionalEntropy_congr_ae line 350
  35. lemma OAI.Rokhlin.randomConditionalEntropy_chain line 376
  36. lemma OAI.Rokhlin.randomConditionalEntropy_pair_le line 389
  37. lemma OAI.Rokhlin.randomConditionalEntropy_mutual_factor line 397
  38. lemma OAI.Rokhlin.randomEntropy_fintype_one line 410
  39. lemma OAI.Rokhlin.randomConditionalEntropy_fintype_one line 416
  40. def OAI.Rokhlin.integerWord line 422
  41. lemma OAI.Rokhlin.measurable_integerWord line 426
  42. lemma OAI.Rokhlin.integerWord_pair line 429
  43. lemma OAI.Rokhlin.integerWord_add line 448
  44. lemma OAI.Rokhlin.integerWord_succ line 454
  45. theorem OAI.Rokhlin.entropy_rate_of_decreasing_increments line 474
  46. lemma OAI.Rokhlin.entropy_block_lower line 489
  47. theorem OAI.Rokhlin.entropy_zero_of_tail_bounds line 500
  48. lemma OAI.Rokhlin.integerWord_subword line 549
  49. lemma OAI.Rokhlin.integerWord_subword_measurable line 558
  50. lemma OAI.Rokhlin.pastWord_comap_mono line 564
  51. lemma OAI.Rokhlin.windowWord_comap_mono line 574
  52. lemma OAI.Rokhlin.integerWord_translate line 589
  53. lemma OAI.Rokhlin.integerWord_entropy_translate line 596
  54. lemma OAI.Rokhlin.conditionalEntropy_past_translate line 601
  55. lemma OAI.Rokhlin.entropy_increment_past line 610
  56. theorem OAI.Rokhlin.stationary_entropy_rate line 619
  57. def OAI.Rokhlin.completedFactor line 650
  58. lemma OAI.Rokhlin.completedFactor_le line 665
  59. lemma OAI.Rokhlin.le_completedFactor line 668
  60. lemma OAI.Rokhlin.completedFactor_mono line 671
  61. lemma OAI.Rokhlin.completedFactor_congr_set line 676
  62. lemma OAI.Rokhlin.measurable_completedFactor_of_ae line 682
  63. lemma OAI.Rokhlin.completedFactor_iInf_measurable line 690
  64. lemma OAI.Rokhlin.aeStrong_limit_factor line 705
  65. lemma OAI.Rokhlin.simpleFunc_aeStrong_of_completed line 720
  66. lemma OAI.Rokhlin.aeStrong_of_measurable_completed line 746
  67. lemma OAI.Rokhlin.set_approx_iSup_completed line 759
  68. def OAI.Rokhlin.pickFiniteBit line 798
  69. lemma OAI.Rokhlin.pickFiniteBit_eq line 802
  70. lemma OAI.Rokhlin.finite_approx_iSup_completed line 808
  71. lemma OAI.Rokhlin.randomConditionalEntropy_tendsto_condition line 856
  72. lemma OAI.Rokhlin.finite_approx_completed_sequence line 879
  73. lemma OAI.Rokhlin.exists_conditional_entropy_lt_of_completed line 891
  74. lemma OAI.Rokhlin.conditional_entropy_lower_of_completed line 908
  75. lemma OAI.Rokhlin.integerWord_conditional_succ line 936
  76. lemma OAI.Rokhlin.integerWord_conditional_le_sum line 953
  77. lemma OAI.Rokhlin.integerWord_conditional_lower line 966
  78. abbrev OAI.Rokhlin.processPast line 986
  79. abbrev OAI.Rokhlin.processFull line 989
  80. lemma OAI.Rokhlin.processPast_le line 993
  81. lemma OAI.Rokhlin.processFull_le line 997
  82. lemma OAI.Rokhlin.processPast_zero_le_full line 1002
  83. lemma OAI.Rokhlin.tail_word_conditional_lower line 1022
  84. lemma OAI.Rokhlin.tail_word_conditional_upper line 1041
  85. theorem OAI.Rokhlin.tail_process_entropy_zero line 1062
  86. lemma OAI.Rokhlin.antitone_projection_tendsto line 1110
  87. lemma OAI.Rokhlin.lpMeas_completed_eq line 1138
  88. lemma OAI.Rokhlin.lpMeas_completed_iInf line 1148
  89. lemma OAI.Rokhlin.reverse_conditional_L2 line 1162
  90. lemma OAI.Rokhlin.reverse_tail_pairing line 1188
  91. lemma OAI.Rokhlin.reverse_tail_pairing_of_bound line 1208
  92. lemma OAI.Rokhlin.processPast_eq_generators line 1228
  93. lemma OAI.Rokhlin.processPast_mono line 1250
  94. lemma OAI.Rokhlin.completedFactor_comap line 1257
  95. lemma OAI.Rokhlin.processPast_comap line 1270
  96. abbrev OAI.Rokhlin.processTail line 1281
  97. lemma OAI.Rokhlin.processTail_le line 1284
  98. lemma OAI.Rokhlin.processTail_le_past line 1287
  99. lemma OAI.Rokhlin.processTail_comap line 1292
  100. lemma OAI.Rokhlin.measurable_tail_translate line 1302
  101. lemma OAI.Rokhlin.antitone_starProjection_tendsto line 1316
  102. lemma OAI.Rokhlin.lpMeas_iInf_antitone line 1335
  103. lemma OAI.Rokhlin.condExpL2_antitone_tendsto line 1371
  104. lemma OAI.Rokhlin.integral_norm_L2_le line 1396
  105. lemma OAI.Rokhlin.condExp_antitone_L1_tendsto line 1402
  106. def OAI.Rokhlin.clippedConditional line 1432
  107. lemma OAI.Rokhlin.clippedConditional_bounds line 1436
  108. lemma OAI.Rokhlin.clippedConditional_measurable line 1441
  109. lemma OAI.Rokhlin.clippedConditional_ae line 1446
  110. lemma OAI.Rokhlin.clippedConditional_mean line 1456
  111. lemma OAI.Rokhlin.exists_simple_interval_approx line 1462
  112. lemma OAI.Rokhlin.reverse_condExp_completed_L1 line 1489