OAI/Probability/ThreeState/Messages.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Likelihood messages, compact couplings and subsequential posterior limits.

  1. abbrev OAI.ThreeState.Message line 12
  2. instance OAI.ThreeState.(instance at line 14) line 14
  3. lemma OAI.ThreeState.Message.nonneg line 16
  4. lemma OAI.ThreeState.Message.sum line 17
  5. lemma OAI.ThreeState.Message.le_three line 18
  6. lemma OAI.ThreeState.message_isCompact line 23
  7. instance OAI.ThreeState.(instance at line 37) line 37
  8. def OAI.ThreeState.uninformative line 38
  9. def OAI.ThreeState.likelihood line 41
  10. lemma OAI.ThreeState.likelihood_apply line 47
  11. lemma OAI.ThreeState.weighted_likelihood line 50
  12. lemma OAI.ThreeState.hasMean_likelihood line 56
  13. lemma OAI.ThreeState.mean_likelihood line 60
  14. def OAI.ThreeState.likelihoodPMF line 66
  15. def OAI.ThreeState.likelihoodLaw line 69
  16. lemma OAI.ThreeState.mean_likelihoodPMF line 72
  17. lemma OAI.ThreeState.integral_likelihoodLaw line 77
  18. lemma OAI.ThreeState.abs_likelihood line 96
  19. lemma OAI.ThreeState.abs_likelihood_square line 101
  20. lemma OAI.ThreeState.mean_likelihood_mul line 109
  21. lemma OAI.ThreeState.mean_joint_likelihood_mul line 117
  22. lemma OAI.ThreeState.mean_joint_likelihood_square line 129
  23. lemma OAI.ThreeState.joint_map_fst line 170
  24. lemma OAI.ThreeState.joint_map_snd line 176
  25. def OAI.ThreeState.messageCouplingPMF line 182
  26. def OAI.ThreeState.messageCoupling line 186
  27. lemma OAI.ThreeState.messageCouplingPMF_fst line 189
  28. lemma OAI.ThreeState.messageCouplingPMF_snd line 196
  29. lemma OAI.ThreeState.messageCoupling_fst line 203
  30. lemma OAI.ThreeState.messageCoupling_snd line 209
  31. lemma OAI.ThreeState.integral_messageCoupling line 215
  32. def OAI.ThreeState.coordinateSecond line 227
  33. lemma OAI.ThreeState.coordinateSecond_nonneg line 230
  34. lemma OAI.ThreeState.coordinateSecond_bind_le line 233
  35. def OAI.ThreeState.squareJump line 240
  36. lemma OAI.ThreeState.squareJump_nonneg line 245
  37. lemma OAI.ThreeState.integral_squareJump line 247
  38. theorem OAI.ThreeState.likelihood_common_subsequence line 255