OAI/MeasureTheory/SelfSimilar/UpperBound.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.EntropyRateDimension.System.sum_words_cons line 12
  2. theorem OAI.EntropyRateDimension.System.completeMap_cons line 19
  3. theorem OAI.EntropyRateDimension.System.wordWeight_cons line 24
  4. def OAI.EntropyRateDimension.System.wordMap line 28
  5. theorem OAI.EntropyRateDimension.System.wordMap_measurable line 31
  6. theorem OAI.EntropyRateDimension.System.wordMap_cons line 34
  7. theorem OAI.EntropyRateDimension.System.selfSimilar_words line 40
  8. theorem OAI.EntropyRateDimension.System.mapMass_dot line 65
  9. theorem OAI.EntropyRateDimension.System.wordWeight_expect_sum line 70
  10. theorem OAI.EntropyRateDimension.System.completeMap_log_slope line 84
  11. theorem OAI.EntropyRateDimension.System.completeMap_abs_lt_one line 89
  12. def OAI.EntropyRateDimension.System.compressed line 98
  13. theorem OAI.EntropyRateDimension.System.selfSimilar_compressed line 116
  14. theorem OAI.EntropyRateDimension.System.compressed_lyapunov line 139
  15. theorem OAI.EntropyRateDimension.System.compressed_symbol_entropy line 150
  16. theorem OAI.EntropyRateDimension.Coding.exponent_symbol_entropy_bound line 167
  17. theorem OAI.EntropyRateDimension.System.mapSupport_nonempty line 194
  18. theorem OAI.EntropyRateDimension.System.exponent_le_walkEntropy line 198
  19. theorem OAI.EntropyRateDimension.System.exponent_le_rate line 215
  20. theorem OAI.EntropyRateDimension.System.exponent_le_one line 222
  21. theorem OAI.EntropyRateDimension.System.main_upper_bound line 229