:: Definition and Some Properties of Information Entropy
:: by Bo Zhang and Yatsuka Nakamura
::
:: Received July 9, 2007
:: Copyright (c) 2007-2011 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

proof end;

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 ) )

proof end;

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 ) )

proof end;

theorem Th4: :: ENTROPY1:4

for a, b being Real st a > 1 & b > 1 holds
log (a,b) > 0

proof end;

theorem Th5: :: ENTROPY1:5

for a, b being Real st a > 0 & a <> 1 & b > 0 holds
- (log (a,b)) = log (a,(1 / b))

proof end;

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)))

proof end;

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)

proof end;

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)

proof end;

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) )

proof end;

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 )

proof end;

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 V43() FinSequence-like FinSubsequence-like complex-yielding V146() V147() nonnegative FinSequence of REAL ;
existence
ex b₁ being FinSequence of REAL st b₁ is nonnegative

proof end;

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

proof end;

definition

let p be FinSequence of REAL ;
let k be Element of NAT ;
pred p 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

proof end;

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) )

proof end;

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

proof end;

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

proof end;

registration

cluster ProbFinS -> non empty nonnegative FinSequence of REAL ;
coherence
for b₁ being FinSequence of REAL st b₁ is ProbFinS holds
( not b₁ is empty & b₁ is nonnegative )

proof end;

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

proof end;

theorem Th16: :: ENTROPY1:16

for i being non empty Nat holds i |-> (1 / i) is ProbFinS FinSequence of REAL

proof end;

registration

cluster tabular with_sum=1 -> non empty-yielding FinSequence of REAL * ;
coherence
for b₁ being Matrix of REAL st b₁ is with_sum=1 holds
not b₁ is empty-yielding

proof end;

cluster tabular Joint_Probability -> non empty-yielding FinSequence of REAL * ;
coherence
for b₁ being Matrix of REAL st b₁ is Joint_Probability holds
not b₁ is empty-yielding ;

end;

theorem :: ENTROPY1:17

for M being Matrix of REAL st M = {} holds
SumAll M = 0

proof end;

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)

proof end;

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 )

proof end;

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)*>

proof end;

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) ) ) )

proof end;

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 ) ) )

proof end;

theorem Th23: :: ENTROPY1:23

for p, q being ProbFinS FinSequence of REAL holds (ColVec2Mx p) * (LineVec2Mx q) is Joint_Probability

proof end;

definition

let n be Nat;
let MR be Matrix of n, REAL ;
attr MR 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 V43() FinSequence-like FinSubsequence-like tabular diagonal Matrix of n,n, REAL ;
existence
ex b₁ being Matrix of n, REAL st b₁ is diagonal

proof end;

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 )

proof end;

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 b₁ being diagonal Matrix of len p, REAL st
for j being Element of NAT st j in dom p holds
b₁ * (j,j) = p . j

proof end;

uniqueness
for b₁, b₂ being diagonal Matrix of len p, REAL st ( for j being Element of NAT st j in dom p holds
b₁ * (j,j) = p . j ) & ( for j being Element of NAT st j in dom p holds
b₂ * (j,j) = p . j ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines Vec2DiagMx ENTROPY1:def 4 :
for p being FinSequence of REAL
for b₂ being diagonal Matrix of len p, REAL holds
( b₂ = Vec2DiagMx p iff for j being Element of NAT st j in dom p holds
b₂ * (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 ) ) ) )

proof end;

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)) ) ) )

proof end;

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)) ) ) )

proof end;

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

proof end;

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)

proof end;

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)

proof end;

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) ) ) )

proof end;

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

proof end;

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

proof end;

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 )

proof end;

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) )

proof end;

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) )

proof end;

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)))

proof end;

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))

proof end;

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 b₁ being FinSequence of D st b₁ = {} ) & ( not len M = 0 implies ex b₁ being FinSequence of D ex p being FinSequence of D * st
( b₁ = 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)) ) ) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of D holds
( ( len M = 0 & b₁ = {} & b₂ = {} implies b₁ = b₂ ) & ( not len M = 0 & ex p being FinSequence of D * st
( b₁ = 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
( b₂ = 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 b₁ = b₂ ) )

proof end;

consistency
for b₁ 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 b₃ being FinSequence of D holds
( ( len M = 0 implies ( b₃ = Mx2FinS M iff b₃ = {} ) ) & ( not len M = 0 implies ( b₃ = Mx2FinS M iff ex p being FinSequence of D * st
( b₃ = 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)

proof end;

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) )

proof end;

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)) )

proof end;

theorem Th42: :: ENTROPY1:42

for MR being Matrix of REAL holds SumAll MR = Sum (Mx2FinS MR)

proof end;

theorem Th43: :: ENTROPY1:43

for MR being Matrix of REAL holds
( MR is m-nonnegative iff Mx2FinS MR is nonnegative )

proof end;

theorem Th44: :: ENTROPY1:44

for MR being Matrix of REAL holds
( MR is Joint_Probability iff Mx2FinS MR is ProbFinS )

proof end;

theorem Th45: :: ENTROPY1:45

for p, q being ProbFinS FinSequence of REAL holds Mx2FinS ((ColVec2Mx p) * (LineVec2Mx q)) is ProbFinS

proof end;

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

proof end;

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 b₁ being FinSequence of REAL st
( len b₁ = len p & ( for k being Nat st k in dom b₁ holds
( ( p . k > 0 implies b₁ . k = log (a,(p . k)) ) & ( p . k = 0 implies b₁ . k = 0 ) ) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of REAL st len b₁ = len p & ( for k being Nat st k in dom b₁ holds
( ( p . k > 0 implies b₁ . k = log (a,(p . k)) ) & ( p . k = 0 implies b₁ . k = 0 ) ) ) & len b₂ = len p & ( for k being Nat st k in dom b₂ holds
( ( p . k > 0 implies b₂ . k = log (a,(p . k)) ) & ( p . k = 0 implies b₂ . k = 0 ) ) ) holds
b₁ = b₂

proof end;

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 b₃ being FinSequence of REAL holds
( b₃ = FinSeq_log (a,p) iff ( len b₃ = len p & ( for k being Nat st k in dom b₃ holds
( ( p . k > 0 implies b₃ . k = log (a,(p . k)) ) & ( p . k = 0 implies b₃ . 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))) ) ) )

proof end;

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))) ) )

proof end;

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)))) ) ) )

proof end;

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)))

proof end;

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)))))

proof end;

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

proof end;

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 b₁ being Matrix of REAL st
( len b₁ = len MR & width b₁ = width MR & ( for k being Element of NAT st k in dom b₁ holds
b₁ . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) )

proof end;

uniqueness
for b₁, b₂ being Matrix of REAL st len b₁ = len MR & width b₁ = width MR & ( for k being Element of NAT st k in dom b₁ holds
b₁ . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) & len b₂ = len MR & width b₂ = width MR & ( for k being Element of NAT st k in dom b₂ holds
b₂ . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines Infor_FinSeq_of ENTROPY1:def 8 :
for MR being Matrix of REAL st MR is m-nonnegative holds
for b₂ being Matrix of REAL holds
( b₂ = Infor_FinSeq_of MR iff ( len b₂ = len MR & width b₂ = width MR & ( for k being Element of NAT st k in dom b₂ holds
b₂ . 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))

proof end;

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)))) ) ) )

proof end;

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

proof end;

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

proof end;

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 ) ) )

proof end;

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) ) ) )

proof end;

theorem Th59: :: ENTROPY1:59

for M being m-nonnegative Matrix of REAL holds Mx2FinS (Infor_FinSeq_of M) = Infor_FinSeq_of (Mx2FinS M)

proof end;

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))

proof end;

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)

proof end;

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 b₁ being FinSequence of REAL st
( len b₁ = len MR & ( for k being Element of NAT st k in dom b₁ holds
b₁ . k = Entropy (Line (MR,k)) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of REAL st len b₁ = len MR & ( for k being Element of NAT st k in dom b₁ holds
b₁ . k = Entropy (Line (MR,k)) ) & len b₂ = len MR & ( for k being Element of NAT st k in dom b₂ holds
b₂ . k = Entropy (Line (MR,k)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines Entropy_of_Cond_Prob ENTROPY1:def 11 :
for MR being Matrix of REAL
for b₂ being FinSequence of REAL holds
( b₂ = Entropy_of_Cond_Prob MR iff ( len b₂ = len MR & ( for k being Element of NAT st k in dom b₂ holds
b₂ . 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)) ) ) )

proof end;

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))

proof end;

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)))))

proof end;

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))))

proof end;