OAI/MeasureTheory/SelfSimilar/Coding.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EntropyRateDimension.Coding.shift line 21
  2. def OAI.EntropyRateDimension.Coding.slope line 23
  3. def OAI.EntropyRateDimension.Coding.term line 26
  4. def OAI.EntropyRateDimension.Coding.point line 29
  5. theorem OAI.EntropyRateDimension.Coding.slope_zero line 32
  6. theorem OAI.EntropyRateDimension.Coding.slope_succ line 35
  7. theorem OAI.EntropyRateDimension.Coding.slope_shift line 40
  8. theorem OAI.EntropyRateDimension.Coding.abs_slope_le line 46
  9. theorem OAI.EntropyRateDimension.Coding.abs_term_le line 56
  10. theorem OAI.EntropyRateDimension.Coding.term_summable line 62
  11. theorem OAI.EntropyRateDimension.Coding.point_shift line 68
  12. theorem OAI.EntropyRateDimension.Coding.slope_measurable line 82
  13. theorem OAI.EntropyRateDimension.Coding.term_measurable line 88
  14. theorem OAI.EntropyRateDimension.Coding.point_measurable line 91
  15. def OAI.EntropyRateDimension.Coding.symbolMeasure line 98
  16. instance OAI.EntropyRateDimension.Coding.symbolMeasure_probability line 101
  17. def OAI.EntropyRateDimension.Coding.addressMeasure line 108
  18. instance OAI.EntropyRateDimension.Coding.addressMeasure_probability line 111
  19. def OAI.EntropyRateDimension.Coding.law line 114
  20. instance OAI.EntropyRateDimension.Coding.law_probability line 116
  21. theorem OAI.EntropyRateDimension.Coding.head_tail_point_law line 119
  22. theorem OAI.EntropyRateDimension.Coding.law_selfSimilar line 129