:: Definition and Some Properties of Information Entropy :: by Bo Zhang and Yatsuka Nakamura :: :: Received July 9, 2007 :: Copyright (c) 2007-2012 Association of Mizar Users begin theorem Th1: :: ENTROPY1:1 for k, i, l, j being Element of NAT st k <> 0 & i < l & l <= j & k divides l holds i div k < j div k proofend; theorem Th2: :: ENTROPY1:2 for r being Real st r > 0 holds ( ln . r <= r - 1 & ( r = 1 implies ln . r = r - 1 ) & ( ln . r = r - 1 implies r = 1 ) & ( r <> 1 implies ln . r < r - 1 ) & ( ln . r < r - 1 implies r <> 1 ) ) proofend; theorem Th3: :: ENTROPY1:3 for r being Real st r > 0 holds ( log (number_e,r) <= r - 1 & ( r = 1 implies log (number_e,r) = r - 1 ) & ( log (number_e,r) = r - 1 implies r = 1 ) & ( r <> 1 implies log (number_e,r) < r - 1 ) & ( log (number_e,r) < r - 1 implies r <> 1 ) ) proofend; theorem Th4: :: ENTROPY1:4 for a, b being Real st a > 1 & b > 1 holds log (a,b) > 0 proofend; theorem Th5: :: ENTROPY1:5 for a, b being Real st a > 0 & a <> 1 & b > 0 holds - (log (a,b)) = log (a,(1 / b)) proofend; theorem Th6: :: ENTROPY1:6 for a, b, c being Real st a > 0 & a <> 1 & b >= 0 & c >= 0 holds (b * c) * (log (a,(b * c))) = ((b * c) * (log (a,b))) + ((b * c) * (log (a,c))) proofend; theorem Th7: :: ENTROPY1:7 for q, q1, q2 being FinSequence of REAL st len q1 = len q & len q1 = len q2 & ( for k being Element of NAT st k in dom q1 holds q . k = (q1 . k) + (q2 . k) ) holds Sum q = (Sum q1) + (Sum q2) proofend; theorem Th8: :: ENTROPY1:8 for q, q1, q2 being FinSequence of REAL st len q1 = len q & len q1 = len q2 & ( for k being Element of NAT st k in dom q1 holds q . k = (q1 . k) - (q2 . k) ) holds Sum q = (Sum q1) - (Sum q2) proofend; theorem Th9: :: ENTROPY1:9 for p being FinSequence of REAL st len p >= 1 holds ex q being FinSequence of REAL st ( len q = len p & q . 1 = p . 1 & ( for k being Element of NAT st 0 <> k & k < len p holds q . (k + 1) = (q . k) + (p . (k + 1)) ) & Sum p = q . (len p) ) proofend; notation let p be FinSequence of REAL ; synonym nonnegative p for nonnegative-yielding ; end; definition let p be FinSequence of REAL ; redefine attr p is nonnegative-yielding means :Def1: :: ENTROPY1:def 1 for i being Element of NAT st i in dom p holds p . i >= 0 ; compatibility ( p is nonnegative iff for i being Element of NAT st i in dom p holds p . i >= 0 ) proofend; end; :: deftheorem Def1 defines nonnegative ENTROPY1:def_1_:_ for p being FinSequence of REAL holds ( p is nonnegative iff for i being Element of NAT st i in dom p holds p . i >= 0 ); registration cluster Relation-like NAT -defined REAL -valued Function-like V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() nonnegative for FinSequence of REAL ; existence ex b1 being FinSequence of REAL st b1 is nonnegative proofend; end; theorem Th10: :: ENTROPY1:10 for r being Real for p being FinSequence of REAL st p is nonnegative & r >= 0 holds r * p is nonnegative proofend; definition let p be FinSequence of REAL ; let k be Element of NAT ; predp has_onlyone_value_in k means :Def2: :: ENTROPY1:def 2 ( k in dom p & ( for i being Element of NAT st i in dom p & i <> k holds p . i = 0 ) ); end; :: deftheorem Def2 defines has_onlyone_value_in ENTROPY1:def_2_:_ for p being FinSequence of REAL for k being Element of NAT holds ( p has_onlyone_value_in k iff ( k in dom p & ( for i being Element of NAT st i in dom p & i <> k holds p . i = 0 ) ) ); theorem :: ENTROPY1:11 for k, i being Element of NAT for p being FinSequence of REAL st p has_onlyone_value_in k & i <> k holds p . i = 0 proofend; theorem Th12: :: ENTROPY1:12 for k being Element of NAT for p, q being FinSequence of REAL st len p = len q & p has_onlyone_value_in k holds ( mlt (p,q) has_onlyone_value_in k & (mlt (p,q)) . k = (p . k) * (q . k) ) proofend; theorem Th13: :: ENTROPY1:13 for k being Element of NAT for p being FinSequence of REAL st p has_onlyone_value_in k holds Sum p = p . k proofend; theorem Th14: :: ENTROPY1:14 for p being FinSequence of REAL st p is nonnegative holds for k being Element of NAT st k in dom p & p . k = Sum p holds p has_onlyone_value_in k proofend; registration cluster ProbFinS -> non empty nonnegative for FinSequence of REAL ; coherence for b1 being FinSequence of REAL st b1 is ProbFinS holds ( not b1 is empty & b1 is nonnegative ) proofend; end; theorem Th15: :: ENTROPY1:15 for p being ProbFinS FinSequence of REAL for k being Element of NAT st k in dom p & p . k = 1 holds p has_onlyone_value_in k proofend; theorem Th16: :: ENTROPY1:16 for i being non empty Nat holds i |-> (1 / i) is ProbFinS FinSequence of REAL proofend; registration cluster tabular with_sum=1 -> non empty-yielding for FinSequence of REAL * ; coherence for b1 being Matrix of REAL st b1 is with_sum=1 holds not b1 is empty-yielding proofend; cluster tabular Joint_Probability -> non empty-yielding for FinSequence of REAL * ; coherence for b1 being Matrix of REAL st b1 is Joint_Probability holds not b1 is empty-yielding ; end; theorem :: ENTROPY1:17 for M being Matrix of REAL st M = {} holds SumAll M = 0 proofend; theorem Th18: :: ENTROPY1:18 for D being non empty set for M being Matrix of D for i being Element of NAT st i in dom M holds dom (M . i) = Seg (width M) proofend; theorem Th19: :: ENTROPY1:19 for MR being Matrix of REAL holds ( MR is m-nonnegative iff for i being Element of NAT st i in dom MR holds Line (MR,i) is nonnegative ) proofend; begin theorem Th20: :: ENTROPY1:20 for p being FinSequence of REAL for j being Element of NAT st j in dom p holds Col ((LineVec2Mx p),j) = <*(p . j)*> proofend; theorem Th21: :: ENTROPY1:21 for p being non empty FinSequence of REAL for q being FinSequence of REAL for M being Matrix of REAL holds ( M = (ColVec2Mx p) * (LineVec2Mx q) iff ( len M = len p & width M = len q & ( for i, j being Element of NAT st [i,j] in Indices M holds M * (i,j) = (p . i) * (q . j) ) ) ) proofend; theorem Th22: :: ENTROPY1:22 for p being non empty FinSequence of REAL for q being FinSequence of REAL for M being Matrix of REAL holds ( M = (ColVec2Mx p) * (LineVec2Mx q) iff ( len M = len p & width M = len q & ( for i being Element of NAT st i in dom M holds Line (M,i) = (p . i) * q ) ) ) proofend; theorem Th23: :: ENTROPY1:23 for p, q being ProbFinS FinSequence of REAL holds (ColVec2Mx p) * (LineVec2Mx q) is Joint_Probability proofend; definition let n be Nat; let MR be Matrix of n, REAL ; attrMR is diagonal means :Def3: :: ENTROPY1:def 3 for i, j being Element of NAT st [i,j] in Indices MR & MR * (i,j) <> 0 holds i = j; end; :: deftheorem Def3 defines diagonal ENTROPY1:def_3_:_ for n being Nat for MR being Matrix of n, REAL holds ( MR is diagonal iff for i, j being Element of NAT st [i,j] in Indices MR & MR * (i,j) <> 0 holds i = j ); registration let n be Nat; cluster Relation-like NAT -defined REAL * -valued Function-like V47() FinSequence-like FinSubsequence-like tabular diagonal for Matrix of n,n, REAL ; existence ex b1 being Matrix of n, REAL st b1 is diagonal proofend; end; theorem Th24: :: ENTROPY1:24 for n being Nat for MR being Matrix of n, REAL holds ( MR is diagonal iff for i being Element of NAT st i in dom MR holds Line (MR,i) has_onlyone_value_in i ) proofend; definition let p be FinSequence of REAL ; func Vec2DiagMx p -> diagonal Matrix of len p, REAL means :Def4: :: ENTROPY1:def 4 for j being Element of NAT st j in dom p holds it * (j,j) = p . j; existence ex b1 being diagonal Matrix of len p, REAL st for j being Element of NAT st j in dom p holds b1 * (j,j) = p . j proofend; uniqueness for b1, b2 being diagonal Matrix of len p, REAL st ( for j being Element of NAT st j in dom p holds b1 * (j,j) = p . j ) & ( for j being Element of NAT st j in dom p holds b2 * (j,j) = p . j ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines Vec2DiagMx ENTROPY1:def_4_:_ for p being FinSequence of REAL for b2 being diagonal Matrix of len p, REAL holds ( b2 = Vec2DiagMx p iff for j being Element of NAT st j in dom p holds b2 * (j,j) = p . j ); theorem Th25: :: ENTROPY1:25 for p being FinSequence of REAL for MR being Matrix of REAL holds ( MR = Vec2DiagMx p iff ( len MR = len p & width MR = len p & ( for i being Element of NAT st i in dom MR holds ( Line (MR,i) has_onlyone_value_in i & (Line (MR,i)) . i = p . i ) ) ) ) proofend; theorem Th26: :: ENTROPY1:26 for p being FinSequence of REAL for MR, MR1 being Matrix of REAL st len p = len MR holds ( MR1 = (Vec2DiagMx p) * MR iff ( len MR1 = len p & width MR1 = width MR & ( for i, j being Element of NAT st [i,j] in Indices MR1 holds MR1 * (i,j) = (p . i) * (MR * (i,j)) ) ) ) proofend; theorem Th27: :: ENTROPY1:27 for p being FinSequence of REAL for MR, MR1 being Matrix of REAL st len p = len MR holds ( MR1 = (Vec2DiagMx p) * MR iff ( len MR1 = len p & width MR1 = width MR & ( for i being Element of NAT st i in dom MR1 holds Line (MR1,i) = (p . i) * (Line (MR,i)) ) ) ) proofend; theorem Th28: :: ENTROPY1:28 for p being ProbFinS FinSequence of REAL for M being non empty-yielding Conditional_Probability Matrix of REAL st len p = len M holds (Vec2DiagMx p) * M is Joint_Probability proofend; theorem Th29: :: ENTROPY1:29 for D being non empty set for M being Matrix of D for p being FinSequence of D * st len p = len M & p . 1 = M . 1 & ( for k being Element of NAT st k >= 1 & k < len M holds p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds for k being Element of NAT st k in dom p holds len (p . k) = k * (width M) proofend; theorem Th30: :: ENTROPY1:30 for D being non empty set for M being Matrix of D for p being FinSequence of D * st len p = len M & p . 1 = M . 1 & ( for k being Element of NAT st k >= 1 & k < len M holds p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds for i, j being Element of NAT st i in dom p & j in dom p & i <= j holds dom (p . i) c= dom (p . j) proofend; theorem Th31: :: ENTROPY1:31 for D being non empty set for M being Matrix of D for p being FinSequence of D * st len p = len M & p . 1 = M . 1 & ( for k being Element of NAT st k >= 1 & k < len M holds p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds ( len (p . 1) = width M & ( for j being Element of NAT st [1,j] in Indices M holds ( j in dom (p . 1) & (p . 1) . j = M * (1,j) ) ) ) proofend; theorem Th32: :: ENTROPY1:32 for D being non empty set for M being Matrix of D for p being FinSequence of D * st len p = len M & ( for k being Element of NAT st k >= 1 & k < len M holds p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds for j being Element of NAT st j >= 1 & j < len p holds for l being Element of NAT st l in dom (p . j) holds (p . j) . l = (p . (j + 1)) . l proofend; theorem Th33: :: ENTROPY1:33 for D being non empty set for M being Matrix of D for p being FinSequence of D * st len p = len M & p . 1 = M . 1 & ( for k being Element of NAT st k >= 1 & k < len M holds p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds for i, j being Element of NAT st i in dom p & j in dom p & i <= j holds for l being Element of NAT st l in dom (p . i) holds (p . i) . l = (p . j) . l proofend; theorem Th34: :: ENTROPY1:34 for D being non empty set for M being Matrix of D for p being FinSequence of D * st len p = len M & p . 1 = M . 1 & ( for k being Element of NAT st k >= 1 & k < len M holds p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds for j being Element of NAT st j >= 1 & j < len p holds for l being Element of NAT st l in Seg (width M) holds ( (j * (width M)) + l in dom (p . (j + 1)) & (p . (j + 1)) . ((j * (width M)) + l) = (M . (j + 1)) . l ) proofend; theorem Th35: :: ENTROPY1:35 for D being non empty set for M being Matrix of D for p being FinSequence of D * st len p = len M & p . 1 = M . 1 & ( for k being Element of NAT st k >= 1 & k < len M holds p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds for i, j being Element of NAT st [i,j] in Indices M holds ( ((i - 1) * (width M)) + j in dom (p . i) & M * (i,j) = (p . i) . (((i - 1) * (width M)) + j) ) proofend; theorem Th36: :: ENTROPY1:36 for D being non empty set for M being Matrix of D for p being FinSequence of D * st len p = len M & p . 1 = M . 1 & ( for k being Element of NAT st k >= 1 & k < len M holds p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds for i, j being Element of NAT st [i,j] in Indices M holds ( ((i - 1) * (width M)) + j in dom (p . (len M)) & M * (i,j) = (p . (len M)) . (((i - 1) * (width M)) + j) ) proofend; theorem Th37: :: ENTROPY1:37 for M being Matrix of REAL for p being FinSequence of REAL * st ( for k being Element of NAT st k >= 1 & k < len M holds p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds for k being Element of NAT st k >= 1 & k < len M holds Sum (p . (k + 1)) = (Sum (p . k)) + (Sum (M . (k + 1))) proofend; theorem Th38: :: ENTROPY1:38 for M being Matrix of REAL for p being FinSequence of REAL * st len p = len M & p . 1 = M . 1 & ( for k being Element of NAT st k >= 1 & k < len M holds p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds SumAll M = Sum (p . (len M)) proofend; definition let D be non empty set ; let M be Matrix of D; func Mx2FinS M -> FinSequence of D means :Def5: :: ENTROPY1:def 5 it = {} if len M = 0 otherwise ex p being FinSequence of D * st ( it = p . (len M) & len p = len M & p . 1 = M . 1 & ( for k being Element of NAT st k >= 1 & k < len M holds p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ); existence ( ( len M = 0 implies ex b1 being FinSequence of D st b1 = {} ) & ( not len M = 0 implies ex b1 being FinSequence of D ex p being FinSequence of D * st ( b1 = p . (len M) & len p = len M & p . 1 = M . 1 & ( for k being Element of NAT st k >= 1 & k < len M holds p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) ) ) proofend; uniqueness for b1, b2 being FinSequence of D holds ( ( len M = 0 & b1 = {} & b2 = {} implies b1 = b2 ) & ( not len M = 0 & ex p being FinSequence of D * st ( b1 = p . (len M) & len p = len M & p . 1 = M . 1 & ( for k being Element of NAT st k >= 1 & k < len M holds p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) & ex p being FinSequence of D * st ( b2 = p . (len M) & len p = len M & p . 1 = M . 1 & ( for k being Element of NAT st k >= 1 & k < len M holds p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) implies b1 = b2 ) ) proofend; consistency for b1 being FinSequence of D holds verum ; end; :: deftheorem Def5 defines Mx2FinS ENTROPY1:def_5_:_ for D being non empty set for M being Matrix of D for b3 being FinSequence of D holds ( ( len M = 0 implies ( b3 = Mx2FinS M iff b3 = {} ) ) & ( not len M = 0 implies ( b3 = Mx2FinS M iff ex p being FinSequence of D * st ( b3 = p . (len M) & len p = len M & p . 1 = M . 1 & ( for k being Element of NAT st k >= 1 & k < len M holds p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) ) ) ); theorem Th39: :: ENTROPY1:39 for D being non empty set for M being Matrix of D holds len (Mx2FinS M) = (len M) * (width M) proofend; theorem Th40: :: ENTROPY1:40 for D being non empty set for M being Matrix of D for i, j being Element of NAT st [i,j] in Indices M holds ( ((i - 1) * (width M)) + j in dom (Mx2FinS M) & M * (i,j) = (Mx2FinS M) . (((i - 1) * (width M)) + j) ) proofend; theorem Th41: :: ENTROPY1:41 for D being non empty set for M being Matrix of D for k, l being Element of NAT st k in dom (Mx2FinS M) & l = k - 1 holds ( [((l div (width M)) + 1),((l mod (width M)) + 1)] in Indices M & (Mx2FinS M) . k = M * (((l div (width M)) + 1),((l mod (width M)) + 1)) ) proofend; theorem Th42: :: ENTROPY1:42 for MR being Matrix of REAL holds SumAll MR = Sum (Mx2FinS MR) proofend; theorem Th43: :: ENTROPY1:43 for MR being Matrix of REAL holds ( MR is m-nonnegative iff Mx2FinS MR is nonnegative ) proofend; theorem Th44: :: ENTROPY1:44 for MR being Matrix of REAL holds ( MR is Joint_Probability iff Mx2FinS MR is ProbFinS ) proofend; theorem Th45: :: ENTROPY1:45 for p, q being ProbFinS FinSequence of REAL holds Mx2FinS ((ColVec2Mx p) * (LineVec2Mx q)) is ProbFinS proofend; theorem :: ENTROPY1:46 for p being ProbFinS FinSequence of REAL for M being non empty-yielding Conditional_Probability Matrix of REAL st len p = len M holds Mx2FinS ((Vec2DiagMx p) * M) is ProbFinS proofend; begin definition let a be Real; let p be FinSequence of REAL ; assume A1: p is nonnegative ; func FinSeq_log (a,p) -> FinSequence of REAL means :Def6: :: ENTROPY1:def 6 ( len it = len p & ( for k being Nat st k in dom it holds ( ( p . k > 0 implies it . k = log (a,(p . k)) ) & ( p . k = 0 implies it . k = 0 ) ) ) ); existence ex b1 being FinSequence of REAL st ( len b1 = len p & ( for k being Nat st k in dom b1 holds ( ( p . k > 0 implies b1 . k = log (a,(p . k)) ) & ( p . k = 0 implies b1 . k = 0 ) ) ) ) proofend; uniqueness for b1, b2 being FinSequence of REAL st len b1 = len p & ( for k being Nat st k in dom b1 holds ( ( p . k > 0 implies b1 . k = log (a,(p . k)) ) & ( p . k = 0 implies b1 . k = 0 ) ) ) & len b2 = len p & ( for k being Nat st k in dom b2 holds ( ( p . k > 0 implies b2 . k = log (a,(p . k)) ) & ( p . k = 0 implies b2 . k = 0 ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def6 defines FinSeq_log ENTROPY1:def_6_:_ for a being Real for p being FinSequence of REAL st p is nonnegative holds for b3 being FinSequence of REAL holds ( b3 = FinSeq_log (a,p) iff ( len b3 = len p & ( for k being Nat st k in dom b3 holds ( ( p . k > 0 implies b3 . k = log (a,(p . k)) ) & ( p . k = 0 implies b3 . k = 0 ) ) ) ) ); definition let p be FinSequence of REAL ; func Infor_FinSeq_of p -> FinSequence of REAL equals :: ENTROPY1:def 7 mlt (p,(FinSeq_log (2,p))); correctness coherence mlt (p,(FinSeq_log (2,p))) is FinSequence of REAL ; ; end; :: deftheorem defines Infor_FinSeq_of ENTROPY1:def_7_:_ for p being FinSequence of REAL holds Infor_FinSeq_of p = mlt (p,(FinSeq_log (2,p))); theorem Th47: :: ENTROPY1:47 for p being nonnegative FinSequence of REAL for q being FinSequence of REAL holds ( q = Infor_FinSeq_of p iff ( len q = len p & ( for k being Element of NAT st k in dom q holds q . k = (p . k) * (log (2,(p . k))) ) ) ) proofend; theorem Th48: :: ENTROPY1:48 for p being nonnegative FinSequence of REAL for k being Element of NAT st k in dom p holds ( ( p . k = 0 implies (Infor_FinSeq_of p) . k = 0 ) & ( p . k > 0 implies (Infor_FinSeq_of p) . k = (p . k) * (log (2,(p . k))) ) ) proofend; theorem :: ENTROPY1:49 for p being nonnegative FinSequence of REAL for q being FinSequence of REAL holds ( q = - (Infor_FinSeq_of p) iff ( len q = len p & ( for k being Element of NAT st k in dom q holds q . k = (p . k) * (log (2,(1 / (p . k)))) ) ) ) proofend; theorem Th50: :: ENTROPY1:50 for r1, r2 being Real for p being nonnegative FinSequence of REAL st r1 >= 0 & r2 >= 0 holds for i being Element of NAT st i in dom p & p . i = r1 * r2 holds (Infor_FinSeq_of p) . i = ((r1 * r2) * (log (2,r1))) + ((r1 * r2) * (log (2,r2))) proofend; theorem Th51: :: ENTROPY1:51 for r being Real for p being nonnegative FinSequence of REAL st r >= 0 holds Infor_FinSeq_of (r * p) = ((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p))))) proofend; theorem Th52: :: ENTROPY1:52 for p being non empty ProbFinS FinSequence of REAL for k being Element of NAT st k in dom p holds (Infor_FinSeq_of p) . k <= 0 proofend; definition let MR be Matrix of REAL; assume A1: MR is m-nonnegative ; func Infor_FinSeq_of MR -> Matrix of REAL means :Def8: :: ENTROPY1:def 8 ( len it = len MR & width it = width MR & ( for k being Element of NAT st k in dom it holds it . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) ); existence ex b1 being Matrix of REAL st ( len b1 = len MR & width b1 = width MR & ( for k being Element of NAT st k in dom b1 holds b1 . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) ) proofend; uniqueness for b1, b2 being Matrix of REAL st len b1 = len MR & width b1 = width MR & ( for k being Element of NAT st k in dom b1 holds b1 . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) & len b2 = len MR & width b2 = width MR & ( for k being Element of NAT st k in dom b2 holds b2 . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) holds b1 = b2 proofend; end; :: deftheorem Def8 defines Infor_FinSeq_of ENTROPY1:def_8_:_ for MR being Matrix of REAL st MR is m-nonnegative holds for b2 being Matrix of REAL holds ( b2 = Infor_FinSeq_of MR iff ( len b2 = len MR & width b2 = width MR & ( for k being Element of NAT st k in dom b2 holds b2 . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) ) ); theorem Th53: :: ENTROPY1:53 for M being m-nonnegative Matrix of REAL for k being Element of NAT st k in dom M holds Line ((Infor_FinSeq_of M),k) = Infor_FinSeq_of (Line (M,k)) proofend; theorem Th54: :: ENTROPY1:54 for M being m-nonnegative Matrix of REAL for M1 being Matrix of REAL holds ( M1 = Infor_FinSeq_of M iff ( len M1 = len M & width M1 = width M & ( for i, j being Element of NAT st [i,j] in Indices M1 holds M1 * (i,j) = (M * (i,j)) * (log (2,(M * (i,j)))) ) ) ) proofend; definition let p be FinSequence of REAL ; func Entropy p -> Real equals :: ENTROPY1:def 9 - (Sum (Infor_FinSeq_of p)); correctness coherence - (Sum (Infor_FinSeq_of p)) is Real; ; end; :: deftheorem defines Entropy ENTROPY1:def_9_:_ for p being FinSequence of REAL holds Entropy p = - (Sum (Infor_FinSeq_of p)); theorem :: ENTROPY1:55 for p being non empty ProbFinS FinSequence of REAL holds Entropy p >= 0 proofend; theorem :: ENTROPY1:56 for p being non empty ProbFinS FinSequence of REAL st ex k being Element of NAT st ( k in dom p & p . k = 1 ) holds Entropy p = 0 proofend; theorem Th57: :: ENTROPY1:57 for p, q being non empty ProbFinS FinSequence of REAL for pp, qq being FinSequence of REAL st len p = len q & len pp = len p & len qq = len q & ( for k being Element of NAT st k in dom p holds ( p . k > 0 & q . k > 0 & pp . k = - ((p . k) * (log (2,(p . k)))) & qq . k = - ((p . k) * (log (2,(q . k)))) ) ) holds ( Sum pp <= Sum qq & ( ( for k being Element of NAT st k in dom p holds p . k = q . k ) implies Sum pp = Sum qq ) & ( Sum pp = Sum qq implies for k being Element of NAT st k in dom p holds p . k = q . k ) & ( ex k being Element of NAT st ( k in dom p & p . k <> q . k ) implies Sum pp < Sum qq ) & ( Sum pp < Sum qq implies ex k being Element of NAT st ( k in dom p & p . k <> q . k ) ) ) proofend; theorem :: ENTROPY1:58 for p being non empty ProbFinS FinSequence of REAL st ( for k being Element of NAT st k in dom p holds p . k > 0 ) holds ( Entropy p <= log (2,(len p)) & ( ( for k being Element of NAT st k in dom p holds p . k = 1 / (len p) ) implies Entropy p = log (2,(len p)) ) & ( Entropy p = log (2,(len p)) implies for k being Element of NAT st k in dom p holds p . k = 1 / (len p) ) & ( ex k being Element of NAT st ( k in dom p & p . k <> 1 / (len p) ) implies Entropy p < log (2,(len p)) ) & ( Entropy p < log (2,(len p)) implies ex k being Element of NAT st ( k in dom p & p . k <> 1 / (len p) ) ) ) proofend; theorem Th59: :: ENTROPY1:59 for M being m-nonnegative Matrix of REAL holds Mx2FinS (Infor_FinSeq_of M) = Infor_FinSeq_of (Mx2FinS M) proofend; theorem Th60: :: ENTROPY1:60 for p, q being ProbFinS FinSequence of REAL for M being Matrix of REAL st M = (ColVec2Mx p) * (LineVec2Mx q) holds SumAll (Infor_FinSeq_of M) = (Sum (Infor_FinSeq_of p)) + (Sum (Infor_FinSeq_of q)) proofend; definition let MR be Matrix of REAL; func Entropy_of_Joint_Prob MR -> Real equals :: ENTROPY1:def 10 Entropy (Mx2FinS MR); coherence Entropy (Mx2FinS MR) is Real ; end; :: deftheorem defines Entropy_of_Joint_Prob ENTROPY1:def_10_:_ for MR being Matrix of REAL holds Entropy_of_Joint_Prob MR = Entropy (Mx2FinS MR); theorem :: ENTROPY1:61 for p, q being ProbFinS FinSequence of REAL holds Entropy_of_Joint_Prob ((ColVec2Mx p) * (LineVec2Mx q)) = (Entropy p) + (Entropy q) proofend; definition let MR be Matrix of REAL; func Entropy_of_Cond_Prob MR -> FinSequence of REAL means :Def11: :: ENTROPY1:def 11 ( len it = len MR & ( for k being Element of NAT st k in dom it holds it . k = Entropy (Line (MR,k)) ) ); existence ex b1 being FinSequence of REAL st ( len b1 = len MR & ( for k being Element of NAT st k in dom b1 holds b1 . k = Entropy (Line (MR,k)) ) ) proofend; uniqueness for b1, b2 being FinSequence of REAL st len b1 = len MR & ( for k being Element of NAT st k in dom b1 holds b1 . k = Entropy (Line (MR,k)) ) & len b2 = len MR & ( for k being Element of NAT st k in dom b2 holds b2 . k = Entropy (Line (MR,k)) ) holds b1 = b2 proofend; end; :: deftheorem Def11 defines Entropy_of_Cond_Prob ENTROPY1:def_11_:_ for MR being Matrix of REAL for b2 being FinSequence of REAL holds ( b2 = Entropy_of_Cond_Prob MR iff ( len b2 = len MR & ( for k being Element of NAT st k in dom b2 holds b2 . k = Entropy (Line (MR,k)) ) ) ); theorem Th62: :: ENTROPY1:62 for M being non empty-yielding Conditional_Probability Matrix of REAL for p being FinSequence of REAL holds ( p = Entropy_of_Cond_Prob M iff ( len p = len M & ( for k being Element of NAT st k in dom p holds p . k = - (Sum ((Infor_FinSeq_of M) . k)) ) ) ) proofend; theorem Th63: :: ENTROPY1:63 for M being non empty-yielding Conditional_Probability Matrix of REAL holds Entropy_of_Cond_Prob M = - (LineSum (Infor_FinSeq_of M)) proofend; theorem Th64: :: ENTROPY1:64 for p being ProbFinS FinSequence of REAL for M being non empty-yielding Conditional_Probability Matrix of REAL st len p = len M holds for M1 being Matrix of REAL st M1 = (Vec2DiagMx p) * M holds SumAll (Infor_FinSeq_of M1) = (Sum (Infor_FinSeq_of p)) + (Sum (mlt (p,(LineSum (Infor_FinSeq_of M))))) proofend; theorem :: ENTROPY1:65 for p being ProbFinS FinSequence of REAL for M being non empty-yielding Conditional_Probability Matrix of REAL st len p = len M holds Entropy_of_Joint_Prob ((Vec2DiagMx p) * M) = (Entropy p) + (Sum (mlt (p,(Entropy_of_Cond_Prob M)))) proofend;