OAI/Probability/ThreeState/EntropyRecursion.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Independent-branch entropy identities and correlation corrections.

  1. lemma OAI.ThreeState.iid_integral_weighted_single line 12
  2. lemma OAI.ThreeState.iid_integral_weighted_pair line 30
  3. lemma OAI.ThreeState.iid_integral_weighted_sum line 55
  4. lemma OAI.ThreeState.iid_integral_weighted_sum_sq line 67
  5. lemma OAI.ThreeState.integral_avg line 113
  6. lemma OAI.ThreeState.integral_permMessage line 119
  7. lemma OAI.ThreeState.symmetric_integral_coordinate line 126
  8. lemma OAI.ThreeState.mLog_perm line 136
  9. lemma OAI.ThreeState.mCenteredLog_perm line 139
  10. lemma OAI.ThreeState.edgeMessage_perm line 143
  11. lemma OAI.ThreeState.integral_avg_eq_coordinate line 146
  12. lemma OAI.ThreeState.integral_edge_centered line 155
  13. lemma OAI.ThreeState.integral_edge_centered_sq line 169
  14. lemma OAI.ThreeState.weighted_avg_combine line 191
  15. lemma OAI.ThreeState.weighted_entropyJ line 201
  16. lemma OAI.ThreeState.weighted_entropyB line 208
  17. def OAI.ThreeState.edgeCoordinateMap line 213
  18. def OAI.ThreeState.edgeCenteredMap line 216
  19. lemma OAI.ThreeState.integral_degree_entropyJ line 220
  20. lemma OAI.ThreeState.integral_degree_entropyB line 244
  21. lemma OAI.ThreeState.additive_entropyJ line 271
  22. lemma OAI.ThreeState.hasMean_factorialSecond line 281
  23. lemma OAI.ThreeState.additive_entropyB line 286
  24. def OAI.ThreeState.correlationEntropy line 311
  25. lemma OAI.ThreeState.continuous_log_normalizer line 316
  26. lemma OAI.ThreeState.continuous_entropyI_combine line 320
  27. lemma OAI.ThreeState.weighted_entropyI line 328
  28. def OAI.ThreeState.edgeLogMap line 340
  29. lemma OAI.ThreeState.integral_degree_entropyI line 344
  30. lemma OAI.ThreeState.correlationEntropy_nonneg line 373
  31. lemma OAI.ThreeState.correlationEntropy_bound line 389
  32. lemma OAI.ThreeState.hasMean_correlationEntropy line 411
  33. lemma OAI.ThreeState.additive_entropyI line 418
  34. lemma OAI.ThreeState.entropy_identity line 433