OAI/Probability/ThreeState/Update.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Branchwise likelihood updates and their independent product measures.

  1. def OAI.ThreeState.edgeMessage line 12
  2. lemma OAI.ThreeState.continuous_edgeMessage line 26
  3. lemma OAI.ThreeState.channel_decompose line 32
  4. lemma OAI.ThreeState.channel_message line 37
  5. lemma OAI.ThreeState.mass_channelPMF line 44
  6. def OAI.ThreeState.edgeLaw line 48
  7. lemma OAI.ThreeState.mass_edgeLaw line 51
  8. def OAI.ThreeState.sigmaPMF line 64
  9. lemma OAI.ThreeState.sigmaPMF_apply line 67
  10. lemma OAI.ThreeState.mass_sigmaPMF line 78
  11. lemma OAI.ThreeState.mass_iidVector line 82
  12. def OAI.ThreeState.productReference line 87
  13. def OAI.ThreeState.composeLaw line 90
  14. def OAI.ThreeState.productWeight line 94
  15. def OAI.ThreeState.normalizer line 97
  16. lemma OAI.ThreeState.productWeight_nonneg line 100
  17. lemma OAI.ThreeState.normalizer_nonneg line 104
  18. lemma OAI.ThreeState.productWeight_sum line 107
  19. def OAI.ThreeState.combineMessage line 110
  20. lemma OAI.ThreeState.mass_composeLaw line 119
  21. lemma OAI.ThreeState.mass_marginal_composeLaw line 126
  22. lemma OAI.ThreeState.weighted_combineMessage line 136
  23. lemma OAI.ThreeState.likelihood_composeLaw line 149
  24. lemma OAI.ThreeState.weighted_test_composeLaw line 160
  25. lemma OAI.ThreeState.hasMean_weighted_compose line 173
  26. lemma OAI.ThreeState.mean_test_compose line 184
  27. lemma OAI.ThreeState.iidVector_outer_pi line 199
  28. lemma OAI.ThreeState.iidVector_toMeasure line 223
  29. def OAI.ThreeState.iidMeasure line 233
  30. lemma OAI.ThreeState.continuous_iidMeasure line 236
  31. lemma OAI.ThreeState.likelihoodPMF_iid_toMeasure line 239
  32. lemma OAI.ThreeState.integral_iid_likelihood line 244