begin
theorem Th1:
theorem Th2:
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 ) )
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
:: deftheorem Def1 defines nonnegative ENTROPY1:def 1 :
theorem Th10:
:: deftheorem Def2 defines has_onlyone_value_in ENTROPY1:def 2 :
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem
theorem Th18:
theorem Th19:
begin
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
:: deftheorem Def3 defines diagonal ENTROPY1:def 3 :
theorem Th24:
:: deftheorem Def4 defines Vec2DiagMx ENTROPY1:def 4 :
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
:: deftheorem Def5 defines Mx2FinS ENTROPY1:def 5 :
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem
begin
:: deftheorem Def6 defines FinSeq_log ENTROPY1:def 6 :
:: deftheorem defines Infor_FinSeq_of ENTROPY1:def 7 :
theorem Th47:
theorem Th48:
theorem
theorem Th50:
theorem Th51:
theorem Th52:
definition
let MR be
Matrix of
REAL ;
assume A1:
MR is
m-nonnegative
;
func Infor_FinSeq_of MR -> Matrix of
REAL means :
Def8:
(
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)) ) )
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
end;
:: deftheorem Def8 defines Infor_FinSeq_of ENTROPY1:def 8 :
theorem Th53:
theorem Th54:
:: deftheorem defines Entropy ENTROPY1:def 9 :
theorem
theorem
theorem Th57:
theorem
theorem Th59:
theorem Th60:
:: deftheorem defines Entropy_of_Joint_Prob ENTROPY1:def 10 :
theorem
:: deftheorem Def11 defines Entropy_of_Cond_Prob ENTROPY1:def 11 :
theorem Th62:
theorem Th63:
theorem Th64:
theorem