OAI/Probability/ThreeState/Observation.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Ordered and unlabelled boundary observations and information degradation.

  1. def OAI.ThreeState.iidVector line 12
  2. lemma OAI.ThreeState.iidVector_map line 16
  3. lemma OAI.ThreeState.iidVector_ofFn line 35
  4. lemma OAI.ThreeState.iidVector_apply line 48
  5. abbrev OAI.ThreeState.OrderedObservation line 72
  6. def OAI.ThreeState.orderedLaw line 76
  7. def OAI.ThreeState.forgetOrder line 82
  8. lemma OAI.ThreeState.orderedLaw_forget line 86
  9. lemma OAI.ThreeState.orderedAdvantage_dominates line 107
  10. def OAI.ThreeState.vectorTraverse line 121
  11. lemma OAI.ThreeState.vectorTraverse_cons line 126
  12. lemma OAI.ThreeState.iidVector_bind_traverse line 131
  13. def OAI.ThreeState.orderedGrow line 144
  14. lemma OAI.ThreeState.orderedLaw_grow line 149
  15. lemma OAI.ThreeState.ordered_likelihood_common_subsequence line 164
  16. instance OAI.ThreeState.pmfCommApplicative line 175
  17. lemma OAI.ThreeState.list_traverse_nil line 182
  18. lemma OAI.ThreeState.list_traverse_cons line 185
  19. lemma OAI.ThreeState.multiset_traverse_list line 192
  20. lemma OAI.ThreeState.iidList_bind_traverse line 196
  21. lemma OAI.ThreeState.iidList_multiset_bind line 209
  22. def OAI.ThreeState.grow line 218
  23. theorem OAI.ThreeState.observedLaw_grow line 224
  24. theorem OAI.ThreeState.observedAdvantage_antitone line 247
  25. theorem OAI.ThreeState.observedAdvantage_tendsto line 259