src/HOL/Probability/Information.thy
changeset 36649 bfd8c550faa6
parent 36624 25153c08655e
child 38656 d5d342611edb
equal deleted inserted replaced
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: