OAI/Probability/DirectionalWalk/TotalEntropy.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalZeroOne.map_add_product line 17
  2. def OAI.DirectionalZeroOne.threeCount line 27
  3. def OAI.DirectionalZeroOne.threeTotal line 30
  4. def OAI.DirectionalZeroOne.threeCountLaw line 33
  5. def OAI.DirectionalZeroOne.totalCountLaw line 36
  6. instance OAI.DirectionalZeroOne.threeCountLaw_probability line 39
  7. instance OAI.DirectionalZeroOne.totalCountLaw_probability line 43
  8. lemma OAI.DirectionalZeroOne.threeChunkLaw_marked line 47
  9. lemma OAI.DirectionalZeroOne.bufferedChunkLaw_marked line 66
  10. lemma OAI.DirectionalZeroOne.totalCountLaw_bounds line 79
  11. lemma OAI.DirectionalZeroOne.atomInfo_integrable_nat_bounded line 94
  12. lemma OAI.DirectionalZeroOne.marked_count_entropy_difference line 111
  13. lemma OAI.DirectionalZeroOne.integrable_informationOf_lattice line 133
  14. lemma OAI.DirectionalZeroOne.listTotal_nth_integrable line 144
  15. lemma OAI.DirectionalZeroOne.listTotal_window_integrable line 165