OAI/MeasureTheory/SelfSimilar/BlockWords.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.EntropyRateDimension.FiniteEntropy.observableEntropy_reindex line 10
  2. def OAI.EntropyRateDimension.System.blocks line 32
  3. theorem OAI.EntropyRateDimension.System.selfSimilar_blocks line 41
  4. theorem OAI.EntropyRateDimension.System.blocks_lyapunov line 44
  5. def OAI.EntropyRateDimension.System.flattenWordEquiv line 50
  6. theorem OAI.EntropyRateDimension.System.flattenWordEquiv_apply line 54
  7. theorem OAI.EntropyRateDimension.System.wordAffine_blocks line 58
  8. theorem OAI.EntropyRateDimension.System.completeMap_flatten line 66
  9. theorem OAI.EntropyRateDimension.System.wordWeight_flatten line 83
  10. theorem OAI.EntropyRateDimension.System.blocks_walkEntropy line 91
  11. theorem OAI.EntropyRateDimension.System.blocks_entropyRate_lower line 99
  12. def OAI.EntropyRateDimension.System.wordType line 114
  13. theorem OAI.EntropyRateDimension.System.ratio_wordType line 119