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


theorem Th1: :: ENTROPY1:1
for i, j, k, l being Nat st k <> 0 & i < l & l <= j & k divides l holds
i div k < j div k
proof end;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

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 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 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 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 Nat st i in dom p holds
p . i >= 0 ;
compatibility
( p is nonnegative iff for i being 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 Nat st i in dom p holds
p . i >= 0 );

registration
cluster Relation-like NAT -defined REAL -valued Function-like V50() FinSequence-like FinSubsequence-like V165() V166() V167() nonnegative for FinSequence of REAL ;
existence
ex b1 being FinSequence of REAL st b1 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 Nat;
pred p has_onlyone_value_in k means :: ENTROPY1:def 2
( k in dom p & ( for i being Nat st i in dom p & i <> k holds
p . i = 0 ) );
end;

:: deftheorem defines has_onlyone_value_in ENTROPY1:def 2 :
for p being FinSequence of REAL
for k being Nat holds
( p has_onlyone_value_in k iff ( k in dom p & ( for i being Nat st i in dom p & i <> k holds
p . i = 0 ) ) );

theorem :: ENTROPY1:11
for i, k being 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 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 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 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 for FinSequence of REAL ;
coherence
for b1 being FinSequence of REAL st b1 is ProbFinS holds
( not b1 is empty & b1 is nonnegative ) by MATRPROB:def 5, RVSUM_1:72;
end;

theorem Th15: :: ENTROPY1:15
for p being ProbFinS FinSequence of REAL
for k being 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 zero Nat holds i |-> (1 / i) is ProbFinS FinSequence of REAL
proof end;

registration
cluster tabular with_sum=1 -> V3() for FinSequence of REAL * ;
coherence
for b1 being Matrix of REAL st b1 is with_sum=1 holds
not b1 is V3()
proof end;
cluster tabular Joint_Probability -> V3() for FinSequence of REAL * ;
coherence
for b1 being Matrix of REAL st b1 is Joint_Probability holds
not b1 is V3() ;
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 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 Nat st i in dom MR holds
Line (MR,i) is nonnegative )
proof end;

theorem Th20: :: ENTROPY1:20
for p being FinSequence of REAL
for j being 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 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 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 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 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 V50() FinSequence-like FinSubsequence-like tabular V118( REAL ,n,n) diagonal for FinSequence of REAL * ;
existence
ex b1 being Matrix of n,REAL st b1 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 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 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 Nat st j in dom p holds
b1 * (j,j) = p . j
proof end;
uniqueness
for b1, b2 being diagonal Matrix of len p,REAL st ( for j being Nat st j in dom p holds
b1 * (j,j) = p . j ) & ( for j being Nat st j in dom p holds
b2 * (j,j) = p . j ) holds
b1 = b2
proof end;
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 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 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 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 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 V3() 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 Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds
for k being 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 Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds
for i, j being 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 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 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 Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds
for j being Nat st j >= 1 & j < len p holds
for l being 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 Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds
for i, j being Nat st i in dom p & j in dom p & i <= j holds
for l being 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 Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds
for j being Nat st j >= 1 & j < len p holds
for l being 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 Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds
for i, j being 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 Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds
for i, j being 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 Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds
for k being 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 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 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 Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) ) )
proof end;
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 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 Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) implies b1 = b2 ) )
proof end;
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 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 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 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 by Th23, Th44;

theorem :: ENTROPY1:46
for p being ProbFinS FinSequence of REAL
for M being V3() Conditional_Probability Matrix of REAL st len p = len M holds
Mx2FinS ((Vec2DiagMx p) * M) is ProbFinS by Th28, Th44;

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 ) ) ) )
proof end;
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
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 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 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 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 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 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 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 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 Nat st k in dom b1 holds
b1 . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) )
proof end;
uniqueness
for b1, b2 being Matrix of REAL st len b1 = len MR & width b1 = width MR & ( for k being 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 Nat st k in dom b2 holds
b2 . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) holds
b1 = b2
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 b2 being Matrix of REAL holds
( b2 = Infor_FinSeq_of MR iff ( len b2 = len MR & width b2 = width MR & ( for k being 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 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 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 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 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 Nat st k in dom p holds
p . k = q . k ) implies Sum pp = Sum qq ) & ( Sum pp = Sum qq implies for k being Nat st k in dom p holds
p . k = q . k ) & ( ex k being Nat st
( k in dom p & p . k <> q . k ) implies Sum pp < Sum qq ) & ( Sum pp < Sum qq implies ex k being 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 Nat st k in dom p holds
p . k > 0 ) holds
( Entropy p <= log (2,(len p)) & ( ( for k being 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 Nat st k in dom p holds
p . k = 1 / (len p) ) & ( ex k being 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 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 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 Nat st k in dom b1 holds
b1 . k = Entropy (Line (MR,k)) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len MR & ( for k being Nat st k in dom b1 holds
b1 . k = Entropy (Line (MR,k)) ) & len b2 = len MR & ( for k being Nat st k in dom b2 holds
b2 . k = Entropy (Line (MR,k)) ) holds
b1 = b2
proof end;
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 Nat st k in dom b2 holds
b2 . k = Entropy (Line (MR,k)) ) ) );

theorem Th62: :: ENTROPY1:62
for M being V3() 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 Nat st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ) ) )
proof end;

theorem Th63: :: ENTROPY1:63
for M being V3() 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 V3() 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 V3() 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;