OAI/Probability/ThreeState/DegreePosterior.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Posterior laws by offspring degree and monotonicity of their moments.

  1. lemma OAI.ThreeState.continuous_integral_message line 13
  2. lemma OAI.ThreeState.continuous_pairIncrement line 17
  3. def OAI.ThreeState.degreePosterior line 21
  4. lemma OAI.ThreeState.integral_iid_cons line 25
  5. lemma OAI.ThreeState.normalizer_cons line 44
  6. lemma OAI.ThreeState.combineMessage_cons line 54
  7. def OAI.ThreeState.pairOperator line 71
  8. lemma OAI.ThreeState.integral_degree_succ line 76
  9. lemma OAI.ThreeState.correlationEntropy_zero line 89
  10. lemma OAI.ThreeState.correlationEntropy_succ line 93
  11. lemma OAI.ThreeState.messageX_sq_tangent line 132
  12. lemma OAI.ThreeState.integral_weighted_pair_deviation line 144
  13. lemma OAI.ThreeState.pairOperator_square_lower line 160
  14. lemma OAI.ThreeState.degree_nu_monotone line 186