OAI/MeasureTheory/SelfSimilar/FiniteDistribution.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.EntropyRateDimension.FiniteDistribution line 12
  2. def OAI.EntropyRateDimension.FiniteDistribution.entropy line 23
  3. def OAI.EntropyRateDimension.FiniteDistribution.tv line 26
  4. theorem OAI.EntropyRateDimension.FiniteDistribution.sum_on line 29
  5. theorem OAI.EntropyRateDimension.FiniteDistribution.entropy_on line 34
  6. theorem OAI.EntropyRateDimension.FiniteDistribution.tv_on line 40
  7. def OAI.EntropyRateDimension.FiniteDistribution.mix line 48
  8. def OAI.EntropyRateDimension.FiniteDistribution.js line 60
  9. theorem OAI.EntropyRateDimension.FiniteDistribution.js_on line 63
  10. theorem OAI.EntropyRateDimension.FiniteDistribution.js_nonneg line 69
  11. theorem OAI.EntropyRateDimension.FiniteDistribution.tv_nonneg line 75
  12. theorem OAI.EntropyRateDimension.FiniteDistribution.tv_sq_le_two_js line 78
  13. theorem OAI.EntropyRateDimension.FiniteDistribution.js_le_tv line 85
  14. theorem OAI.EntropyRateDimension.FiniteDistribution.tv_triangle line 92
  15. def OAI.EntropyRateDimension.FiniteDistribution.map line 101
  16. theorem OAI.EntropyRateDimension.FiniteDistribution.map_weight_on line 108
  17. theorem OAI.EntropyRateDimension.FiniteDistribution.entropy_map_on line 114
  18. theorem OAI.EntropyRateDimension.FiniteDistribution.mix_map_entropy line 122
  19. theorem OAI.EntropyRateDimension.FiniteDistribution.js_map_le line 137
  20. theorem OAI.EntropyRateDimension.FiniteDistribution.tv_map_le line 148
  21. theorem OAI.EntropyRateDimension.FiniteDistribution.entropy_congr line 168
  22. theorem OAI.EntropyRateDimension.FiniteDistribution.tv_congr line 173
  23. theorem OAI.EntropyRateDimension.FiniteDistribution.js_congr line 178
  24. theorem OAI.EntropyRateDimension.FiniteDistribution.map_weight_comp line 188
  25. theorem OAI.EntropyRateDimension.FiniteDistribution.map_weight_of_injective line 193
  26. theorem OAI.EntropyRateDimension.FiniteDistribution.map_weight_id line 203
  27. theorem OAI.EntropyRateDimension.FiniteDistribution.entropy_map_injective line 207
  28. theorem OAI.EntropyRateDimension.FiniteDistribution.tv_map_injective line 221
  29. theorem OAI.EntropyRateDimension.FiniteDistribution.js_map_equiv line 235
  30. def OAI.EntropyRateDimension.FiniteDistribution.translate line 247
  31. theorem OAI.EntropyRateDimension.FiniteDistribution.translate_weight line 250
  32. theorem OAI.EntropyRateDimension.FiniteDistribution.tv_translate line 255
  33. theorem OAI.EntropyRateDimension.FiniteDistribution.translate_add line 259
  34. theorem OAI.EntropyRateDimension.FiniteDistribution.tv_translate_two line 266
  35. theorem OAI.EntropyRateDimension.FiniteDistribution.js_two_step_coarsen line 275
  36. theorem OAI.EntropyRateDimension.FiniteDistribution.tv_le_one line 289
  37. theorem OAI.EntropyRateDimension.FiniteDistribution.js_le_log_two line 304
  38. theorem OAI.EntropyRateDimension.FiniteDistribution.map_translate_div_two line 310