OAI/MeasureTheory/SelfSimilar/MeasureEntropy.lean

GitHub source file

102 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EntropyRateDimension.MeasureEntropy.mass line 13
  2. def OAI.EntropyRateDimension.MeasureEntropy.entropy line 16
  3. theorem OAI.EntropyRateDimension.MeasureEntropy.mass_nonneg line 19
  4. theorem OAI.EntropyRateDimension.MeasureEntropy.mass_le_one line 22
  5. theorem OAI.EntropyRateDimension.MeasureEntropy.entropy_nonneg line 26
  6. theorem OAI.EntropyRateDimension.MeasureEntropy.mass_eq_zero_of_ae line 30
  7. theorem OAI.EntropyRateDimension.MeasureEntropy.entropy_eq_sum line 40
  8. theorem OAI.EntropyRateDimension.MeasureEntropy.mass_sum line 47
  9. def OAI.EntropyRateDimension.MeasureEntropy.CompactlyCarried line 80
  10. def OAI.EntropyRateDimension.MeasureEntropy.label line 83
  11. def OAI.EntropyRateDimension.MeasureEntropy.grid line 85
  12. def OAI.EntropyRateDimension.MeasureEntropy.averaged line 87
  13. theorem OAI.EntropyRateDimension.MeasureEntropy.label_measurable line 90
  14. theorem OAI.EntropyRateDimension.MeasureEntropy.label_joint_measurable line 93
  15. theorem OAI.EntropyRateDimension.MeasureEntropy.measurable_mass_label line 96
  16. theorem OAI.EntropyRateDimension.MeasureEntropy.measurable_grid line 102
  17. theorem OAI.EntropyRateDimension.MeasureEntropy.label_in_interval line 106
  18. theorem OAI.EntropyRateDimension.MeasureEntropy.label_ae_finite line 111
  19. theorem OAI.EntropyRateDimension.MeasureEntropy.grid_eq_sum line 117
  20. theorem OAI.EntropyRateDimension.MeasureEntropy.label_ae_uniform line 123
  21. theorem OAI.EntropyRateDimension.MeasureEntropy.grid_nonneg line 131
  22. theorem OAI.EntropyRateDimension.MeasureEntropy.grid_le_card line 134
  23. theorem OAI.EntropyRateDimension.MeasureEntropy.grid_integrable line 146
  24. theorem OAI.EntropyRateDimension.MeasureEntropy.averaged_nonneg line 155
  25. theorem OAI.EntropyRateDimension.MeasureEntropy.mass_comp line 158
  26. theorem OAI.EntropyRateDimension.MeasureEntropy.entropy_comp line 185
  27. theorem OAI.EntropyRateDimension.MeasureEntropy.entropy_comp_injective line 194
  28. theorem OAI.EntropyRateDimension.MeasureEntropy.mass_map line 203
  29. theorem OAI.EntropyRateDimension.MeasureEntropy.entropy_map line 212
  30. theorem OAI.EntropyRateDimension.MeasureEntropy.grid_periodic line 218
  31. theorem OAI.EntropyRateDimension.MeasureEntropy.grid_translate line 230
  32. theorem OAI.EntropyRateDimension.MeasureEntropy.grid_scale_pos line 239
  33. theorem OAI.EntropyRateDimension.MeasureEntropy.entropy_comp_le line 249
  34. theorem OAI.EntropyRateDimension.MeasureEntropy.entropy_pair_le line 257
  35. theorem OAI.EntropyRateDimension.MeasureEntropy.averaged_eq_intervalIntegral line 281
  36. theorem OAI.EntropyRateDimension.MeasureEntropy.grid_intervalIntegrable line 285
  37. theorem OAI.EntropyRateDimension.MeasureEntropy.averaged_translate line 291
  38. theorem OAI.EntropyRateDimension.MeasureEntropy.averaged_scale_pos line 299
  39. theorem OAI.EntropyRateDimension.MeasureEntropy.averaged_grid_nsmul line 304
  40. theorem OAI.EntropyRateDimension.MeasureEntropy.label_nested line 314
  41. theorem OAI.EntropyRateDimension.MeasureEntropy.entropy_congr_ae line 324
  42. theorem OAI.EntropyRateDimension.MeasureEntropy.ae_label_reflect line 333
  43. theorem OAI.EntropyRateDimension.MeasureEntropy.grid_reflect_ae line 353
  44. theorem OAI.EntropyRateDimension.MeasureEntropy.averaged_reflect line 367
  45. theorem OAI.EntropyRateDimension.MeasureEntropy.CompactlyCarried.map_affine line 383
  46. theorem OAI.EntropyRateDimension.MeasureEntropy.averaged_scale line 398
  47. theorem OAI.EntropyRateDimension.MeasureEntropy.averaged_affine line 415
  48. theorem OAI.EntropyRateDimension.MeasureEntropy.entropy_le_add_of_reconstruct line 427
  49. theorem OAI.EntropyRateDimension.MeasureEntropy.entropy_le_log_card line 443
  50. theorem OAI.EntropyRateDimension.MeasureEntropy.floor_relative_bounds line 451
  51. def OAI.EntropyRateDimension.MeasureEntropy.relativeLabel line 463
  52. theorem OAI.EntropyRateDimension.MeasureEntropy.relativeLabel_measurable line 466
  53. theorem OAI.EntropyRateDimension.MeasureEntropy.relativeLabel_mem line 471
  54. theorem OAI.EntropyRateDimension.MeasureEntropy.grid_le_grid_add_log line 486
  55. theorem OAI.EntropyRateDimension.MeasureEntropy.grid_le_grid_add_log_two line 506
  56. theorem OAI.EntropyRateDimension.MeasureEntropy.grid_le_grid_add_log_ratio line 517
  57. theorem OAI.EntropyRateDimension.MeasureEntropy.averaged_le_averaged_add_log_two line 527
  58. theorem OAI.EntropyRateDimension.MeasureEntropy.averaged_le_averaged_add_log_ratio line 537
  59. theorem OAI.EntropyRateDimension.MeasureEntropy.nested_grid_bounds line 547
  60. theorem OAI.EntropyRateDimension.MeasureEntropy.averaged_nested_bounds line 581
  61. theorem OAI.EntropyRateDimension.MeasureEntropy.mass_mixture line 600
  62. theorem OAI.EntropyRateDimension.MeasureEntropy.entropy_coarsening_mixture line 613
  63. theorem OAI.EntropyRateDimension.MeasureEntropy.nested_grid_mixture line 641
  64. theorem OAI.EntropyRateDimension.MeasureEntropy.grid_nsmul_intervalIntegrable line 670
  65. theorem OAI.EntropyRateDimension.MeasureEntropy.averaged_nested_mixture line 677
  66. theorem OAI.EntropyRateDimension.MeasureEntropy.CompactlyCarried.mixture line 705
  67. theorem OAI.EntropyRateDimension.MeasureEntropy.mixture_probability line 721
  68. theorem OAI.EntropyRateDimension.MeasureEntropy.averaged_nested_translate_mixture line 730
  69. theorem OAI.EntropyRateDimension.MeasureEntropy.entropy_summable line 755
  70. theorem OAI.EntropyRateDimension.MeasureEntropy.mass_summable line 762
  71. theorem OAI.EntropyRateDimension.MeasureEntropy.mass_tsum line 768
  72. def OAI.EntropyRateDimension.MeasureEntropy.fairShift line 775
  73. theorem OAI.EntropyRateDimension.MeasureEntropy.fairShift_probability line 778
  74. theorem OAI.EntropyRateDimension.MeasureEntropy.CompactlyCarried.fairShift line 786
  75. theorem OAI.EntropyRateDimension.MeasureEntropy.label_add_scale line 792
  76. theorem OAI.EntropyRateDimension.MeasureEntropy.mass_fairShift line 800
  77. theorem OAI.EntropyRateDimension.MeasureEntropy.mass_int_div_two line 823
  78. theorem OAI.EntropyRateDimension.MeasureEntropy.mass_nested_two line 841
  79. theorem OAI.EntropyRateDimension.MeasureEntropy.mass_fairShift_odd line 851
  80. theorem OAI.EntropyRateDimension.MeasureEntropy.mass_fairShift_even line 859
  81. theorem OAI.EntropyRateDimension.MeasureEntropy.entropy_half_mass line 873
  82. theorem OAI.EntropyRateDimension.MeasureEntropy.grid_fairShift line 893
  83. theorem OAI.EntropyRateDimension.MeasureEntropy.averaged_fairShift line 928
  84. def OAI.EntropyRateDimension.MeasureEntropy.observationLaw line 970
  85. def OAI.EntropyRateDimension.MeasureEntropy.gridLaw line 977
  86. theorem OAI.EntropyRateDimension.MeasureEntropy.gridLaw_weight line 983
  87. theorem OAI.EntropyRateDimension.MeasureEntropy.gridLaw_entropy line 987
  88. def OAI.EntropyRateDimension.MeasureEntropy.gridDeficit line 991
  89. theorem OAI.EntropyRateDimension.MeasureEntropy.gridDeficit_eq_js line 994
  90. theorem OAI.EntropyRateDimension.MeasureEntropy.gridDeficit_bounds line 1011
  91. theorem OAI.EntropyRateDimension.MeasureEntropy.gridLaw_coarsen_two line 1017
  92. theorem OAI.EntropyRateDimension.MeasureEntropy.gridDeficit_double_sq line 1034
  93. theorem OAI.EntropyRateDimension.MeasureEntropy.gridDeficit_integrable line 1050
  94. theorem OAI.EntropyRateDimension.MeasureEntropy.integral_gridDeficit line 1056
  95. def OAI.EntropyRateDimension.MeasureEntropy.deficit line 1067
  96. theorem OAI.EntropyRateDimension.MeasureEntropy.deficit_bounds line 1070
  97. theorem OAI.EntropyRateDimension.MeasureEntropy.gridDeficit_sq_integrable line 1080
  98. theorem OAI.EntropyRateDimension.MeasureEntropy.integral_gridDeficit_double_shift line 1090
  99. theorem OAI.EntropyRateDimension.MeasureEntropy.deficit_double_sq line 1109
  100. theorem OAI.EntropyRateDimension.MeasureEntropy.deficit_dyadic_tendsto_zero line 1135
  101. theorem OAI.EntropyRateDimension.MeasureEntropy.sum_dyadic_deficit line 1156
  102. theorem OAI.EntropyRateDimension.MeasureEntropy.wide_window_saturation line 1168