:: Definition and Some Properties of Information Entropy :: by Bo Zhang and Yatsuka Nakamura :: :: Received July 9, 2007 :: Copyright (c) 2007-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, SUBSET_1, NAT_1, REAL_1, FINSEQ_1, MATRIX_1, CARD_1, ARYTM_3, XXREAL_0, INT_1, ARYTM_1, RELAT_1, TAYLOR_1, FUNCT_1, XXREAL_1, LIMFUNC1, POWER, PARTFUN1, FDIFF_1, ORDINAL2, TARSKI, CARD_3, SEQ_1, SUPINF_2, PARTFUN3, RVSUM_1, ORDINAL4, FINSEQ_2, MATRPROB, MATRIXC1, TREES_1, INCSP_1, MATRIXR1, FVSUM_1, ZFMISC_1, FUNCOP_1, ENTROPY1, FUNCT_7, XCMPLX_0; notations TARSKI, SUBSET_1, XBOOLE_0, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, ORDINAL1, NAT_1, NAT_D, NUMBERS, RELAT_1, FUNCT_1, VALUED_1, SEQ_1, ZFMISC_1, PARTFUN1, FUNCOP_1, RVSUM_1, FINSEQ_1, NEWTON, FINSEQ_2, MATRIXR1, MATRIX_0, PARTFUN3, POWER, LIMFUNC1, RCOMP_1, MATRPROB, FDIFF_1, TAYLOR_1, FCONT_1; constructors REAL_1, NAT_D, BINOP_2, MATRIX_3, MATRIXR1, MATRLIN, MATRPROB, PARTFUN3, PARTFUN2, FDIFF_1, FCONT_1, POWER, LIMFUNC1, SIN_COS, TAYLOR_1, INTEGRA1, XXREAL_2, RVSUM_1, RELSET_1, NEWTON, NUMBERS; registrations MATRPROB, RELSET_1, NAT_1, MEMBERED, ORDINAL1, XREAL_0, FCONT_3, RCOMP_1, XXREAL_0, NUMBERS, XBOOLE_0, VALUED_0, FINSEQ_1, CARD_1, XXREAL_2, FINSEQ_2, RVSUM_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Preliminaries reserve D for non empty set, i,j,k,l for Nat, n for Nat, x for set, a,b,c,r,r1,r2 for Real, p,q for FinSequence of REAL, MR,MR1 for Matrix of REAL; theorem :: ENTROPY1:1 k <> 0 & i < l & l <= j & k divides l implies i div k < j div k; theorem :: ENTROPY1:2 r > 0 implies ln.r <= r - 1 & (r = 1 iff ln.r = r - 1) & (r <> 1 iff ln.r < r - 1); theorem :: ENTROPY1:3 r > 0 implies log(number_e,r) <= r - 1 & (r = 1 iff log(number_e, r) = r - 1) & (r <> 1 iff log(number_e,r) < r - 1); theorem :: ENTROPY1:4 a>1 & b>1 implies log(a,b) > 0; theorem :: ENTROPY1:5 a>0 & a<>1 & b>0 implies -log(a,b) = log(a,1/b); theorem :: ENTROPY1:6 a>0 & a<>1 & b>=0 & c>=0 implies b*c*log(a,b*c) = b*c*log(a,b)+b* c*log(a,c); theorem :: ENTROPY1:7 for q,q1,q2 being FinSequence of REAL st len q1 = len q & len q1 = len q2 & (for k st k in dom q1 holds q.k = q1.k + q2.k) holds Sum q = Sum q1 + Sum q2; theorem :: ENTROPY1:8 for q,q1,q2 being FinSequence of REAL st len q1 = len q & len q1 = len q2 & (for k st k in dom q1 holds q.k = q1.k - q2.k) holds Sum q = Sum q1 - Sum q2; theorem :: ENTROPY1:9 len p >= 1 implies ex q st len q = len p & q.1 = p.1 & (for k st 0 <> k & k < len p holds q.(k+1) = q.k + p.(k+1)) & Sum p = q.(len p); notation let p; synonym p is nonnegative for p is nonnegative-yielding; end; definition let p; redefine attr p is nonnegative means :: ENTROPY1:def 1 for i st i in dom p holds p.i >= 0; end; registration cluster nonnegative for FinSequence of REAL; end; theorem :: ENTROPY1:10 p is nonnegative & r>=0 implies r*p is nonnegative; definition let p,k; pred p has_onlyone_value_in k means :: ENTROPY1:def 2 k in dom p & for i st i in dom p & i<>k holds p.i=0; end; theorem :: ENTROPY1:11 p has_onlyone_value_in k & i<>k implies p.i=0; theorem :: ENTROPY1:12 len p = len q & p has_onlyone_value_in k implies mlt(p,q) has_onlyone_value_in k & mlt(p,q).k = p.k * q.k; theorem :: ENTROPY1:13 p has_onlyone_value_in k implies Sum p = p.k; theorem :: ENTROPY1:14 p is nonnegative implies for k st k in dom p & p.k = Sum p holds p has_onlyone_value_in k; registration cluster ProbFinS -> non empty nonnegative for FinSequence of REAL; end; theorem :: ENTROPY1:15 for p being ProbFinS FinSequence of REAL for k st k in dom p & p .k = 1 holds p has_onlyone_value_in k; theorem :: ENTROPY1:16 for i being non zero Nat holds i |-> (1/i) is ProbFinS FinSequence of REAL; registration cluster with_sum=1 -> non empty-yielding for Matrix of REAL; cluster Joint_Probability -> non empty-yielding for Matrix of REAL; end; theorem :: ENTROPY1:17 for M being Matrix of REAL st M = {} holds SumAll M = 0; theorem :: ENTROPY1:18 for M being Matrix of D holds for i st i in dom M holds dom(M.i) = Seg width M; theorem :: ENTROPY1:19 MR is m-nonnegative iff for i st i in dom MR holds Line(MR,i) is nonnegative; begin :: Properties on Transformations between Vector and Matrix theorem :: ENTROPY1:20 for j st j in dom p holds Col(LineVec2Mx p,j) = <*p.j*>; theorem :: 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 st [i,j] in Indices M holds M*(i,j) = p.i * q.j); theorem :: 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 st i in dom M holds Line(M,i) = p.i * q); theorem :: ENTROPY1:23 for p,q being ProbFinS FinSequence of REAL holds (ColVec2Mx p) * (LineVec2Mx q) is Joint_Probability; definition let n; let MR be Matrix of n,REAL; attr MR is diagonal means :: ENTROPY1:def 3 for i,j st [i,j] in Indices MR & MR*(i,j) <> 0 holds i=j; end; registration let n; cluster diagonal for Matrix of n,REAL; end; theorem :: ENTROPY1:24 for MR being Matrix of n,REAL holds MR is diagonal iff for i st i in dom MR holds Line(MR,i) has_onlyone_value_in i; definition let p; func Vec2DiagMx p -> diagonal Matrix of len p,REAL means :: ENTROPY1:def 4 for j st j in dom p holds it*(j,j) = p.j; end; theorem :: ENTROPY1:25 MR=Vec2DiagMx p iff len MR = len p & width MR = len p & for i st i in dom MR holds Line(MR,i) has_onlyone_value_in i & Line(MR,i).i=p.i; theorem :: ENTROPY1:26 len p = len MR implies (MR1 = (Vec2DiagMx p) * MR iff len MR1 = len p & width MR1 = width MR & for i,j st [i,j] in Indices MR1 holds MR1*(i,j) = p.i * (MR*(i,j))); theorem :: ENTROPY1:27 len p = len MR implies (MR1 = (Vec2DiagMx p) * MR iff len MR1 = len p & width MR1 = width MR & for i st i in dom MR1 holds Line(MR1,i) = p.i * Line(MR,i)); theorem :: 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; theorem :: ENTROPY1:29 for M being Matrix of D for p being FinSequence of D* st len p = len M & p.1 = M.1 & (for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1 )) holds for k st k in dom p holds len (p.k) = k * width M; theorem :: ENTROPY1:30 for M being Matrix of D for p being FinSequence of D* st len p = len M & p.1 = M.1 & (for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1 )) holds for i,j st i in dom p & j in dom p & i <= j holds dom (p.i) c= dom (p. j); theorem :: ENTROPY1:31 for M being Matrix of D for p being FinSequence of D* st len p = len M & p.1 = M.1 & (for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1 )) holds len (p.1) = width M & for j st [1,j] in Indices M holds j in dom (p.1) & (p.1).j = M*(1,j); theorem :: ENTROPY1:32 for M being Matrix of D for p being FinSequence of D* st len p = len M & (for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1)) holds for j st j >= 1 & j < len p holds for l st l in dom(p.j) holds (p.j).l = (p.(j+1)). l; theorem :: ENTROPY1:33 for M being Matrix of D for p being FinSequence of D* st len p = len M & p.1 = M.1 & (for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1 )) holds for i,j st i in dom p & j in dom p & i <= j holds for l st l in dom(p. i) holds (p.i).l = (p.j).l; theorem :: ENTROPY1:34 for M being Matrix of D for p being FinSequence of D* st len p = len M & p.1 = M.1 & (for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1 )) holds for j st j >= 1 & j < len p holds for l 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; theorem :: ENTROPY1:35 for M being Matrix of D for p being FinSequence of D* st len p = len M & p.1 = M.1 & (for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1 )) holds for i,j 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); theorem :: ENTROPY1:36 for M being Matrix of D for p being FinSequence of D* st len p = len M & p.1 = M.1 & (for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1 )) holds for i,j 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); theorem :: ENTROPY1:37 for M being Matrix of REAL for p being FinSequence of REAL* st ( for k st k >= 1 & k < len M holds p.(k+1)=(p.k) ^ M.(k+1)) holds for k st k >= 1 & k < len M holds Sum(p.(k+1))=Sum(p.k)+Sum(M.(k+1)); theorem :: 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 st k >= 1 & k < len M holds p.(k+1)=(p.k) ^ M.(k+1)) holds SumAll M = Sum(p.(len M)); definition let D be non empty set; let M be Matrix of D; func Mx2FinS(M) -> FinSequence of D means :: 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 st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1); end; theorem :: ENTROPY1:39 for M being Matrix of D holds len Mx2FinS(M) = len M * width M; theorem :: ENTROPY1:40 for M being Matrix of D for i,j 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); theorem :: ENTROPY1:41 for M being Matrix of D for k,l 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)); theorem :: ENTROPY1:42 SumAll MR = Sum Mx2FinS MR; theorem :: ENTROPY1:43 MR is m-nonnegative iff Mx2FinS(MR) is nonnegative; theorem :: ENTROPY1:44 MR is Joint_Probability iff Mx2FinS(MR) is ProbFinS; theorem :: ENTROPY1:45 for p,q being ProbFinS FinSequence of REAL holds Mx2FinS(( ColVec2Mx p) * (LineVec2Mx q)) is ProbFinS; 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; begin :: Information Entropy definition let a be Real; let p; assume that p is nonnegative; func FinSeq_log(a,p) -> FinSequence of REAL means :: ENTROPY1:def 6 len it = len p & for k be Nat st k in dom it holds (p.k > 0 implies it.k = log(a,p.k)) & (p.k = 0 implies it.k = 0); end; definition let p; func Infor_FinSeq_of p -> FinSequence of REAL equals :: ENTROPY1:def 7 mlt(p,FinSeq_log(2,p)); end; theorem :: ENTROPY1:47 for p being nonnegative FinSequence of REAL for q holds q = Infor_FinSeq_of p iff len q = len p & for k st k in dom q holds q.k = p.k * log (2,p.k); theorem :: ENTROPY1:48 for p being nonnegative FinSequence of REAL for k 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)); theorem :: ENTROPY1:49 for p being nonnegative FinSequence of REAL for q holds q = - Infor_FinSeq_of p iff (len q = len p & for k st k in dom q holds q.k = p.k * log(2,1/(p.k))); theorem :: ENTROPY1:50 for p being nonnegative FinSequence of REAL st r1>=0 & r2>=0 holds for i 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); theorem :: ENTROPY1:51 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))); theorem :: ENTROPY1:52 for p being non empty ProbFinS FinSequence of REAL for k st k in dom p holds (Infor_FinSeq_of p).k <= 0; definition let MR; assume MR is m-nonnegative; func Infor_FinSeq_of MR -> Matrix of REAL means :: ENTROPY1:def 8 len it = len MR & width it = width MR & for k st k in dom it holds it.k=mlt(Line(MR,k),FinSeq_log (2,Line(MR,k))); end; theorem :: ENTROPY1:53 for M being m-nonnegative Matrix of REAL for k st k in dom M holds Line(Infor_FinSeq_of M,k) = Infor_FinSeq_of Line(M,k); theorem :: 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 st [i,j] in Indices M1 holds M1*(i,j)=M*(i,j)*log(2,M*(i,j)); definition let p being FinSequence of REAL; func Entropy p -> Real equals :: ENTROPY1:def 9 -Sum Infor_FinSeq_of p; end; theorem :: ENTROPY1:55 for p being non empty ProbFinS FinSequence of REAL holds Entropy p >= 0; theorem :: ENTROPY1:56 for p being non empty ProbFinS FinSequence of REAL st ex k st k in dom p & p.k = 1 holds Entropy p = 0; theorem :: ENTROPY1:57 for p,q being non empty ProbFinS FinSequence of REAL, pp,qq being FinSequence of REAL st len p = len q & len pp = len p & len qq = len q & (for k 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 st k in dom p holds p.k=q.k) iff Sum pp = Sum qq) & ((ex k st k in dom p & p.k<>q.k) iff Sum pp < Sum qq); theorem :: ENTROPY1:58 for p being non empty ProbFinS FinSequence of REAL st (for k st k in dom p holds p.k>0) holds Entropy p <= log(2,len p) & ((for k st k in dom p holds p.k=1/(len p)) iff Entropy p=log(2,len p)) & ((ex k st k in dom p & p.k<> 1/(len p)) iff Entropy p Real equals :: ENTROPY1:def 10 Entropy Mx2FinS MR; end; theorem :: ENTROPY1:61 for p,q being ProbFinS FinSequence of REAL holds Entropy_of_Joint_Prob ((ColVec2Mx p) * (LineVec2Mx q)) = Entropy p + Entropy q; definition let MR; func Entropy_of_Cond_Prob MR -> FinSequence of REAL means :: ENTROPY1:def 11 len it = len MR & for k st k in dom it holds it.k = Entropy Line(MR,k); end; theorem :: 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 st k in dom p holds p.k = -Sum ((Infor_FinSeq_of M).k); theorem :: ENTROPY1:63 for M being non empty-yielding Conditional_Probability Matrix of REAL holds Entropy_of_Cond_Prob M = -LineSum Infor_FinSeq_of M; theorem :: 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)); 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);