:: ENTROPY1 semantic presentation
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
let k, i, l, j be Element of NAT ; ::_thesis: ( k <> 0 & i < l & l <= j & k divides l implies i div k < j div k )
assume that
A1: k <> 0 and
A2: i < l and
A3: l <= j and
A4: k divides l ; ::_thesis: i div k < j div k
A5: l mod k = 0 by A1, A4, PEPIN:6;
i + (i mod k) >= i by NAT_1:11;
then i - (i mod k) <= (i + (i mod k)) - (i mod k) by XREAL_1:9;
then i - (i mod k) < l by A2, XXREAL_0:2;
then A6: (i - (i mod k)) / k < l / k by A1, XREAL_1:74;
i = (k * (i div k)) + (i mod k) by A1, NAT_D:2;
then (k / k) * (i div k) = (i - (i mod k)) / k ;
then A7: 1 * (i div k) = (i - (i mod k)) / k by A1, XCMPLX_1:60;
l = (k * (l div k)) + (l mod k) by A1, NAT_D:2
.= k * (l div k) by A5 ;
then (k / k) * (l div k) = l / k ;
then A8: 1 * (l div k) = l / k by A1, XCMPLX_1:60;
l div k <= j div k by A3, NAT_2:24;
hence i div k < j div k by A8, A7, A6, XXREAL_0:2; ::_thesis: verum
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
let r be Real; ::_thesis: ( r > 0 implies ( 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 ) ) )
set Z2 = ].0,1.[;
set Z1 = right_open_halfline 1;
reconsider f2 = log_ number_e as PartFunc of REAL,REAL ;
deffunc H1( Real) -> Element of REAL = $1 - 1;
defpred S1[ set ] means $1 in REAL ;
set Z = right_open_halfline 0;
A1: 1 in right_open_halfline 0 by XXREAL_1:235;
1 in { g where g is Real : 0 < g } ;
then A2: 1 in right_open_halfline 0 by XXREAL_1:230;
consider f1 being PartFunc of REAL,REAL such that
A3: ( ( for r being Real holds
( r in dom f1 iff S1[r] ) ) & ( for r being Real st r in dom f1 holds
f1 . r = H1(r) ) ) from SEQ_1:sch_3();
dom f1 is Subset of REAL by RELAT_1:def_18;
then A4: dom f1 = REAL by A3, FDIFF_1:1;
A5: for r being Real st r in right_open_halfline 0 holds
f1 . r = (1 * r) + (- 1)
proof
let r be Real; ::_thesis: ( r in right_open_halfline 0 implies f1 . r = (1 * r) + (- 1) )
assume r in right_open_halfline 0 ; ::_thesis: f1 . r = (1 * r) + (- 1)
f1 . r = r - 1 by A3;
hence f1 . r = (1 * r) + (- 1) ; ::_thesis: verum
end;
then A6: f1 is_differentiable_on right_open_halfline 0 by A4, FDIFF_1:23;
set f = f1 - f2;
A7: number_e <> 1 by TAYLOR_1:11;
assume A8: r > 0 ; ::_thesis: ( 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 ) )
dom f2 = right_open_halfline 0 by TAYLOR_1:def_2;
then A9: dom (f1 - f2) = (right_open_halfline 0) /\ REAL by A4, VALUED_1:12
.= right_open_halfline 0 by XBOOLE_1:28 ;
A10: for x being Real st x > 0 holds
(f1 - f2) . x = (x - 1) - (ln . x)
proof
let x be Real; ::_thesis: ( x > 0 implies (f1 - f2) . x = (x - 1) - (ln . x) )
assume x > 0 ; ::_thesis: (f1 - f2) . x = (x - 1) - (ln . x)
then x in { g where g is Real : 0 < g } ;
then A11: x in dom (f1 - f2) by A9, XXREAL_1:230;
(f1 - f2) . x = (f1 . x) - (f2 . x) by A11, VALUED_1:13;
hence (f1 - f2) . x = (x - 1) - (ln . x) by A3; ::_thesis: verum
end;
then A12: (f1 - f2) . 1 = (1 - 1) - (ln . 1)
.= - (log (number_e,1)) by A2, TAYLOR_1:def_2
.= - 0 by A7, POWER:51, TAYLOR_1:11
.= 0 ;
A13: f1 is_differentiable_on right_open_halfline 0 by A4, A5, FDIFF_1:23;
A14: now__::_thesis:_for_r_being_Real_st_r_in_right_open_halfline_0_holds_
diff_(f1,r)_=_1
let r be Real; ::_thesis: ( r in right_open_halfline 0 implies diff (f1,r) = 1 )
assume A15: r in right_open_halfline 0 ; ::_thesis: diff (f1,r) = 1
thus diff (f1,r) = (f1 `| (right_open_halfline 0)) . r by A13, A15, FDIFF_1:def_7
.= 1 by A4, A5, A15, FDIFF_1:23 ; ::_thesis: verum
end;
A16: ( f1 - f2 is_differentiable_on right_open_halfline 0 & ( for r being Real st r in right_open_halfline 0 holds
diff ((f1 - f2),r) = 1 - (1 / r) ) )
proof
thus A17: f1 - f2 is_differentiable_on right_open_halfline 0 by A9, A6, FDIFF_1:19, TAYLOR_1:18; ::_thesis: for r being Real st r in right_open_halfline 0 holds
diff ((f1 - f2),r) = 1 - (1 / r)
hereby ::_thesis: verum
let r be Real; ::_thesis: ( r in right_open_halfline 0 implies diff ((f1 - f2),r) = 1 - (1 / r) )
assume A18: r in right_open_halfline 0 ; ::_thesis: diff ((f1 - f2),r) = 1 - (1 / r)
((f1 - f2) `| (right_open_halfline 0)) . r = (diff (f1,r)) - (diff (f2,r)) by A9, A6, A18, FDIFF_1:19, TAYLOR_1:18
.= 1 - (diff (f2,r)) by A14, A18
.= 1 - (1 / r) by A18, TAYLOR_1:18 ;
hence diff ((f1 - f2),r) = 1 - (1 / r) by A17, A18, FDIFF_1:def_7; ::_thesis: verum
end;
end;
then A19: (f1 - f2) | (right_open_halfline 0) is continuous by FDIFF_1:25;
A20: right_open_halfline 1 c= right_open_halfline 0 by XXREAL_1:46;
A21: for r being Real st r in right_open_halfline 1 holds
diff ((f1 - f2),r) > 0
proof
let r be Real; ::_thesis: ( r in right_open_halfline 1 implies diff ((f1 - f2),r) > 0 )
assume A22: r in right_open_halfline 1 ; ::_thesis: diff ((f1 - f2),r) > 0
r in { g where g is Real : 1 < g } by A22, XXREAL_1:230;
then A23: ex g1 being Real st
( g1 = r & 1 < g1 ) ;
diff ((f1 - f2),r) = 1 - (1 / r) by A16, A20, A22;
hence diff ((f1 - f2),r) > 0 by A23, XREAL_1:50, XREAL_1:212; ::_thesis: verum
end;
A24: for r being Real st r in right_open_halfline 1 holds
(f1 - f2) . r > 0
proof
assume ex r being Real st
( r in right_open_halfline 1 & not (f1 - f2) . r > 0 ) ; ::_thesis: contradiction
then consider r1 being Real such that
A25: r1 in right_open_halfline 1 and
A26: (f1 - f2) . r1 <= 0 ;
A27: [.1,r1.] c= dom (f1 - f2) by A1, A9, A20, A25, XXREAL_2:def_12;
r1 in { g where g is Real : 1 < g } by A25, XXREAL_1:230;
then A28: ex g1 being Real st
( g1 = r1 & 1 < g1 ) ;
A29: f1 - f2 is_differentiable_on ].1,r1.[ by A16, FDIFF_1:26, XXREAL_1:247;
A30: (f1 - f2) | [.1,r1.] is continuous by A19, FCONT_1:16, XXREAL_1:249;
percases ( (f1 - f2) . r1 = 0 or (f1 - f2) . r1 < 0 ) by A26;
suppose (f1 - f2) . r1 = 0 ; ::_thesis: contradiction
then consider r2 being Real such that
A31: r2 in ].1,r1.[ and
A32: diff ((f1 - f2),r2) = 0 by A12, A28, A30, A29, A27, ROLLE:1;
ex g1 being Real st
( g1 = r2 & 1 < g1 & g1 < r1 ) by A31;
then r2 in { g where g is Real : 1 < g } ;
then r2 in right_open_halfline 1 by XXREAL_1:230;
hence contradiction by A21, A32; ::_thesis: verum
end;
supposeA33: (f1 - f2) . r1 < 0 ; ::_thesis: contradiction
consider r3 being Real such that
A34: r3 in ].1,r1.[ and
A35: diff ((f1 - f2),r3) = (((f1 - f2) . r1) - ((f1 - f2) . 1)) / (r1 - 1) by A28, A30, A29, A27, ROLLE:3;
ex g1 being Real st
( g1 = r3 & 1 < g1 & g1 < r1 ) by A34;
then r3 in { g where g is Real : 1 < g } ;
then A36: r3 in right_open_halfline 1 by XXREAL_1:230;
r1 - 1 > 0 by A28, XREAL_1:50;
hence contradiction by A12, A21, A33, A35, A36; ::_thesis: verum
end;
end;
end;
A37: for r being Real st r > 1 holds
(f1 - f2) . r > 0
proof
let r be Real; ::_thesis: ( r > 1 implies (f1 - f2) . r > 0 )
assume r > 1 ; ::_thesis: (f1 - f2) . r > 0
then r in { g where g is Real : 1 < g } ;
then r in right_open_halfline 1 by XXREAL_1:230;
hence (f1 - f2) . r > 0 by A24; ::_thesis: verum
end;
A38: ].0,1.[ c= right_open_halfline 0 by XXREAL_1:247;
A39: for r being Real st r in ].0,1.[ holds
diff ((f1 - f2),r) < 0
proof
let r be Real; ::_thesis: ( r in ].0,1.[ implies diff ((f1 - f2),r) < 0 )
assume A40: r in ].0,1.[ ; ::_thesis: diff ((f1 - f2),r) < 0
then ex g1 being Real st
( g1 = r & 0 < g1 & g1 < 1 ) ;
then A41: 1 < 1 / r by XREAL_1:187;
diff ((f1 - f2),r) = 1 - (1 / r) by A16, A38, A40;
hence diff ((f1 - f2),r) < 0 by A41, XREAL_1:49; ::_thesis: verum
end;
A42: for r being Real st r in ].0,1.[ holds
(f1 - f2) . r > 0
proof
assume ex r being Real st
( r in ].0,1.[ & not (f1 - f2) . r > 0 ) ; ::_thesis: contradiction
then consider r1 being Real such that
A43: r1 in ].0,1.[ and
A44: (f1 - f2) . r1 <= 0 ;
A45: [.r1,1.] c= dom (f1 - f2) by A1, A9, A38, A43, XXREAL_2:def_12;
A46: ex g1 being Real st
( g1 = r1 & 0 < g1 & g1 < 1 ) by A43;
then A47: (f1 - f2) | [.r1,1.] is continuous by A19, FCONT_1:16, XXREAL_1:249;
A48: f1 - f2 is_differentiable_on ].r1,1.[ by A16, A46, FDIFF_1:26, XXREAL_1:247;
percases ( (f1 - f2) . r1 = 0 or (f1 - f2) . r1 < 0 ) by A44;
suppose (f1 - f2) . r1 = 0 ; ::_thesis: contradiction
then consider r2 being Real such that
A49: r2 in ].r1,1.[ and
A50: diff ((f1 - f2),r2) = 0 by A12, A46, A47, A45, A48, ROLLE:1;
ex g1 being Real st
( g1 = r2 & r1 < g1 & g1 < 1 ) by A49;
then r2 in { g where g is Real : ( 0 < g & g < 1 ) } by A46;
hence contradiction by A39, A50; ::_thesis: verum
end;
supposeA51: (f1 - f2) . r1 < 0 ; ::_thesis: contradiction
A52: 1 - r1 > 0 by A46, XREAL_1:50;
consider r3 being Real such that
A53: r3 in ].r1,1.[ and
A54: diff ((f1 - f2),r3) = (((f1 - f2) . 1) - ((f1 - f2) . r1)) / (1 - r1) by A46, A47, A45, A48, ROLLE:3;
ex g1 being Real st
( g1 = r3 & r1 < g1 & g1 < 1 ) by A53;
then r3 in ].0,1.[ by A46;
hence contradiction by A12, A39, A51, A54, A52; ::_thesis: verum
end;
end;
end;
A55: for r being Real st r > 0 & r < 1 holds
(f1 - f2) . r > 0
proof
let r be Real; ::_thesis: ( r > 0 & r < 1 implies (f1 - f2) . r > 0 )
assume that
A56: r > 0 and
A57: r < 1 ; ::_thesis: (f1 - f2) . r > 0
r in { g where g is Real : ( 0 < g & g < 1 ) } by A56, A57;
hence (f1 - f2) . r > 0 by A42; ::_thesis: verum
end;
for r being Real st r > 0 holds
(f1 - f2) . r >= 0
proof
let r be Real; ::_thesis: ( r > 0 implies (f1 - f2) . r >= 0 )
assume A58: r > 0 ; ::_thesis: (f1 - f2) . r >= 0
percases ( r < 1 or r = 1 or r > 1 ) by XXREAL_0:1;
suppose r < 1 ; ::_thesis: (f1 - f2) . r >= 0
hence (f1 - f2) . r >= 0 by A55, A58; ::_thesis: verum
end;
suppose r = 1 ; ::_thesis: (f1 - f2) . r >= 0
hence (f1 - f2) . r >= 0 by A12; ::_thesis: verum
end;
suppose r > 1 ; ::_thesis: (f1 - f2) . r >= 0
hence (f1 - f2) . r >= 0 by A37; ::_thesis: verum
end;
end;
end;
then (f1 - f2) . r >= 0 by A8;
then (r - 1) - (ln . r) >= 0 by A10, A8;
then (r - 1) - 0 >= ln . r by XREAL_1:11;
hence ln . r <= r - 1 ; ::_thesis: ( ( 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 ) )
thus A59: ( r = 1 iff ln . r = r - 1 ) ::_thesis: ( r <> 1 iff ln . r < r - 1 )
proof
hereby ::_thesis: ( ln . r = r - 1 implies r = 1 )
assume r = 1 ; ::_thesis: ln . r = r - 1
then (r - 1) - (ln . r) = 0 by A10, A12;
hence ln . r = r - 1 ; ::_thesis: verum
end;
assume ln . r = r - 1 ; ::_thesis: r = 1
then A60: (r - 1) - (ln . r) = 0 ;
assume A61: r <> 1 ; ::_thesis: contradiction
percases ( r < 1 or r > 1 ) by A61, XXREAL_0:1;
suppose r < 1 ; ::_thesis: contradiction
then (f1 - f2) . r > 0 by A55, A8;
hence contradiction by A10, A8, A60; ::_thesis: verum
end;
supposeA62: r > 1 ; ::_thesis: contradiction
then (f1 - f2) . r > 0 by A37;
hence contradiction by A10, A60, A62; ::_thesis: verum
end;
end;
end;
thus ( r <> 1 iff ln . r < r - 1 ) ::_thesis: verum
proof
hereby ::_thesis: ( ln . r < r - 1 implies r <> 1 )
assume r <> 1 ; ::_thesis: ln . r < r - 1
then A63: ( r - 1 > 0 or 1 - r > 0 ) by XREAL_1:55;
percases ( r < 1 or r > 1 ) by A63, XREAL_1:47;
suppose r < 1 ; ::_thesis: ln . r < r - 1
then (f1 - f2) . r > 0 by A55, A8;
then (r - 1) - (ln . r) > 0 by A10, A8;
hence ln . r < r - 1 by XREAL_1:47; ::_thesis: verum
end;
supposeA64: r > 1 ; ::_thesis: ln . r < r - 1
then (f1 - f2) . r > 0 by A37;
then (r - 1) - (ln . r) > 0 by A10, A64;
hence ln . r < r - 1 by XREAL_1:47; ::_thesis: verum
end;
end;
end;
assume A65: ln . r < r - 1 ; ::_thesis: r <> 1
assume r = 1 ; ::_thesis: contradiction
hence contradiction by A59, A65; ::_thesis: verum
end;
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
let r be Real; ::_thesis: ( r > 0 implies ( 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 ) ) )
assume A1: r > 0 ; ::_thesis: ( 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 ) )
then r in { g where g is Real : 0 < g } ;
then r in right_open_halfline 0 by XXREAL_1:230;
then log (number_e,r) = ln . r by TAYLOR_1:def_2;
hence ( 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 ) ) by A1, Th2; ::_thesis: verum
end;
theorem Th4: :: ENTROPY1:4
for a, b being Real st a > 1 & b > 1 holds
log (a,b) > 0
proof
let a, b be Real; ::_thesis: ( a > 1 & b > 1 implies log (a,b) > 0 )
assume that
A1: a > 1 and
A2: b > 1 ; ::_thesis: log (a,b) > 0
A3: a to_power (log (a,b)) > 1 by A1, A2, POWER:def_3;
assume A4: log (a,b) <= 0 ; ::_thesis: contradiction
percases ( log (a,b) = 0 or log (a,b) < 0 ) by A4;
suppose log (a,b) = 0 ; ::_thesis: contradiction
hence contradiction by A3, POWER:24; ::_thesis: verum
end;
suppose log (a,b) < 0 ; ::_thesis: contradiction
hence contradiction by A1, A3, POWER:36; ::_thesis: verum
end;
end;
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
let a, b be Real; ::_thesis: ( a > 0 & a <> 1 & b > 0 implies - (log (a,b)) = log (a,(1 / b)) )
assume that
A1: a > 0 and
A2: a <> 1 and
A3: b > 0 ; ::_thesis: - (log (a,b)) = log (a,(1 / b))
thus - (log (a,b)) = 0 - (log (a,b))
.= (log (a,1)) - (log (a,b)) by A1, A2, POWER:51
.= log (a,(1 / b)) by A1, A2, A3, POWER:54 ; ::_thesis: verum
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
let a, b, c be Real; ::_thesis: ( a > 0 & a <> 1 & b >= 0 & c >= 0 implies (b * c) * (log (a,(b * c))) = ((b * c) * (log (a,b))) + ((b * c) * (log (a,c))) )
assume that
A1: a > 0 and
A2: a <> 1 and
A3: b >= 0 and
A4: c >= 0 ; ::_thesis: (b * c) * (log (a,(b * c))) = ((b * c) * (log (a,b))) + ((b * c) * (log (a,c)))
percases ( ( b > 0 & c = 0 ) or ( b = 0 & c = 0 ) or ( b = 0 & c > 0 ) or ( b > 0 & c > 0 ) ) by A3, A4;
suppose ( b > 0 & c = 0 ) ; ::_thesis: (b * c) * (log (a,(b * c))) = ((b * c) * (log (a,b))) + ((b * c) * (log (a,c)))
hence (b * c) * (log (a,(b * c))) = ((b * c) * (log (a,b))) + ((b * c) * (log (a,c))) ; ::_thesis: verum
end;
suppose ( b = 0 & c = 0 ) ; ::_thesis: (b * c) * (log (a,(b * c))) = ((b * c) * (log (a,b))) + ((b * c) * (log (a,c)))
hence (b * c) * (log (a,(b * c))) = ((b * c) * (log (a,b))) + ((b * c) * (log (a,c))) ; ::_thesis: verum
end;
suppose ( b = 0 & c > 0 ) ; ::_thesis: (b * c) * (log (a,(b * c))) = ((b * c) * (log (a,b))) + ((b * c) * (log (a,c)))
hence (b * c) * (log (a,(b * c))) = ((b * c) * (log (a,b))) + ((b * c) * (log (a,c))) ; ::_thesis: verum
end;
suppose ( b > 0 & c > 0 ) ; ::_thesis: (b * c) * (log (a,(b * c))) = ((b * c) * (log (a,b))) + ((b * c) * (log (a,c)))
hence (b * c) * (log (a,(b * c))) = (b * c) * ((log (a,b)) + (log (a,c))) by A1, A2, POWER:53
.= ((b * c) * (log (a,b))) + ((b * c) * (log (a,c))) ;
::_thesis: verum
end;
end;
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
let q, q1, q2 be FinSequence of REAL ; ::_thesis: ( 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) ) implies Sum q = (Sum q1) + (Sum q2) )
assume that
A1: len q1 = len q and
A2: len q1 = len q2 and
A3: for k being Element of NAT st k in dom q1 holds
q . k = (q1 . k) + (q2 . k) ; ::_thesis: Sum q = (Sum q1) + (Sum q2)
for k being Element of NAT st k in dom q1 holds
q . k = (q1 /. k) + (q2 /. k)
proof
let k be Element of NAT ; ::_thesis: ( k in dom q1 implies q . k = (q1 /. k) + (q2 /. k) )
assume A4: k in dom q1 ; ::_thesis: q . k = (q1 /. k) + (q2 /. k)
A5: k in dom q2 by A2, A4, FINSEQ_3:29;
thus q . k = (q1 . k) + (q2 . k) by A3, A4
.= (q1 /. k) + (q2 . k) by A4, PARTFUN1:def_6
.= (q1 /. k) + (q2 /. k) by A5, PARTFUN1:def_6 ; ::_thesis: verum
end;
hence Sum q = (Sum q1) + (Sum q2) by A1, A2, INTEGRA1:21; ::_thesis: verum
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
let q, q1, q2 be FinSequence of REAL ; ::_thesis: ( 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) ) implies Sum q = (Sum q1) - (Sum q2) )
assume that
A1: len q1 = len q and
A2: len q1 = len q2 and
A3: for k being Element of NAT st k in dom q1 holds
q . k = (q1 . k) - (q2 . k) ; ::_thesis: Sum q = (Sum q1) - (Sum q2)
for k being Element of NAT st k in dom q1 holds
q . k = (q1 /. k) - (q2 /. k)
proof
let k be Element of NAT ; ::_thesis: ( k in dom q1 implies q . k = (q1 /. k) - (q2 /. k) )
assume A4: k in dom q1 ; ::_thesis: q . k = (q1 /. k) - (q2 /. k)
A5: k in dom q2 by A2, A4, FINSEQ_3:29;
thus q . k = (q1 . k) - (q2 . k) by A3, A4
.= (q1 /. k) - (q2 . k) by A4, PARTFUN1:def_6
.= (q1 /. k) - (q2 /. k) by A5, PARTFUN1:def_6 ; ::_thesis: verum
end;
hence Sum q = (Sum q1) - (Sum q2) by A1, A2, INTEGRA1:22; ::_thesis: verum
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
let p be FinSequence of REAL ; ::_thesis: ( len p >= 1 implies 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) ) )
assume A1: len p >= 1 ; ::_thesis: 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) )
then consider r being Real_Sequence such that
A2: r . 1 = p . 1 and
A3: for n being Nat st 0 <> n & n < len p holds
r . (n + 1) = (r . n) + (p . (n + 1)) and
A4: Sum p = r . (len p) by PROB_3:63;
A5: 1 in dom p by A1, FINSEQ_3:25;
deffunc H1( Nat) -> Element of REAL = r . $1;
consider q being FinSequence such that
A6: ( len q = len p & ( for k being Nat st k in dom q holds
q . k = H1(k) ) ) from FINSEQ_1:sch_2();
A7: rng q c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng q or x in REAL )
assume x in rng q ; ::_thesis: x in REAL
then consider j being Nat such that
A8: j in dom q and
A9: q . j = x by FINSEQ_2:10;
q . j = r . j by A6, A8;
hence x in REAL by A9; ::_thesis: verum
end;
A10: dom q = dom p by A6, FINSEQ_3:29;
reconsider q = q as FinSequence of REAL by A7, FINSEQ_1:def_4;
A11: now__::_thesis:_for_k_being_Element_of_NAT_st_0_<>_k_&_k_<_len_p_holds_
q_._(k_+_1)_=_(q_._k)_+_(p_._(k_+_1))
let k be Element of NAT ; ::_thesis: ( 0 <> k & k < len p implies q . (k + 1) = (q . k) + (p . (k + 1)) )
assume that
A12: 0 <> k and
A13: k < len p ; ::_thesis: q . (k + 1) = (q . k) + (p . (k + 1))
k >= 1 by A12, NAT_1:14;
then A14: k in dom q by A6, A13, FINSEQ_3:25;
A15: k + 1 >= 1 by NAT_1:14;
k + 1 <= len p by A13, NAT_1:13;
then k + 1 in dom q by A6, A15, FINSEQ_3:25;
hence q . (k + 1) = r . (k + 1) by A6
.= (r . k) + (p . (k + 1)) by A3, A12, A13
.= (q . k) + (p . (k + 1)) by A6, A14 ;
::_thesis: verum
end;
take q ; ::_thesis: ( 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) )
len p in dom q by A1, A6, FINSEQ_3:25;
hence ( 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) ) by A2, A4, A6, A10, A5, A11; ::_thesis: verum
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
hereby ::_thesis: ( ( for i being Element of NAT st i in dom p holds
p . i >= 0 ) implies p is nonnegative )
assume A1: p is nonnegative ; ::_thesis: for i being Element of NAT st i in dom p holds
p . i >= 0
let i be Element of NAT ; ::_thesis: ( i in dom p implies p . i >= 0 )
assume i in dom p ; ::_thesis: p . i >= 0
then p . i in rng p by FUNCT_1:3;
hence p . i >= 0 by A1, PARTFUN3:def_4; ::_thesis: verum
end;
assume A2: for i being Element of NAT st i in dom p holds
p . i >= 0 ; ::_thesis: p is nonnegative
let r be real number ; :: according to PARTFUN3:def_4 ::_thesis: ( not r in rng p or 0 <= r )
assume r in rng p ; ::_thesis: 0 <= r
then ex j being Nat st
( j in dom p & r = p . j ) by FINSEQ_2:10;
hence 0 <= r by A2; ::_thesis: verum
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 V47() FinSequence-like FinSubsequence-like complex-yielding V158() V159() nonnegative for FinSequence of REAL ;
existence
ex b1 being FinSequence of REAL st b1 is nonnegative
proof
take <*1*> ; ::_thesis: <*1*> is nonnegative
<*1*> is nonnegative
proof
set p = <*1*>;
for i being Element of NAT st i in dom <*1*> holds
<*1*> . i >= 0
proof
let i be Element of NAT ; ::_thesis: ( i in dom <*1*> implies <*1*> . i >= 0 )
assume i in dom <*1*> ; ::_thesis: <*1*> . i >= 0
then A1: i in Seg 1 by FINSEQ_1:def_8;
then A2: i <= 1 by FINSEQ_1:1;
i >= 1 by A1, FINSEQ_1:1;
then i = 1 by A2, XXREAL_0:1;
hence <*1*> . i >= 0 by FINSEQ_1:40; ::_thesis: verum
end;
hence <*1*> is nonnegative by Def1; ::_thesis: verum
end;
hence <*1*> is nonnegative ; ::_thesis: verum
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
let r be Real; ::_thesis: for p being FinSequence of REAL st p is nonnegative & r >= 0 holds
r * p is nonnegative
let p be FinSequence of REAL ; ::_thesis: ( p is nonnegative & r >= 0 implies r * p is nonnegative )
assume that
A1: p is nonnegative and
A2: r >= 0 ; ::_thesis: r * p is nonnegative
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_(r_*_p)_holds_
(r_*_p)_._k_>=_0
let k be Element of NAT ; ::_thesis: ( k in dom (r * p) implies (r * p) . k >= 0 )
assume k in dom (r * p) ; ::_thesis: (r * p) . k >= 0
then k in dom p by VALUED_1:def_5;
then A3: p . k >= 0 by A1, Def1;
(r * p) . k = r * (p . k) by RVSUM_1:44;
hence (r * p) . k >= 0 by A2, A3; ::_thesis: verum
end;
hence r * p is nonnegative by Def1; ::_thesis: verum
end;
definition
let p be FinSequence of REAL ;
let k be Element of NAT ;
predp 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
let k, i be Element of NAT ; ::_thesis: for p being FinSequence of REAL st p has_onlyone_value_in k & i <> k holds
p . i = 0
let p be FinSequence of REAL ; ::_thesis: ( p has_onlyone_value_in k & i <> k implies p . i = 0 )
assume that
A1: p has_onlyone_value_in k and
A2: i <> k ; ::_thesis: p . i = 0
percases ( not i in dom p or i in dom p ) ;
suppose not i in dom p ; ::_thesis: p . i = 0
hence p . i = 0 by FUNCT_1:def_2; ::_thesis: verum
end;
suppose i in dom p ; ::_thesis: p . i = 0
hence p . i = 0 by A1, A2, Def2; ::_thesis: verum
end;
end;
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
let k be Element of NAT ; ::_thesis: 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) )
let p, q be FinSequence of REAL ; ::_thesis: ( len p = len q & p has_onlyone_value_in k implies ( mlt (p,q) has_onlyone_value_in k & (mlt (p,q)) . k = (p . k) * (q . k) ) )
assume that
A1: len p = len q and
A2: p has_onlyone_value_in k ; ::_thesis: ( mlt (p,q) has_onlyone_value_in k & (mlt (p,q)) . k = (p . k) * (q . k) )
len (mlt (p,q)) = len p by A1, MATRPROB:30;
then A3: dom (mlt (p,q)) = dom p by FINSEQ_3:29;
A4: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(mlt_(p,q))_&_i_<>_k_holds_
(mlt_(p,q))_._i_=_0
let i be Element of NAT ; ::_thesis: ( i in dom (mlt (p,q)) & i <> k implies (mlt (p,q)) . i = 0 )
assume that
A5: i in dom (mlt (p,q)) and
A6: i <> k ; ::_thesis: (mlt (p,q)) . i = 0
thus (mlt (p,q)) . i = (p . i) * (q . i) by RVSUM_1:59
.= 0 * (q . i) by A2, A3, A5, A6, Def2
.= 0 ; ::_thesis: verum
end;
k in dom (mlt (p,q)) by A2, A3, Def2;
hence ( mlt (p,q) has_onlyone_value_in k & (mlt (p,q)) . k = (p . k) * (q . k) ) by A4, Def2, RVSUM_1:59; ::_thesis: verum
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
let k be Element of NAT ; ::_thesis: for p being FinSequence of REAL st p has_onlyone_value_in k holds
Sum p = p . k
let p be FinSequence of REAL ; ::_thesis: ( p has_onlyone_value_in k implies Sum p = p . k )
assume that
A1: k in dom p and
A2: for i being Element of NAT st i in dom p & i <> k holds
p . i = 0 ; :: according to ENTROPY1:def_2 ::_thesis: Sum p = p . k
reconsider a = p . k as Element of REAL ;
reconsider p1 = p | (Seg k) as FinSequence of REAL by FINSEQ_1:18;
p1 c= p by TREES_1:def_1;
then consider p2 being FinSequence such that
A3: p = p1 ^ p2 by TREES_1:1;
reconsider p2 = p2 as FinSequence of REAL by A3, FINSEQ_1:36;
A4: dom p2 = Seg (len p2) by FINSEQ_1:def_3;
1 <= k by A1, FINSEQ_3:25;
then k in Seg k by FINSEQ_1:3;
then A5: k in (dom p) /\ (Seg k) by A1, XBOOLE_0:def_4;
then A6: k in dom p1 by RELAT_1:61;
A7: for i being Element of NAT st i in Seg (len p2) holds
p2 . i = 0
proof
let i be Element of NAT ; ::_thesis: ( i in Seg (len p2) implies p2 . i = 0 )
A8: len p1 <= (len p1) + i by NAT_1:12;
A9: k <= len p1 by A6, FINSEQ_3:25;
assume i in Seg (len p2) ; ::_thesis: p2 . i = 0
then A10: i in dom p2 by FINSEQ_1:def_3;
then 0 <> i by FINSEQ_3:25;
then len p1 <> (len p1) + i ;
then A11: k <> (len p1) + i by A9, A8, XXREAL_0:1;
thus p2 . i = p . ((len p1) + i) by A3, A10, FINSEQ_1:def_7
.= 0 by A2, A3, A10, A11, FINSEQ_1:28 ; ::_thesis: verum
end;
A12: now__::_thesis:_for_j_being_Nat_st_j_in_dom_p2_holds_
p2_._j_=_((len_p2)_|->_0)_._j
let j be Nat; ::_thesis: ( j in dom p2 implies p2 . j = ((len p2) |-> 0) . j )
assume A13: j in dom p2 ; ::_thesis: p2 . j = ((len p2) |-> 0) . j
hence p2 . j = 0 by A7, A4
.= ((len p2) |-> 0) . j by A4, A13, FINSEQ_2:57 ;
::_thesis: verum
end;
p1 <> {} by A5, RELAT_1:38, RELAT_1:61;
then len p1 <> 0 ;
then consider p3 being FinSequence of REAL , x being Element of REAL such that
A14: p1 = p3 ^ <*x*> by FINSEQ_2:19;
k <= len p by A1, FINSEQ_3:25;
then A15: k = len p1 by FINSEQ_1:17
.= (len p3) + (len <*x*>) by A14, FINSEQ_1:22
.= (len p3) + 1 by FINSEQ_1:39 ;
then A16: x = p1 . k by A14, FINSEQ_1:42
.= a by A3, A6, FINSEQ_1:def_7 ;
A17: dom p3 = Seg (len p3) by FINSEQ_1:def_3;
A18: for i being Element of NAT st i in Seg (len p3) holds
p3 . i = 0
proof
let i be Element of NAT ; ::_thesis: ( i in Seg (len p3) implies p3 . i = 0 )
assume A19: i in Seg (len p3) ; ::_thesis: p3 . i = 0
then i <= len p3 by FINSEQ_1:1;
then A20: i <> k by A15, NAT_1:13;
A21: i in dom p3 by A19, FINSEQ_1:def_3;
then A22: i in dom p1 by A14, FINSEQ_2:15;
thus p3 . i = p1 . i by A14, A21, FINSEQ_1:def_7
.= p . i by A3, A22, FINSEQ_1:def_7
.= 0 by A2, A3, A20, A22, FINSEQ_2:15 ; ::_thesis: verum
end;
A23: now__::_thesis:_for_j_being_Nat_st_j_in_dom_p3_holds_
p3_._j_=_((len_p3)_|->_0)_._j
let j be Nat; ::_thesis: ( j in dom p3 implies p3 . j = ((len p3) |-> 0) . j )
assume A24: j in dom p3 ; ::_thesis: p3 . j = ((len p3) |-> 0) . j
hence p3 . j = 0 by A18, A17
.= ((len p3) |-> 0) . j by A17, A24, FINSEQ_2:57 ;
::_thesis: verum
end;
len ((len p3) |-> 0) = len p3 by CARD_1:def_7;
then A25: p3 = (len p3) |-> 0 by A23, FINSEQ_2:9;
len ((len p2) |-> 0) = len p2 by CARD_1:def_7;
then p2 = (len p2) |-> 0 by A12, FINSEQ_2:9;
then Sum p = (Sum (p3 ^ <*x*>)) + (Sum ((len p2) |-> 0)) by A3, A14, RVSUM_1:75
.= (Sum (p3 ^ <*x*>)) + 0 by RVSUM_1:81
.= (Sum ((len p3) |-> 0)) + x by A25, RVSUM_1:74
.= 0 + a by A16, RVSUM_1:81
.= p . k ;
hence Sum p = p . k ; ::_thesis: verum
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
let p be FinSequence of REAL ; ::_thesis: ( p is nonnegative implies for k being Element of NAT st k in dom p & p . k = Sum p holds
p has_onlyone_value_in k )
assume A1: p is nonnegative ; ::_thesis: for k being Element of NAT st k in dom p & p . k = Sum p holds
p has_onlyone_value_in k
let k1 be Element of NAT ; ::_thesis: ( k1 in dom p & p . k1 = Sum p implies p has_onlyone_value_in k1 )
assume that
A2: k1 in dom p and
A3: p . k1 = Sum p ; ::_thesis: p has_onlyone_value_in k1
k1 <= len p by A2, FINSEQ_3:25;
then consider j1 being Nat such that
A4: k1 + j1 = len p by NAT_1:10;
reconsider j1 = j1 as Element of NAT by ORDINAL1:def_12;
A5: k1 >= 1 by A2, FINSEQ_3:25;
for i being Element of NAT holds
( not i in dom p or not i <> k1 or not p . i <> 0 )
proof
assume ex i being Element of NAT st
( i in dom p & i <> k1 & p . i <> 0 ) ; ::_thesis: contradiction
then consider k2 being Element of NAT such that
A6: k2 in dom p and
A7: k2 <> k1 and
A8: p . k2 <> 0 ;
A9: p . k2 > 0 by A1, A6, A8, Def1;
k2 <= len p by A6, FINSEQ_3:25;
then consider j2 being Nat such that
A10: k2 + j2 = len p by NAT_1:10;
reconsider j2 = j2 as Element of NAT by ORDINAL1:def_12;
A11: k2 >= 1 by A6, FINSEQ_3:25;
percases ( k1 > k2 or k1 < k2 ) by A7, XXREAL_0:1;
supposeA12: k1 > k2 ; ::_thesis: contradiction
consider p1, p2 being FinSequence of REAL such that
A13: len p1 = k2 and
A14: len p2 = j2 and
A15: p = p1 ^ p2 by A10, FINSEQ_2:23;
A16: for k being Nat st k in dom p2 holds
p2 . k >= 0
proof
let k be Nat; ::_thesis: ( k in dom p2 implies p2 . k >= 0 )
assume A17: k in dom p2 ; ::_thesis: p2 . k >= 0
k >= 1 by A17, FINSEQ_3:25;
then A18: k2 + k >= 1 + 0 by XREAL_1:7;
k <= j2 by A14, A17, FINSEQ_3:25;
then k2 + k <= len p by A10, XREAL_1:7;
then A19: k2 + k in dom p by A18, FINSEQ_3:25;
p2 . k = p . (k2 + k) by A13, A15, A17, FINSEQ_1:def_7;
hence p2 . k >= 0 by A1, A19, Def1; ::_thesis: verum
end;
k2 in Seg k2 by A11, FINSEQ_1:3;
then A20: k2 in dom p1 by A13, FINSEQ_1:def_3;
( p1 . k2 > 0 & ( for k being Nat st k in dom p1 holds
p1 . k >= 0 ) )
proof
thus p1 . k2 > 0 by A9, A15, A20, FINSEQ_1:def_7; ::_thesis: for k being Nat st k in dom p1 holds
p1 . k >= 0
A21: dom p1 c= dom p by A15, FINSEQ_1:26;
let k be Nat; ::_thesis: ( k in dom p1 implies p1 . k >= 0 )
assume A22: k in dom p1 ; ::_thesis: p1 . k >= 0
p1 . k = p . k by A15, A22, FINSEQ_1:def_7;
hence p1 . k >= 0 by A1, A22, A21, Def1; ::_thesis: verum
end;
then A23: Sum p1 > 0 by A20, RVSUM_1:85;
not k1 in Seg k2 by A12, FINSEQ_1:1;
then not k1 in dom p1 by A13, FINSEQ_1:def_3;
then consider kk being Nat such that
A24: kk in dom p2 and
A25: k1 = k2 + kk by A2, A13, A15, FINSEQ_1:25;
p2 . kk = p . k1 by A13, A15, A24, A25, FINSEQ_1:def_7;
then A26: Sum p2 >= p . k1 by A24, A16, MATRPROB:5;
Sum p = (Sum p1) + (Sum p2) by A15, RVSUM_1:75;
then Sum p > (p . k1) + 0 by A23, A26, XREAL_1:8;
hence contradiction by A3; ::_thesis: verum
end;
supposeA27: k1 < k2 ; ::_thesis: contradiction
consider p1, p2 being FinSequence of REAL such that
A28: len p1 = k1 and
A29: len p2 = j1 and
A30: p = p1 ^ p2 by A4, FINSEQ_2:23;
A31: for k being Nat st k in dom p2 holds
p2 . k >= 0
proof
let k be Nat; ::_thesis: ( k in dom p2 implies p2 . k >= 0 )
assume A32: k in dom p2 ; ::_thesis: p2 . k >= 0
k >= 1 by A32, FINSEQ_3:25;
then A33: k1 + k >= 1 + 0 by XREAL_1:7;
k <= j1 by A29, A32, FINSEQ_3:25;
then k1 + k <= len p by A4, XREAL_1:7;
then A34: k1 + k in dom p by A33, FINSEQ_3:25;
p2 . k = p . (k1 + k) by A28, A30, A32, FINSEQ_1:def_7;
hence p2 . k >= 0 by A1, A34, Def1; ::_thesis: verum
end;
k1 in Seg k1 by A5, FINSEQ_1:3;
then A35: k1 in dom p1 by A28, FINSEQ_1:def_3;
( p1 . k1 = p . k1 & ( for k being Nat st k in dom p1 holds
p1 . k >= 0 ) )
proof
thus p1 . k1 = p . k1 by A30, A35, FINSEQ_1:def_7; ::_thesis: for k being Nat st k in dom p1 holds
p1 . k >= 0
A36: dom p1 c= dom p by A30, FINSEQ_1:26;
let k be Nat; ::_thesis: ( k in dom p1 implies p1 . k >= 0 )
assume A37: k in dom p1 ; ::_thesis: p1 . k >= 0
p1 . k = p . k by A30, A37, FINSEQ_1:def_7;
hence p1 . k >= 0 by A1, A37, A36, Def1; ::_thesis: verum
end;
then A38: Sum p1 >= p . k1 by A35, MATRPROB:5;
not k2 in Seg k1 by A27, FINSEQ_1:1;
then not k2 in dom p1 by A28, FINSEQ_1:def_3;
then consider kk being Nat such that
A39: kk in dom p2 and
A40: k2 = k1 + kk by A6, A28, A30, FINSEQ_1:25;
p2 . kk = p . k2 by A28, A30, A39, A40, FINSEQ_1:def_7;
then A41: Sum p2 > 0 by A9, A39, A31, RVSUM_1:85;
Sum p = (Sum p1) + (Sum p2) by A30, RVSUM_1:75;
then Sum p > (p . k1) + 0 by A38, A41, XREAL_1:8;
hence contradiction by A3; ::_thesis: verum
end;
end;
end;
hence p has_onlyone_value_in k1 by A2, Def2; ::_thesis: verum
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 )
proof
let p be FinSequence of REAL ; ::_thesis: ( p is ProbFinS implies ( not p is empty & p is nonnegative ) )
assume A1: p is ProbFinS ; ::_thesis: ( not p is empty & p is nonnegative )
hence not p is empty by MATRPROB:def_5, RVSUM_1:72; ::_thesis: p is nonnegative
for i being Element of NAT st i in dom p holds
p . i >= 0 by A1, MATRPROB:def_5;
hence p is nonnegative by Def1; ::_thesis: verum
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
let p be ProbFinS FinSequence of REAL ; ::_thesis: for k being Element of NAT st k in dom p & p . k = 1 holds
p has_onlyone_value_in k
let k be Element of NAT ; ::_thesis: ( k in dom p & p . k = 1 implies p has_onlyone_value_in k )
assume that
A1: k in dom p and
A2: p . k = 1 ; ::_thesis: p has_onlyone_value_in k
p . k = Sum p by A2, MATRPROB:def_5;
hence p has_onlyone_value_in k by A1, Th14; ::_thesis: verum
end;
theorem Th16: :: ENTROPY1:16
for i being non empty Nat holds i |-> (1 / i) is ProbFinS FinSequence of REAL
proof
let i be non empty Nat; ::_thesis: i |-> (1 / i) is ProbFinS FinSequence of REAL
reconsider i = i as non empty Element of NAT by ORDINAL1:def_12;
A1: for k being Element of NAT st k in dom (i |-> (1 / i)) holds
(i |-> (1 / i)) . k >= 0
proof
let k be Element of NAT ; ::_thesis: ( k in dom (i |-> (1 / i)) implies (i |-> (1 / i)) . k >= 0 )
assume k in dom (i |-> (1 / i)) ; ::_thesis: (i |-> (1 / i)) . k >= 0
then k in Seg i by FUNCOP_1:13;
hence (i |-> (1 / i)) . k >= 0 by FUNCOP_1:7; ::_thesis: verum
end;
Sum (i |-> (1 / i)) = i * (1 / i) by RVSUM_1:80
.= 1 by XCMPLX_1:106 ;
hence i |-> (1 / i) is ProbFinS FinSequence of REAL by A1, MATRPROB:def_5; ::_thesis: verum
end;
registration
cluster tabular with_sum=1 -> non empty-yielding for FinSequence of REAL * ;
coherence
for b1 being Matrix of REAL st b1 is with_sum=1 holds
not b1 is empty-yielding
proof
let M be Matrix of REAL; ::_thesis: ( M is with_sum=1 implies not M is empty-yielding )
assume A1: M is with_sum=1 ; ::_thesis: not M is empty-yielding
assume A2: M is empty-yielding ; ::_thesis: contradiction
percases ( len M = 0 or ( width M = 0 & len M > 0 ) ) by A2, GOBOARD1:def_3;
suppose len M = 0 ; ::_thesis: contradiction
then SumAll M = 0 by MATRPROB:23;
hence contradiction by A1, MATRPROB:def_7; ::_thesis: verum
end;
suppose ( width M = 0 & len M > 0 ) ; ::_thesis: contradiction
then reconsider M1 = M as Matrix of len M, 0 , REAL by MATRIX_1:20;
SumAll M1 = 0 by MATRPROB:24;
hence contradiction by A1, MATRPROB:def_7; ::_thesis: verum
end;
end;
end;
cluster tabular Joint_Probability -> non empty-yielding for FinSequence of REAL * ;
coherence
for b1 being Matrix of REAL st b1 is Joint_Probability holds
not b1 is empty-yielding ;
end;
theorem :: ENTROPY1:17
for M being Matrix of REAL st M = {} holds
SumAll M = 0
proof
let M be Matrix of REAL; ::_thesis: ( M = {} implies SumAll M = 0 )
assume M = {} ; ::_thesis: SumAll M = 0
then reconsider M1 = M as Matrix of 0 , width M, REAL by MATRIX_1:13;
len M1 = 0 by MATRIX_1:22;
hence SumAll M = 0 by MATRPROB:23; ::_thesis: verum
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
let D be non empty set ; ::_thesis: for M being Matrix of D
for i being Element of NAT st i in dom M holds
dom (M . i) = Seg (width M)
let M be Matrix of D; ::_thesis: for i being Element of NAT st i in dom M holds
dom (M . i) = Seg (width M)
let i be Element of NAT ; ::_thesis: ( i in dom M implies dom (M . i) = Seg (width M) )
assume i in dom M ; ::_thesis: dom (M . i) = Seg (width M)
hence dom (M . i) = dom (Line (M,i)) by MATRIX_2:16
.= Seg (len (Line (M,i))) by FINSEQ_1:def_3
.= Seg (width M) by MATRIX_1:def_7 ;
::_thesis: verum
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
let MR be Matrix of REAL; ::_thesis: ( MR is m-nonnegative iff for i being Element of NAT st i in dom MR holds
Line (MR,i) is nonnegative )
hereby ::_thesis: ( ( for i being Element of NAT st i in dom MR holds
Line (MR,i) is nonnegative ) implies MR is m-nonnegative )
assume A1: MR is m-nonnegative ; ::_thesis: for i being Element of NAT st i in dom MR holds
Line (MR,i) is nonnegative
let i be Element of NAT ; ::_thesis: ( i in dom MR implies Line (MR,i) is nonnegative )
assume A2: i in dom MR ; ::_thesis: Line (MR,i) is nonnegative
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_(Line_(MR,i))_holds_
(Line_(MR,i))_._k_>=_0
let k be Element of NAT ; ::_thesis: ( k in dom (Line (MR,i)) implies (Line (MR,i)) . k >= 0 )
assume k in dom (Line (MR,i)) ; ::_thesis: (Line (MR,i)) . k >= 0
then A3: k in dom (MR . i) by A2, MATRIX_2:16;
then k in Seg (width MR) by A2, Th18;
then A4: (Line (MR,i)) . k = MR * (i,k) by MATRIX_1:def_7;
[i,k] in Indices MR by A2, A3, MATRPROB:13;
hence (Line (MR,i)) . k >= 0 by A1, A4, MATRPROB:def_6; ::_thesis: verum
end;
hence Line (MR,i) is nonnegative by Def1; ::_thesis: verum
end;
assume A5: for i being Element of NAT st i in dom MR holds
Line (MR,i) is nonnegative ; ::_thesis: MR is m-nonnegative
now__::_thesis:_for_i,_j_being_Element_of_NAT_st_[i,j]_in_Indices_MR_holds_
MR_*_(i,j)_>=_0
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices MR implies MR * (i,j) >= 0 )
assume A6: [i,j] in Indices MR ; ::_thesis: MR * (i,j) >= 0
A7: j in Seg (width MR) by A6, MATRPROB:12;
then j in Seg (len (Line (MR,i))) by MATRIX_1:def_7;
then A8: j in dom (Line (MR,i)) by FINSEQ_1:def_3;
i in Seg (len MR) by A6, MATRPROB:12;
then i in dom MR by FINSEQ_1:def_3;
then A9: Line (MR,i) is nonnegative by A5;
MR * (i,j) = (Line (MR,i)) . j by A7, MATRIX_1:def_7;
hence MR * (i,j) >= 0 by A8, A9, Def1; ::_thesis: verum
end;
hence MR is m-nonnegative by MATRPROB:def_6; ::_thesis: verum
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
let p be FinSequence of REAL ; ::_thesis: for j being Element of NAT st j in dom p holds
Col ((LineVec2Mx p),j) = <*(p . j)*>
set M = LineVec2Mx p;
let j be Element of NAT ; ::_thesis: ( j in dom p implies Col ((LineVec2Mx p),j) = <*(p . j)*> )
assume A1: j in dom p ; ::_thesis: Col ((LineVec2Mx p),j) = <*(p . j)*>
A2: dom <*(p . j)*> = Seg 1 by FINSEQ_1:def_8;
A3: len (Col ((LineVec2Mx p),j)) = len (LineVec2Mx p) by MATRIX_1:def_8;
then len (Col ((LineVec2Mx p),j)) = 1 by MATRIXR1:def_10;
then A4: dom (Col ((LineVec2Mx p),j)) = dom <*(p . j)*> by A2, FINSEQ_1:def_3;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_(Col_((LineVec2Mx_p),j))_holds_
(Col_((LineVec2Mx_p),j))_._k_=_<*(p_._j)*>_._k
let k be Nat; ::_thesis: ( k in dom (Col ((LineVec2Mx p),j)) implies (Col ((LineVec2Mx p),j)) . k = <*(p . j)*> . k )
assume A5: k in dom (Col ((LineVec2Mx p),j)) ; ::_thesis: (Col ((LineVec2Mx p),j)) . k = <*(p . j)*> . k
A6: k <= 1 by A2, A4, A5, FINSEQ_1:1;
k >= 1 by A2, A4, A5, FINSEQ_1:1;
then A7: k = 1 by A6, XXREAL_0:1;
k in dom (LineVec2Mx p) by A3, A5, FINSEQ_3:29;
hence (Col ((LineVec2Mx p),j)) . k = (LineVec2Mx p) * (k,j) by MATRIX_1:def_8
.= p . j by A1, A7, MATRIXR1:def_10
.= <*(p . j)*> . k by A7, FINSEQ_1:def_8 ;
::_thesis: verum
end;
hence Col ((LineVec2Mx p),j) = <*(p . j)*> by A4, FINSEQ_1:13; ::_thesis: verum
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
let p be non empty FinSequence of REAL ; ::_thesis: 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) ) ) )
let q be FinSequence of REAL ; ::_thesis: 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) ) ) )
let M be Matrix of REAL; ::_thesis: ( 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) ) ) )
set M1 = ColVec2Mx p;
set M2 = LineVec2Mx q;
A1: len (ColVec2Mx p) = len p by MATRIXR1:def_9;
A2: len (LineVec2Mx q) = 1 by MATRIXR1:def_10;
A3: len p > 0 ;
then A4: width (ColVec2Mx p) = 1 by MATRIXR1:def_9;
A5: width (LineVec2Mx q) = len q by MATRIXR1:def_10;
hereby ::_thesis: ( 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) ) implies M = (ColVec2Mx p) * (LineVec2Mx q) )
assume A6: M = (ColVec2Mx p) * (LineVec2Mx q) ; ::_thesis: ( 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) ) )
then A7: len M = len (ColVec2Mx p) by A4, A2, MATRPROB:39;
thus ( len M = len p & width M = len q ) by A1, A4, A2, A5, A6, MATRPROB:39; ::_thesis: for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) = (p . i) * (q . j)
A8: width M = width (LineVec2Mx q) by A4, A2, A6, MATRPROB:39;
thus for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) = (p . i) * (q . j) ::_thesis: verum
proof
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices M implies M * (i,j) = (p . i) * (q . j) )
assume A9: [i,j] in Indices M ; ::_thesis: M * (i,j) = (p . i) * (q . j)
A10: i in Seg (len M) by A9, MATRPROB:12;
then A11: i in dom p by A1, A7, FINSEQ_1:def_3;
j in Seg (width M) by A9, MATRPROB:12;
then A12: j in dom q by A5, A8, FINSEQ_1:def_3;
i in dom (ColVec2Mx p) by A7, A10, FINSEQ_1:def_3;
then A13: Line ((ColVec2Mx p),i) = (ColVec2Mx p) . i by MATRIX_2:16
.= <*(p . i)*> by A3, A11, MATRIXR1:def_9 ;
thus M * (i,j) = (Line ((ColVec2Mx p),i)) "*" (Col ((LineVec2Mx q),j)) by A4, A2, A6, A9, MATRPROB:39
.= <*(p . i)*> "*" <*(q . j)*> by A12, A13, Th20
.= Sum (mlt (<*(p . i)*>,<*(q . j)*>)) by RVSUM_1:def_16
.= Sum <*((p . i) * (q . j))*> by RVSUM_1:62
.= (p . i) * (q . j) by RVSUM_1:73 ; ::_thesis: verum
end;
end;
assume that
A14: len M = len p and
A15: width M = len q and
A16: for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) = (p . i) * (q . j) ; ::_thesis: M = (ColVec2Mx p) * (LineVec2Mx q)
for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) = (Line ((ColVec2Mx p),i)) "*" (Col ((LineVec2Mx q),j))
proof
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices M implies M * (i,j) = (Line ((ColVec2Mx p),i)) "*" (Col ((LineVec2Mx q),j)) )
assume A17: [i,j] in Indices M ; ::_thesis: M * (i,j) = (Line ((ColVec2Mx p),i)) "*" (Col ((LineVec2Mx q),j))
j in Seg (width M) by A17, MATRPROB:12;
then A18: j in dom q by A15, FINSEQ_1:def_3;
A19: i in Seg (len M) by A17, MATRPROB:12;
then A20: i in dom (ColVec2Mx p) by A1, A14, FINSEQ_1:def_3;
i in dom p by A14, A19, FINSEQ_1:def_3;
then A21: <*(p . i)*> = (ColVec2Mx p) . i by A3, MATRIXR1:def_9
.= Line ((ColVec2Mx p),i) by A20, MATRIX_2:16 ;
thus M * (i,j) = (p . i) * (q . j) by A16, A17
.= Sum <*((p . i) * (q . j))*> by RVSUM_1:73
.= Sum (mlt (<*(p . i)*>,<*(q . j)*>)) by RVSUM_1:62
.= <*(p . i)*> "*" <*(q . j)*> by RVSUM_1:def_16
.= (Line ((ColVec2Mx p),i)) "*" (Col ((LineVec2Mx q),j)) by A18, A21, Th20 ; ::_thesis: verum
end;
hence M = (ColVec2Mx p) * (LineVec2Mx q) by A1, A4, A2, A5, A14, A15, MATRPROB:39; ::_thesis: verum
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
let p be non empty FinSequence of REAL ; ::_thesis: 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 ) ) )
let q be FinSequence of REAL ; ::_thesis: 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 ) ) )
let M be Matrix of REAL; ::_thesis: ( 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 ) ) )
set M1 = ColVec2Mx p;
set M2 = LineVec2Mx q;
hereby ::_thesis: ( 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 ) implies M = (ColVec2Mx p) * (LineVec2Mx q) )
assume A1: M = (ColVec2Mx p) * (LineVec2Mx q) ; ::_thesis: ( 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 ) )
hence ( len M = len p & width M = len q ) by Th21; ::_thesis: for i being Element of NAT st i in dom M holds
Line (M,i) = (p . i) * q
thus for i being Element of NAT st i in dom M holds
Line (M,i) = (p . i) * q ::_thesis: verum
proof
let i be Element of NAT ; ::_thesis: ( i in dom M implies Line (M,i) = (p . i) * q )
assume i in dom M ; ::_thesis: Line (M,i) = (p . i) * q
then A2: i in Seg (len M) by FINSEQ_1:def_3;
A3: for j being Nat st j in dom (Line (M,i)) holds
(Line (M,i)) . j = ((p . i) * q) . j
proof
let j be Nat; ::_thesis: ( j in dom (Line (M,i)) implies (Line (M,i)) . j = ((p . i) * q) . j )
assume j in dom (Line (M,i)) ; ::_thesis: (Line (M,i)) . j = ((p . i) * q) . j
then j in Seg (len (Line (M,i))) by FINSEQ_1:def_3;
then A4: j in Seg (width M) by MATRIX_1:def_7;
then A5: [i,j] in Indices M by A2, MATRPROB:12;
A6: j in NAT by ORDINAL1:def_12;
thus (Line (M,i)) . j = M * (i,j) by A4, MATRIX_1:def_7
.= (p . i) * (q . j) by A1, A6, A5, Th21
.= ((p . i) * q) . j by RVSUM_1:44 ; ::_thesis: verum
end;
dom (Line (M,i)) = Seg (len (Line (M,i))) by FINSEQ_1:def_3
.= Seg (width M) by MATRIX_1:def_7
.= Seg (len q) by A1, Th21
.= dom q by FINSEQ_1:def_3
.= dom ((p . i) * q) by VALUED_1:def_5 ;
hence Line (M,i) = (p . i) * q by A3, FINSEQ_1:13; ::_thesis: verum
end;
end;
assume that
A7: len M = len p and
A8: width M = len q and
A9: for i being Element of NAT st i in dom M holds
Line (M,i) = (p . i) * q ; ::_thesis: M = (ColVec2Mx p) * (LineVec2Mx q)
for i, j being Element of NAT st [i,j] in Indices M holds
M * (i,j) = (p . i) * (q . j)
proof
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices M implies M * (i,j) = (p . i) * (q . j) )
assume A10: [i,j] in Indices M ; ::_thesis: M * (i,j) = (p . i) * (q . j)
A11: i in dom M by A10, MATRPROB:13;
j in Seg (width M) by A10, MATRPROB:12;
hence M * (i,j) = (Line (M,i)) . j by MATRIX_1:def_7
.= ((p . i) * q) . j by A9, A11
.= (p . i) * (q . j) by RVSUM_1:44 ;
::_thesis: verum
end;
hence M = (ColVec2Mx p) * (LineVec2Mx q) by A7, A8, Th21; ::_thesis: verum
end;
theorem Th23: :: ENTROPY1:23
for p, q being ProbFinS FinSequence of REAL holds (ColVec2Mx p) * (LineVec2Mx q) is Joint_Probability
proof
let p, q be ProbFinS FinSequence of REAL ; ::_thesis: (ColVec2Mx p) * (LineVec2Mx q) is Joint_Probability
set M = (ColVec2Mx p) * (LineVec2Mx q);
A1: len ((ColVec2Mx p) * (LineVec2Mx q)) = len p by Th22;
A2: LineSum ((ColVec2Mx p) * (LineVec2Mx q)) = p
proof
set M1 = LineSum ((ColVec2Mx p) * (LineVec2Mx q));
A3: len (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) = len ((ColVec2Mx p) * (LineVec2Mx q)) by MATRPROB:20;
then A4: dom (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) = dom ((ColVec2Mx p) * (LineVec2Mx q)) by FINSEQ_3:29;
A5: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(LineSum_((ColVec2Mx_p)_*_(LineVec2Mx_q)))_holds_
(LineSum_((ColVec2Mx_p)_*_(LineVec2Mx_q)))_._k_=_p_._k
let k be Nat; ::_thesis: ( k in dom (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) implies (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) . k = p . k )
assume A6: k in dom (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) ; ::_thesis: (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) . k = p . k
k in Seg (len ((ColVec2Mx p) * (LineVec2Mx q))) by A3, A6, FINSEQ_1:def_3;
hence (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) . k = Sum (Line (((ColVec2Mx p) * (LineVec2Mx q)),k)) by MATRPROB:20
.= Sum ((p . k) * q) by A4, A6, Th22
.= (p . k) * (Sum q) by RVSUM_1:87
.= (p . k) * 1 by MATRPROB:def_5
.= p . k ;
::_thesis: verum
end;
dom (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) = dom p by A1, A3, FINSEQ_3:29;
hence LineSum ((ColVec2Mx p) * (LineVec2Mx q)) = p by A5, FINSEQ_1:13; ::_thesis: verum
end;
A7: width ((ColVec2Mx p) * (LineVec2Mx q)) = len q by Th22;
now__::_thesis:_for_i,_j_being_Element_of_NAT_st_[i,j]_in_Indices_((ColVec2Mx_p)_*_(LineVec2Mx_q))_holds_
((ColVec2Mx_p)_*_(LineVec2Mx_q))_*_(i,j)_>=_0
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices ((ColVec2Mx p) * (LineVec2Mx q)) implies ((ColVec2Mx p) * (LineVec2Mx q)) * (i,j) >= 0 )
assume A8: [i,j] in Indices ((ColVec2Mx p) * (LineVec2Mx q)) ; ::_thesis: ((ColVec2Mx p) * (LineVec2Mx q)) * (i,j) >= 0
i in Seg (len p) by A1, A8, MATRPROB:12;
then i in dom p by FINSEQ_1:def_3;
then A9: p . i >= 0 by MATRPROB:def_5;
j in Seg (len q) by A7, A8, MATRPROB:12;
then j in dom q by FINSEQ_1:def_3;
then A10: q . j >= 0 by MATRPROB:def_5;
((ColVec2Mx p) * (LineVec2Mx q)) * (i,j) = (p . i) * (q . j) by A8, Th21;
hence ((ColVec2Mx p) * (LineVec2Mx q)) * (i,j) >= 0 by A9, A10; ::_thesis: verum
end;
then A11: (ColVec2Mx p) * (LineVec2Mx q) is m-nonnegative by MATRPROB:def_6;
SumAll ((ColVec2Mx p) * (LineVec2Mx q)) = Sum (LineSum ((ColVec2Mx p) * (LineVec2Mx q))) by MATRPROB:def_3
.= 1 by A2, MATRPROB:def_5 ;
then (ColVec2Mx p) * (LineVec2Mx q) is with_sum=1 by MATRPROB:def_7;
hence (ColVec2Mx p) * (LineVec2Mx q) is Joint_Probability by A11; ::_thesis: verum
end;
definition
let n be Nat;
let MR be Matrix of n, REAL ;
attrMR 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 V47() FinSequence-like FinSubsequence-like tabular diagonal for Matrix of n,n, REAL ;
existence
ex b1 being Matrix of n, REAL st b1 is diagonal
proof
deffunc H1( set , set ) -> Element of NAT = 0 ;
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
consider M being Matrix of n1, REAL such that
A1: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = H1(i,j) from MATRIX_1:sch_1();
reconsider M1 = M as Matrix of n, REAL ;
take M1 ; ::_thesis: M1 is diagonal
for i, j being Element of NAT st [i,j] in Indices M & M * (i,j) <> 0 holds
i = j by A1;
hence M1 is diagonal by Def3; ::_thesis: verum
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
let n be Nat; ::_thesis: 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 )
let MR be Matrix of n, REAL ; ::_thesis: ( MR is diagonal iff for i being Element of NAT st i in dom MR holds
Line (MR,i) has_onlyone_value_in i )
A1: width MR = n by MATRIX_1:24;
len MR = n by MATRIX_1:24;
then A2: dom MR = Seg (width MR) by A1, FINSEQ_1:def_3;
hereby ::_thesis: ( ( for i being Element of NAT st i in dom MR holds
Line (MR,i) has_onlyone_value_in i ) implies MR is diagonal )
assume A3: MR is diagonal ; ::_thesis: for i being Element of NAT st i in dom MR holds
Line (MR,i) has_onlyone_value_in i
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_MR_holds_
Line_(MR,i)_has_onlyone_value_in_i
let i be Element of NAT ; ::_thesis: ( i in dom MR implies Line (MR,i) has_onlyone_value_in i )
assume A4: i in dom MR ; ::_thesis: Line (MR,i) has_onlyone_value_in i
A5: len (Line (MR,i)) = width MR by MATRIX_1:def_7;
A6: now__::_thesis:_for_j_being_Element_of_NAT_st_j_in_dom_(Line_(MR,i))_&_j_<>_i_holds_
(Line_(MR,i))_._j_=_0
let j be Element of NAT ; ::_thesis: ( j in dom (Line (MR,i)) & j <> i implies (Line (MR,i)) . j = 0 )
assume that
A7: j in dom (Line (MR,i)) and
A8: j <> i ; ::_thesis: (Line (MR,i)) . j = 0
j in dom (MR . i) by A4, A7, MATRIX_2:16;
then A9: [i,j] in Indices MR by A4, MATRPROB:13;
j in Seg (width MR) by A5, A7, FINSEQ_1:def_3;
hence (Line (MR,i)) . j = MR * (i,j) by MATRIX_1:def_7
.= 0 by A3, A8, A9, Def3 ;
::_thesis: verum
end;
i in dom (Line (MR,i)) by A2, A4, A5, FINSEQ_1:def_3;
hence Line (MR,i) has_onlyone_value_in i by A6, Def2; ::_thesis: verum
end;
hence for i being Element of NAT st i in dom MR holds
Line (MR,i) has_onlyone_value_in i ; ::_thesis: verum
end;
assume A10: for i being Element of NAT st i in dom MR holds
Line (MR,i) has_onlyone_value_in i ; ::_thesis: MR is diagonal
for i, j being Element of NAT st [i,j] in Indices MR & MR * (i,j) <> 0 holds
i = j
proof
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices MR & MR * (i,j) <> 0 implies i = j )
assume that
A11: [i,j] in Indices MR and
A12: MR * (i,j) <> 0 ; ::_thesis: i = j
A13: i in dom MR by A11, MATRPROB:13;
then A14: Line (MR,i) has_onlyone_value_in i by A10;
j in dom (MR . i) by A11, MATRPROB:13;
then A15: j in dom (Line (MR,i)) by A13, MATRIX_2:16;
assume A16: i <> j ; ::_thesis: contradiction
len (Line (MR,i)) = width MR by MATRIX_1:def_7;
then dom (Line (MR,i)) = Seg (width MR) by FINSEQ_1:def_3;
then MR * (i,j) = (Line (MR,i)) . j by A15, MATRIX_1:def_7
.= 0 by A16, A15, A14, Def2 ;
hence contradiction by A12; ::_thesis: verum
end;
hence MR is diagonal by Def3; ::_thesis: verum
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 b1 being diagonal Matrix of len p, REAL st
for j being Element of NAT st j in dom p holds
b1 * (j,j) = p . j
proof
defpred S1[ Nat, Nat, Element of REAL ] means ( ( $1 = $2 implies $3 = p . $1 ) & ( $1 <> $2 implies $3 = 0 ) );
A1: for i, j being Nat st [i,j] in [:(Seg (len p)),(Seg (len p)):] holds
ex x being Element of REAL st S1[i,j,x]
proof
let i, j be Nat; ::_thesis: ( [i,j] in [:(Seg (len p)),(Seg (len p)):] implies ex x being Element of REAL st S1[i,j,x] )
assume [i,j] in [:(Seg (len p)),(Seg (len p)):] ; ::_thesis: ex x being Element of REAL st S1[i,j,x]
( i = j implies S1[i,j,p . i] ) ;
hence ex x being Element of REAL st S1[i,j,x] ; ::_thesis: verum
end;
consider M being Matrix of len p, REAL such that
A2: for i, j being Nat st [i,j] in Indices M holds
S1[i,j,M * (i,j)] from MATRIX_1:sch_2(A1);
for i, j being Element of NAT st [i,j] in Indices M & M * (i,j) <> 0 holds
i = j by A2;
then reconsider M1 = M as diagonal Matrix of len p, REAL by Def3;
take M1 ; ::_thesis: for j being Element of NAT st j in dom p holds
M1 * (j,j) = p . j
len M = len p by MATRIX_1:24;
then A3: Seg (len M1) = dom p by FINSEQ_1:def_3;
width M = len p by MATRIX_1:24;
then A4: Seg (width M1) = dom p by FINSEQ_1:def_3;
for j being Element of NAT st j in dom p holds
M1 * (j,j) = p . j
proof
let j be Element of NAT ; ::_thesis: ( j in dom p implies M1 * (j,j) = p . j )
assume j in dom p ; ::_thesis: M1 * (j,j) = p . j
then [j,j] in Indices M1 by A4, A3, MATRPROB:12;
hence M1 * (j,j) = p . j by A2; ::_thesis: verum
end;
hence for j being Element of NAT st j in dom p holds
M1 * (j,j) = p . j ; ::_thesis: verum
end;
uniqueness
for b1, b2 being diagonal Matrix of len p, REAL st ( for j being Element of NAT st j in dom p holds
b1 * (j,j) = p . j ) & ( for j being Element of NAT st j in dom p holds
b2 * (j,j) = p . j ) holds
b1 = b2
proof
let M1, M2 be diagonal Matrix of len p, REAL ; ::_thesis: ( ( for j being Element of NAT st j in dom p holds
M1 * (j,j) = p . j ) & ( for j being Element of NAT st j in dom p holds
M2 * (j,j) = p . j ) implies M1 = M2 )
assume that
A5: for j being Element of NAT st j in dom p holds
M1 * (j,j) = p . j and
A6: for j being Element of NAT st j in dom p holds
M2 * (j,j) = p . j ; ::_thesis: M1 = M2
width M1 = len p by MATRIX_1:24;
then A7: Seg (width M1) = dom p by FINSEQ_1:def_3;
A8: Indices M1 = Indices M2 by MATRIX_1:26;
now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_M1_holds_
M1_*_(i,j)_=_M2_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (b1,b2) = M2 * (b1,b2) )
assume A9: [i,j] in Indices M1 ; ::_thesis: M1 * (b1,b2) = M2 * (b1,b2)
reconsider i1 = i, j1 = j as Element of NAT by ORDINAL1:def_12;
A10: [i1,j1] in Indices M1 by A9;
then A11: j1 in Seg (width M1) by MATRPROB:12;
percases ( i = j or i <> j ) ;
supposeA12: i = j ; ::_thesis: M1 * (b1,b2) = M2 * (b1,b2)
hence M1 * (i,j) = p . j by A5, A7, A11
.= M2 * (i,j) by A6, A7, A11, A12 ;
::_thesis: verum
end;
supposeA13: i <> j ; ::_thesis: M1 * (b1,b2) = M2 * (b1,b2)
hence M1 * (i,j) = 0 by A10, Def3
.= M2 * (i,j) by A8, A10, A13, Def3 ;
::_thesis: verum
end;
end;
end;
hence M1 = M2 by MATRIX_1:27; ::_thesis: verum
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 Element of 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 Element of NAT st i in dom MR holds
( Line (MR,i) has_onlyone_value_in i & (Line (MR,i)) . i = p . i ) ) ) )
proof
let p be FinSequence of REAL ; ::_thesis: 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 ) ) ) )
let MR be Matrix of REAL; ::_thesis: ( 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 ) ) ) )
hereby ::_thesis: ( 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 ) ) implies MR = Vec2DiagMx p )
assume A1: MR = Vec2DiagMx p ; ::_thesis: ( 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 ) ) )
then reconsider M1 = MR as diagonal Matrix of len p, REAL ;
A2: len M1 = len p by MATRIX_1:24;
then A3: dom MR = dom p by FINSEQ_3:29;
thus ( len MR = len p & width MR = len p ) by A2, MATRIX_1:24; ::_thesis: 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 )
width M1 = len p by MATRIX_1:24;
then A4: Seg (width MR) = dom p by FINSEQ_1:def_3;
thus 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 ) ::_thesis: verum
proof
let i be Element of NAT ; ::_thesis: ( i in dom MR implies ( Line (MR,i) has_onlyone_value_in i & (Line (MR,i)) . i = p . i ) )
assume A5: i in dom MR ; ::_thesis: ( Line (MR,i) has_onlyone_value_in i & (Line (MR,i)) . i = p . i )
A6: Line (M1,i) has_onlyone_value_in i by A5, Th24;
(Line (MR,i)) . i = MR * (i,i) by A3, A4, A5, MATRIX_1:def_7
.= p . i by A1, A3, A5, Def4 ;
hence ( Line (MR,i) has_onlyone_value_in i & (Line (MR,i)) . i = p . i ) by A6; ::_thesis: verum
end;
end;
assume that
A7: len MR = len p and
A8: width MR = len p and
A9: 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 ) ; ::_thesis: MR = Vec2DiagMx p
reconsider MM = MR as Matrix of len p, REAL by A7, A8, MATRIX_2:7;
for i being Element of NAT st i in dom MM holds
Line (MM,i) has_onlyone_value_in i by A9;
then reconsider MM = MM as diagonal Matrix of len p, REAL by Th24;
for j being Element of NAT st j in dom p holds
MM * (j,j) = p . j
proof
A10: dom MM = dom p by A7, FINSEQ_3:29;
let j be Element of NAT ; ::_thesis: ( j in dom p implies MM * (j,j) = p . j )
assume A11: j in dom p ; ::_thesis: MM * (j,j) = p . j
Seg (width MM) = dom p by A8, FINSEQ_1:def_3;
hence MM * (j,j) = (Line (MM,j)) . j by A11, MATRIX_1:def_7
.= p . j by A9, A11, A10 ;
::_thesis: verum
end;
hence MR = Vec2DiagMx p by Def4; ::_thesis: verum
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
let p be FinSequence of REAL ; ::_thesis: 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)) ) ) )
let MR, MR1 be Matrix of REAL; ::_thesis: ( len p = len MR implies ( 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)) ) ) ) )
set MM = Vec2DiagMx p;
A1: len (Vec2DiagMx p) = len p by Th25;
A2: width (Vec2DiagMx p) = len p by Th25;
assume A3: len p = len MR ; ::_thesis: ( 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)) ) ) )
then A4: dom p = dom MR by FINSEQ_3:29;
hereby ::_thesis: ( 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)) ) implies MR1 = (Vec2DiagMx p) * MR )
assume A5: MR1 = (Vec2DiagMx p) * MR ; ::_thesis: ( 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)) ) )
hence ( len MR1 = len p & width MR1 = width MR ) by A3, A1, A2, MATRPROB:39; ::_thesis: for i, j being Element of NAT st [i,j] in Indices MR1 holds
MR1 * (i,j) = (p . i) * (MR * (i,j))
A6: len MR1 = len (Vec2DiagMx p) by A3, A2, A5, MATRPROB:39;
then A7: dom MR1 = dom (Vec2DiagMx p) by FINSEQ_3:29;
A8: dom MR1 = dom p by A1, A6, FINSEQ_3:29;
thus for i, j being Element of NAT st [i,j] in Indices MR1 holds
MR1 * (i,j) = (p . i) * (MR * (i,j)) ::_thesis: verum
proof
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices MR1 implies MR1 * (i,j) = (p . i) * (MR * (i,j)) )
assume A9: [i,j] in Indices MR1 ; ::_thesis: MR1 * (i,j) = (p . i) * (MR * (i,j))
i in Seg (len MR1) by A9, MATRPROB:12;
then A10: i in dom MR1 by FINSEQ_1:def_3;
then A11: (Line ((Vec2DiagMx p),i)) . i = p . i by A7, Th25;
set q = mlt ((Line ((Vec2DiagMx p),i)),(Col (MR,j)));
A12: len (Line ((Vec2DiagMx p),i)) = width (Vec2DiagMx p) by MATRIX_1:def_7;
A13: len (Col (MR,j)) = len MR by MATRIX_1:def_8;
A14: Line ((Vec2DiagMx p),i) has_onlyone_value_in i by A7, A10, Th25;
then A15: (mlt ((Line ((Vec2DiagMx p),i)),(Col (MR,j)))) . i = ((Line ((Vec2DiagMx p),i)) . i) * ((Col (MR,j)) . i) by A3, A2, A12, A13, Th12;
thus MR1 * (i,j) = (Line ((Vec2DiagMx p),i)) "*" (Col (MR,j)) by A3, A2, A5, A9, MATRPROB:39
.= Sum (mlt ((Line ((Vec2DiagMx p),i)),(Col (MR,j)))) by RVSUM_1:def_16
.= (p . i) * ((Col (MR,j)) . i) by A3, A2, A14, A11, A12, A13, A15, Th12, Th13
.= (p . i) * (MR * (i,j)) by A4, A8, A10, MATRIX_1:def_8 ; ::_thesis: verum
end;
end;
assume that
A16: len MR1 = len p and
A17: width MR1 = width MR and
A18: for i, j being Element of NAT st [i,j] in Indices MR1 holds
MR1 * (i,j) = (p . i) * (MR * (i,j)) ; ::_thesis: MR1 = (Vec2DiagMx p) * MR
A19: dom MR1 = dom (Vec2DiagMx p) by A1, A16, FINSEQ_3:29;
A20: dom MR = dom MR1 by A3, A16, FINSEQ_3:29;
for i, j being Element of NAT st [i,j] in Indices MR1 holds
MR1 * (i,j) = (Line ((Vec2DiagMx p),i)) "*" (Col (MR,j))
proof
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices MR1 implies MR1 * (i,j) = (Line ((Vec2DiagMx p),i)) "*" (Col (MR,j)) )
assume A21: [i,j] in Indices MR1 ; ::_thesis: MR1 * (i,j) = (Line ((Vec2DiagMx p),i)) "*" (Col (MR,j))
i in Seg (len MR1) by A21, MATRPROB:12;
then A22: i in dom MR1 by FINSEQ_1:def_3;
then A23: (Line ((Vec2DiagMx p),i)) . i = p . i by A19, Th25;
set q = mlt ((Line ((Vec2DiagMx p),i)),(Col (MR,j)));
A24: len (Line ((Vec2DiagMx p),i)) = width (Vec2DiagMx p) by MATRIX_1:def_7;
A25: len (Col (MR,j)) = len MR by MATRIX_1:def_8;
A26: Line ((Vec2DiagMx p),i) has_onlyone_value_in i by A19, A22, Th25;
then A27: (mlt ((Line ((Vec2DiagMx p),i)),(Col (MR,j)))) . i = ((Line ((Vec2DiagMx p),i)) . i) * ((Col (MR,j)) . i) by A3, A2, A24, A25, Th12;
thus MR1 * (i,j) = (p . i) * (MR * (i,j)) by A18, A21
.= (p . i) * ((Col (MR,j)) . i) by A20, A22, MATRIX_1:def_8
.= Sum (mlt ((Line ((Vec2DiagMx p),i)),(Col (MR,j)))) by A3, A2, A26, A23, A24, A25, A27, Th12, Th13
.= (Line ((Vec2DiagMx p),i)) "*" (Col (MR,j)) by RVSUM_1:def_16 ; ::_thesis: verum
end;
hence MR1 = (Vec2DiagMx p) * MR by A3, A1, A2, A16, A17, MATRPROB:39; ::_thesis: verum
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
let p be FinSequence of REAL ; ::_thesis: 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)) ) ) )
let MR, MR1 be Matrix of REAL; ::_thesis: ( len p = len MR implies ( 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)) ) ) ) )
set MM = Vec2DiagMx p;
assume A1: len p = len MR ; ::_thesis: ( 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)) ) ) )
hereby ::_thesis: ( 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)) ) implies MR1 = (Vec2DiagMx p) * MR )
assume A2: MR1 = (Vec2DiagMx p) * MR ; ::_thesis: ( 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)) ) )
hence ( len MR1 = len p & width MR1 = width MR ) by A1, Th26; ::_thesis: for i being Element of NAT st i in dom MR1 holds
Line (MR1,i) = (p . i) * (Line (MR,i))
A3: width MR1 = width MR by A1, A2, Th26;
thus for i being Element of NAT st i in dom MR1 holds
Line (MR1,i) = (p . i) * (Line (MR,i)) ::_thesis: verum
proof
let i be Element of NAT ; ::_thesis: ( i in dom MR1 implies Line (MR1,i) = (p . i) * (Line (MR,i)) )
assume i in dom MR1 ; ::_thesis: Line (MR1,i) = (p . i) * (Line (MR,i))
then A4: i in Seg (len MR1) by FINSEQ_1:def_3;
A5: for j being Nat st j in dom (Line (MR1,i)) holds
(Line (MR1,i)) . j = ((p . i) * (Line (MR,i))) . j
proof
let j be Nat; ::_thesis: ( j in dom (Line (MR1,i)) implies (Line (MR1,i)) . j = ((p . i) * (Line (MR,i))) . j )
assume j in dom (Line (MR1,i)) ; ::_thesis: (Line (MR1,i)) . j = ((p . i) * (Line (MR,i))) . j
then j in Seg (len (Line (MR1,i))) by FINSEQ_1:def_3;
then A6: j in Seg (width MR1) by MATRIX_1:def_7;
then A7: [i,j] in Indices MR1 by A4, MATRPROB:12;
A8: j in NAT by ORDINAL1:def_12;
thus (Line (MR1,i)) . j = MR1 * (i,j) by A6, MATRIX_1:def_7
.= (p . i) * (MR * (i,j)) by A1, A2, A8, A7, Th26
.= (p . i) * ((Line (MR,i)) . j) by A3, A6, MATRIX_1:def_7
.= ((p . i) * (Line (MR,i))) . j by RVSUM_1:44 ; ::_thesis: verum
end;
dom (Line (MR1,i)) = Seg (len (Line (MR1,i))) by FINSEQ_1:def_3
.= Seg (width MR1) by MATRIX_1:def_7
.= Seg (len (Line (MR,i))) by A3, MATRIX_1:def_7
.= dom (Line (MR,i)) by FINSEQ_1:def_3
.= dom ((p . i) * (Line (MR,i))) by VALUED_1:def_5 ;
hence Line (MR1,i) = (p . i) * (Line (MR,i)) by A5, FINSEQ_1:13; ::_thesis: verum
end;
end;
assume that
A9: len MR1 = len p and
A10: width MR1 = width MR and
A11: for i being Element of NAT st i in dom MR1 holds
Line (MR1,i) = (p . i) * (Line (MR,i)) ; ::_thesis: MR1 = (Vec2DiagMx p) * MR
for i, j being Element of NAT st [i,j] in Indices MR1 holds
MR1 * (i,j) = (p . i) * (MR * (i,j))
proof
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices MR1 implies MR1 * (i,j) = (p . i) * (MR * (i,j)) )
assume A12: [i,j] in Indices MR1 ; ::_thesis: MR1 * (i,j) = (p . i) * (MR * (i,j))
A13: i in dom MR1 by A12, MATRPROB:13;
A14: j in Seg (width MR1) by A12, MATRPROB:12;
hence MR1 * (i,j) = (Line (MR1,i)) . j by MATRIX_1:def_7
.= ((p . i) * (Line (MR,i))) . j by A11, A13
.= (p . i) * ((Line (MR,i)) . j) by RVSUM_1:44
.= (p . i) * (MR * (i,j)) by A10, A14, MATRIX_1:def_7 ;
::_thesis: verum
end;
hence MR1 = (Vec2DiagMx p) * MR by A1, A9, A10, Th26; ::_thesis: verum
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
let p be ProbFinS FinSequence of REAL ; ::_thesis: for M being non empty-yielding Conditional_Probability Matrix of REAL st len p = len M holds
(Vec2DiagMx p) * M is Joint_Probability
let M be non empty-yielding Conditional_Probability Matrix of REAL; ::_thesis: ( len p = len M implies (Vec2DiagMx p) * M is Joint_Probability )
set M1 = (Vec2DiagMx p) * M;
assume A1: len p = len M ; ::_thesis: (Vec2DiagMx p) * M is Joint_Probability
then A2: len ((Vec2DiagMx p) * M) = len p by Th26;
A3: LineSum ((Vec2DiagMx p) * M) = p
proof
set M2 = LineSum ((Vec2DiagMx p) * M);
A4: len (LineSum ((Vec2DiagMx p) * M)) = len ((Vec2DiagMx p) * M) by MATRPROB:20;
then A5: dom (LineSum ((Vec2DiagMx p) * M)) = dom M by A1, A2, FINSEQ_3:29;
A6: dom (LineSum ((Vec2DiagMx p) * M)) = dom ((Vec2DiagMx p) * M) by A4, FINSEQ_3:29;
A7: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(LineSum_((Vec2DiagMx_p)_*_M))_holds_
(LineSum_((Vec2DiagMx_p)_*_M))_._k_=_p_._k
let k be Nat; ::_thesis: ( k in dom (LineSum ((Vec2DiagMx p) * M)) implies (LineSum ((Vec2DiagMx p) * M)) . k = p . k )
assume A8: k in dom (LineSum ((Vec2DiagMx p) * M)) ; ::_thesis: (LineSum ((Vec2DiagMx p) * M)) . k = p . k
k in Seg (len ((Vec2DiagMx p) * M)) by A4, A8, FINSEQ_1:def_3;
hence (LineSum ((Vec2DiagMx p) * M)) . k = Sum (Line (((Vec2DiagMx p) * M),k)) by MATRPROB:20
.= Sum ((p . k) * (Line (M,k))) by A1, A6, A8, Th27
.= (p . k) * (Sum (Line (M,k))) by RVSUM_1:87
.= (p . k) * (Sum (M . k)) by A5, A8, MATRIX_2:16
.= (p . k) * 1 by A5, A8, MATRPROB:def_9
.= p . k ;
::_thesis: verum
end;
dom (LineSum ((Vec2DiagMx p) * M)) = dom p by A2, A4, FINSEQ_3:29;
hence LineSum ((Vec2DiagMx p) * M) = p by A7, FINSEQ_1:13; ::_thesis: verum
end;
A9: width ((Vec2DiagMx p) * M) = width M by A1, Th26;
now__::_thesis:_for_i,_j_being_Element_of_NAT_st_[i,j]_in_Indices_((Vec2DiagMx_p)_*_M)_holds_
((Vec2DiagMx_p)_*_M)_*_(i,j)_>=_0
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices ((Vec2DiagMx p) * M) implies ((Vec2DiagMx p) * M) * (i,j) >= 0 )
assume A10: [i,j] in Indices ((Vec2DiagMx p) * M) ; ::_thesis: ((Vec2DiagMx p) * M) * (i,j) >= 0
A11: j in Seg (width M) by A9, A10, MATRPROB:12;
i in Seg (len p) by A2, A10, MATRPROB:12;
then i in dom p by FINSEQ_1:def_3;
then A12: p . i >= 0 by MATRPROB:def_5;
i in Seg (len M) by A1, A2, A10, MATRPROB:12;
then [i,j] in Indices M by A11, MATRPROB:12;
then A13: M * (i,j) >= 0 by MATRPROB:def_6;
((Vec2DiagMx p) * M) * (i,j) = (p . i) * (M * (i,j)) by A1, A10, Th26;
hence ((Vec2DiagMx p) * M) * (i,j) >= 0 by A12, A13; ::_thesis: verum
end;
then A14: (Vec2DiagMx p) * M is m-nonnegative by MATRPROB:def_6;
SumAll ((Vec2DiagMx p) * M) = Sum (LineSum ((Vec2DiagMx p) * M)) by MATRPROB:def_3
.= 1 by A3, MATRPROB:def_5 ;
then (Vec2DiagMx p) * M is with_sum=1 by MATRPROB:def_7;
hence (Vec2DiagMx p) * M is Joint_Probability by A14; ::_thesis: verum
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
let D be non empty set ; ::_thesis: 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)
let M be Matrix of D; ::_thesis: 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)
let p be FinSequence of D * ; ::_thesis: ( 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 for k being Element of NAT st k in dom p holds
len (p . k) = k * (width M) )
assume that
A1: len p = len M and
A2: p . 1 = M . 1 and
A3: for k being Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ; ::_thesis: for k being Element of NAT st k in dom p holds
len (p . k) = k * (width M)
defpred S1[ Element of NAT ] means ( $1 >= 1 & $1 <= len M implies len (p . $1) = $1 * (width M) );
A4: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A5: ( n >= 1 & n <= len M implies len (p . n) = n * (width M) ) ; ::_thesis: S1[n + 1]
assume that
A6: n + 1 >= 1 and
A7: n + 1 <= len M ; ::_thesis: len (p . (n + 1)) = (n + 1) * (width M)
now__::_thesis:_len_(p_._(n_+_1))_=_(n_+_1)_*_(width_M)
percases ( n = 0 or n <> 0 ) ;
supposeA8: n = 0 ; ::_thesis: len (p . (n + 1)) = (n + 1) * (width M)
then 1 in dom M by A7, FINSEQ_3:25;
hence len (p . (n + 1)) = (n + 1) * (width M) by A2, A8, MATRIX_1:42; ::_thesis: verum
end;
supposeA9: n <> 0 ; ::_thesis: len (p . (n + 1)) = (n + 1) * (width M)
A10: n + 1 in dom M by A6, A7, FINSEQ_3:25;
n < len M by A7, NAT_1:13;
then p . (n + 1) = (p . n) ^ (M . (n + 1)) by A3, A9, NAT_1:14;
then len (p . (n + 1)) = (len (p . n)) + (len (M . (n + 1))) by FINSEQ_1:22
.= (n * (width M)) + (width M) by A5, A7, A9, A10, MATRIX_1:42, NAT_1:13, NAT_1:14
.= (n + 1) * (width M) ;
hence len (p . (n + 1)) = (n + 1) * (width M) ; ::_thesis: verum
end;
end;
end;
hence len (p . (n + 1)) = (n + 1) * (width M) ; ::_thesis: verum
end;
A11: S1[ 0 ] ;
A12: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A11, A4);
let k be Element of NAT ; ::_thesis: ( k in dom p implies len (p . k) = k * (width M) )
assume k in dom p ; ::_thesis: len (p . k) = k * (width M)
then A13: k in Seg (len p) by FINSEQ_1:def_3;
then A14: k <= len p by FINSEQ_1:1;
k >= 1 by A13, FINSEQ_1:1;
hence len (p . k) = k * (width M) by A1, A12, A14; ::_thesis: verum
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
let D be non empty set ; ::_thesis: 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)
let M be Matrix of D; ::_thesis: 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)
let p be FinSequence of D * ; ::_thesis: ( 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 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) )
assume that
A1: len p = len M and
A2: p . 1 = M . 1 and
A3: for k being Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ; ::_thesis: 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)
let i, j be Element of NAT ; ::_thesis: ( i in dom p & j in dom p & i <= j implies dom (p . i) c= dom (p . j) )
assume that
A4: i in dom p and
A5: j in dom p and
A6: i <= j ; ::_thesis: dom (p . i) c= dom (p . j)
A7: len (p . j) = j * (width M) by A1, A2, A3, A5, Th29;
len (p . i) = i * (width M) by A1, A2, A3, A4, Th29;
then len (p . i) <= len (p . j) by A6, A7, NAT_1:4;
then Seg (len (p . i)) c= Seg (len (p . j)) by FINSEQ_1:5;
then dom (p . i) c= Seg (len (p . j)) by FINSEQ_1:def_3;
hence dom (p . i) c= dom (p . j) by FINSEQ_1:def_3; ::_thesis: verum
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
let D be non empty set ; ::_thesis: 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) ) ) )
let M be Matrix of D; ::_thesis: 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) ) ) )
let p be FinSequence of D * ; ::_thesis: ( 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 ( 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) ) ) ) )
assume that
A1: len p = len M and
A2: p . 1 = M . 1 and
A3: for k being Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ; ::_thesis: ( 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) ) ) )
percases ( len M = 0 or len M > 0 ) ;
supposeA4: len M = 0 ; ::_thesis: ( 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) ) ) )
then p = {} by A1;
then p . 1 = {} by FUNCT_1:def_2, RELAT_1:38;
hence len (p . 1) = width M by A4, MATRIX_1:def_3; ::_thesis: for j being Element of NAT st [1,j] in Indices M holds
( j in dom (p . 1) & (p . 1) . j = M * (1,j) )
let j be Element of NAT ; ::_thesis: ( [1,j] in Indices M implies ( j in dom (p . 1) & (p . 1) . j = M * (1,j) ) )
A5: Seg (len M) = {} by A4;
assume [1,j] in Indices M ; ::_thesis: ( j in dom (p . 1) & (p . 1) . j = M * (1,j) )
hence ( j in dom (p . 1) & (p . 1) . j = M * (1,j) ) by A5, MATRPROB:12; ::_thesis: verum
end;
suppose len M > 0 ; ::_thesis: ( 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) ) ) )
then 1 <= len p by A1, NAT_1:14;
then 1 in Seg (len p) by FINSEQ_1:1;
then 1 in dom p by FINSEQ_1:def_3;
hence A6: len (p . 1) = 1 * (width M) by A1, A2, A3, Th29
.= width M ;
::_thesis: for j being Element of NAT st [1,j] in Indices M holds
( j in dom (p . 1) & (p . 1) . j = M * (1,j) )
let j be Element of NAT ; ::_thesis: ( [1,j] in Indices M implies ( j in dom (p . 1) & (p . 1) . j = M * (1,j) ) )
assume A7: [1,j] in Indices M ; ::_thesis: ( j in dom (p . 1) & (p . 1) . j = M * (1,j) )
j in Seg (width M) by A7, MATRPROB:12;
hence ( j in dom (p . 1) & (p . 1) . j = M * (1,j) ) by A2, A6, A7, FINSEQ_1:def_3, MATRPROB:14; ::_thesis: verum
end;
end;
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
let D be non empty set ; ::_thesis: 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
let M be Matrix of D; ::_thesis: 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
let p be FinSequence of D * ; ::_thesis: ( 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)) ) implies 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 )
assume that
A1: len p = len M and
A2: for k being Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ; ::_thesis: 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
let j be Element of NAT ; ::_thesis: ( j >= 1 & j < len p implies for l being Element of NAT st l in dom (p . j) holds
(p . j) . l = (p . (j + 1)) . l )
assume that
A3: j >= 1 and
A4: j < len p ; ::_thesis: for l being Element of NAT st l in dom (p . j) holds
(p . j) . l = (p . (j + 1)) . l
A5: p . (j + 1) = (p . j) ^ (M . (j + 1)) by A1, A2, A3, A4;
let l be Element of NAT ; ::_thesis: ( l in dom (p . j) implies (p . j) . l = (p . (j + 1)) . l )
assume l in dom (p . j) ; ::_thesis: (p . j) . l = (p . (j + 1)) . l
hence (p . j) . l = (p . (j + 1)) . l by A5, FINSEQ_1:def_7; ::_thesis: verum
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
let D be non empty set ; ::_thesis: 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
let M be Matrix of D; ::_thesis: 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
let p be FinSequence of D * ; ::_thesis: ( 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 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 )
assume that
A1: len p = len M and
A2: p . 1 = M . 1 and
A3: for k being Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ; ::_thesis: 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
defpred S1[ Element of NAT ] means ( $1 in dom p implies for i being Element of NAT st i in dom p & i <= $1 holds
for l being Element of NAT st l in dom (p . i) holds
(p . i) . l = (p . $1) . l );
A4: for j being Element of NAT st S1[j] holds
S1[j + 1]
proof
let j be Element of NAT ; ::_thesis: ( S1[j] implies S1[j + 1] )
assume A5: ( j in dom p implies for i being Element of NAT st i 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 ) ; ::_thesis: S1[j + 1]
assume A6: j + 1 in dom p ; ::_thesis: for i being Element of NAT st i in dom p & i <= j + 1 holds
for l being Element of NAT st l in dom (p . i) holds
(p . i) . l = (p . (j + 1)) . l
then A7: j + 1 <= len p by FINSEQ_3:25;
j + 1 >= 1 by A6, FINSEQ_3:25;
then A8: ( j + 1 = 1 or j + 1 > 1 ) by XXREAL_0:1;
let i be Element of NAT ; ::_thesis: ( i in dom p & i <= j + 1 implies for l being Element of NAT st l in dom (p . i) holds
(p . i) . l = (p . (j + 1)) . l )
assume that
A9: i in dom p and
A10: i <= j + 1 ; ::_thesis: for l being Element of NAT st l in dom (p . i) holds
(p . i) . l = (p . (j + 1)) . l
i in Seg (len p) by A9, FINSEQ_1:def_3;
then A11: i >= 1 by FINSEQ_1:1;
percases ( j + 1 = 1 or j >= 1 ) by A8, NAT_1:13;
suppose j + 1 = 1 ; ::_thesis: for l being Element of NAT st l in dom (p . i) holds
(p . i) . l = (p . (j + 1)) . l
hence for l being Element of NAT st l in dom (p . i) holds
(p . i) . l = (p . (j + 1)) . l by A10, A11, XXREAL_0:1; ::_thesis: verum
end;
supposeA12: j >= 1 ; ::_thesis: for l being Element of NAT st l in dom (p . i) holds
(p . i) . l = (p . (j + 1)) . l
A13: j < len p by A7, NAT_1:13;
then A14: j in Seg (len p) by A12, FINSEQ_1:1;
then A15: j in dom p by FINSEQ_1:def_3;
thus for l being Element of NAT st l in dom (p . i) holds
(p . i) . l = (p . (j + 1)) . l ::_thesis: verum
proof
let l be Element of NAT ; ::_thesis: ( l in dom (p . i) implies (p . i) . l = (p . (j + 1)) . l )
assume A16: l in dom (p . i) ; ::_thesis: (p . i) . l = (p . (j + 1)) . l
percases ( i <= j or i = j + 1 ) by A10, NAT_1:8;
supposeA17: i <= j ; ::_thesis: (p . i) . l = (p . (j + 1)) . l
then A18: dom (p . i) c= dom (p . j) by A1, A2, A3, A9, A15, Th30;
thus (p . i) . l = (p . j) . l by A5, A9, A14, A16, A17, FINSEQ_1:def_3
.= (p . (j + 1)) . l by A1, A3, A12, A13, A16, A18, Th32 ; ::_thesis: verum
end;
suppose i = j + 1 ; ::_thesis: (p . i) . l = (p . (j + 1)) . l
hence (p . i) . l = (p . (j + 1)) . l ; ::_thesis: verum
end;
end;
end;
end;
end;
end;
A19: S1[ 0 ] ;
for j being Element of NAT holds S1[j] from NAT_1:sch_1(A19, A4);
hence 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 ; ::_thesis: verum
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
let D be non empty set ; ::_thesis: 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 )
let M be Matrix of D; ::_thesis: 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 )
let p be FinSequence of D * ; ::_thesis: ( 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 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 ) )
assume that
A1: len p = len M and
A2: p . 1 = M . 1 and
A3: for k being Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ; ::_thesis: 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 )
let j be Element of NAT ; ::_thesis: ( j >= 1 & j < len p implies 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 ) )
assume that
A4: j >= 1 and
A5: j < len p ; ::_thesis: 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 )
A6: j + 1 >= 1 by A4, NAT_1:13;
j in Seg (len p) by A4, A5, FINSEQ_1:1;
then j in dom p by FINSEQ_1:def_3;
then A7: len (p . j) = j * (width M) by A1, A2, A3, Th29;
let l be Element of NAT ; ::_thesis: ( l in Seg (width M) implies ( (j * (width M)) + l in dom (p . (j + 1)) & (p . (j + 1)) . ((j * (width M)) + l) = (M . (j + 1)) . l ) )
assume A8: l in Seg (width M) ; ::_thesis: ( (j * (width M)) + l in dom (p . (j + 1)) & (p . (j + 1)) . ((j * (width M)) + l) = (M . (j + 1)) . l )
A9: l <= width M by A8, FINSEQ_1:1;
j + 1 <= len M by A1, A5, NAT_1:13;
then j + 1 in Seg (len M) by A6, FINSEQ_1:1;
then A10: j + 1 in dom M by FINSEQ_1:def_3;
then A11: l in dom (M . (j + 1)) by A8, Th18;
l >= 1 by A8, FINSEQ_1:1;
then A12: (j * (width M)) + l >= 0 + 1 by XREAL_1:7;
dom p = dom M by A1, FINSEQ_3:29;
then len (p . (j + 1)) = (j + 1) * (width M) by A1, A2, A3, A10, Th29
.= (j * (width M)) + (width M) ;
then (j * (width M)) + l <= len (p . (j + 1)) by A9, XREAL_1:7;
then (j * (width M)) + l in Seg (len (p . (j + 1))) by A12, FINSEQ_1:1;
hence (j * (width M)) + l in dom (p . (j + 1)) by FINSEQ_1:def_3; ::_thesis: (p . (j + 1)) . ((j * (width M)) + l) = (M . (j + 1)) . l
p . (j + 1) = (p . j) ^ (M . (j + 1)) by A1, A3, A4, A5;
hence (p . (j + 1)) . ((j * (width M)) + l) = (M . (j + 1)) . l by A11, A7, FINSEQ_1:def_7; ::_thesis: verum
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
let D be non empty set ; ::_thesis: 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) )
let M be Matrix of D; ::_thesis: 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) )
let p be FinSequence of D * ; ::_thesis: ( 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 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) ) )
assume that
A1: len p = len M and
A2: p . 1 = M . 1 and
A3: for k being Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ; ::_thesis: 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) )
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices M implies ( ((i - 1) * (width M)) + j in dom (p . i) & M * (i,j) = (p . i) . (((i - 1) * (width M)) + j) ) )
assume A4: [i,j] in Indices M ; ::_thesis: ( ((i - 1) * (width M)) + j in dom (p . i) & M * (i,j) = (p . i) . (((i - 1) * (width M)) + j) )
A5: j in Seg (width M) by A4, MATRPROB:12;
i in Seg (len M) by A4, MATRPROB:12;
then A6: i in dom M by FINSEQ_1:def_3;
then A7: i >= 1 by FINSEQ_3:25;
A8: i <= len M by A6, FINSEQ_3:25;
percases ( i > 1 or i = 1 ) by A7, XXREAL_0:1;
supposeA9: i > 1 ; ::_thesis: ( ((i - 1) * (width M)) + j in dom (p . i) & M * (i,j) = (p . i) . (((i - 1) * (width M)) + j) )
then reconsider ii = i - 1 as Element of NAT by NAT_1:20;
i < (len M) + 1 by A8, NAT_1:13;
then A10: i - 1 < ((len M) + 1) - 1 by XREAL_1:14;
ii + 1 > 1 by A9;
then A11: ii >= 1 by NAT_1:13;
then (p . (ii + 1)) . ((ii * (width M)) + j) = (M . (ii + 1)) . j by A1, A2, A3, A5, A10, Th34;
hence ( ((i - 1) * (width M)) + j in dom (p . i) & M * (i,j) = (p . i) . (((i - 1) * (width M)) + j) ) by A1, A2, A3, A4, A5, A11, A10, Th34, MATRPROB:14; ::_thesis: verum
end;
suppose i = 1 ; ::_thesis: ( ((i - 1) * (width M)) + j in dom (p . i) & M * (i,j) = (p . i) . (((i - 1) * (width M)) + j) )
hence ( ((i - 1) * (width M)) + j in dom (p . i) & M * (i,j) = (p . i) . (((i - 1) * (width M)) + j) ) by A1, A2, A3, A4, Th31; ::_thesis: verum
end;
end;
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
let D be non empty set ; ::_thesis: 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) )
let M be Matrix of D; ::_thesis: 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) )
let p be FinSequence of D * ; ::_thesis: ( 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 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) ) )
assume that
A1: len p = len M and
A2: p . 1 = M . 1 and
A3: for k being Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ; ::_thesis: 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) )
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices M implies ( ((i - 1) * (width M)) + j in dom (p . (len M)) & M * (i,j) = (p . (len M)) . (((i - 1) * (width M)) + j) ) )
assume A4: [i,j] in Indices M ; ::_thesis: ( ((i - 1) * (width M)) + j in dom (p . (len M)) & M * (i,j) = (p . (len M)) . (((i - 1) * (width M)) + j) )
A5: ((i - 1) * (width M)) + j in dom (p . i) by A1, A2, A3, A4, Th35;
A6: M * (i,j) = (p . i) . (((i - 1) * (width M)) + j) by A1, A2, A3, A4, Th35;
A7: i in Seg (len M) by A4, MATRPROB:12;
then A8: len M <> 0 ;
A9: i <= len M by A7, FINSEQ_1:1;
len M >= 1 by A8, NAT_1:14;
then len M in Seg (len p) by A1, FINSEQ_1:1;
then A10: len M in dom p by FINSEQ_1:def_3;
A11: i in dom p by A1, A7, FINSEQ_1:def_3;
then dom (p . i) c= dom (p . (len M)) by A1, A2, A3, A9, A10, Th30;
hence ( ((i - 1) * (width M)) + j in dom (p . (len M)) & M * (i,j) = (p . (len M)) . (((i - 1) * (width M)) + j) ) by A1, A2, A3, A9, A11, A10, A5, A6, Th33; ::_thesis: verum
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
let M be Matrix of REAL; ::_thesis: 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)))
let p be FinSequence of REAL * ; ::_thesis: ( ( for k being Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) implies for k being Element of NAT st k >= 1 & k < len M holds
Sum (p . (k + 1)) = (Sum (p . k)) + (Sum (M . (k + 1))) )
assume A1: for k being Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ; ::_thesis: for k being Element of NAT st k >= 1 & k < len M holds
Sum (p . (k + 1)) = (Sum (p . k)) + (Sum (M . (k + 1)))
let k be Element of NAT ; ::_thesis: ( k >= 1 & k < len M implies Sum (p . (k + 1)) = (Sum (p . k)) + (Sum (M . (k + 1))) )
assume that
A2: k >= 1 and
A3: k < len M ; ::_thesis: Sum (p . (k + 1)) = (Sum (p . k)) + (Sum (M . (k + 1)))
p . (k + 1) = (p . k) ^ (M . (k + 1)) by A1, A2, A3;
hence Sum (p . (k + 1)) = (Sum (p . k)) + (Sum (M . (k + 1))) by RVSUM_1:75; ::_thesis: verum
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
let M be Matrix of REAL; ::_thesis: 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))
let p be FinSequence of REAL * ; ::_thesis: ( 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 SumAll M = Sum (p . (len M)) )
assume that
A1: len p = len M and
A2: p . 1 = M . 1 and
A3: for k being Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ; ::_thesis: SumAll M = Sum (p . (len M))
percases ( len M = 0 or len M > 0 ) ;
supposeA4: len M = 0 ; ::_thesis: SumAll M = Sum (p . (len M))
then p = {} by A1;
hence Sum (p . (len M)) = 0 by FUNCT_1:def_2, RELAT_1:38, RVSUM_1:72
.= SumAll M by A4, MATRPROB:23 ;
::_thesis: verum
end;
supposeA5: len M > 0 ; ::_thesis: SumAll M = Sum (p . (len M))
then A6: len M >= 1 by NAT_1:14;
set q = LineSum M;
A7: len (LineSum M) = len M by MATRPROB:def_1;
then consider qq being FinSequence of REAL such that
A8: len qq = len (LineSum M) and
A9: qq . 1 = (LineSum M) . 1 and
A10: for k being Element of NAT st 0 <> k & k < len (LineSum M) holds
qq . (k + 1) = (qq . k) + ((LineSum M) . (k + 1)) and
A11: Sum (LineSum M) = qq . (len (LineSum M)) by A5, Th9, NAT_1:14;
A12: len qq = len M by A8, MATRPROB:def_1
.= len (Sum p) by A1, MATRPROB:def_1 ;
A13: dom qq = Seg (len qq) by FINSEQ_1:def_3;
A14: len (Sum p) = len p by MATRPROB:def_1;
then A15: dom (Sum p) = dom p by FINSEQ_3:29;
for j being Nat st j in dom qq holds
qq . j = (Sum p) . j
proof
defpred S1[ Nat] means ( $1 in dom qq implies qq . $1 = (Sum p) . $1 );
A16: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A17: S1[k] ; ::_thesis: S1[k + 1]
assume A18: k + 1 in dom qq ; ::_thesis: qq . (k + 1) = (Sum p) . (k + 1)
then A19: k + 1 <= len qq by A13, FINSEQ_1:1;
A20: k + 1 in dom (Sum p) by A1, A7, A14, A8, A13, A18, FINSEQ_1:def_3;
A21: k + 1 in dom M by A7, A8, A13, A18, FINSEQ_1:def_3;
k + 1 >= 1 by A13, A18, FINSEQ_1:1;
then A22: ( k + 1 = 1 or k + 1 > 1 ) by XXREAL_0:1;
percases ( k + 1 = 1 or k >= 1 ) by A22, NAT_1:13;
supposeA23: k + 1 = 1 ; ::_thesis: qq . (k + 1) = (Sum p) . (k + 1)
A24: 1 in Seg (len M) by A6, FINSEQ_1:1;
then A25: 1 in dom M by FINSEQ_1:def_3;
A26: 1 in dom p by A1, A24, FINSEQ_1:def_3;
qq . (k + 1) = Sum (Line (M,1)) by A9, A23, A24, MATRPROB:20
.= Sum (M . 1) by A25, MATRIX_2:16
.= (Sum p) . 1 by A2, A15, A26, MATRPROB:def_1 ;
hence qq . (k + 1) = (Sum p) . (k + 1) by A23; ::_thesis: verum
end;
supposeA27: k >= 1 ; ::_thesis: qq . (k + 1) = (Sum p) . (k + 1)
A28: k < len qq by A19, NAT_1:13;
then A29: k < len M by A8, MATRPROB:def_1;
k in Seg (len qq) by A27, A28, FINSEQ_1:1;
then A30: k in dom (Sum p) by A12, FINSEQ_1:def_3;
qq . (k + 1) = (qq . k) + ((LineSum M) . (k + 1)) by A8, A10, A27, A28
.= (Sum (p . k)) + ((LineSum M) . (k + 1)) by A13, A17, A27, A28, A30, FINSEQ_1:1, MATRPROB:def_1
.= (Sum (p . k)) + (Sum (Line (M,(k + 1)))) by A7, A8, A13, A18, MATRPROB:20
.= (Sum (p . k)) + (Sum (M . (k + 1))) by A21, MATRIX_2:16
.= Sum (p . (k + 1)) by A3, A27, A29, Th37
.= (Sum p) . (k + 1) by A20, MATRPROB:def_1 ;
hence qq . (k + 1) = (Sum p) . (k + 1) ; ::_thesis: verum
end;
end;
end;
A31: S1[ 0 ] by A13, FINSEQ_1:1;
for j being Element of NAT holds S1[j] from NAT_1:sch_1(A31, A16);
hence for j being Nat st j in dom qq holds
qq . j = (Sum p) . j ; ::_thesis: verum
end;
then A32: qq = Sum p by A12, FINSEQ_2:9;
len M in Seg (len M) by A5, FINSEQ_1:3;
then A33: len M in dom (Sum p) by A1, A14, FINSEQ_1:def_3;
thus SumAll M = Sum (LineSum M) by MATRPROB:def_3
.= (Sum p) . (len M) by A11, A32, MATRPROB:def_1
.= Sum (p . (len M)) by A33, MATRPROB:def_1 ; ::_thesis: verum
end;
end;
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 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 Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) ) )
proof
thus ( len M = 0 implies ex z being FinSequence of D st z = {} ) ::_thesis: ( 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 Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) )
proof
assume len M = 0 ; ::_thesis: ex z being FinSequence of D st z = {}
<*> D = {} ;
hence ex z being FinSequence of D st z = {} ; ::_thesis: verum
end;
thus ( len M <> 0 implies ex z being FinSequence of D ex p being FinSequence of D * st
( z = 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)) ) ) ) ::_thesis: verum
proof
reconsider M1 = M . 1 as Element of D * by FINSEQ_1:def_11;
defpred S1[ Element of NAT , set , set ] means ex p1, q1 being Element of D * st
( q1 = $2 & p1 = M . ($1 + 1) & $3 = q1 ^ p1 );
assume A1: len M <> 0 ; ::_thesis: ex z being FinSequence of D ex p being FinSequence of D * st
( z = 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)) ) )
A2: for n being Element of NAT st 1 <= n & n < len M holds
for x being Element of D * ex y being Element of D * st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: ( 1 <= n & n < len M implies for x being Element of D * ex y being Element of D * st S1[n,x,y] )
assume that
1 <= n and
A3: n < len M ; ::_thesis: for x being Element of D * ex y being Element of D * st S1[n,x,y]
A4: 1 <= n + 1 by NAT_1:11;
n + 1 <= len M by A3, NAT_1:13;
then n + 1 in dom M by A4, FINSEQ_3:25;
then reconsider p1 = M . (n + 1) as Element of D * by FINSEQ_2:11;
let x be Element of D * ; ::_thesis: ex y being Element of D * st S1[n,x,y]
set y = x ^ p1;
reconsider y = x ^ p1 as Element of D * by FINSEQ_1:def_11;
take y ; ::_thesis: S1[n,x,y]
take p1 ; ::_thesis: ex q1 being Element of D * st
( q1 = x & p1 = M . (n + 1) & y = q1 ^ p1 )
take x ; ::_thesis: ( x = x & p1 = M . (n + 1) & y = x ^ p1 )
thus ( x = x & p1 = M . (n + 1) & y = x ^ p1 ) ; ::_thesis: verum
end;
ex p being FinSequence of D * st
( len p = len M & ( p . 1 = M1 or len M = 0 ) & ( for n being Element of NAT st 1 <= n & n < len M holds
S1[n,p . n,p . (n + 1)] ) ) from RECDEF_1:sch_4(A2);
then consider p being FinSequence of D * such that
A5: len p = len M and
A6: ( p . 1 = M1 or len M = 0 ) and
A7: for n being Element of NAT st 1 <= n & n < len M holds
S1[n,p . n,p . (n + 1)] ;
reconsider z = p . (len M) as FinSequence of D ;
take z ; ::_thesis: ex p being FinSequence of D * st
( z = 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)) ) )
for n being Element of NAT st 1 <= n & n < len M holds
p . (n + 1) = (p . n) ^ (M . (n + 1))
proof
let n be Element of NAT ; ::_thesis: ( 1 <= n & n < len M implies p . (n + 1) = (p . n) ^ (M . (n + 1)) )
assume that
A8: 1 <= n and
A9: n < len M ; ::_thesis: p . (n + 1) = (p . n) ^ (M . (n + 1))
ex p1, q1 being Element of D * st
( q1 = p . n & p1 = M . (n + 1) & p . (n + 1) = q1 ^ p1 ) by A7, A8, A9;
hence p . (n + 1) = (p . n) ^ (M . (n + 1)) ; ::_thesis: verum
end;
hence ex p being FinSequence of D * st
( z = 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)) ) ) by A1, A5, A6; ::_thesis: verum
end;
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 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
( b2 = 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 b1 = b2 ) )
proof
let z1, z2 be FinSequence of D; ::_thesis: ( ( len M = 0 & z1 = {} & z2 = {} implies z1 = z2 ) & ( not len M = 0 & ex p being FinSequence of D * st
( z1 = 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
( z2 = 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 z1 = z2 ) )
thus ( len M = 0 & z1 = {} & z2 = {} implies z1 = z2 ) ; ::_thesis: ( not len M = 0 & ex p being FinSequence of D * st
( z1 = 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
( z2 = 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 z1 = z2 )
assume len M <> 0 ; ::_thesis: ( for p being FinSequence of D * holds
( not z1 = p . (len M) or not len p = len M or not p . 1 = M . 1 or ex k being Element of NAT st
( k >= 1 & k < len M & not p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) or for p being FinSequence of D * holds
( not z2 = p . (len M) or not len p = len M or not p . 1 = M . 1 or ex k being Element of NAT st
( k >= 1 & k < len M & not p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) or z1 = z2 )
then A10: len M >= 1 by NAT_1:14;
given p1 being FinSequence of D * such that A11: z1 = p1 . (len M) and
len p1 = len M and
A12: p1 . 1 = M . 1 and
A13: for k being Element of NAT st k >= 1 & k < len M holds
p1 . (k + 1) = (p1 . k) ^ (M . (k + 1)) ; ::_thesis: ( for p being FinSequence of D * holds
( not z2 = p . (len M) or not len p = len M or not p . 1 = M . 1 or ex k being Element of NAT st
( k >= 1 & k < len M & not p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) or z1 = z2 )
given p2 being FinSequence of D * such that A14: z2 = p2 . (len M) and
len p2 = len M and
A15: p2 . 1 = M . 1 and
A16: for k being Element of NAT st k >= 1 & k < len M holds
p2 . (k + 1) = (p2 . k) ^ (M . (k + 1)) ; ::_thesis: z1 = z2
for k being Element of NAT st k >= 1 & k <= len M holds
p1 . k = p2 . k
proof
defpred S1[ Element of NAT ] means ( $1 >= 1 & $1 <= len M implies p1 . $1 = p2 . $1 );
A17: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A18: ( n >= 1 & n <= len M implies p1 . n = p2 . n ) ; ::_thesis: S1[n + 1]
assume that
n + 1 >= 1 and
A19: n + 1 <= len M ; ::_thesis: p1 . (n + 1) = p2 . (n + 1)
now__::_thesis:_p1_._(n_+_1)_=_p2_._(n_+_1)
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: p1 . (n + 1) = p2 . (n + 1)
hence p1 . (n + 1) = p2 . (n + 1) by A12, A15; ::_thesis: verum
end;
supposeA20: n <> 0 ; ::_thesis: p1 . (n + 1) = p2 . (n + 1)
A21: n < len M by A19, NAT_1:13;
hence p1 . (n + 1) = (p2 . n) ^ (M . (n + 1)) by A13, A18, A20, NAT_1:14
.= p2 . (n + 1) by A16, A20, A21, NAT_1:14 ;
::_thesis: verum
end;
end;
end;
hence p1 . (n + 1) = p2 . (n + 1) ; ::_thesis: verum
end;
A22: S1[ 0 ] ;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A22, A17); ::_thesis: verum
end;
hence z1 = z2 by A10, A11, A14; ::_thesis: verum
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 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
let D be non empty set ; ::_thesis: for M being Matrix of D holds len (Mx2FinS M) = (len M) * (width M)
let M be Matrix of D; ::_thesis: len (Mx2FinS M) = (len M) * (width M)
percases ( len M = 0 or len M > 0 ) ;
supposeA1: len M = 0 ; ::_thesis: len (Mx2FinS M) = (len M) * (width M)
then Mx2FinS M = {} by Def5;
hence len (Mx2FinS M) = (len M) * (width M) by A1; ::_thesis: verum
end;
supposeA2: len M > 0 ; ::_thesis: len (Mx2FinS M) = (len M) * (width M)
then consider p being FinSequence of D * such that
A3: Mx2FinS M = p . (len M) and
A4: len p = len M and
A5: p . 1 = M . 1 and
A6: for k being Element of NAT st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) by Def5;
len M in Seg (len M) by A2, FINSEQ_1:3;
then len M in dom p by A4, FINSEQ_1:def_3;
hence len (Mx2FinS M) = (len M) * (width M) by A3, A4, A5, A6, Th29; ::_thesis: verum
end;
end;
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
let D be non empty set ; ::_thesis: 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) )
let M be Matrix of D; ::_thesis: 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) )
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices M implies ( ((i - 1) * (width M)) + j in dom (Mx2FinS M) & M * (i,j) = (Mx2FinS M) . (((i - 1) * (width M)) + j) ) )
assume A1: [i,j] in Indices M ; ::_thesis: ( ((i - 1) * (width M)) + j in dom (Mx2FinS M) & M * (i,j) = (Mx2FinS M) . (((i - 1) * (width M)) + j) )
Seg (len M) <> {} by A1, MATRPROB:12;
then len M <> 0 ;
then ex p being FinSequence of D * st
( Mx2FinS M = 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)) ) ) by Def5;
hence ( ((i - 1) * (width M)) + j in dom (Mx2FinS M) & M * (i,j) = (Mx2FinS M) . (((i - 1) * (width M)) + j) ) by A1, Th36; ::_thesis: verum
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
let D be non empty set ; ::_thesis: 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)) )
let M be Matrix of D; ::_thesis: 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)) )
let k, l be Element of NAT ; ::_thesis: ( k in dom (Mx2FinS M) & l = k - 1 implies ( [((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)) ) )
assume that
A1: k in dom (Mx2FinS M) and
A2: l = k - 1 ; ::_thesis: ( [((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)) )
set jj = (l mod (width M)) + 1;
set ii = (l div (width M)) + 1;
A3: len (Mx2FinS M) = (len M) * (width M) by Th39;
k in Seg (len (Mx2FinS M)) by A1, FINSEQ_1:def_3;
then k <= len (Mx2FinS M) by FINSEQ_1:1;
then k < ((len M) * (width M)) + 1 by A3, NAT_1:13;
then A4: k - 1 < (((len M) * (width M)) + 1) - 1 by XREAL_1:9;
A5: Mx2FinS M <> {} by A1;
then A6: width M <> 0 by A3;
A7: width M > 0 by A5, A3;
then A8: l = ((l div (width M)) * (width M)) + (l mod (width M)) by NAT_D:2;
width M divides (len M) * (width M) by NAT_D:def_3;
then l div (width M) < ((len M) * (width M)) div (width M) by A2, A6, A4, Th1;
then l div (width M) < len M by A6, NAT_D:18;
then A9: (l div (width M)) + 1 <= len M by NAT_1:13;
l mod (width M) < width M by A7, NAT_D:1;
then A10: (l mod (width M)) + 1 <= width M by NAT_1:13;
(l mod (width M)) + 1 >= 1 by NAT_1:11;
then A11: (l mod (width M)) + 1 in Seg (width M) by A10, FINSEQ_1:1;
(l div (width M)) + 1 >= 1 by NAT_1:11;
then (l div (width M)) + 1 in Seg (len M) by A9, FINSEQ_1:1;
hence [((l div (width M)) + 1),((l mod (width M)) + 1)] in Indices M by A11, MATRPROB:12; ::_thesis: (Mx2FinS M) . k = M * (((l div (width M)) + 1),((l mod (width M)) + 1))
then M * (((l div (width M)) + 1),((l mod (width M)) + 1)) = (Mx2FinS M) . (((((l div (width M)) + 1) - 1) * (width M)) + ((l mod (width M)) + 1)) by Th40
.= (Mx2FinS M) . k by A2, A8 ;
hence (Mx2FinS M) . k = M * (((l div (width M)) + 1),((l mod (width M)) + 1)) ; ::_thesis: verum
end;
theorem Th42: :: ENTROPY1:42
for MR being Matrix of REAL holds SumAll MR = Sum (Mx2FinS MR)
proof
let MR be Matrix of REAL; ::_thesis: SumAll MR = Sum (Mx2FinS MR)
percases ( len MR = 0 or len MR > 0 ) ;
supposeA1: len MR = 0 ; ::_thesis: SumAll MR = Sum (Mx2FinS MR)
hence Sum (Mx2FinS MR) = 0 by Def5, RVSUM_1:72
.= SumAll MR by A1, MATRPROB:23 ;
::_thesis: verum
end;
suppose len MR > 0 ; ::_thesis: SumAll MR = Sum (Mx2FinS MR)
then ex p being FinSequence of REAL * st
( Mx2FinS MR = p . (len MR) & len p = len MR & p . 1 = MR . 1 & ( for k being Element of NAT st k >= 1 & k < len MR holds
p . (k + 1) = (p . k) ^ (MR . (k + 1)) ) ) by Def5;
hence SumAll MR = Sum (Mx2FinS MR) by Th38; ::_thesis: verum
end;
end;
end;
theorem Th43: :: ENTROPY1:43
for MR being Matrix of REAL holds
( MR is m-nonnegative iff Mx2FinS MR is nonnegative )
proof
let MR be Matrix of REAL; ::_thesis: ( MR is m-nonnegative iff Mx2FinS MR is nonnegative )
hereby ::_thesis: ( Mx2FinS MR is nonnegative implies MR is m-nonnegative )
assume A1: MR is m-nonnegative ; ::_thesis: Mx2FinS MR is nonnegative
for k being Element of NAT st k in dom (Mx2FinS MR) holds
(Mx2FinS MR) . k >= 0
proof
let i be Element of NAT ; ::_thesis: ( i in dom (Mx2FinS MR) implies (Mx2FinS MR) . i >= 0 )
assume A2: i in dom (Mx2FinS MR) ; ::_thesis: (Mx2FinS MR) . i >= 0
i in Seg (len (Mx2FinS MR)) by A2, FINSEQ_1:def_3;
then i >= 1 by FINSEQ_1:1;
then reconsider l = i - 1 as Element of NAT by NAT_1:21;
A3: (Mx2FinS MR) . i = MR * (((l div (width MR)) + 1),((l mod (width MR)) + 1)) by A2, Th41;
[((l div (width MR)) + 1),((l mod (width MR)) + 1)] in Indices MR by A2, Th41;
hence (Mx2FinS MR) . i >= 0 by A1, A3, MATRPROB:def_6; ::_thesis: verum
end;
hence Mx2FinS MR is nonnegative by Def1; ::_thesis: verum
end;
assume A4: Mx2FinS MR is nonnegative ; ::_thesis: MR is m-nonnegative
now__::_thesis:_for_i,_j_being_Element_of_NAT_st_[i,j]_in_Indices_MR_holds_
MR_*_(i,j)_>=_0
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices MR implies MR * (i,j) >= 0 )
assume A5: [i,j] in Indices MR ; ::_thesis: MR * (i,j) >= 0
A6: MR * (i,j) = (Mx2FinS MR) . (((i - 1) * (width MR)) + j) by A5, Th40;
((i - 1) * (width MR)) + j in dom (Mx2FinS MR) by A5, Th40;
hence MR * (i,j) >= 0 by A4, A6, Def1; ::_thesis: verum
end;
hence MR is m-nonnegative by MATRPROB:def_6; ::_thesis: verum
end;
theorem Th44: :: ENTROPY1:44
for MR being Matrix of REAL holds
( MR is Joint_Probability iff Mx2FinS MR is ProbFinS )
proof
let MR be Matrix of REAL; ::_thesis: ( MR is Joint_Probability iff Mx2FinS MR is ProbFinS )
hereby ::_thesis: ( Mx2FinS MR is ProbFinS implies MR is Joint_Probability )
assume MR is Joint_Probability ; ::_thesis: Mx2FinS MR is ProbFinS
then reconsider MRR = MR as Joint_Probability Matrix of REAL ;
A1: MRR is m-nonnegative with_sum=1 Matrix of REAL ;
then Mx2FinS MR is nonnegative by Th43;
then A2: for i being Element of NAT st i in dom (Mx2FinS MR) holds
(Mx2FinS MR) . i >= 0 by Def1;
Sum (Mx2FinS MR) = SumAll MR by Th42
.= 1 by A1, MATRPROB:def_7 ;
hence Mx2FinS MR is ProbFinS by A2, MATRPROB:def_5; ::_thesis: verum
end;
assume Mx2FinS MR is ProbFinS ; ::_thesis: MR is Joint_Probability
then reconsider pp = Mx2FinS MR as ProbFinS FinSequence of REAL ;
reconsider p = pp as non empty ProbFinS FinSequence of REAL ;
SumAll MR = Sum p by Th42
.= 1 by MATRPROB:def_5 ;
then A3: MR is with_sum=1 by MATRPROB:def_7;
p is nonnegative ;
then MR is m-nonnegative by Th43;
hence MR is Joint_Probability by A3; ::_thesis: verum
end;
theorem Th45: :: ENTROPY1:45
for p, q being ProbFinS FinSequence of REAL holds Mx2FinS ((ColVec2Mx p) * (LineVec2Mx q)) is ProbFinS
proof
let p, q be ProbFinS FinSequence of REAL ; ::_thesis: Mx2FinS ((ColVec2Mx p) * (LineVec2Mx q)) is ProbFinS
(ColVec2Mx p) * (LineVec2Mx q) is Joint_Probability Matrix of REAL by Th23;
hence Mx2FinS ((ColVec2Mx p) * (LineVec2Mx q)) is ProbFinS by Th44; ::_thesis: verum
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
let p be non empty ProbFinS FinSequence of REAL ; ::_thesis: for M being non empty-yielding Conditional_Probability Matrix of REAL st len p = len M holds
Mx2FinS ((Vec2DiagMx p) * M) is ProbFinS
let M be non empty-yielding Conditional_Probability Matrix of REAL; ::_thesis: ( len p = len M implies Mx2FinS ((Vec2DiagMx p) * M) is ProbFinS )
assume len p = len M ; ::_thesis: Mx2FinS ((Vec2DiagMx p) * M) is ProbFinS
then (Vec2DiagMx p) * M is Joint_Probability Matrix of REAL by Th28;
hence Mx2FinS ((Vec2DiagMx p) * M) is ProbFinS by Th44; ::_thesis: verum
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 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
defpred S1[ Nat, set ] means ( ( p . $1 > 0 implies $2 = log (a,(p . $1)) ) & ( p . $1 = 0 implies $2 = 0 ) );
A2: for k being Nat st k in Seg (len p) holds
ex x being Element of REAL st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len p) implies ex x being Element of REAL st S1[k,x] )
assume k in Seg (len p) ; ::_thesis: ex x being Element of REAL st S1[k,x]
then A3: k in dom p by FINSEQ_1:def_3;
percases ( p . k > 0 or p . k = 0 ) by A1, A3, Def1;
supposeA4: p . k > 0 ; ::_thesis: ex x being Element of REAL st S1[k,x]
take log (a,(p . k)) ; ::_thesis: S1[k, log (a,(p . k))]
thus S1[k, log (a,(p . k))] by A4; ::_thesis: verum
end;
supposeA5: p . k = 0 ; ::_thesis: ex x being Element of REAL st S1[k,x]
take 0 ; ::_thesis: S1[k, 0 ]
thus S1[k, 0 ] by A5; ::_thesis: verum
end;
end;
end;
consider pp being FinSequence of REAL such that
A6: ( dom pp = Seg (len p) & ( for k being Nat st k in Seg (len p) holds
S1[k,pp . k] ) ) from FINSEQ_1:sch_5(A2);
len pp = len p by A6, FINSEQ_1:def_3;
hence 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 ) ) ) ) by A6; ::_thesis: verum
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
let p1, p2 be FinSequence of REAL ; ::_thesis: ( len p1 = len p & ( for k being Nat st k in dom p1 holds
( ( p . k > 0 implies p1 . k = log (a,(p . k)) ) & ( p . k = 0 implies p1 . k = 0 ) ) ) & len p2 = len p & ( for k being Nat st k in dom p2 holds
( ( p . k > 0 implies p2 . k = log (a,(p . k)) ) & ( p . k = 0 implies p2 . k = 0 ) ) ) implies p1 = p2 )
assume that
A7: len p1 = len p and
A8: for k being Nat st k in dom p1 holds
( ( p . k > 0 implies p1 . k = log (a,(p . k)) ) & ( p . k = 0 implies p1 . k = 0 ) ) and
A9: len p2 = len p and
A10: for k being Nat st k in dom p2 holds
( ( p . k > 0 implies p2 . k = log (a,(p . k)) ) & ( p . k = 0 implies p2 . k = 0 ) ) ; ::_thesis: p1 = p2
A11: for k being Nat st k in dom p1 holds
p1 . k = p2 . k
proof
let k be Nat; ::_thesis: ( k in dom p1 implies p1 . k = p2 . k )
assume A12: k in dom p1 ; ::_thesis: p1 . k = p2 . k
then A13: k in dom p by A7, FINSEQ_3:29;
A14: k in dom p2 by A7, A9, A12, FINSEQ_3:29;
percases ( p . k > 0 or p . k = 0 ) by A1, A13, Def1;
supposeA15: p . k > 0 ; ::_thesis: p1 . k = p2 . k
hence p1 . k = log (a,(p . k)) by A8, A12
.= p2 . k by A10, A14, A15 ;
::_thesis: verum
end;
supposeA16: p . k = 0 ; ::_thesis: p1 . k = p2 . k
hence p1 . k = 0 by A8, A12
.= p2 . k by A10, A14, A16 ;
::_thesis: verum
end;
end;
end;
dom p1 = Seg (len p2) by A7, A9, FINSEQ_1:def_3
.= dom p2 by FINSEQ_1:def_3 ;
hence p1 = p2 by A11, FINSEQ_1:13; ::_thesis: verum
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 Element of NAT st k in dom q holds
q . k = (p . k) * (log (2,(p . k))) ) ) )
proof
let p be nonnegative FinSequence of REAL ; ::_thesis: 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))) ) ) )
let q be FinSequence of REAL ; ::_thesis: ( 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))) ) ) )
set pp = mlt (p,(FinSeq_log (2,p)));
A1: len p = len (FinSeq_log (2,p)) by Def6;
then A2: len (mlt (p,(FinSeq_log (2,p)))) = len p by MATRPROB:30;
hereby ::_thesis: ( len q = len p & ( for k being Element of NAT st k in dom q holds
q . k = (p . k) * (log (2,(p . k))) ) implies q = Infor_FinSeq_of p )
assume A3: q = Infor_FinSeq_of p ; ::_thesis: ( len q = len p & ( for k being Element of NAT st k in dom q holds
q . k = (p . k) * (log (2,(p . k))) ) )
thus ( len q = len p & ( for k being Element of NAT st k in dom q holds
q . k = (p . k) * (log (2,(p . k))) ) ) ::_thesis: verum
proof
A4: dom p = dom q by A2, A3, FINSEQ_3:29;
thus len q = len p by A1, A3, MATRPROB:30; ::_thesis: for k being Element of NAT st k in dom q holds
q . k = (p . k) * (log (2,(p . k)))
let k be Element of NAT ; ::_thesis: ( k in dom q implies q . k = (p . k) * (log (2,(p . k))) )
assume A5: k in dom q ; ::_thesis: q . k = (p . k) * (log (2,(p . k)))
A6: q . k = (p . k) * ((FinSeq_log (2,p)) . k) by A3, RVSUM_1:59;
A7: k in dom (FinSeq_log (2,p)) by A1, A2, A3, A5, FINSEQ_3:29;
percases ( p . k = 0 or p . k > 0 ) by A5, A4, Def1;
suppose p . k = 0 ; ::_thesis: q . k = (p . k) * (log (2,(p . k)))
hence q . k = (p . k) * (log (2,(p . k))) by A6; ::_thesis: verum
end;
suppose p . k > 0 ; ::_thesis: q . k = (p . k) * (log (2,(p . k)))
hence q . k = (p . k) * (log (2,(p . k))) by A6, A7, Def6; ::_thesis: verum
end;
end;
end;
end;
assume that
A8: len q = len p and
A9: for k being Element of NAT st k in dom q holds
q . k = (p . k) * (log (2,(p . k))) ; ::_thesis: q = Infor_FinSeq_of p
A10: dom q = dom p by A8, FINSEQ_3:29;
len q = len (mlt (p,(FinSeq_log (2,p)))) by A1, A8, MATRPROB:30;
then A11: dom q = dom (mlt (p,(FinSeq_log (2,p)))) by FINSEQ_3:29;
A12: dom p = dom (FinSeq_log (2,p)) by A1, FINSEQ_3:29;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_q_holds_
q_._k_=_(mlt_(p,(FinSeq_log_(2,p))))_._k
let k be Nat; ::_thesis: ( k in dom q implies q . b1 = (mlt (p,(FinSeq_log (2,p)))) . b1 )
assume A13: k in dom q ; ::_thesis: q . b1 = (mlt (p,(FinSeq_log (2,p)))) . b1
A14: (mlt (p,(FinSeq_log (2,p)))) . k = (p . k) * ((FinSeq_log (2,p)) . k) by RVSUM_1:59;
percases ( p . k = 0 or p . k > 0 ) by A10, A13, Def1;
supposeA15: p . k = 0 ; ::_thesis: q . b1 = (mlt (p,(FinSeq_log (2,p)))) . b1
hence q . k = 0 * (log (2,(p . k))) by A9, A13
.= (mlt (p,(FinSeq_log (2,p)))) . k by A14, A15 ;
::_thesis: verum
end;
suppose p . k > 0 ; ::_thesis: (mlt (p,(FinSeq_log (2,p)))) . b1 = q . b1
then (FinSeq_log (2,p)) . k = log (2,(p . k)) by A12, A10, A13, Def6;
hence (mlt (p,(FinSeq_log (2,p)))) . k = (p . k) * (log (2,(p . k))) by RVSUM_1:59
.= q . k by A9, A13 ;
::_thesis: verum
end;
end;
end;
hence q = Infor_FinSeq_of p by A11, FINSEQ_1:13; ::_thesis: verum
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
let p be nonnegative FinSequence of REAL ; ::_thesis: 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))) ) )
A1: dom p = Seg (len p) by FINSEQ_1:def_3
.= Seg (len (Infor_FinSeq_of p)) by Th47
.= dom (Infor_FinSeq_of p) by FINSEQ_1:def_3 ;
let k be Element of NAT ; ::_thesis: ( k in dom p implies ( ( 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))) ) ) )
assume A2: k in dom p ; ::_thesis: ( ( 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))) ) )
hereby ::_thesis: ( p . k > 0 implies (Infor_FinSeq_of p) . k = (p . k) * (log (2,(p . k))) )
assume p . k = 0 ; ::_thesis: (Infor_FinSeq_of p) . k = 0
hence (Infor_FinSeq_of p) . k = 0 * (log (2,(p . k))) by A2, A1, Th47
.= 0 ;
::_thesis: verum
end;
thus ( p . k > 0 implies (Infor_FinSeq_of p) . k = (p . k) * (log (2,(p . k))) ) by A2, A1, Th47; ::_thesis: verum
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
let p be nonnegative FinSequence of REAL ; ::_thesis: 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)))) ) ) )
let q be FinSequence of REAL ; ::_thesis: ( 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)))) ) ) )
set p0 = Infor_FinSeq_of p;
hereby ::_thesis: ( 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)))) ) implies q = - (Infor_FinSeq_of p) )
assume A1: q = - (Infor_FinSeq_of p) ; ::_thesis: ( 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)))) ) )
then A2: dom q = dom (Infor_FinSeq_of p) by VALUED_1:8;
A3: Seg (len q) = dom q by FINSEQ_1:def_3
.= Seg (len (Infor_FinSeq_of p)) by A2, FINSEQ_1:def_3
.= Seg (len p) by Th47 ;
for k being Element of NAT st k in dom q holds
q . k = (p . k) * (log (2,(1 / (p . k))))
proof
let k be Element of NAT ; ::_thesis: ( k in dom q implies q . k = (p . k) * (log (2,(1 / (p . k)))) )
assume A4: k in dom q ; ::_thesis: q . k = (p . k) * (log (2,(1 / (p . k))))
k in Seg (len q) by A4, FINSEQ_1:def_3;
then A5: k in dom p by A3, FINSEQ_1:def_3;
A6: q . k = - ((Infor_FinSeq_of p) . k) by A1, RVSUM_1:17;
then A7: q . k = - ((p . k) * (log (2,(p . k)))) by A2, A4, Th47
.= (p . k) * (- (log (2,(p . k)))) ;
percases ( p . k = 0 or p . k > 0 ) by A5, Def1;
supposeA8: p . k = 0 ; ::_thesis: q . k = (p . k) * (log (2,(1 / (p . k))))
then (Infor_FinSeq_of p) . k = 0 by A5, Th48;
hence q . k = (p . k) * (log (2,(1 / (p . k)))) by A6, A8; ::_thesis: verum
end;
suppose p . k > 0 ; ::_thesis: q . k = (p . k) * (log (2,(1 / (p . k))))
hence q . k = (p . k) * (log (2,(1 / (p . k)))) by A7, Th5; ::_thesis: verum
end;
end;
end;
hence ( 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)))) ) ) by A3, FINSEQ_1:6; ::_thesis: verum
end;
assume that
A9: len q = len p and
A10: for k being Element of NAT st k in dom q holds
q . k = (p . k) * (log (2,(1 / (p . k)))) ; ::_thesis: q = - (Infor_FinSeq_of p)
A11: dom q = Seg (len q) by FINSEQ_1:def_3
.= Seg (len (Infor_FinSeq_of p)) by A9, Th47
.= dom (Infor_FinSeq_of p) by FINSEQ_1:def_3 ;
A12: for k being Nat st k in dom q holds
(- (Infor_FinSeq_of p)) . k = q . k
proof
let k be Nat; ::_thesis: ( k in dom q implies (- (Infor_FinSeq_of p)) . k = q . k )
assume A13: k in dom q ; ::_thesis: (- (Infor_FinSeq_of p)) . k = q . k
then k in Seg (len p) by A9, FINSEQ_1:def_3;
then A14: k in dom p by FINSEQ_1:def_3;
percases ( p . k = 0 or p . k > 0 ) by A14, Def1;
supposeA15: p . k = 0 ; ::_thesis: (- (Infor_FinSeq_of p)) . k = q . k
thus (- (Infor_FinSeq_of p)) . k = - ((Infor_FinSeq_of p) . k) by RVSUM_1:17
.= - 0 by A14, A15, Th48
.= (p . k) * (log (2,(1 / (p . k)))) by A15
.= q . k by A10, A13 ; ::_thesis: verum
end;
supposeA16: p . k > 0 ; ::_thesis: (- (Infor_FinSeq_of p)) . k = q . k
thus (- (Infor_FinSeq_of p)) . k = - ((Infor_FinSeq_of p) . k) by RVSUM_1:17
.= - ((p . k) * (log (2,(p . k)))) by A11, A13, Th47
.= (p . k) * (- (log (2,(p . k))))
.= (p . k) * (log (2,(1 / (p . k)))) by A16, Th5
.= q . k by A10, A13 ; ::_thesis: verum
end;
end;
end;
dom q = dom (- (Infor_FinSeq_of p)) by A11, VALUED_1:8;
hence q = - (Infor_FinSeq_of p) by A12, FINSEQ_1:13; ::_thesis: verum
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
let r1, r2 be Real; ::_thesis: 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)))
let p be nonnegative FinSequence of REAL ; ::_thesis: ( r1 >= 0 & r2 >= 0 implies 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))) )
assume that
A1: r1 >= 0 and
A2: r2 >= 0 ; ::_thesis: 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)))
let i be Element of NAT ; ::_thesis: ( i in dom p & p . i = r1 * r2 implies (Infor_FinSeq_of p) . i = ((r1 * r2) * (log (2,r1))) + ((r1 * r2) * (log (2,r2))) )
assume that
A3: i in dom p and
A4: p . i = r1 * r2 ; ::_thesis: (Infor_FinSeq_of p) . i = ((r1 * r2) * (log (2,r1))) + ((r1 * r2) * (log (2,r2)))
len p = len (Infor_FinSeq_of p) by Th47;
then i in dom (Infor_FinSeq_of p) by A3, FINSEQ_3:29;
hence (Infor_FinSeq_of p) . i = (r1 * r2) * (log (2,(r1 * r2))) by A4, Th47
.= ((r1 * r2) * (log (2,r1))) + ((r1 * r2) * (log (2,r2))) by A1, A2, Th6 ;
::_thesis: verum
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
let r be Real; ::_thesis: 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)))))
let p be nonnegative FinSequence of REAL ; ::_thesis: ( r >= 0 implies Infor_FinSeq_of (r * p) = ((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p))))) )
assume A1: r >= 0 ; ::_thesis: Infor_FinSeq_of (r * p) = ((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p)))))
reconsider q = r * p as nonnegative FinSequence of REAL by A1, Th10;
set qq = Infor_FinSeq_of q;
A2: dom q = dom p by VALUED_1:def_5;
A3: dom ((r * (log (2,r))) * p) = dom p by VALUED_1:def_5;
A4: len (FinSeq_log (2,p)) = len p by Def6;
then len (mlt (p,(FinSeq_log (2,p)))) = len p by MATRPROB:30;
then dom (mlt (p,(FinSeq_log (2,p)))) = dom p by FINSEQ_3:29;
then dom (r * (mlt (p,(FinSeq_log (2,p))))) = dom p by VALUED_1:def_5;
then len ((r * (log (2,r))) * p) = len (r * (mlt (p,(FinSeq_log (2,p))))) by A3, FINSEQ_3:29;
then len (((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p)))))) = len ((r * (log (2,r))) * p) by INTEGRA5:2;
then A5: dom (((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p)))))) = dom ((r * (log (2,r))) * p) by FINSEQ_3:29;
len q = len (Infor_FinSeq_of q) by Th47;
then A6: dom q = dom (Infor_FinSeq_of q) by FINSEQ_3:29;
A7: dom (FinSeq_log (2,p)) = dom p by A4, FINSEQ_3:29;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_(Infor_FinSeq_of_q)_holds_
(Infor_FinSeq_of_q)_._k_=_(((r_*_(log_(2,r)))_*_p)_+_(r_*_(mlt_(p,(FinSeq_log_(2,p))))))_._k
let k be Nat; ::_thesis: ( k in dom (Infor_FinSeq_of q) implies (Infor_FinSeq_of q) . b1 = (((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p)))))) . b1 )
assume A8: k in dom (Infor_FinSeq_of q) ; ::_thesis: (Infor_FinSeq_of q) . b1 = (((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p)))))) . b1
A9: q . k = r * (p . k) by RVSUM_1:44;
p . k >= 0 by A2, A6, A8, Def1;
then A10: (Infor_FinSeq_of q) . k = ((r * (p . k)) * (log (2,r))) + ((r * (p . k)) * (log (2,(p . k)))) by A1, A6, A8, A9, Th50;
A11: ((r * (log (2,r))) * p) . k = (r * (log (2,r))) * (p . k) by RVSUM_1:44;
A12: (r * (mlt (p,(FinSeq_log (2,p))))) . k = r * ((mlt (p,(FinSeq_log (2,p)))) . k) by RVSUM_1:44
.= r * ((p . k) * ((FinSeq_log (2,p)) . k)) by RVSUM_1:59
.= (r * (p . k)) * ((FinSeq_log (2,p)) . k) ;
percases ( p . k > 0 or p . k = 0 ) by A2, A6, A8, Def1;
suppose p . k > 0 ; ::_thesis: (Infor_FinSeq_of q) . b1 = (((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p)))))) . b1
then (Infor_FinSeq_of q) . k = (((r * (log (2,r))) * p) . k) + ((r * (mlt (p,(FinSeq_log (2,p))))) . k) by A2, A6, A7, A8, A10, A11, A12, Def6;
hence (Infor_FinSeq_of q) . k = (((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p)))))) . k by A2, A6, A3, A5, A8, VALUED_1:def_1; ::_thesis: verum
end;
suppose p . k = 0 ; ::_thesis: (Infor_FinSeq_of q) . b1 = (((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p)))))) . b1
hence (Infor_FinSeq_of q) . k = (((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p)))))) . k by A2, A6, A3, A5, A8, A10, A11, A12, VALUED_1:def_1; ::_thesis: verum
end;
end;
end;
hence Infor_FinSeq_of (r * p) = ((r * (log (2,r))) * p) + (r * (mlt (p,(FinSeq_log (2,p))))) by A2, A6, A3, A5, FINSEQ_1:13; ::_thesis: verum
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
let p be non empty ProbFinS FinSequence of REAL ; ::_thesis: for k being Element of NAT st k in dom p holds
(Infor_FinSeq_of p) . k <= 0
let k be Element of NAT ; ::_thesis: ( k in dom p implies (Infor_FinSeq_of p) . k <= 0 )
assume A1: k in dom p ; ::_thesis: (Infor_FinSeq_of p) . k <= 0
percases ( p . k = 0 or ( p . k > 0 & p . k <= 1 ) ) by A1, MATRPROB:53, MATRPROB:def_5;
suppose p . k = 0 ; ::_thesis: (Infor_FinSeq_of p) . k <= 0
hence (Infor_FinSeq_of p) . k <= 0 by A1, Th48; ::_thesis: verum
end;
supposeA2: ( p . k > 0 & p . k <= 1 ) ; ::_thesis: (Infor_FinSeq_of p) . k <= 0
then A3: (Infor_FinSeq_of p) . k = (p . k) * (log (2,(p . k))) by A1, Th48;
thus (Infor_FinSeq_of p) . k <= 0 ::_thesis: verum
proof
A4: log (2,1) = 0 by POWER:51;
percases ( p . k < 1 or p . k = 1 ) by A2, XXREAL_0:1;
suppose p . k < 1 ; ::_thesis: (Infor_FinSeq_of p) . k <= 0
then log (2,(p . k)) < 0 by A2, A4, POWER:57;
hence (Infor_FinSeq_of p) . k <= 0 by A2, A3; ::_thesis: verum
end;
suppose p . k = 1 ; ::_thesis: (Infor_FinSeq_of p) . k <= 0
hence (Infor_FinSeq_of p) . k <= 0 by A3, POWER:51; ::_thesis: verum
end;
end;
end;
end;
end;
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 b1 being Matrix of REAL st
( len b1 = len MR & width b1 = width MR & ( for k being Element of NAT st k in dom b1 holds
b1 . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) )
proof
deffunc H1( Nat) -> FinSequence of REAL = mlt ((Line (MR,$1)),(FinSeq_log (2,(Line (MR,$1)))));
consider p being FinSequence such that
A2: len p = len MR and
A3: for k being Nat st k in dom p holds
p . k = H1(k) from FINSEQ_1:sch_2();
A4: rng p c= REAL *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in REAL * )
assume x in rng p ; ::_thesis: x in REAL *
then consider j being Nat such that
A5: j in dom p and
A6: x = p . j by FINSEQ_2:10;
p . j = mlt ((Line (MR,j)),(FinSeq_log (2,(Line (MR,j))))) by A3, A5;
hence x in REAL * by A6, FINSEQ_1:def_11; ::_thesis: verum
end;
A7: for x being set st x in rng p holds
ex q being FinSequence st
( q = x & len q = width MR )
proof
let x be set ; ::_thesis: ( x in rng p implies ex q being FinSequence st
( q = x & len q = width MR ) )
assume x in rng p ; ::_thesis: ex q being FinSequence st
( q = x & len q = width MR )
then consider j being Nat such that
A8: j in dom p and
A9: x = p . j by FINSEQ_2:10;
j in dom MR by A2, A8, FINSEQ_3:29;
then Line (MR,j) is nonnegative by A1, Th19;
then A10: len (FinSeq_log (2,(Line (MR,j)))) = len (Line (MR,j)) by Def6;
len (Line (MR,j)) = width MR by MATRIX_1:def_7;
then A11: len (mlt ((Line (MR,j)),(FinSeq_log (2,(Line (MR,j)))))) = width MR by A10, MATRPROB:30;
x = mlt ((Line (MR,j)),(FinSeq_log (2,(Line (MR,j))))) by A3, A8, A9;
hence ex q being FinSequence st
( q = x & len q = width MR ) by A11; ::_thesis: verum
end;
then reconsider p = p as Matrix of REAL by A4, FINSEQ_1:def_4, MATRIX_1:def_1;
take p ; ::_thesis: ( len p = len MR & width p = width MR & ( for k being Element of NAT st k in dom p holds
p . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) )
width p = width MR
proof
percases ( len MR = 0 or len MR > 0 ) ;
supposeA12: len MR = 0 ; ::_thesis: width p = width MR
then width p = 0 by A2, MATRIX_1:def_3;
hence width p = width MR by A12, MATRIX_1:def_3; ::_thesis: verum
end;
supposeA13: len MR > 0 ; ::_thesis: width p = width MR
then len p >= 1 by A2, NAT_1:14;
then 1 in Seg (len p) by FINSEQ_1:1;
then A14: 1 in dom p by FINSEQ_1:def_3;
then A15: p . 1 in rng p by FUNCT_1:3;
ex q being FinSequence st
( q = p . 1 & len q = width MR ) by A7, A14, FUNCT_1:3;
hence width p = width MR by A2, A13, A15, MATRIX_1:def_3; ::_thesis: verum
end;
end;
end;
hence ( len p = len MR & width p = width MR & ( for k being Element of NAT st k in dom p holds
p . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) ) by A2, A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Matrix of REAL st len b1 = len MR & width b1 = width MR & ( for k being Element of NAT st k in dom b1 holds
b1 . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) & len b2 = len MR & width b2 = width MR & ( for k being Element of NAT st k in dom b2 holds
b2 . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) holds
b1 = b2
proof
let M1, M2 be Matrix of REAL; ::_thesis: ( len M1 = len MR & width M1 = width MR & ( for k being Element of NAT st k in dom M1 holds
M1 . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) & len M2 = len MR & width M2 = width MR & ( for k being Element of NAT st k in dom M2 holds
M2 . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) implies M1 = M2 )
assume that
A16: len M1 = len MR and
width M1 = width MR and
A17: for k being Element of NAT st k in dom M1 holds
M1 . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) and
A18: len M2 = len MR and
width M2 = width MR and
A19: for k being Element of NAT st k in dom M2 holds
M2 . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ; ::_thesis: M1 = M2
A20: dom M1 = dom M2 by A16, A18, FINSEQ_3:29;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_M1_holds_
M1_._k_=_M2_._k
let k be Nat; ::_thesis: ( k in dom M1 implies M1 . k = M2 . k )
assume A21: k in dom M1 ; ::_thesis: M1 . k = M2 . k
thus M1 . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) by A17, A21
.= M2 . k by A19, A20, A21 ; ::_thesis: verum
end;
hence M1 = M2 by A20, FINSEQ_1:13; ::_thesis: verum
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 Element of 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 Element of NAT st k in dom M holds
Line ((Infor_FinSeq_of M),k) = Infor_FinSeq_of (Line (M,k))
proof
let M be m-nonnegative Matrix of REAL; ::_thesis: for k being Element of NAT st k in dom M holds
Line ((Infor_FinSeq_of M),k) = Infor_FinSeq_of (Line (M,k))
set M1 = Infor_FinSeq_of M;
len (Infor_FinSeq_of M) = len M by Def8;
then A1: dom (Infor_FinSeq_of M) = dom M by FINSEQ_3:29;
let k be Element of NAT ; ::_thesis: ( k in dom M implies Line ((Infor_FinSeq_of M),k) = Infor_FinSeq_of (Line (M,k)) )
assume A2: k in dom M ; ::_thesis: Line ((Infor_FinSeq_of M),k) = Infor_FinSeq_of (Line (M,k))
thus Line ((Infor_FinSeq_of M),k) = (Infor_FinSeq_of M) . k by A2, A1, MATRIX_2:16
.= Infor_FinSeq_of (Line (M,k)) by A2, A1, Def8 ; ::_thesis: verum
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
let M be m-nonnegative Matrix of REAL; ::_thesis: 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)))) ) ) )
let M1 be Matrix of REAL; ::_thesis: ( 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)))) ) ) )
hereby ::_thesis: ( 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)))) ) implies M1 = Infor_FinSeq_of M )
assume A1: M1 = Infor_FinSeq_of M ; ::_thesis: ( 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)))) ) )
then A2: width M1 = width M by Def8;
A3: len M1 = len M by A1, Def8;
now__::_thesis:_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))))
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = (M * (i,j)) * (log (2,(M * (i,j)))) )
assume A4: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = (M * (i,j)) * (log (2,(M * (i,j))))
A5: j in Seg (width M1) by A4, MATRPROB:12;
i in Seg (len M1) by A4, MATRPROB:12;
then A6: i in dom M by A3, FINSEQ_1:def_3;
then reconsider p = Line (M,i) as nonnegative FinSequence of REAL by Th19;
A7: len p = width M by MATRIX_1:def_7;
len p = len (Infor_FinSeq_of p) by Th47;
then A8: j in dom (Infor_FinSeq_of p) by A2, A5, A7, FINSEQ_1:def_3;
A9: p . j = M * (i,j) by A2, A5, MATRIX_1:def_7;
thus M1 * (i,j) = (Line (M1,i)) . j by A5, MATRIX_1:def_7
.= (Infor_FinSeq_of p) . j by A1, A6, Th53
.= (M * (i,j)) * (log (2,(M * (i,j)))) by A9, A8, Th47 ; ::_thesis: verum
end;
hence ( 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)))) ) ) by A1, Def8; ::_thesis: verum
end;
assume that
A10: len M1 = len M and
A11: width M1 = width M and
A12: 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)))) ; ::_thesis: M1 = Infor_FinSeq_of M
A13: dom M1 = dom M by A10, FINSEQ_3:29;
for k being Element of NAT st k in dom M1 holds
M1 . k = mlt ((Line (M,k)),(FinSeq_log (2,(Line (M,k)))))
proof
let k be Element of NAT ; ::_thesis: ( k in dom M1 implies M1 . k = mlt ((Line (M,k)),(FinSeq_log (2,(Line (M,k))))) )
assume A14: k in dom M1 ; ::_thesis: M1 . k = mlt ((Line (M,k)),(FinSeq_log (2,(Line (M,k)))))
A15: len (M1 . k) = width M1 by A14, MATRIX_1:42;
reconsider p = Line (M,k) as nonnegative FinSequence of REAL by A13, A14, Th19;
A16: len p = width M by MATRIX_1:def_7;
A17: len (FinSeq_log (2,p)) = len p by Def6;
then len (mlt (p,(FinSeq_log (2,p)))) = len p by MATRPROB:30;
then A18: dom (M1 . k) = dom (mlt (p,(FinSeq_log (2,p)))) by A11, A16, A15, FINSEQ_3:29;
A19: k in Seg (len M) by A10, A14, FINSEQ_1:def_3;
now__::_thesis:_for_j_being_Nat_st_j_in_dom_(M1_._k)_holds_
(M1_._k)_._j_=_(mlt_(p,(FinSeq_log_(2,p))))_._j
let j be Nat; ::_thesis: ( j in dom (M1 . k) implies (M1 . k) . b1 = (mlt (p,(FinSeq_log (2,p)))) . b1 )
assume A20: j in dom (M1 . k) ; ::_thesis: (M1 . k) . b1 = (mlt (p,(FinSeq_log (2,p)))) . b1
A21: j in Seg (width M) by A11, A15, A20, FINSEQ_1:def_3;
then A22: p . j = M * (k,j) by MATRIX_1:def_7;
A23: [k,j] in Indices M by A19, A21, MATRPROB:12;
A24: (mlt (p,(FinSeq_log (2,p)))) . j = (p . j) * ((FinSeq_log (2,p)) . j) by RVSUM_1:59
.= (M * (k,j)) * ((FinSeq_log (2,p)) . j) by A21, MATRIX_1:def_7 ;
A25: j in dom (FinSeq_log (2,p)) by A16, A17, A21, FINSEQ_1:def_3;
A26: j in NAT by ORDINAL1:def_12;
A27: [k,j] in Indices M1 by A14, A20, MATRPROB:13;
then A28: (M1 . k) . j = M1 * (k,j) by A26, MATRPROB:14
.= (M * (k,j)) * (log (2,(M * (k,j)))) by A12, A26, A27 ;
percases ( M * (k,j) = 0 or M * (k,j) > 0 ) by A26, A23, MATRPROB:def_6;
suppose M * (k,j) = 0 ; ::_thesis: (M1 . k) . b1 = (mlt (p,(FinSeq_log (2,p)))) . b1
hence (M1 . k) . j = (mlt (p,(FinSeq_log (2,p)))) . j by A28, A24; ::_thesis: verum
end;
suppose M * (k,j) > 0 ; ::_thesis: (mlt (p,(FinSeq_log (2,p)))) . b1 = (M1 . k) . b1
hence (mlt (p,(FinSeq_log (2,p)))) . j = (M1 . k) . j by A25, A28, A22, A24, Def6; ::_thesis: verum
end;
end;
end;
hence M1 . k = mlt ((Line (M,k)),(FinSeq_log (2,(Line (M,k))))) by A18, FINSEQ_1:13; ::_thesis: verum
end;
hence M1 = Infor_FinSeq_of M by A10, A11, Def8; ::_thesis: verum
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
let p be non empty ProbFinS FinSequence of REAL ; ::_thesis: Entropy p >= 0
set p1 = - (Infor_FinSeq_of p);
A1: dom p = Seg (len p) by FINSEQ_1:def_3
.= Seg (len (Infor_FinSeq_of p)) by Th47
.= dom (Infor_FinSeq_of p) by FINSEQ_1:def_3 ;
A2: for k being Nat st k in dom (- (Infor_FinSeq_of p)) holds
(- (Infor_FinSeq_of p)) . k >= 0
proof
let k be Nat; ::_thesis: ( k in dom (- (Infor_FinSeq_of p)) implies (- (Infor_FinSeq_of p)) . k >= 0 )
assume k in dom (- (Infor_FinSeq_of p)) ; ::_thesis: (- (Infor_FinSeq_of p)) . k >= 0
then k in dom p by A1, VALUED_1:8;
then (Infor_FinSeq_of p) . k <= 0 by Th52;
then - ((Infor_FinSeq_of p) . k) >= - 0 ;
hence (- (Infor_FinSeq_of p)) . k >= 0 by RVSUM_1:17; ::_thesis: verum
end;
Entropy p = Sum (- (Infor_FinSeq_of p)) by RVSUM_1:88;
hence Entropy p >= 0 by A2, RVSUM_1:84; ::_thesis: verum
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
let p be non empty ProbFinS FinSequence of REAL ; ::_thesis: ( ex k being Element of NAT st
( k in dom p & p . k = 1 ) implies Entropy p = 0 )
assume ex k being Element of NAT st
( k in dom p & p . k = 1 ) ; ::_thesis: Entropy p = 0
then consider k1 being Element of NAT such that
A1: k1 in dom p and
A2: p . k1 = 1 ;
set q = Infor_FinSeq_of p;
len (Infor_FinSeq_of p) = len p by Th47;
then A3: dom (Infor_FinSeq_of p) = dom p by FINSEQ_3:29;
A4: p has_onlyone_value_in k1 by A1, A2, Th15;
for k being Element of NAT st k in dom (Infor_FinSeq_of p) holds
(Infor_FinSeq_of p) . k = 0
proof
let k be Element of NAT ; ::_thesis: ( k in dom (Infor_FinSeq_of p) implies (Infor_FinSeq_of p) . k = 0 )
assume A5: k in dom (Infor_FinSeq_of p) ; ::_thesis: (Infor_FinSeq_of p) . k = 0
percases ( k = k1 or k <> k1 ) ;
suppose k = k1 ; ::_thesis: (Infor_FinSeq_of p) . k = 0
hence (Infor_FinSeq_of p) . k = 1 * (log (2,1)) by A2, A5, Th47
.= 0 by POWER:51 ;
::_thesis: verum
end;
suppose k <> k1 ; ::_thesis: (Infor_FinSeq_of p) . k = 0
then A6: p . k = 0 by A4, A3, A5, Def2;
thus (Infor_FinSeq_of p) . k = (p . k) * (log (2,(p . k))) by A5, Th47
.= 0 by A6 ; ::_thesis: verum
end;
end;
end;
then for x being set st x in dom (Infor_FinSeq_of p) holds
(Infor_FinSeq_of p) . x = 0 ;
then Infor_FinSeq_of p = (dom (Infor_FinSeq_of p)) --> 0 by FUNCOP_1:11;
then Infor_FinSeq_of p = (len (Infor_FinSeq_of p)) |-> 0 by FINSEQ_1:def_3;
then Sum (Infor_FinSeq_of p) = 0 by RVSUM_1:81;
hence Entropy p = 0 ; ::_thesis: verum
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
let p, q be non empty ProbFinS FinSequence of REAL ; ::_thesis: 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 ) ) )
let pp, qq be FinSequence of REAL ; ::_thesis: ( 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)))) ) ) implies ( 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 ) ) ) )
assume that
A1: len p = len q and
A2: len pp = len p and
A3: len qq = len q and
A4: 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)))) ) ; ::_thesis: ( 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 ) ) )
set p1 = pp - qq;
A5: number_e <> 1 by TAYLOR_1:11;
A6: len (pp - qq) = len p by A1, A2, A3, RVSUM_1:116;
then A7: dom (pp - qq) = dom pp by A2, FINSEQ_3:29;
then for k being Element of NAT st k in dom pp holds
(pp - qq) . k = (pp . k) - (qq . k) by VALUED_1:13;
then A8: (Sum pp) - (Sum qq) = Sum (pp - qq) by A1, A2, A3, A6, Th8;
A9: dom pp = Seg (len pp) by FINSEQ_1:def_3
.= dom p by A2, FINSEQ_1:def_3 ;
A10: for k being Element of NAT st k in dom p holds
(pp - qq) . k = ((p . k) * (log (2,number_e))) * (log (number_e,((q . k) / (p . k))))
proof
let k be Element of NAT ; ::_thesis: ( k in dom p implies (pp - qq) . k = ((p . k) * (log (2,number_e))) * (log (number_e,((q . k) / (p . k)))) )
assume A11: k in dom p ; ::_thesis: (pp - qq) . k = ((p . k) * (log (2,number_e))) * (log (number_e,((q . k) / (p . k))))
A12: pp . k = - ((p . k) * (log (2,(p . k)))) by A4, A11;
A13: qq . k = - ((p . k) * (log (2,(q . k)))) by A4, A11;
A14: p . k > 0 by A4, A11;
then A15: - (log (2,(p . k))) = log (2,(1 / (p . k))) by Th5;
A16: q . k > 0 by A4, A11;
then (q . k) / (p . k) > 0 by A14, XREAL_1:139;
then A17: log (2,((q . k) / (p . k))) = (log (2,number_e)) * (log (number_e,((q . k) / (p . k)))) by A5, POWER:56, TAYLOR_1:11;
thus (pp - qq) . k = (pp . k) - (qq . k) by A7, A9, A11, VALUED_1:13
.= (p . k) * ((log (2,(1 / (p . k)))) + (log (2,(q . k)))) by A12, A13, A15
.= (p . k) * (log (2,((1 / (p . k)) * (q . k)))) by A14, A16, POWER:53
.= ((p . k) * (log (2,number_e))) * (log (number_e,((q . k) / (p . k)))) by A17 ; ::_thesis: verum
end;
set n = len p;
deffunc H1( Nat) -> Element of REAL = ((p . $1) * (log (2,number_e))) * (((q . $1) / (p . $1)) - 1);
consider p2 being FinSequence of REAL such that
A18: len p2 = len p and
A19: for k being Nat st k in dom p2 holds
p2 . k = H1(k) from FINSEQ_2:sch_1();
A20: dom p2 = Seg (len p2) by FINSEQ_1:def_3
.= dom p by A18, FINSEQ_1:def_3 ;
A21: len (pp - qq) = len p by A1, A2, A3, RVSUM_1:116;
then A22: pp - qq is Element of (len p) -tuples_on REAL by FINSEQ_2:92;
A23: dom p2 = Seg (len p) by A18, FINSEQ_1:def_3;
A24: len (q - p) = len q by A1, RVSUM_1:116;
A25: for k being Element of NAT st k in dom q holds
(q - p) . k = (q . k) - (p . k)
proof
let k be Element of NAT ; ::_thesis: ( k in dom q implies (q - p) . k = (q . k) - (p . k) )
assume k in dom q ; ::_thesis: (q - p) . k = (q . k) - (p . k)
then k in dom (q - p) by A24, FINSEQ_3:29;
hence (q - p) . k = (q . k) - (p . k) by VALUED_1:13; ::_thesis: verum
end;
A26: dom p = Seg (len p) by FINSEQ_1:def_3;
A27: dom (q - p) = dom p2 by A1, A18, A24, FINSEQ_3:29;
A28: for k being Nat st k in dom p2 holds
p2 . k = ((log (2,number_e)) * (q - p)) . k
proof
let k be Nat; ::_thesis: ( k in dom p2 implies p2 . k = ((log (2,number_e)) * (q - p)) . k )
assume A29: k in dom p2 ; ::_thesis: p2 . k = ((log (2,number_e)) * (q - p)) . k
A30: p . k > 0 by A4, A20, A29;
thus p2 . k = ((log (2,number_e)) * (p . k)) * (((q . k) / (p . k)) - 1) by A19, A29
.= (log (2,number_e)) * ((((p . k) / (p . k)) * (q . k)) - (p . k))
.= (log (2,number_e)) * ((1 * (q . k)) - (p . k)) by A30, XCMPLX_1:60
.= (log (2,number_e)) * ((q - p) . k) by A27, A29, VALUED_1:13
.= ((log (2,number_e)) * (q - p)) . k by RVSUM_1:44 ; ::_thesis: verum
end;
dom p2 = dom ((log (2,number_e)) * (q - p)) by A27, VALUED_1:def_5;
then A31: Sum p2 = Sum ((log (2,number_e)) * (q - p)) by A28, FINSEQ_1:13
.= (log (2,number_e)) * (Sum (q - p)) by RVSUM_1:87
.= (log (2,number_e)) * ((Sum q) - (Sum p)) by A1, A24, A25, Th8
.= (log (2,number_e)) * (1 - (Sum p)) by MATRPROB:def_5
.= (log (2,number_e)) * (1 - 1) by MATRPROB:def_5
.= 0 ;
number_e - 0 > 2 - 1 by TAYLOR_1:11, XREAL_1:15;
then A32: log (2,number_e) > 0 by Th4;
A33: for k being Nat st k in Seg (len p) holds
(pp - qq) . k <= p2 . k
proof
let k be Nat; ::_thesis: ( k in Seg (len p) implies (pp - qq) . k <= p2 . k )
assume A34: k in Seg (len p) ; ::_thesis: (pp - qq) . k <= p2 . k
A35: k in dom p by A34, FINSEQ_1:def_3;
then A36: p . k > 0 by A4;
q . k > 0 by A4, A35;
then (q . k) / (p . k) > 0 by A36, XREAL_1:139;
then log (number_e,((q . k) / (p . k))) <= ((q . k) / (p . k)) - 1 by Th3;
then ((p . k) * (log (2,number_e))) * (log (number_e,((q . k) / (p . k)))) <= ((p . k) * (log (2,number_e))) * (((q . k) / (p . k)) - 1) by A32, A36, XREAL_1:64;
then (pp - qq) . k <= ((p . k) * (log (2,number_e))) * (((q . k) / (p . k)) - 1) by A10, A35;
hence (pp - qq) . k <= p2 . k by A19, A23, A34; ::_thesis: verum
end;
A37: p2 is Element of (len p) -tuples_on REAL by A18, FINSEQ_2:92;
hence Sum pp <= Sum qq by A8, A33, A22, A31, RVSUM_1:82, XREAL_1:50; ::_thesis: ( ( ( 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 ) ) )
A38: ( ex k being Element of NAT st
( k in Seg (len p) & p . k <> q . k ) implies Sum pp < Sum qq )
proof
assume ex k being Element of NAT st
( k in Seg (len p) & p . k <> q . k ) ; ::_thesis: Sum pp < Sum qq
then consider k1 being Nat such that
A39: k1 in Seg (len p) and
A40: p . k1 <> q . k1 ;
A41: k1 in dom p by A39, FINSEQ_1:def_3;
then A42: p . k1 > 0 by A4;
then A43: (p . k1) * (log (2,number_e)) > 0 by A32, XREAL_1:129;
q . k1 > 0 by A4, A41;
then A44: (q . k1) / (p . k1) > 0 by A42, XREAL_1:139;
(q . k1) / (p . k1) <> 1 by A40, XCMPLX_1:58;
then log (number_e,((q . k1) / (p . k1))) < ((q . k1) / (p . k1)) - 1 by A44, Th3;
then ((p . k1) * (log (2,number_e))) * (log (number_e,((q . k1) / (p . k1)))) < ((p . k1) * (log (2,number_e))) * (((q . k1) / (p . k1)) - 1) by A43, XREAL_1:68;
then (pp - qq) . k1 < ((p . k1) * (log (2,number_e))) * (((q . k1) / (p . k1)) - 1) by A10, A41;
then (pp - qq) . k1 < p2 . k1 by A19, A23, A39;
then (Sum pp) - (Sum qq) < 0 by A8, A33, A22, A37, A31, A39, RVSUM_1:83;
hence Sum pp < Sum qq by XREAL_1:48; ::_thesis: verum
end;
A45: dom (pp - qq) = dom p2 by A21, A18, FINSEQ_3:29;
thus ( ( for k being Element of NAT st k in dom p holds
p . k = q . k ) iff Sum pp = Sum qq ) ::_thesis: ( ex k being Element of NAT st
( k in dom p & p . k <> q . k ) iff Sum pp < Sum qq )
proof
hereby ::_thesis: ( Sum pp = Sum qq implies for k being Element of NAT st k in dom p holds
p . k = q . k )
assume A46: for k being Element of NAT st k in dom p holds
p . k = q . k ; ::_thesis: Sum pp = Sum qq
for k being Nat st k in dom p holds
(pp - qq) . k = p2 . k
proof
let k be Nat; ::_thesis: ( k in dom p implies (pp - qq) . k = p2 . k )
assume A47: k in dom p ; ::_thesis: (pp - qq) . k = p2 . k
A48: p . k = q . k by A46, A47;
p . k > 0 by A4, A47;
then (q . k) / (p . k) = 1 by A48, XCMPLX_1:60;
then ((p . k) * (log (2,number_e))) * (log (number_e,((q . k) / (p . k)))) = ((p . k) * (log (2,number_e))) * (((q . k) / (p . k)) - 1) by Th3;
then A49: (pp - qq) . k = ((p . k) * (log (2,number_e))) * (((q . k) / (p . k)) - 1) by A10, A47;
k in Seg (len p) by A47, FINSEQ_1:def_3;
hence (pp - qq) . k = p2 . k by A19, A23, A49; ::_thesis: verum
end;
then Sum (pp - qq) = 0 by A20, A45, A31, FINSEQ_1:13;
hence Sum pp = Sum qq by A8; ::_thesis: verum
end;
assume A50: Sum pp = Sum qq ; ::_thesis: for k being Element of NAT st k in dom p holds
p . k = q . k
assume ex k being Element of NAT st
( k in dom p & not p . k = q . k ) ; ::_thesis: contradiction
hence contradiction by A26, A38, A50; ::_thesis: verum
end;
hence ( ex k being Element of NAT st
( k in dom p & p . k <> q . k ) iff Sum pp < Sum qq ) by A26, A38; ::_thesis: verum
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
let p be non empty ProbFinS FinSequence of REAL ; ::_thesis: ( ( for k being Element of NAT st k in dom p holds
p . k > 0 ) implies ( 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) ) ) ) )
assume A1: for k being Element of NAT st k in dom p holds
p . k > 0 ; ::_thesis: ( 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) ) ) )
set p3 = - (Infor_FinSeq_of p);
set n = len p;
reconsider n1 = len p as non empty Element of NAT ;
reconsider nn = 1 / n1 as Element of REAL ;
reconsider p1 = (len p) |-> nn as FinSequence of REAL ;
deffunc H1( Nat) -> Element of REAL = - ((p . $1) * (log (2,(p1 . $1))));
consider p2 being FinSequence of REAL such that
A2: len p2 = len p and
A3: for k being Nat st k in dom p2 holds
p2 . k = H1(k) from FINSEQ_2:sch_1();
A4: dom p2 = Seg (len p) by A2, FINSEQ_1:def_3;
A5: for k being Nat st k in dom p2 holds
p2 . k = ((- (log (2,(1 / n1)))) * p) . k
proof
let k be Nat; ::_thesis: ( k in dom p2 implies p2 . k = ((- (log (2,(1 / n1)))) * p) . k )
assume A6: k in dom p2 ; ::_thesis: p2 . k = ((- (log (2,(1 / n1)))) * p) . k
thus p2 . k = - ((p . k) * (log (2,(p1 . k)))) by A3, A6
.= - ((p . k) * (log (2,(1 / n1)))) by A4, A6, FINSEQ_2:57
.= (- (log (2,(1 / n1)))) * (p . k)
.= ((- (log (2,(1 / n1)))) * p) . k by RVSUM_1:44 ; ::_thesis: verum
end;
A7: len p1 = len p by CARD_1:def_7;
A8: dom (Infor_FinSeq_of p) = Seg (len (Infor_FinSeq_of p)) by FINSEQ_1:def_3
.= Seg (len p) by Th47 ;
A9: ( len (- (Infor_FinSeq_of p)) = len p & ( for k being Element of NAT st k in Seg (len p) holds
(- (Infor_FinSeq_of p)) . k = - ((p . k) * (log (2,(p . k)))) ) )
proof
dom (- (Infor_FinSeq_of p)) = Seg (len p) by A8, VALUED_1:8;
hence len (- (Infor_FinSeq_of p)) = len p by FINSEQ_1:def_3; ::_thesis: for k being Element of NAT st k in Seg (len p) holds
(- (Infor_FinSeq_of p)) . k = - ((p . k) * (log (2,(p . k))))
hereby ::_thesis: verum
let k be Element of NAT ; ::_thesis: ( k in Seg (len p) implies (- (Infor_FinSeq_of p)) . k = - ((p . k) * (log (2,(p . k)))) )
assume A10: k in Seg (len p) ; ::_thesis: (- (Infor_FinSeq_of p)) . k = - ((p . k) * (log (2,(p . k))))
thus (- (Infor_FinSeq_of p)) . k = - ((Infor_FinSeq_of p) . k) by RVSUM_1:17
.= - ((p . k) * (log (2,(p . k)))) by A8, A10, Th47 ; ::_thesis: verum
end;
end;
dom p2 = dom p by A2, FINSEQ_3:29;
then dom p2 = dom ((- (log (2,(1 / n1)))) * p) by VALUED_1:def_5;
then p2 = (- (log (2,(1 / n1)))) * p by A5, FINSEQ_1:13;
then A11: Sum p2 = (- (log (2,(1 / n1)))) * (Sum p) by RVSUM_1:87
.= (- (log (2,(1 / n1)))) * 1 by MATRPROB:def_5
.= log (2,(1 / (1 / n1))) by Th5
.= log (2,(len p)) ;
A12: p1 is non empty ProbFinS FinSequence of REAL by Th16;
A13: dom p = Seg (len p) by FINSEQ_1:def_3;
then A14: for k being Element of NAT st k in dom p holds
( p . k > 0 & p1 . k > 0 & (- (Infor_FinSeq_of p)) . k = - ((p . k) * (log (2,(p . k)))) & p2 . k = - ((p . k) * (log (2,(p1 . k)))) ) by A1, A3, A4, A9, FINSEQ_2:57;
A15: Sum (- (Infor_FinSeq_of p)) = Entropy p by RVSUM_1:88;
hence Entropy p <= log (2,(len p)) by A7, A12, A2, A9, A14, A11, Th57; ::_thesis: ( ( ( 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) ) ) )
thus ( ( for k being Element of NAT st k in dom p holds
p . k = 1 / (len p) ) iff Entropy p = log (2,(len p)) ) ::_thesis: ( ex k being Element of NAT st
( k in dom p & p . k <> 1 / (len p) ) iff Entropy p < log (2,(len p)) )
proof
hereby ::_thesis: ( Entropy p = log (2,(len p)) implies for k being Element of NAT st k in dom p holds
p . k = 1 / (len p) )
assume A16: for k being Element of NAT st k in dom p holds
p . k = 1 / (len p) ; ::_thesis: Entropy p = log (2,(len p))
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_p_holds_
p_._k_=_p1_._k
let k be Element of NAT ; ::_thesis: ( k in dom p implies p . k = p1 . k )
assume A17: k in dom p ; ::_thesis: p . k = p1 . k
thus p . k = 1 / (len p) by A16, A17
.= p1 . k by A13, A17, FINSEQ_2:57 ; ::_thesis: verum
end;
hence Entropy p = log (2,(len p)) by A7, A12, A2, A9, A14, A15, A11, Th57; ::_thesis: verum
end;
assume A18: Entropy p = log (2,(len p)) ; ::_thesis: for k being Element of NAT st k in dom p holds
p . k = 1 / (len p)
hereby ::_thesis: verum
let k be Element of NAT ; ::_thesis: ( k in dom p implies p . k = 1 / (len p) )
assume A19: k in dom p ; ::_thesis: p . k = 1 / (len p)
hence p . k = p1 . k by A7, A12, A2, A9, A14, A15, A11, A18, Th57
.= 1 / (len p) by A13, A19, FINSEQ_2:57 ;
::_thesis: verum
end;
end;
A20: ( ( for k being Element of NAT st k in dom p holds
p . k = p1 . k ) iff Sum (- (Infor_FinSeq_of p)) = Sum p2 ) by A7, A12, A2, A9, A14, Th57;
thus ( ex k being Element of NAT st
( k in dom p & p . k <> 1 / (len p) ) iff Entropy p < log (2,(len p)) ) ::_thesis: verum
proof
hereby ::_thesis: ( Entropy p < log (2,(len p)) implies ex k being Element of NAT st
( k in dom p & p . k <> 1 / (len p) ) )
assume ex k being Element of NAT st
( k in dom p & p . k <> 1 / (len p) ) ; ::_thesis: Entropy p < log (2,(len p))
then consider k1 being Nat such that
A21: k1 in dom p and
A22: p . k1 <> 1 / (len p) ;
p1 . k1 <> p . k1 by A13, A21, A22, FINSEQ_2:57;
hence Entropy p < log (2,(len p)) by A7, A12, A2, A9, A14, A15, A11, A21, Th57; ::_thesis: verum
end;
assume Entropy p < log (2,(len p)) ; ::_thesis: ex k being Element of NAT st
( k in dom p & p . k <> 1 / (len p) )
then consider k1 being Nat such that
A23: k1 in dom p and
A24: p . k1 <> p1 . k1 by A20, A11, RVSUM_1:88;
p1 . k1 = 1 / (len p) by A13, A23, FINSEQ_2:57;
hence ex k being Element of NAT st
( k in dom p & p . k <> 1 / (len p) ) by A23, A24; ::_thesis: verum
end;
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
let M be m-nonnegative Matrix of REAL; ::_thesis: Mx2FinS (Infor_FinSeq_of M) = Infor_FinSeq_of (Mx2FinS M)
reconsider p = Mx2FinS M as nonnegative FinSequence of REAL by Th43;
set pp = Infor_FinSeq_of p;
set qq = Mx2FinS (Infor_FinSeq_of M);
set MM = Infor_FinSeq_of M;
A1: len p = (len M) * (width M) by Th39;
A2: width (Infor_FinSeq_of M) = width M by Def8;
len (Infor_FinSeq_of M) = len M by Def8;
then A3: len (Mx2FinS (Infor_FinSeq_of M)) = (len M) * (width M) by A2, Th39;
len (Infor_FinSeq_of p) = len p by Th47;
then A4: dom (Mx2FinS (Infor_FinSeq_of M)) = dom (Infor_FinSeq_of p) by A1, A3, FINSEQ_3:29;
A5: dom (Mx2FinS (Infor_FinSeq_of M)) = dom p by A1, A3, FINSEQ_3:29;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_(Mx2FinS_(Infor_FinSeq_of_M))_holds_
(Infor_FinSeq_of_p)_._k_=_(Mx2FinS_(Infor_FinSeq_of_M))_._k
let k be Nat; ::_thesis: ( k in dom (Mx2FinS (Infor_FinSeq_of M)) implies (Infor_FinSeq_of p) . k = (Mx2FinS (Infor_FinSeq_of M)) . k )
assume A6: k in dom (Mx2FinS (Infor_FinSeq_of M)) ; ::_thesis: (Infor_FinSeq_of p) . k = (Mx2FinS (Infor_FinSeq_of M)) . k
k in Seg (len (Mx2FinS (Infor_FinSeq_of M))) by A6, FINSEQ_1:def_3;
then k >= 1 by FINSEQ_1:1;
then reconsider l = k - 1 as Element of NAT by NAT_1:21;
set jj = (l mod (width (Infor_FinSeq_of M))) + 1;
set ii = (l div (width (Infor_FinSeq_of M))) + 1;
A7: [((l div (width (Infor_FinSeq_of M))) + 1),((l mod (width (Infor_FinSeq_of M))) + 1)] in Indices (Infor_FinSeq_of M) by A6, Th41;
A8: (Mx2FinS (Infor_FinSeq_of M)) . k = (Infor_FinSeq_of M) * (((l div (width (Infor_FinSeq_of M))) + 1),((l mod (width (Infor_FinSeq_of M))) + 1)) by A6, Th41;
A9: p . k = M * (((l div (width (Infor_FinSeq_of M))) + 1),((l mod (width (Infor_FinSeq_of M))) + 1)) by A2, A5, A6, Th41;
thus (Infor_FinSeq_of p) . k = (p . k) * (log (2,(p . k))) by A4, A6, Th47
.= (Mx2FinS (Infor_FinSeq_of M)) . k by A7, A8, A9, Th54 ; ::_thesis: verum
end;
hence Mx2FinS (Infor_FinSeq_of M) = Infor_FinSeq_of (Mx2FinS M) by A4, FINSEQ_1:13; ::_thesis: verum
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
let p, q be ProbFinS FinSequence of REAL ; ::_thesis: 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))
set p1 = Infor_FinSeq_of p;
set p2 = (Sum (Infor_FinSeq_of q)) * p;
A1: len (Infor_FinSeq_of p) = len p by Th47;
dom ((Sum (Infor_FinSeq_of q)) * p) = dom p by VALUED_1:def_5;
then A2: len (Infor_FinSeq_of p) = len ((Sum (Infor_FinSeq_of q)) * p) by A1, FINSEQ_3:29;
len (FinSeq_log (2,q)) = len q by Def6;
then A3: len (mlt (q,(FinSeq_log (2,q)))) = len q by MATRPROB:30;
let M be Matrix of REAL; ::_thesis: ( M = (ColVec2Mx p) * (LineVec2Mx q) implies SumAll (Infor_FinSeq_of M) = (Sum (Infor_FinSeq_of p)) + (Sum (Infor_FinSeq_of q)) )
assume A4: M = (ColVec2Mx p) * (LineVec2Mx q) ; ::_thesis: SumAll (Infor_FinSeq_of M) = (Sum (Infor_FinSeq_of p)) + (Sum (Infor_FinSeq_of q))
reconsider M = M as Joint_Probability Matrix of REAL by A4, Th23;
set M1 = Infor_FinSeq_of M;
set L = LineSum (Infor_FinSeq_of M);
A5: len (LineSum (Infor_FinSeq_of M)) = len (Infor_FinSeq_of M) by MATRPROB:def_1;
then A6: dom (LineSum (Infor_FinSeq_of M)) = dom (Infor_FinSeq_of M) by FINSEQ_3:29;
A7: len (Infor_FinSeq_of M) = len M by Def8;
then A8: dom (Infor_FinSeq_of M) = dom M by FINSEQ_3:29;
A9: len M = len p by A4, Th22;
then A10: dom M = dom p by FINSEQ_3:29;
A11: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_(LineSum_(Infor_FinSeq_of_M))_holds_
(LineSum_(Infor_FinSeq_of_M))_._k_=_((p_._k)_*_(log_(2,(p_._k))))_+_((p_._k)_*_(Sum_(Infor_FinSeq_of_q)))
let k be Element of NAT ; ::_thesis: ( k in dom (LineSum (Infor_FinSeq_of M)) implies (LineSum (Infor_FinSeq_of M)) . k = ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of q))) )
assume A12: k in dom (LineSum (Infor_FinSeq_of M)) ; ::_thesis: (LineSum (Infor_FinSeq_of M)) . k = ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of q)))
reconsider pp = Line (M,k) as nonnegative FinSequence of REAL by A6, A8, A12, Th19;
A13: pp = (p . k) * q by A4, A6, A8, A12, Th22;
dom (((p . k) * (log (2,(p . k)))) * q) = dom q by VALUED_1:def_5;
then A14: len (((p . k) * (log (2,(p . k)))) * q) = len q by FINSEQ_3:29;
dom ((p . k) * (mlt (q,(FinSeq_log (2,q))))) = dom (mlt (q,(FinSeq_log (2,q)))) by VALUED_1:def_5;
then A15: len (((p . k) * (log (2,(p . k)))) * q) = len ((p . k) * (mlt (q,(FinSeq_log (2,q))))) by A3, A14, FINSEQ_3:29;
A16: p . k >= 0 by A6, A8, A10, A12, Def1;
thus (LineSum (Infor_FinSeq_of M)) . k = Sum ((Infor_FinSeq_of M) . k) by A12, MATRPROB:def_1
.= Sum (Line ((Infor_FinSeq_of M),k)) by A6, A12, MATRIX_2:16
.= Sum (Infor_FinSeq_of pp) by A6, A8, A12, Th53
.= Sum ((((p . k) * (log (2,(p . k)))) * q) + ((p . k) * (mlt (q,(FinSeq_log (2,q)))))) by A13, A16, Th51
.= (Sum (((p . k) * (log (2,(p . k)))) * q)) + (Sum ((p . k) * (mlt (q,(FinSeq_log (2,q)))))) by A15, INTEGRA5:2
.= (((p . k) * (log (2,(p . k)))) * (Sum q)) + (Sum ((p . k) * (mlt (q,(FinSeq_log (2,q)))))) by RVSUM_1:87
.= (((p . k) * (log (2,(p . k)))) * 1) + (Sum ((p . k) * (mlt (q,(FinSeq_log (2,q)))))) by MATRPROB:def_5
.= ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of q))) by RVSUM_1:87 ; ::_thesis: verum
end;
A17: dom (Infor_FinSeq_of p) = dom (LineSum (Infor_FinSeq_of M)) by A9, A7, A5, A1, FINSEQ_3:29;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_(Infor_FinSeq_of_p)_holds_
(LineSum_(Infor_FinSeq_of_M))_._k_=_((Infor_FinSeq_of_p)_._k)_+_(((Sum_(Infor_FinSeq_of_q))_*_p)_._k)
let k be Element of NAT ; ::_thesis: ( k in dom (Infor_FinSeq_of p) implies (LineSum (Infor_FinSeq_of M)) . k = ((Infor_FinSeq_of p) . k) + (((Sum (Infor_FinSeq_of q)) * p) . k) )
assume A18: k in dom (Infor_FinSeq_of p) ; ::_thesis: (LineSum (Infor_FinSeq_of M)) . k = ((Infor_FinSeq_of p) . k) + (((Sum (Infor_FinSeq_of q)) * p) . k)
thus (LineSum (Infor_FinSeq_of M)) . k = ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of q))) by A11, A17, A18
.= ((Infor_FinSeq_of p) . k) + ((p . k) * (Sum (Infor_FinSeq_of q))) by A18, Th47
.= ((Infor_FinSeq_of p) . k) + (((Sum (Infor_FinSeq_of q)) * p) . k) by RVSUM_1:44 ; ::_thesis: verum
end;
then Sum (LineSum (Infor_FinSeq_of M)) = (Sum (Infor_FinSeq_of p)) + (Sum ((Sum (Infor_FinSeq_of q)) * p)) by A9, A7, A5, A1, A2, Th7
.= (Sum (Infor_FinSeq_of p)) + ((Sum (Infor_FinSeq_of q)) * (Sum p)) by RVSUM_1:87
.= (Sum (Infor_FinSeq_of p)) + ((Sum (Infor_FinSeq_of q)) * 1) by MATRPROB:def_5
.= (Sum (Infor_FinSeq_of p)) + (Sum (Infor_FinSeq_of q)) ;
hence SumAll (Infor_FinSeq_of M) = (Sum (Infor_FinSeq_of p)) + (Sum (Infor_FinSeq_of q)) by MATRPROB:def_3; ::_thesis: verum
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
let p, q be ProbFinS FinSequence of REAL ; ::_thesis: Entropy_of_Joint_Prob ((ColVec2Mx p) * (LineVec2Mx q)) = (Entropy p) + (Entropy q)
set M = (ColVec2Mx p) * (LineVec2Mx q);
reconsider M = (ColVec2Mx p) * (LineVec2Mx q) as Joint_Probability Matrix of REAL by Th23;
set pp = Mx2FinS ((ColVec2Mx p) * (LineVec2Mx q));
reconsider pp = Mx2FinS ((ColVec2Mx p) * (LineVec2Mx q)) as ProbFinS FinSequence of REAL by Th45;
(Entropy p) + (Entropy q) = - ((Sum (Infor_FinSeq_of p)) + (Sum (Infor_FinSeq_of q)))
.= - (SumAll (Infor_FinSeq_of M)) by Th60
.= - (Sum (Mx2FinS (Infor_FinSeq_of M))) by Th42
.= - (Sum (Infor_FinSeq_of pp)) by Th59 ;
hence Entropy_of_Joint_Prob ((ColVec2Mx p) * (LineVec2Mx q)) = (Entropy p) + (Entropy q) ; ::_thesis: verum
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 b1 being FinSequence of REAL st
( len b1 = len MR & ( for k being Element of NAT st k in dom b1 holds
b1 . k = Entropy (Line (MR,k)) ) )
proof
deffunc H1( Nat) -> Real = Entropy (Line (MR,$1));
consider p being FinSequence of REAL such that
A1: len p = len MR and
A2: for k being Nat st k in dom p holds
p . k = H1(k) from FINSEQ_2:sch_1();
take p ; ::_thesis: ( len p = len MR & ( for k being Element of NAT st k in dom p holds
p . k = Entropy (Line (MR,k)) ) )
thus ( len p = len MR & ( for k being Element of NAT st k in dom p holds
p . k = Entropy (Line (MR,k)) ) ) by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len MR & ( for k being Element of NAT st k in dom b1 holds
b1 . k = Entropy (Line (MR,k)) ) & len b2 = len MR & ( for k being Element of NAT st k in dom b2 holds
b2 . k = Entropy (Line (MR,k)) ) holds
b1 = b2
proof
let p1, p2 be FinSequence of REAL ; ::_thesis: ( len p1 = len MR & ( for k being Element of NAT st k in dom p1 holds
p1 . k = Entropy (Line (MR,k)) ) & len p2 = len MR & ( for k being Element of NAT st k in dom p2 holds
p2 . k = Entropy (Line (MR,k)) ) implies p1 = p2 )
assume that
A3: len p1 = len MR and
A4: for k being Element of NAT st k in dom p1 holds
p1 . k = Entropy (Line (MR,k)) and
A5: len p2 = len MR and
A6: for k being Element of NAT st k in dom p2 holds
p2 . k = Entropy (Line (MR,k)) ; ::_thesis: p1 = p2
A7: dom p1 = dom p2 by A3, A5, FINSEQ_3:29;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_p1_holds_
p1_._k_=_p2_._k
let k be Nat; ::_thesis: ( k in dom p1 implies p1 . k = p2 . k )
assume A8: k in dom p1 ; ::_thesis: p1 . k = p2 . k
thus p1 . k = Entropy (Line (MR,k)) by A4, A8
.= p2 . k by A6, A7, A8 ; ::_thesis: verum
end;
hence p1 = p2 by A7, FINSEQ_1:13; ::_thesis: verum
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 Element of NAT st k in dom b2 holds
b2 . 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
let M be non empty-yielding Conditional_Probability Matrix of REAL; ::_thesis: 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)) ) ) )
let p be FinSequence of REAL ; ::_thesis: ( 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)) ) ) )
A1: len (Infor_FinSeq_of M) = len M by Def8;
hereby ::_thesis: ( len p = len M & ( for k being Element of NAT st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ) implies p = Entropy_of_Cond_Prob M )
assume A2: p = Entropy_of_Cond_Prob M ; ::_thesis: ( len p = len M & ( for k being Element of NAT st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ) )
then A3: len p = len M by Def11;
then A4: dom p = dom M by FINSEQ_3:29;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_p_holds_
p_._k_=_-_(Sum_((Infor_FinSeq_of_M)_._k))
let k be Element of NAT ; ::_thesis: ( k in dom p implies p . k = - (Sum ((Infor_FinSeq_of M) . k)) )
assume A5: k in dom p ; ::_thesis: p . k = - (Sum ((Infor_FinSeq_of M) . k))
A6: k in dom (Infor_FinSeq_of M) by A1, A3, A5, FINSEQ_3:29;
thus p . k = Entropy (Line (M,k)) by A2, A5, Def11
.= - (Sum (Line ((Infor_FinSeq_of M),k))) by A4, A5, Th53
.= - (Sum ((Infor_FinSeq_of M) . k)) by A6, MATRIX_2:16 ; ::_thesis: verum
end;
hence ( len p = len M & ( for k being Element of NAT st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ) ) by A2, Def11; ::_thesis: verum
end;
assume that
A7: len p = len M and
A8: for k being Element of NAT st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ; ::_thesis: p = Entropy_of_Cond_Prob M
A9: dom p = dom M by A7, FINSEQ_3:29;
A10: dom (Infor_FinSeq_of M) = dom M by A1, FINSEQ_3:29;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_p_holds_
p_._k_=_Entropy_(Line_(M,k))
let k be Element of NAT ; ::_thesis: ( k in dom p implies p . k = Entropy (Line (M,k)) )
assume A11: k in dom p ; ::_thesis: p . k = Entropy (Line (M,k))
thus p . k = - (Sum ((Infor_FinSeq_of M) . k)) by A8, A11
.= - (Sum (Line ((Infor_FinSeq_of M),k))) by A10, A9, A11, MATRIX_2:16
.= Entropy (Line (M,k)) by A9, A11, Th53 ; ::_thesis: verum
end;
hence p = Entropy_of_Cond_Prob M by A7, Def11; ::_thesis: verum
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
let M be non empty-yielding Conditional_Probability Matrix of REAL; ::_thesis: Entropy_of_Cond_Prob M = - (LineSum (Infor_FinSeq_of M))
set p = Entropy_of_Cond_Prob M;
set q = - (LineSum (Infor_FinSeq_of M));
A1: dom (- (LineSum (Infor_FinSeq_of M))) = dom (LineSum (Infor_FinSeq_of M)) by VALUED_1:8;
then len (- (LineSum (Infor_FinSeq_of M))) = len (LineSum (Infor_FinSeq_of M)) by FINSEQ_3:29;
then len (- (LineSum (Infor_FinSeq_of M))) = len (Infor_FinSeq_of M) by MATRPROB:def_1;
then A2: len (- (LineSum (Infor_FinSeq_of M))) = len M by Def8;
len (Entropy_of_Cond_Prob M) = len M by Th62;
then A3: dom (Entropy_of_Cond_Prob M) = dom (- (LineSum (Infor_FinSeq_of M))) by A2, FINSEQ_3:29;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_(Entropy_of_Cond_Prob_M)_holds_
(Entropy_of_Cond_Prob_M)_._k_=_(-_(LineSum_(Infor_FinSeq_of_M)))_._k
let k be Nat; ::_thesis: ( k in dom (Entropy_of_Cond_Prob M) implies (Entropy_of_Cond_Prob M) . k = (- (LineSum (Infor_FinSeq_of M))) . k )
assume A4: k in dom (Entropy_of_Cond_Prob M) ; ::_thesis: (Entropy_of_Cond_Prob M) . k = (- (LineSum (Infor_FinSeq_of M))) . k
thus (Entropy_of_Cond_Prob M) . k = - (Sum ((Infor_FinSeq_of M) . k)) by A4, Th62
.= - ((Sum (Infor_FinSeq_of M)) . k) by A1, A3, A4, MATRPROB:def_1
.= (- (LineSum (Infor_FinSeq_of M))) . k by RVSUM_1:17 ; ::_thesis: verum
end;
hence Entropy_of_Cond_Prob M = - (LineSum (Infor_FinSeq_of M)) by A3, FINSEQ_1:13; ::_thesis: verum
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
let p be ProbFinS FinSequence of REAL ; ::_thesis: 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)))))
let M be non empty-yielding Conditional_Probability Matrix of REAL; ::_thesis: ( len p = len M implies 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))))) )
assume A1: len p = len M ; ::_thesis: 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)))))
let M1 be Matrix of REAL; ::_thesis: ( M1 = (Vec2DiagMx p) * M implies SumAll (Infor_FinSeq_of M1) = (Sum (Infor_FinSeq_of p)) + (Sum (mlt (p,(LineSum (Infor_FinSeq_of M))))) )
assume A2: M1 = (Vec2DiagMx p) * M ; ::_thesis: SumAll (Infor_FinSeq_of M1) = (Sum (Infor_FinSeq_of p)) + (Sum (mlt (p,(LineSum (Infor_FinSeq_of M)))))
reconsider M1 = M1 as Joint_Probability Matrix of REAL by A1, A2, Th28;
A3: len M1 = len p by A1, A2, Th26;
then A4: dom M1 = dom p by FINSEQ_3:29;
set M2 = Infor_FinSeq_of M1;
set L = LineSum (Infor_FinSeq_of M1);
A5: len (LineSum (Infor_FinSeq_of M1)) = len (Infor_FinSeq_of M1) by MATRPROB:def_1;
then A6: dom (LineSum (Infor_FinSeq_of M1)) = dom (Infor_FinSeq_of M1) by FINSEQ_3:29;
A7: len (Infor_FinSeq_of M1) = len M1 by Def8;
then A8: dom (Infor_FinSeq_of M1) = dom M1 by FINSEQ_3:29;
A9: dom p = dom M by A1, FINSEQ_3:29;
A10: for k being Element of NAT st k in dom (LineSum (Infor_FinSeq_of M1)) holds
(LineSum (Infor_FinSeq_of M1)) . k = ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of (Line (M,k)))))
proof
let k be Element of NAT ; ::_thesis: ( k in dom (LineSum (Infor_FinSeq_of M1)) implies (LineSum (Infor_FinSeq_of M1)) . k = ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of (Line (M,k))))) )
assume A11: k in dom (LineSum (Infor_FinSeq_of M1)) ; ::_thesis: (LineSum (Infor_FinSeq_of M1)) . k = ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of (Line (M,k)))))
reconsider pp = Line (M1,k) as nonnegative FinSequence of REAL by A6, A8, A11, Th19;
A12: p . k >= 0 by A6, A8, A4, A11, Def1;
reconsider q = Line (M,k) as non empty ProbFinS FinSequence of REAL by A6, A8, A4, A9, A11, MATRPROB:60;
A13: pp = (p . k) * q by A1, A2, A6, A8, A11, Th27;
dom (((p . k) * (log (2,(p . k)))) * q) = dom q by VALUED_1:def_5;
then A14: len (((p . k) * (log (2,(p . k)))) * q) = len q by FINSEQ_3:29;
len (FinSeq_log (2,q)) = len q by Def6;
then A15: len (mlt (q,(FinSeq_log (2,q)))) = len q by MATRPROB:30;
dom ((p . k) * (mlt (q,(FinSeq_log (2,q))))) = dom (mlt (q,(FinSeq_log (2,q)))) by VALUED_1:def_5;
then A16: len ((p . k) * (mlt (q,(FinSeq_log (2,q))))) = len (mlt (q,(FinSeq_log (2,q)))) by FINSEQ_3:29;
(LineSum (Infor_FinSeq_of M1)) . k = Sum ((Infor_FinSeq_of M1) . k) by A11, MATRPROB:def_1
.= Sum (Line ((Infor_FinSeq_of M1),k)) by A6, A11, MATRIX_2:16
.= Sum (Infor_FinSeq_of pp) by A6, A8, A11, Th53
.= Sum ((((p . k) * (log (2,(p . k)))) * q) + ((p . k) * (mlt (q,(FinSeq_log (2,q)))))) by A13, A12, Th51
.= (Sum (((p . k) * (log (2,(p . k)))) * q)) + (Sum ((p . k) * (mlt (q,(FinSeq_log (2,q)))))) by A15, A14, A16, INTEGRA5:2
.= (((p . k) * (log (2,(p . k)))) * (Sum q)) + (Sum ((p . k) * (mlt (q,(FinSeq_log (2,q)))))) by RVSUM_1:87
.= (((p . k) * (log (2,(p . k)))) * 1) + (Sum ((p . k) * (mlt (q,(FinSeq_log (2,q)))))) by MATRPROB:def_5
.= ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of q))) by RVSUM_1:87 ;
hence (LineSum (Infor_FinSeq_of M1)) . k = ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of (Line (M,k))))) ; ::_thesis: verum
end;
set M3 = Infor_FinSeq_of M;
set L2 = LineSum (Infor_FinSeq_of M);
set p2 = mlt (p,(LineSum (Infor_FinSeq_of M)));
set p1 = Infor_FinSeq_of p;
A17: len (Infor_FinSeq_of p) = len p by Th47;
then A18: dom (Infor_FinSeq_of p) = dom M by A1, FINSEQ_3:29;
A19: len (Infor_FinSeq_of M) = len M by Def8;
then A20: len (LineSum (Infor_FinSeq_of M)) = len p by A1, MATRPROB:def_1;
then A21: len (mlt (p,(LineSum (Infor_FinSeq_of M)))) = len p by MATRPROB:30;
A22: dom (Infor_FinSeq_of p) = dom (Infor_FinSeq_of M) by A1, A19, A17, FINSEQ_3:29;
A23: dom (LineSum (Infor_FinSeq_of M)) = dom (Infor_FinSeq_of p) by A20, A17, FINSEQ_3:29;
A24: dom (Infor_FinSeq_of p) = dom (LineSum (Infor_FinSeq_of M1)) by A3, A7, A5, A17, FINSEQ_3:29;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_(Infor_FinSeq_of_p)_holds_
(LineSum_(Infor_FinSeq_of_M1))_._k_=_((Infor_FinSeq_of_p)_._k)_+_((mlt_(p,(LineSum_(Infor_FinSeq_of_M))))_._k)
let k be Element of NAT ; ::_thesis: ( k in dom (Infor_FinSeq_of p) implies (LineSum (Infor_FinSeq_of M1)) . k = ((Infor_FinSeq_of p) . k) + ((mlt (p,(LineSum (Infor_FinSeq_of M)))) . k) )
assume A25: k in dom (Infor_FinSeq_of p) ; ::_thesis: (LineSum (Infor_FinSeq_of M1)) . k = ((Infor_FinSeq_of p) . k) + ((mlt (p,(LineSum (Infor_FinSeq_of M)))) . k)
A26: (mlt (p,(LineSum (Infor_FinSeq_of M)))) . k = (p . k) * ((LineSum (Infor_FinSeq_of M)) . k) by RVSUM_1:59
.= (p . k) * (Sum ((Infor_FinSeq_of M) . k)) by A23, A25, MATRPROB:def_1
.= (p . k) * (Sum (Line ((Infor_FinSeq_of M),k))) by A22, A25, MATRIX_2:16
.= (p . k) * (Sum (Infor_FinSeq_of (Line (M,k)))) by A18, A25, Th53 ;
thus (LineSum (Infor_FinSeq_of M1)) . k = ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of (Line (M,k))))) by A10, A24, A25
.= ((Infor_FinSeq_of p) . k) + ((mlt (p,(LineSum (Infor_FinSeq_of M)))) . k) by A25, A26, Th47 ; ::_thesis: verum
end;
then Sum (LineSum (Infor_FinSeq_of M1)) = (Sum (Infor_FinSeq_of p)) + (Sum (mlt (p,(LineSum (Infor_FinSeq_of M))))) by A3, A7, A5, A17, A21, Th7;
hence SumAll (Infor_FinSeq_of M1) = (Sum (Infor_FinSeq_of p)) + (Sum (mlt (p,(LineSum (Infor_FinSeq_of M))))) by MATRPROB:def_3; ::_thesis: verum
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
let p be ProbFinS FinSequence of REAL ; ::_thesis: 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))))
let M be non empty-yielding Conditional_Probability Matrix of REAL; ::_thesis: ( len p = len M implies Entropy_of_Joint_Prob ((Vec2DiagMx p) * M) = (Entropy p) + (Sum (mlt (p,(Entropy_of_Cond_Prob M)))) )
set M1 = (Vec2DiagMx p) * M;
assume A1: len p = len M ; ::_thesis: Entropy_of_Joint_Prob ((Vec2DiagMx p) * M) = (Entropy p) + (Sum (mlt (p,(Entropy_of_Cond_Prob M))))
then reconsider M1 = (Vec2DiagMx p) * M as Joint_Probability Matrix of REAL by Th28;
A2: (Entropy p) + (Sum (mlt (p,(Entropy_of_Cond_Prob M)))) = (- (Sum (Infor_FinSeq_of p))) + (Sum (mlt (p,(- (LineSum (Infor_FinSeq_of M)))))) by Th63
.= (- (Sum (Infor_FinSeq_of p))) + (Sum (- (mlt (p,(LineSum (Infor_FinSeq_of M)))))) by RVSUM_1:65
.= (- (Sum (Infor_FinSeq_of p))) + (- (Sum (mlt (p,(LineSum (Infor_FinSeq_of M)))))) by RVSUM_1:88 ;
Entropy_of_Joint_Prob M1 = - (Sum (Mx2FinS (Infor_FinSeq_of M1))) by Th59
.= - (SumAll (Infor_FinSeq_of M1)) by Th42
.= - ((Sum (Infor_FinSeq_of p)) + (Sum (mlt (p,(LineSum (Infor_FinSeq_of M)))))) by A1, Th64
.= (- (Sum (Infor_FinSeq_of p))) - (Sum (mlt (p,(LineSum (Infor_FinSeq_of M))))) ;
hence Entropy_of_Joint_Prob ((Vec2DiagMx p) * M) = (Entropy p) + (Sum (mlt (p,(Entropy_of_Cond_Prob M)))) by A2; ::_thesis: verum
end;