OAI/MeasureTheory/SelfSimilar/FiniteEntropy.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EntropyRateDimension.FiniteEntropy.entropy line 13
  2. theorem OAI.EntropyRateDimension.FiniteEntropy.negMulLog_sum_le line 16
  3. def OAI.EntropyRateDimension.FiniteEntropy.mass line 33
  4. def OAI.EntropyRateDimension.FiniteEntropy.observableEntropy line 36
  5. theorem OAI.EntropyRateDimension.FiniteEntropy.mass_nonneg line 39
  6. theorem OAI.EntropyRateDimension.FiniteEntropy.mass_sum line 44
  7. theorem OAI.EntropyRateDimension.FiniteEntropy.observableEntropy_le line 51
  8. theorem OAI.EntropyRateDimension.FiniteEntropy.entropy_product line 64
  9. theorem OAI.EntropyRateDimension.FiniteEntropy.entropy_scale line 70
  10. theorem OAI.EntropyRateDimension.FiniteEntropy.entropy_nonneg line 76
  11. theorem OAI.EntropyRateDimension.FiniteEntropy.entropy_le_log_card line 80
  12. theorem OAI.EntropyRateDimension.FiniteEntropy.entropy_mixture line 104
  13. theorem OAI.EntropyRateDimension.FiniteEntropy.entropy_normalize line 116
  14. theorem OAI.EntropyRateDimension.FiniteEntropy.entropy_chain line 140
  15. theorem OAI.EntropyRateDimension.FiniteEntropy.entropy_joint_le line 159
  16. theorem OAI.EntropyRateDimension.FiniteEntropy.sum_mass_mul line 192
  17. theorem OAI.EntropyRateDimension.FiniteEntropy.mass_eq_zero_of_not_mem line 206
  18. theorem OAI.EntropyRateDimension.FiniteEntropy.observableEntropy_on_superset line 214
  19. theorem OAI.EntropyRateDimension.FiniteEntropy.mass_comp line 225
  20. theorem OAI.EntropyRateDimension.FiniteEntropy.observableEntropy_comp line 233
  21. theorem OAI.EntropyRateDimension.FiniteEntropy.observableEntropy_comp_le line 239
  22. theorem OAI.EntropyRateDimension.FiniteEntropy.mass_pair_fst line 246
  23. theorem OAI.EntropyRateDimension.FiniteEntropy.mass_pair_snd line 259
  24. theorem OAI.EntropyRateDimension.FiniteEntropy.observableEntropy_pair_le line 272
  25. theorem OAI.EntropyRateDimension.FiniteEntropy.observableEntropy_fst_le line 287
  26. def OAI.EntropyRateDimension.FiniteEntropy.conditionalEntropy line 293
  27. theorem OAI.EntropyRateDimension.FiniteEntropy.conditionalEntropy_nonneg line 297
  28. theorem OAI.EntropyRateDimension.FiniteEntropy.conditionalEntropy_le line 303
  29. theorem OAI.EntropyRateDimension.FiniteEntropy.observableEntropy_equiv line 310
  30. theorem OAI.EntropyRateDimension.FiniteEntropy.observableEntropy_swap line 318
  31. theorem OAI.EntropyRateDimension.FiniteEntropy.entropy_table_chain line 325
  32. theorem OAI.EntropyRateDimension.FiniteEntropy.mass_filter_div line 335
  33. theorem OAI.EntropyRateDimension.FiniteEntropy.conditionalEntropy_eq_sum line 342
  34. theorem OAI.EntropyRateDimension.FiniteEntropy.conditionalEntropy_chain line 375
  35. theorem OAI.EntropyRateDimension.FiniteEntropy.conditionalEntropy_reveal_le line 388
  36. theorem OAI.EntropyRateDimension.FiniteEntropy.observableEntropy_const_of line 402
  37. theorem OAI.EntropyRateDimension.FiniteEntropy.observableEntropy_le_log_on_superset line 410
  38. theorem OAI.EntropyRateDimension.FiniteEntropy.conditionalEntropy_le_bad_mass line 419
  39. theorem OAI.EntropyRateDimension.FiniteEntropy.observableEntropy_bool line 463
  40. theorem OAI.EntropyRateDimension.FiniteEntropy.conditionalEntropy_rare_flag line 474
  41. theorem OAI.EntropyRateDimension.FiniteEntropy.binEntropy_bits_le_three_sqrt line 513
  42. theorem OAI.EntropyRateDimension.FiniteEntropy.pair_flag_cost line 530
  43. theorem OAI.EntropyRateDimension.FiniteEntropy.event_union_bound line 541
  44. theorem OAI.EntropyRateDimension.FiniteEntropy.two_exceptions_bound line 560
  45. theorem OAI.EntropyRateDimension.FiniteEntropy.no_large_coordinate line 607
  46. theorem OAI.EntropyRateDimension.FiniteEntropy.mass_subset line 642
  47. theorem OAI.EntropyRateDimension.FiniteEntropy.observableEntropy_subset line 650
  48. theorem OAI.EntropyRateDimension.FiniteEntropy.observableEntropy_congr line 661
  49. theorem OAI.EntropyRateDimension.FiniteEntropy.observableEntropy_le_of_fibers line 676
  50. theorem OAI.EntropyRateDimension.FiniteEntropy.observableEntropy_id line 693
  51. theorem OAI.EntropyRateDimension.FiniteEntropy.conditionalEntropy_disintegrate line 700
  52. theorem OAI.EntropyRateDimension.FiniteEntropy.observableEntropy_eq_of_fibers line 714
  53. theorem OAI.EntropyRateDimension.FiniteEntropy.observableEntropy_of_injective line 725
  54. theorem OAI.EntropyRateDimension.FiniteEntropy.conditionalEntropy_eq_of_fibers line 733
  55. theorem OAI.EntropyRateDimension.FiniteEntropy.conditionalEntropy_condition_swap line 746
  56. theorem OAI.EntropyRateDimension.FiniteEntropy.conditionalEntropy_condition_le line 760
  57. theorem OAI.EntropyRateDimension.FiniteEntropy.observableEntropy_mixture_marginal line 779
  58. theorem OAI.EntropyRateDimension.FiniteEntropy.observableEntropy_mixture_joint line 796
  59. theorem OAI.EntropyRateDimension.FiniteEntropy.conditionalEntropy_mixture line 832
  60. theorem OAI.EntropyRateDimension.FiniteEntropy.observableEntropy_mixture_joint_general line 862
  61. theorem OAI.EntropyRateDimension.FiniteEntropy.conditionalEntropy_mixture_general line 895
  62. theorem OAI.EntropyRateDimension.FiniteEntropy.conditionalEntropy_mono line 925
  63. theorem OAI.EntropyRateDimension.FiniteEntropy.mixture_information_common line 946
  64. theorem OAI.EntropyRateDimension.FiniteEntropy.conditionalEntropy_id line 978
  65. def OAI.EntropyRateDimension.FiniteEntropy.js line 987
  66. theorem OAI.EntropyRateDimension.FiniteEntropy.conditionalEntropy_midpoint line 990
  67. theorem OAI.EntropyRateDimension.FiniteEntropy.js_observable_le line 1007
  68. theorem OAI.EntropyRateDimension.FiniteEntropy.js_nonneg line 1018
  69. theorem OAI.EntropyRateDimension.FiniteEntropy.event_sq_le_two_js line 1030
  70. def OAI.EntropyRateDimension.FiniteEntropy.totalVariation line 1054
  71. theorem OAI.EntropyRateDimension.FiniteEntropy.totalVariation_nonneg line 1057
  72. theorem OAI.EntropyRateDimension.FiniteEntropy.totalVariation_eq_event line 1060
  73. theorem OAI.EntropyRateDimension.FiniteEntropy.totalVariation_sq_le_two_js line 1077
  74. theorem OAI.EntropyRateDimension.FiniteEntropy.sum_min_eq_one_sub_tv line 1084
  75. theorem OAI.EntropyRateDimension.FiniteEntropy.js_le_tv line 1096
  76. theorem OAI.EntropyRateDimension.FiniteEntropy.totalVariation_triangle line 1124