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