OAI/MeasureTheory/SelfSimilar/WordTypes.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.EntropyRateDimension.System.wordAffine_slope line 15
  2. theorem OAI.EntropyRateDimension.System.completeMap_slope line 21
  3. theorem OAI.EntropyRateDimension.System.completeMap_slope_ne_zero line 26
  4. theorem OAI.EntropyRateDimension.System.wordAffine_append line 31
  5. def OAI.EntropyRateDimension.System.blockType line 38
  6. theorem OAI.EntropyRateDimension.System.block_product_eq line 43
  7. theorem OAI.EntropyRateDimension.System.completeMap_slope_blockType line 59
  8. theorem OAI.EntropyRateDimension.System.map_entropy_as_observation line 66
  9. theorem OAI.EntropyRateDimension.System.blockType_entropy_le line 74
  10. theorem OAI.EntropyRateDimension.System.conditional_translation_entropy_lower line 101
  11. theorem OAI.EntropyRateDimension.System.conditional_translation_entropy_rate_lower line 118