:: Definition and Some Properties of Information Entropy
:: by Bo Zhang and Yatsuka Nakamura
::
:: Received July 9, 2007
:: Copyright (c) 2007-2018 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
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 of ;
coherence
for b1 being FinSequence of REAL st b1 is ProbFinS holds
( not b1 is empty & b1 is nonnegative )
by ;
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 Matrix of ;
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 Matrix of ;
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 ()
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 ((),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 = () * () 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 = () * () 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 () * () 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;
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 = () * 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 = () * 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
() * 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 * ()
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 () holds
( (j * ()) + l in dom (p . (j + 1)) & (p . (j + 1)) . ((j * ()) + 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) * ()) + j in dom (p . i) & M * (i,j) = (p . i) . (((i - 1) * ()) + 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) * ()) + j in dom (p . (len M)) & M * (i,j) = (p . (len M)) . (((i - 1) * ()) + 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 () = (len 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) * ()) + j in dom () & M * (i,j) = () . (((i - 1) * ()) + 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 () & l = k - 1 holds
( [((l div ()) + 1),((l mod ()) + 1)] in Indices M & () . k = M * (((l div ()) + 1),((l mod ()) + 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 (() * ()) is ProbFinS by ;

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 (() * M) is ProbFinS by ;

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 () . k = 0 ) & ( p . k > 0 implies () . 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 = - () 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
() . 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
() . 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 ((),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
- ();
correctness
coherence
- () is Real
;
;
end;

:: deftheorem defines Entropy ENTROPY1:def 9 :
for p being FinSequence of REAL holds Entropy 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 ()
proof end;

theorem Th60: :: ENTROPY1:60
for p, q being ProbFinS FinSequence of REAL
for M being Matrix of REAL st M = () * () holds
SumAll () = () + ()
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 (() * ()) = () + ()
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 (() . k)) ) ) )
proof end;

theorem Th63: :: ENTROPY1:63
for M being V3() Conditional_Probability Matrix of REAL holds Entropy_of_Cond_Prob 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 = () * M holds
SumAll () = () + (Sum (mlt (p,())))
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 (() * M) = () + (Sum (mlt (p,)))
proof end;