OAI/Probability/ThreeState/FixedPoints.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Continuity of posterior updates and fixed points of the likelihood law.

  1. lemma OAI.ThreeState.continuous_productWeight line 12
  2. lemma OAI.ThreeState.continuous_normalizer line 19
  3. lemma OAI.ThreeState.continuousAt_combineMessage line 23
  4. def OAI.ThreeState.weightedTest line 46
  5. lemma OAI.ThreeState.weightedTest_bound line 50
  6. lemma OAI.ThreeState.continuous_weightedTest line 57
  7. def OAI.ThreeState.weightedTestMap line 75
  8. def OAI.ThreeState.degreeTest line 79
  9. lemma OAI.ThreeState.continuous_degreeTest line 83
  10. lemma OAI.ThreeState.mean_sigmaPMF line 93
  11. lemma OAI.ThreeState.degreeTest_likelihood line 103
  12. lemma OAI.ThreeState.test_compose_identity line 113
  13. def OAI.ThreeState.coordinateMap line 126
  14. def OAI.ThreeState.Balanced line 130
  15. lemma OAI.ThreeState.balanced_likelihoodLaw line 133
  16. lemma OAI.ThreeState.balanced_limit line 139
  17. lemma OAI.ThreeState.integral_edgeMessage line 148
  18. lemma OAI.ThreeState.integral_productWeight line 160
  19. lemma OAI.ThreeState.integral_normalizer line 168
  20. lemma OAI.ThreeState.degreeTest_bound line 177
  21. lemma OAI.ThreeState.mean_degreeTest_tendsto line 193
  22. def OAI.ThreeState.IsPosteriorFixedPoint line 214
  23. lemma OAI.ThreeState.orderedLaw_succ line 219
  24. lemma OAI.ThreeState.ordered_exists_fixedpoint line 222
  25. def OAI.ThreeState.messageTV line 239
  26. lemma OAI.ThreeState.continuous_messageTV line 241
  27. def OAI.ThreeState.messageTVMap line 247
  28. lemma OAI.ThreeState.posterior_tv_likelihood line 249
  29. lemma OAI.ThreeState.integral_messageTV_likelihood line 258
  30. lemma OAI.ThreeState.advantage_tendsto_of_likelihood line 268
  31. lemma OAI.ThreeState.exists_fixedpoint_advantage line 276