OAI/MeasureTheory/SelfSimilar/TypedLaw.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.EntropyRateDimension.FiniteCondition.mass_pi line 11
  2. theorem OAI.EntropyRateDimension.FiniteCondition.posterior_pi line 33
  3. theorem OAI.EntropyRateDimension.System.sum_words_append line 59
  4. theorem OAI.EntropyRateDimension.System.completeMap_append line 66
  5. theorem OAI.EntropyRateDimension.System.wordWeight_append line 72
  6. theorem OAI.EntropyRateDimension.System.wordMap_append line 76
  7. abbrev OAI.EntropyRateDimension.Typed.tagWord line 89
  8. def OAI.EntropyRateDimension.Typed.prob line 91
  9. theorem OAI.EntropyRateDimension.Typed.prob_as_posterior line 94
  10. theorem OAI.EntropyRateDimension.Typed.prob_nonneg line 98
  11. theorem OAI.EntropyRateDimension.Typed.prob_sum line 102
  12. theorem OAI.EntropyRateDimension.Typed.prob_append line 107
  13. theorem OAI.EntropyRateDimension.Typed.prob_slope line 112
  14. def OAI.EntropyRateDimension.Typed.law line 125
  15. def OAI.EntropyRateDimension.Typed.tail line 129
  16. instance OAI.EntropyRateDimension.Typed.tail_probability line 133
  17. theorem OAI.EntropyRateDimension.Typed.tail_compact line 141
  18. theorem OAI.EntropyRateDimension.Typed.tail_mean line 148
  19. theorem OAI.EntropyRateDimension.Typed.tail_append line 155