OAI/MeasureTheory/SelfSimilar/SuffixLaw.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EntropyRateDimension.Typed.listLaw line 12
  2. def OAI.EntropyRateDimension.Typed.listTail line 14
  3. theorem OAI.EntropyRateDimension.Typed.apply_word_congr line 18
  4. theorem OAI.EntropyRateDimension.Typed.listLaw_ofFn line 24
  5. theorem OAI.EntropyRateDimension.Typed.listTail_ofFn line 31
  6. def OAI.EntropyRateDimension.Typed.listScaledTail line 38
  7. theorem OAI.EntropyRateDimension.Typed.listScaledTail_ofFn line 41
  8. instance OAI.EntropyRateDimension.Typed.listScaledTail_probability line 46
  9. theorem OAI.EntropyRateDimension.Typed.listScaledTail_compact line 50
  10. theorem OAI.EntropyRateDimension.Typed.listScaledTail_append line 54
  11. def OAI.EntropyRateDimension.Typed.suffixLaw line 63
  12. instance OAI.EntropyRateDimension.Typed.suffixLaw_probability line 66
  13. theorem OAI.EntropyRateDimension.Typed.suffixLaw_compact line 70
  14. theorem OAI.EntropyRateDimension.Typed.suffixLaw_convolution line 74
  15. def OAI.EntropyRateDimension.Typed.suffixWindow line 84
  16. theorem OAI.EntropyRateDimension.Typed.suffixWindow_antitone line 88
  17. theorem OAI.EntropyRateDimension.Typed.suffixWindow_bounds line 99
  18. def OAI.EntropyRateDimension.System.listDepth line 111
  19. theorem OAI.EntropyRateDimension.System.listDepth_nonneg line 113
  20. theorem OAI.EntropyRateDimension.System.listDepth_ofFn line 116
  21. theorem OAI.EntropyRateDimension.System.listDepth_append line 120
  22. theorem OAI.EntropyRateDimension.System.listDepth_take_add line 123
  23. theorem OAI.EntropyRateDimension.System.listDepth_monotone line 127
  24. theorem OAI.EntropyRateDimension.System.exists_depth_bound line 134
  25. theorem OAI.EntropyRateDimension.System.listDepth_le line 142
  26. theorem OAI.EntropyRateDimension.System.listDepth_take_le line 150