:: by Bo Zhang and Yatsuka Nakamura

::

:: Received July 9, 2007

:: Copyright (c) 2007-2017 Association of Mizar Users

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

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

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

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

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)

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

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;

definition

let p be FinSequence of REAL ;

( p is nonnegative iff for i being Nat st i in dom p holds

p . i >= 0 )

end;
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 for i being Nat st i in dom p holds

p . i >= 0 ;

( p is nonnegative iff for i being Nat st i in dom p holds

p . i >= 0 )

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

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

ex b_{1} being FinSequence of REAL st b_{1} is nonnegative
end;

cluster Relation-like NAT -defined REAL -valued Function-like V50() FinSequence-like FinSubsequence-like V165() V166() V167() nonnegative for FinSequence of REAL ;

existence ex b

proof 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

for p being FinSequence of REAL st p is nonnegative & r >= 0 holds

r * p is nonnegative

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

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

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

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

for k being Nat st k in dom p & p . k = Sum p holds

p has_onlyone_value_in k

proof end;

registration

coherence

for b_{1} being FinSequence of REAL st b_{1} is ProbFinS holds

( not b_{1} is empty & b_{1} is nonnegative )
by MATRPROB:def 5, RVSUM_1:72;

end;
for b

( not b

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

for k being Nat st k in dom p & p . k = 1 holds

p has_onlyone_value_in k

proof end;

registration

coherence

for b_{1} being Matrix of REAL st b_{1} is with_sum=1 holds

not b_{1} is V3()

for b_{1} being Matrix of REAL st b_{1} is Joint_Probability holds

not b_{1} is V3()
;

end;
for b

not b

proof end;

coherence for b

not b

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)

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 )

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

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

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

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;

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

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;

ex b_{1} being Matrix of n,REAL st b_{1} is diagonal

end;
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 b

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

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 ;

ex b_{1} being diagonal Matrix of len p,REAL st

for j being Nat st j in dom p holds

b_{1} * (j,j) = p . j

for b_{1}, b_{2} being diagonal Matrix of len p,REAL st ( for j being Nat st j in dom p holds

b_{1} * (j,j) = p . j ) & ( for j being Nat st j in dom p holds

b_{2} * (j,j) = p . j ) holds

b_{1} = b_{2}

end;
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 for j being Nat st j in dom p holds

it * (j,j) = p . j;

ex b

for j being Nat st j in dom p holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines Vec2DiagMx ENTROPY1:def 4 :

for p being FinSequence of REAL

for b_{2} being diagonal Matrix of len p,REAL holds

( b_{2} = Vec2DiagMx p iff for j being Nat st j in dom p holds

b_{2} * (j,j) = p . j );

for p being FinSequence of REAL

for b

( b

b

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

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

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

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

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)

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)

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

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

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

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 )

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

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

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

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

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;

( ( len M = 0 implies ex b_{1} being FinSequence of D st b_{1} = {} ) & ( not len M = 0 implies ex b_{1} being FinSequence of D ex p being FinSequence of D * st

( b_{1} = 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)) ) ) ) )

for b_{1}, b_{2} being FinSequence of D holds

( ( len M = 0 & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) & ( not len M = 0 & ex p being FinSequence of D * st

( b_{1} = 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

( b_{2} = 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 b_{1} = b_{2} ) )

for b_{1} being FinSequence of D holds verum
;

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

( ( len M = 0 implies ex b

( b

p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) ) )

proof end;

uniqueness for b

( ( len M = 0 & b

( b

p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) & ex p being FinSequence of D * st

( b

p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) implies b

proof end;

consistency for b

:: deftheorem Def5 defines Mx2FinS ENTROPY1:def 5 :

for D being non empty set

for M being Matrix of D

for b_{3} being FinSequence of D holds

( ( len M = 0 implies ( b_{3} = Mx2FinS M iff b_{3} = {} ) ) & ( not len M = 0 implies ( b_{3} = Mx2FinS M iff ex p being FinSequence of D * st

( b_{3} = 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)) ) ) ) ) );

for D being non empty set

for M being Matrix of D

for b

( ( len M = 0 implies ( b

( b

p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) ) ) );

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

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

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

definition

let a be Real;

let p be FinSequence of REAL ;

assume A1: p is nonnegative ;

ex b_{1} being FinSequence of REAL st

( len b_{1} = len p & ( for k being Nat st k in dom b_{1} holds

( ( p . k > 0 implies b_{1} . k = log (a,(p . k)) ) & ( p . k = 0 implies b_{1} . k = 0 ) ) ) )

for b_{1}, b_{2} being FinSequence of REAL st len b_{1} = len p & ( for k being Nat st k in dom b_{1} holds

( ( p . k > 0 implies b_{1} . k = log (a,(p . k)) ) & ( p . k = 0 implies b_{1} . k = 0 ) ) ) & len b_{2} = len p & ( for k being Nat st k in dom b_{2} holds

( ( p . k > 0 implies b_{2} . k = log (a,(p . k)) ) & ( p . k = 0 implies b_{2} . k = 0 ) ) ) holds

b_{1} = b_{2}

end;
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 ( 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 ) ) ) );

ex b

( len b

( ( p . k > 0 implies b

proof end;

uniqueness for b

( ( p . k > 0 implies b

( ( p . k > 0 implies b

b

proof 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_{3} being FinSequence of REAL holds

( b_{3} = FinSeq_log (a,p) iff ( len b_{3} = len p & ( for k being Nat st k in dom b_{3} holds

( ( p . k > 0 implies b_{3} . k = log (a,(p . k)) ) & ( p . k = 0 implies b_{3} . k = 0 ) ) ) ) );

for a being Real

for p being FinSequence of REAL st p is nonnegative holds

for b

( b

( ( p . k > 0 implies b

definition

let p be FinSequence of REAL ;

correctness

coherence

mlt (p,(FinSeq_log (2,p))) is FinSequence of REAL ;

;

end;
correctness

coherence

mlt (p,(FinSeq_log (2,p))) is FinSequence of REAL ;

;

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

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

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

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

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

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

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

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 ;

ex b_{1} being Matrix of REAL st

( len b_{1} = len MR & width b_{1} = width MR & ( for k being Nat st k in dom b_{1} holds

b_{1} . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) )

for b_{1}, b_{2} being Matrix of REAL st len b_{1} = len MR & width b_{1} = width MR & ( for k being Nat st k in dom b_{1} holds

b_{1} . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) & len b_{2} = len MR & width b_{2} = width MR & ( for k being Nat st k in dom b_{2} holds

b_{2} . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) holds

b_{1} = b_{2}

end;
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 ( 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))))) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def8 defines Infor_FinSeq_of ENTROPY1:def 8 :

for MR being Matrix of REAL st MR is m-nonnegative holds

for b_{2} being Matrix of REAL holds

( b_{2} = Infor_FinSeq_of MR iff ( len b_{2} = len MR & width b_{2} = width MR & ( for k being Nat st k in dom b_{2} holds

b_{2} . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) ) );

for MR being Matrix of REAL st MR is m-nonnegative holds

for b

( b

b

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

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

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
end;

:: deftheorem defines Entropy ENTROPY1:def 9 :

for p being FinSequence of REAL holds Entropy p = - (Sum (Infor_FinSeq_of p));

for p being FinSequence of REAL holds Entropy p = - (Sum (Infor_FinSeq_of p));

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

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

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

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

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;

:: deftheorem defines Entropy_of_Joint_Prob ENTROPY1:def 10 :

for MR being Matrix of REAL holds Entropy_of_Joint_Prob MR = Entropy (Mx2FinS MR);

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;

ex b_{1} being FinSequence of REAL st

( len b_{1} = len MR & ( for k being Nat st k in dom b_{1} holds

b_{1} . k = Entropy (Line (MR,k)) ) )

for b_{1}, b_{2} being FinSequence of REAL st len b_{1} = len MR & ( for k being Nat st k in dom b_{1} holds

b_{1} . k = Entropy (Line (MR,k)) ) & len b_{2} = len MR & ( for k being Nat st k in dom b_{2} holds

b_{2} . k = Entropy (Line (MR,k)) ) holds

b_{1} = b_{2}

end;
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 ( len it = len MR & ( for k being Nat st k in dom it holds

it . k = Entropy (Line (MR,k)) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def11 defines Entropy_of_Cond_Prob ENTROPY1:def 11 :

for MR being Matrix of REAL

for b_{2} being FinSequence of REAL holds

( b_{2} = Entropy_of_Cond_Prob MR iff ( len b_{2} = len MR & ( for k being Nat st k in dom b_{2} holds

b_{2} . k = Entropy (Line (MR,k)) ) ) );

for MR being Matrix of REAL

for b

( b

b

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

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

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

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;