changeset 36649 | bfd8c550faa6 |
parent 36624 | 25153c08655e |
child 38656 | d5d342611edb |
36648:43b66dcd9266 | 36649:bfd8c550faa6 |
---|---|
1 theory Information |
1 theory Information |
2 imports Probability_Space Product_Measure "../Multivariate_Analysis/Convex" |
2 imports Probability_Space Product_Measure Convex |
3 begin |
3 begin |
4 |
4 |
5 section "Convex theory" |
5 section "Convex theory" |
6 |
6 |
7 lemma log_setsum: |
7 lemma log_setsum: |