:: Definition and Some Properties of Information Entropy
:: by Bo Zhang and Yatsuka Nakamura
::
:: Received July 9, 2007
:: Copyright (c) 2007-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, SUBSET_1, NAT_1, REAL_1, FINSEQ_1, MATRIX_1,
CARD_1, ARYTM_3, XXREAL_0, INT_1, ARYTM_1, RELAT_1, TAYLOR_1, FUNCT_1,
XXREAL_1, LIMFUNC1, POWER, PARTFUN1, FDIFF_1, ORDINAL2, TARSKI, CARD_3,
SEQ_1, SUPINF_2, PARTFUN3, RVSUM_1, ORDINAL4, FINSEQ_2, MATRPROB,
MATRIXC1, TREES_1, INCSP_1, MATRIXR1, FVSUM_1, ZFMISC_1, FUNCOP_1,
ENTROPY1, FUNCT_7, XCMPLX_0;
notations TARSKI, SUBSET_1, XBOOLE_0, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1,
ORDINAL1, NAT_1, NAT_D, NUMBERS, RELAT_1, FUNCT_1, VALUED_1, SEQ_1,
ZFMISC_1, PARTFUN1, FUNCOP_1, RVSUM_1, FINSEQ_1, NEWTON, FINSEQ_2,
MATRIXR1, MATRIX_0, PARTFUN3, POWER, LIMFUNC1, RCOMP_1, MATRPROB,
FDIFF_1, TAYLOR_1, FCONT_1;
constructors REAL_1, NAT_D, BINOP_2, MATRIX_3, MATRIXR1, MATRLIN, MATRPROB,
PARTFUN3, PARTFUN2, FDIFF_1, FCONT_1, POWER, LIMFUNC1, SIN_COS, TAYLOR_1,
INTEGRA1, XXREAL_2, RVSUM_1, RELSET_1, NEWTON, NUMBERS;
registrations MATRPROB, RELSET_1, NAT_1, MEMBERED, ORDINAL1, XREAL_0, FCONT_3,
RCOMP_1, XXREAL_0, NUMBERS, XBOOLE_0, VALUED_0, FINSEQ_1, CARD_1,
XXREAL_2, FINSEQ_2, RVSUM_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, PARTFUN3;
equalities FINSEQ_2, LIMFUNC1, RCOMP_1, VALUED_1, XCMPLX_0, TAYLOR_1;
expansions PARTFUN3;
theorems FUNCT_1, NAT_1, XREAL_1, NAT_2, MATRIXR1, XBOOLE_0, PROB_3, INTEGRA5,
FINSEQ_1, MATRIX_0, FINSEQ_2, FINSEQ_3, RVSUM_1, POWER, FDIFF_1, TREES_1,
XBOOLE_1, TAYLOR_1, RELAT_1, ROLLE, FCONT_1, XCMPLX_1, INTEGRA1,
XXREAL_0, ORDINAL1, MATRPROB, FUNCOP_1, PEPIN, NAT_D, PARTFUN1, VALUED_1,
XXREAL_1, XXREAL_2, CARD_1, XREAL_0;
schemes FINSEQ_2, SEQ_1, NAT_1, RECDEF_1, FINSEQ_1, MATRIX_0;
begin :: Preliminaries
reserve D for non empty set,
i,j,k,l for Nat,
n for Nat,
x for set,
a,b,c,r,r1,r2 for Real,
p,q for FinSequence of REAL,
MR,MR1 for Matrix of REAL;
theorem Th1:
k <> 0 & i < l & l <= j & k divides l implies i div k < j div k
proof
assume that
A1: k <> 0 and
A2: i < l and
A3: l <= j and
A4: k divides l;
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 thesis by A8,A7,A6,XXREAL_0:2;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
theorem Th2:
r > 0 implies ln.r <= r - 1 & (r = 1 iff ln.r = r - 1) & (r <> 1
iff ln.r < r - 1)
proof
set Z2 = ].0,1.[;
set Z1 = right_open_halfline(1);
reconsider f2 = log_ number_e as PartFunc of REAL, REAL;
deffunc G(Real) = In($1-1,REAL);
defpred P[object] means $1 in REAL;
set Z = right_open_halfline(0);
A1: 1 in Z by XXREAL_1:235;
1 in {g where g is Real: 0 < g};
then
A2: 1 in Z by XXREAL_1:230;
consider f1 being PartFunc of REAL,REAL such that
A3: (for r being Element of REAL holds r in dom f1 iff P[r]) &
for r being Element of REAL st r in dom f1 holds f1.r =G(r)
from SEQ_1:sch 3;
A4: for r being Real holds r in dom f1 iff P[r]
by XREAL_0:def 1,A3;
dom f1 is Subset of REAL by RELAT_1:def 18;
then
A5: dom f1 = REAL by A4,FDIFF_1:1;
A6: for r st r in Z holds f1.r = 1*r + (-1)
proof
let r such that
r in Z;
reconsider r as Element of REAL by XREAL_0:def 1;
f1.r = G(r) by A3;
hence thesis;
end;
then
A7: f1 is_differentiable_on Z by A5,FDIFF_1:23;
set f = f1 - f2;
A8: number_e <> 1 by TAYLOR_1:11;
assume
A9: r > 0;
dom f2 = Z by TAYLOR_1:def 2;
then
A10: dom f = Z /\ REAL by A5,VALUED_1:12
.= Z by XBOOLE_1:28;
A11: for x be Element of REAL st x > 0 holds f.x = (x - 1) - ln.x
proof
let x be Element of REAL;
assume x > 0;
then x in {g where g is Real: 0<g};
then
A12: x in dom f by A10,XXREAL_1:230;
f.x = f1.x - f2.x by A12,VALUED_1:13
.= G(x) - f2.x by A3;
hence thesis;
end;
then
A13: f.1 = (1 - 1) - ln.jj .= - log(number_e,1) by A2,TAYLOR_1:def 2
.= - 0 by A8,POWER:51,TAYLOR_1:11
.= 0;
A14: f1 is_differentiable_on Z by A5,A6,FDIFF_1:23;
A15: now
let r such that
A16: r in Z;
thus diff(f1,r) = (f1`|Z).r by A14,A16,FDIFF_1:def 7
.= 1 by A5,A6,A16,FDIFF_1:23;
end;
A17: f is_differentiable_on Z & for r st r in Z holds diff(f,r)=1 - 1/r
proof
thus
A18: f is_differentiable_on Z by A10,A7,FDIFF_1:19,TAYLOR_1:18;
hereby
let r such that
A19: r in Z;
((f1-f2)`|Z).r = diff(f1,r) - diff(f2,r) by A10,A7,A19,FDIFF_1:19
,TAYLOR_1:18
.= 1 - diff(f2,r) by A15,A19
.= 1 - 1/r by A19,TAYLOR_1:18;
hence diff(f,r) = 1 - 1/r by A18,A19,FDIFF_1:def 7;
end;
end;
then
A20: f|Z is continuous by FDIFF_1:25;
A21: Z1 c= Z by XXREAL_1:46;
A22: for r st r in Z1 holds diff(f,r) > 0
proof
let r such that
A23: r in Z1;
r in {g where g is Real: 1 < g} by A23,XXREAL_1:230;
then
A24: ex g1 being Real st g1 = r & 1 < g1;
diff(f,r) = 1 - 1/r by A17,A21,A23;
hence thesis by A24,XREAL_1:50,212;
end;
A25: for r st r in Z1 holds f.r > 0
proof
assume not for r st r in Z1 holds f.r > 0;
then consider r1 such that
A26: r1 in Z1 and
A27: f.r1 <= 0;
A28: [.1,r1.] c= dom f by A1,A10,A21,A26,XXREAL_2:def 12;
r1 in {g where g is Real: 1 < g} by A26,XXREAL_1:230;
then
A29: ex g1 being Real st g1 = r1 & 1 < g1;
A30: f is_differentiable_on ].1,r1.[ by A17,FDIFF_1:26,XXREAL_1:247;
A31: f|[.1,r1.] is continuous by A20,FCONT_1:16,XXREAL_1:249;
per cases by A27;
suppose
f.r1 = 0;
then consider r2 being Real such that
A32: r2 in ].1,r1.[ and
A33: diff(f,r2)=0 by A13,A29,A31,A30,A28,ROLLE:1;
ex g1 being Real st g1 = r2 & 1 < g1 & g1 < r1 by A32;
then r2 in {g where g is Real : 1<g};
then r2 in Z1 by XXREAL_1:230;
hence contradiction by A22,A33;
end;
suppose
A34: f.r1 < 0;
consider r3 being Real such that
A35: r3 in ].1,r1.[ and
A36: diff(f,r3)=(f.r1-f.1)/(r1-1) by A29,A31,A30,A28,ROLLE:3;
ex g1 being Real st g1 = r3 & 1 < g1 & g1 < r1 by A35;
then r3 in {g where g is Real : 1<g};
then
A37: r3 in Z1 by XXREAL_1:230;
r1 -1 > 0 by A29,XREAL_1:50;
hence contradiction by A13,A22,A34,A36,A37;
end;
end;
A38: for r st r > 1 holds f.r > 0
proof
let r;
assume r > 1;
then r in {g where g is Real : 1<g };
then r in Z1 by XXREAL_1:230;
hence thesis by A25;
end;
A39: Z2 c= Z by XXREAL_1:247;
A40: for r st r in Z2 holds diff(f,r) < 0
proof
let r;
assume
A41: r in Z2;
then ex g1 being Real st g1 = r & 0 < g1 & g1 < 1;
then
A42: 1 < 1/r by XREAL_1:187;
diff(f,r) = 1 - 1/r by A17,A39,A41;
hence thesis by A42,XREAL_1:49;
end;
A43: for r st r in Z2 holds f.r > 0
proof
assume not for r st r in Z2 holds f.r > 0;
then consider r1 such that
A44: r1 in Z2 and
A45: f.r1 <= 0;
A46: [.r1,1.] c= dom f by A1,A10,A39,A44,XXREAL_2:def 12;
A47: ex g1 being Real st g1 = r1 & 0<g1 & g1<1 by A44;
then
A48: f|[.r1,1.] is continuous by A20,FCONT_1:16,XXREAL_1:249;
A49: f is_differentiable_on ].r1,1.[ by A17,A47,FDIFF_1:26,XXREAL_1:247;
per cases by A45;
suppose
f.r1 = 0;
then consider r2 being Real such that
A50: r2 in ].r1,1.[ and
A51: diff(f,r2)=0 by A13,A47,A48,A46,A49,ROLLE:1;
ex g1 being Real st g1 = r2 & r1 < g1 & g1 < 1 by A50;
then r2 in {g where g is Real : 0<g & g<1 } by A47;
hence contradiction by A40,A51;
end;
suppose
A52: f.r1 < 0;
A53: 1 -r1 > 0 by A47,XREAL_1:50;
consider r3 being Real such that
A54: r3 in ].r1,1.[ and
A55: diff(f,r3)=(f.1-f.r1)/(1-r1) by A47,A48,A46,A49,ROLLE:3;
ex g1 being Real st g1 = r3 & r1 < g1 & g1 < 1 by A54;
then r3 in Z2 by A47;
hence contradiction by A13,A40,A52,A55,A53;
end;
end;
A56: for r st r > 0 & r < 1 holds f.r > 0
proof
let r such that
A57: r > 0 and
A58: r < 1;
r in {g where g is Real : 0<g & g<1 } by A57,A58;
hence thesis by A43;
end;
reconsider rr=r as Element of REAL by XREAL_0:def 1;
for r st r > 0 holds f.r >= 0
proof
let r such that
A59: r > 0;
per cases by XXREAL_0:1;
suppose
r < 1;
hence thesis by A56,A59;
end;
suppose
r = 1;
hence thesis by A13;
end;
suppose
r > 1;
hence thesis by A38;
end;
end;
then f.r >= 0 by A9;
then (r - 1) - ln.rr >= 0 by A11,A9;
then (r - 1) - 0 >= ln.r by XREAL_1:11;
hence ln.r <= r - 1;
thus
A60: r = 1 iff ln.r = r - 1
proof
hereby
assume r = 1;
then (r - 1) - ln.rr = 0 by A11,A13;
hence ln.r = r - 1;
end;
assume ln.r = r - 1;
then
A61: (r - 1) - ln.r = 0;
assume
A62: r <> 1;
per cases by A62,XXREAL_0:1;
suppose
r < 1;
then f.rr > 0 by A56,A9;
hence contradiction by A11,A9,A61;
end;
suppose
A63: r > 1;
then f.rr > 0 by A38;
hence contradiction by A11,A61,A63;
end;
end;
thus r <> 1 iff ln.r < r - 1
proof
hereby
assume r <> 1;
then
A64: r-1>0 or 1-r>0 by XREAL_1:55;
per cases by A64,XREAL_1:47;
suppose
r < 1;
then f.r > 0 by A56,A9;
then (r - 1) - ln.rr > 0 by A11,A9;
hence ln.r < r - 1 by XREAL_1:47;
end;
suppose
A65: r > 1;
then f.r > 0 by A38;
then (r - 1) - ln.rr > 0 by A11,A65;
hence ln.r < r - 1 by XREAL_1:47;
end;
end;
assume
A66: ln.r < r - 1;
assume r = 1;
hence contradiction by A60,A66;
end;
end;
theorem Th3:
r > 0 implies log(number_e,r) <= r - 1 & (r = 1 iff log(number_e,
r) = r - 1) & (r <> 1 iff log(number_e,r) < r - 1)
proof
assume
A1: r>0;
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 thesis by A1,Th2;
end;
theorem Th4:
a>1 & b>1 implies log(a,b) > 0
proof
assume that
A1: a>1 and
A2: b>1;
A3: a to_power log(a,b) > 1 by A1,A2,POWER:def 3;
assume
A4: log(a,b) <=0;
per cases by A4;
suppose
log(a,b) =0;
hence contradiction by A3,POWER:24;
end;
suppose
log(a,b) <0;
hence contradiction by A1,A3,POWER:36;
end;
end;
theorem Th5:
a>0 & a<>1 & b>0 implies -log(a,b) = log(a,1/b)
proof
assume that
A1: a>0 and
A2: a<>1 and
A3: b>0;
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;
end;
theorem Th6:
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)
proof
assume that
A1: a>0 and
A2: a<>1 and
A3: b>=0 and
A4: c>=0;
per cases by A3,A4;
suppose
b>0 & c = 0;
hence thesis;
end;
suppose
b=0 & c = 0;
hence thesis;
end;
suppose
b=0 & c > 0;
hence thesis;
end;
suppose
b>0 & c > 0;
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);
end;
end;
theorem Th7:
for q,q1,q2 being FinSequence of REAL st len q1 = len q & len q1
= len q2 & (for k 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 such that
A1: len q1 = len q and
A2: len q1 = len q2 and
A3: for k st k in dom q1 holds q.k = q1.k + q2.k;
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 such that
A4: k in dom q1;
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;
end;
hence thesis by A1,A2,INTEGRA1:21;
end;
theorem Th8:
for q,q1,q2 being FinSequence of REAL st len q1 = len q & len q1
= len q2 & (for k 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 such that
A1: len q1 = len q and
A2: len q1 = len q2 and
A3: for k st k in dom q1 holds q.k = q1.k - q2.k;
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 such that
A4: k in dom q1;
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;
end;
hence thesis by A1,A2,INTEGRA1:22;
end;
theorem Th9:
len p >= 1 implies ex q st len q = len p & q.1 = p.1 & (for k st
0 <> k & k < len p holds q.(k+1) = q.k + p.(k+1)) & Sum p = q.(len p)
proof
assume
A1: len p >= 1;
then consider r be Real_Sequence such that
A2: r.1 = p.1 and
A3: for n 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 F(Nat) = r.$1;
consider q being FinSequence such that
A6: len q = len p & for k be Nat st k in dom q holds q.k = F(k) from
FINSEQ_1:sch 2;
A7: rng q c= REAL
proof
let x be object;
assume x in rng q;
then consider j being Nat such that
A8: j in dom q and
A9: q.j = x by FINSEQ_2:10;
F(j) = q.j by A6,A8;
hence thesis by A9,XREAL_0:def 1;
end;
A10: dom q = dom p by A6,FINSEQ_3:29;
reconsider q as FinSequence of REAL by A7,FINSEQ_1:def 4;
A11: now
let k such that
A12: 0 <> k and
A13: k < len p;
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;
end;
take q;
len p in dom q by A1,A6,FINSEQ_3:25;
hence thesis by A2,A4,A6,A10,A5,A11;
end;
notation
let p;
synonym p is nonnegative for p is nonnegative-yielding;
end;
definition
let p;
redefine attr p is nonnegative means :: redefines nonnegative (ENTROPY1, synonym) → nonnegative-yielding (PARTFUN3, definition)
:Def1:
for i st i in dom p holds p.i >= 0;
compatibility
proof
thus p is nonnegative implies
for i st i in dom p holds p.i >= 0 by FUNCT_1:3;
assume
A1: for i st i in dom p holds p.i >= 0;
let r be Real;
assume r in rng p;
then ex j being Nat st j in dom p & r = p.j by FINSEQ_2:10;
hence thesis by A1;
end;
end;
registration
cluster nonnegative for FinSequence of REAL;
existence
proof
take <*1*>;
thus thesis;
end;
end;
theorem Th10:
p is nonnegative & r>=0 implies r*p is nonnegative
proof
assume that
A1: p is nonnegative and
A2: r>=0;
now
let k;
assume k in dom (r*p);
then k in dom p by VALUED_1:def 5;
then
A3: p.k >= 0 by A1;
(r*p).k = r*(p.k) by RVSUM_1:44;
hence (r*p).k >= 0 by A2,A3;
end;
hence thesis;
end;
definition
let p,k;
pred p has_onlyone_value_in k means
k in dom p & for i st i in dom p & i<>k holds p.i=0;
end;
theorem
p has_onlyone_value_in k & i<>k implies p.i=0
proof
assume that
A1: p has_onlyone_value_in k and
A2: i<>k;
per cases;
suppose
not i in dom p;
hence thesis by FUNCT_1:def 2;
end;
suppose
i in dom p;
hence thesis by A1,A2;
end;
end;
theorem Th12:
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
proof
assume that
A1: len p = len q and
A2: p has_onlyone_value_in 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
let i such that
A5: i in dom mlt(p,q) and
A6: i <> k;
thus (mlt(p,q)).i = p.i * q.i by RVSUM_1:59
.= 0*q.i by A2,A3,A5,A6
.= 0;
end;
k in dom mlt(p,q) by A2,A3;
hence thesis by A4,RVSUM_1:59;
end;
theorem Th13:
p has_onlyone_value_in k implies Sum p = p.k
proof
assume that
A1: k in dom p and
A2: for i st i in dom p & i<>k holds p.i=0;
reconsider a=p.k as Element of REAL by XREAL_0:def 1;
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 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 st i in Seg len p2 holds p2.i=0
proof
let i;
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;
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;
end;
A12: now
let j be Nat;
assume
A13: j in dom p2;
hence p2.j =0 by A7,A4
.= (len p2 |->0).j by A4,A13,FINSEQ_2:57;
end;
p1 <> {} by A5,RELAT_1:38,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 st i in Seg len p3 holds p3.i=0
proof
let i;
assume
A19: i in Seg len p3;
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;
end;
A23: now
let j be Nat;
assume
A24: j in dom p3;
hence p3.j =0 by A18,A17
.= (len p3 |->0).j by A17,A24,FINSEQ_2:57;
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 thesis;
end;
theorem Th14:
p is nonnegative implies for k st k in dom p & p.k = Sum p holds
p has_onlyone_value_in k
proof
assume
A1: p is nonnegative;
let k1 being Nat such that
A2: k1 in dom p and
A3: p.k1 =Sum p;
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 as Nat;
A5: k1 >=1 by A2,FINSEQ_3:25;
not ex i st i in dom p & i<>k1 & p.i <> 0
proof
assume ex i st i in dom p & i<>k1 & p.i <> 0;
then consider k2 being 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;
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 as Nat;
A11: k2 >=1 by A6,FINSEQ_3:25;
per cases by A7,XXREAL_0:1;
suppose
A12: k1 > k2;
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 such that
A17: k in dom p2;
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 thesis by A1,A19;
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 be Nat st k in dom p1 holds p1.k >= 0
proof
thus p1.k2 > 0 by A9,A15,A20,FINSEQ_1:def 7;
A21: dom p1 c= dom p by A15,FINSEQ_1:26;
let k be Nat such that
A22: k in dom p1;
p1.k = p.k by A15,A22,FINSEQ_1:def 7;
hence thesis by A1,A22,A21;
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 be 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 thesis by A3;
end;
suppose
A27: k1 < k2;
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 be Nat st k in dom p2 holds p2.k >= 0
proof
let k be Nat such that
A32: k in dom p2;
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 thesis by A1,A34;
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 be Nat st k in dom p1 holds p1.k >= 0
proof
thus p1.k1 = p.k1 by A30,A35,FINSEQ_1:def 7;
A36: dom p1 c= dom p by A30,FINSEQ_1:26;
let k be Nat such that
A37: k in dom p1;
p1.k = p.k by A30,A37,FINSEQ_1:def 7;
hence thesis by A1,A37,A36;
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 be 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 thesis by A3;
end;
end;
hence thesis by A2;
end;
registration
cluster ProbFinS -> non empty nonnegative for FinSequence of REAL;
coherence
by MATRPROB:def 5,RVSUM_1:72;
end;
theorem Th15:
for p being ProbFinS FinSequence of REAL for k st k in dom p & p
.k = 1 holds p has_onlyone_value_in k
proof
let p be ProbFinS FinSequence of REAL;
let k such that
A1: k in dom p and
A2: p.k = 1;
p.k = Sum p by A2,MATRPROB:def 5;
hence thesis by A1,Th14;
end;
theorem Th16:
for i being non zero Nat holds i |-> (1/i) is ProbFinS FinSequence of REAL
proof
let i be non zero Nat;
reconsider i as non zero Element of NAT by ORDINAL1:def 12;
A1: for k being Nat st k in dom (i |-> (1/i))
holds (i |-> (1/i)).k >= 0
proof
let k be Nat;
assume k in dom (i |-> (1/i));
then k in Seg i by FUNCOP_1:13;
hence thesis by FUNCOP_1:7;
end;
reconsider 1i = 1/i as Element of REAL by XREAL_0:def 1;
reconsider ii = i |-> 1i as FinSequence of REAL;
Sum(i |-> (1/i)) = i * (1/i) by RVSUM_1:80
.= 1 by XCMPLX_1:106;
then ii is ProbFinS by A1,MATRPROB:def 5;
hence thesis;
end;
registration
cluster with_sum=1 -> non empty-yielding for Matrix of REAL;
coherence
proof
let M be Matrix of REAL such that
A1: M is with_sum=1;
assume
A2: M is empty-yielding;
per cases by A2,MATRIX_0:def 10;
suppose
len M = 0;
then SumAll M = 0 by MATRPROB:23;
hence thesis by A1,MATRPROB:def 7;
end;
suppose
width M = 0 & len M > 0;
then reconsider M1 = M as Matrix of len M,0,REAL by MATRIX_0:20;
SumAll M1 = 0 by MATRPROB:24;
hence thesis by A1,MATRPROB:def 7;
end;
end;
cluster Joint_Probability -> non empty-yielding for Matrix of REAL;
coherence;
end;
theorem
for M being Matrix of REAL st M = {} holds SumAll M = 0
proof
let M be Matrix of REAL;
assume M = {};
then reconsider M1=M as Matrix of 0,width M,REAL by MATRIX_0:13;
len M1 = 0 by MATRIX_0:22;
hence thesis by MATRPROB:23;
end;
theorem Th18:
for M being Matrix of D holds for i st i in dom M holds dom(M.i)
= Seg width M
proof
let M be Matrix of D;
let i;
assume i in dom M;
hence dom(M.i) = dom Line(M,i) by MATRIX_0:60
.= Seg len Line(M,i) by FINSEQ_1:def 3
.= Seg width M by MATRIX_0:def 7;
end;
theorem Th19:
MR is m-nonnegative iff for i st i in dom MR holds Line(MR,i) is nonnegative
proof
hereby
assume
A1: MR is m-nonnegative;
let i such that
A2: i in dom MR;
now
let k;
assume k in dom Line(MR,i);
then
A3: k in dom (MR.i) by A2,MATRIX_0:60;
then k in Seg width MR by A2,Th18;
then
A4: (Line(MR,i)).k = MR*(i,k) by MATRIX_0:def 7;
[i,k] in Indices MR by A2,A3,MATRPROB:13;
hence (Line(MR,i)).k >= 0 by A1,A4,MATRPROB:def 6;
end;
hence Line(MR,i) is nonnegative;
end;
assume
A5: for i st i in dom MR holds Line(MR,i) is nonnegative;
now
let i,j such that
A6: [i,j] in Indices MR;
A7: j in Seg width MR by A6,MATRPROB:12;
then j in Seg len Line(MR,i) by MATRIX_0: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_0:def 7;
hence MR*(i,j) >= 0 by A8,A9;
end;
hence thesis by MATRPROB:def 6;
end;
begin :: Properties on Transformations between Vector and Matrix
theorem Th20:
for j st j in dom p holds Col(LineVec2Mx p,j) = <*p.j*>
proof
set M = LineVec2Mx p;
let j such that
A1: j in dom p;
A2: dom <*p.j*> = Seg 1 by FINSEQ_1:def 8;
A3: len Col(M,j) = len M by MATRIX_0:def 8;
then len Col(M,j) = 1 by MATRIXR1:def 10;
then
A4: dom Col(M,j) = dom <*p.j*> by A2,FINSEQ_1:def 3;
now
let k be Nat such that
A5: k in dom Col(M,j);
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 M by A3,A5,FINSEQ_3:29;
hence (Col(M,j)).k = M*(k,j) by MATRIX_0:def 8
.= p.j by A1,A7,MATRIXR1:def 10
.= (<*p.j*>).k by A7;
end;
hence thesis by A4,FINSEQ_1:13;
end;
theorem Th21:
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 st [i,j] in
Indices M holds M*(i,j) = p.i * q.j)
proof
let p be non empty FinSequence of REAL;
let q be FinSequence of REAL;
let M be Matrix of REAL;
set M1 = ColVec2Mx p;
set M2 = LineVec2Mx q;
A1: len M1 = len p by MATRIXR1:def 9;
A2: len M2 = 1 by MATRIXR1:def 10;
A3: len p > 0;
then
A4: width M1 = 1 by MATRIXR1:def 9;
A5: width M2 = len q by MATRIXR1:def 10;
hereby
assume
A6: M = M1 * M2;
then
A7: len M = len M1 by A4,A2,MATRPROB:39;
thus len M = len p & width M = len q by A1,A4,A2,A5,A6,MATRPROB:39;
A8: width M = width M2 by A4,A2,A6,MATRPROB:39;
thus for i,j st [i,j] in Indices M holds M*(i,j) = p.i * q.j
proof
let i,j such that
A9: [i,j] in Indices M;
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 M1 by A7,A10,FINSEQ_1:def 3;
then
A13: Line(M1,i) = M1.i by MATRIX_0:60
.= <*p.i*> by A3,A11,MATRIXR1:def 9;
thus M*(i,j) = Line(M1,i) "*" Col(M2,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;
end;
end;
assume that
A14: len M = len p and
A15: width M = len q and
A16: for i,j st [i,j] in Indices M holds M*(i,j) = p.i * q.j;
for i,j st [i,j] in Indices M holds M*(i,j) = Line(M1,i) "*" Col(M2,j)
proof
let i,j such that
A17: [i,j] in Indices M;
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 M1 by A1,A14,FINSEQ_1:def 3;
i in dom p by A14,A19,FINSEQ_1:def 3;
then
A21: <*p.i*> = M1.i by A3,MATRIXR1:def 9
.= Line(M1,i) by A20,MATRIX_0:60;
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(M1,i) "*" Col(M2,j) by A18,A21,Th20;
end;
hence thesis by A1,A4,A2,A5,A14,A15,MATRPROB:39;
end;
theorem Th22:
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 st i in dom M holds
Line(M,i) = p.i * q)
proof
let p be non empty FinSequence of REAL, q be FinSequence of REAL, M be
Matrix of REAL;
set M1 = ColVec2Mx p;
set M2 = LineVec2Mx q;
hereby
assume
A1: M = M1 * M2;
hence len M = len p & width M = len q by Th21;
thus for i st i in dom M holds Line(M,i) = p.i * q
proof
let i;
assume i in dom M;
then
A2: i in Seg len M by FINSEQ_1:def 3;
A3: for j be Nat st j in dom Line(M,i) holds (Line(M,i)).j = (p.i * q).j
proof
let j be Nat;
assume j in dom Line(M,i);
then j in Seg len Line(M,i) by FINSEQ_1:def 3;
then
A4: j in Seg width M by MATRIX_0:def 7;
then
A5: [i,j] in Indices M by A2,MATRPROB:12;
thus (Line(M,i)).j = M*(i,j) by A4,MATRIX_0:def 7
.= p.i * q.j by A1,A5,Th21
.= (p.i * q).j by RVSUM_1:44;
end;
dom Line(M,i) = Seg len Line(M,i) by FINSEQ_1:def 3
.= Seg width M by MATRIX_0: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 thesis by A3,FINSEQ_1:13;
end;
end;
assume that
A6: len M = len p and
A7: width M = len q and
A8: for i st i in dom M holds Line(M,i) = p.i * q;
for i,j st [i,j] in Indices M holds M*(i,j) = p.i * q.j
proof
let i,j such that
A9: [i,j] in Indices M;
A10: i in dom M by A9,MATRPROB:13;
j in Seg width M by A9,MATRPROB:12;
hence M*(i,j) = (Line(M,i)).j by MATRIX_0:def 7
.= (p.i * q).j by A8,A10
.= p.i * q.j by RVSUM_1:44;
end;
hence thesis by A6,A7,Th21;
end;
theorem Th23:
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;
set M = (ColVec2Mx p) * (LineVec2Mx q);
A1: len M = len p by Th22;
A2: LineSum M = p
proof
set M1=LineSum M;
A3: len M1 = len M by MATRPROB:20;
then
A4: dom M1 = dom M by FINSEQ_3:29;
A5: now
let k be Nat such that
A6: k in dom M1;
k in Seg len M by A3,A6,FINSEQ_1:def 3;
hence M1.k = Sum(Line(M,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;
end;
dom M1 = dom p by A1,A3,FINSEQ_3:29;
hence thesis by A5,FINSEQ_1:13;
end;
A7: width M = len q by Th22;
now
let i,j such that
A8: [i,j] in Indices M;
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;
M*(i,j) = p.i * q.j by A8,Th21;
hence M*(i,j) >= 0 by A9,A10;
end;
then
A11: M is m-nonnegative by MATRPROB:def 6;
SumAll M = Sum LineSum M by MATRPROB:def 3
.= 1 by A2,MATRPROB:def 5;
then M is with_sum=1 by MATRPROB:def 7;
hence thesis by A11;
end;
definition
let n;
let MR be Matrix of n,REAL;
attr MR is diagonal means
:Def3:
for i,j st [i,j] in Indices MR & MR*(i,j) <> 0 holds i=j;
end;
registration
let n;
cluster diagonal for Matrix of n,REAL;
existence
proof
deffunc F(set,set) = In(0,REAL);
reconsider n1=n as Nat;
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) = F(i,j)
from MATRIX_0:sch 1;
reconsider M1=M as Matrix of n,REAL;
take M1;
for i,j st [i,j] in Indices M & M*(i,j) <> 0 holds i=j by A1;
hence thesis;
end;
end;
theorem Th24:
for MR being Matrix of n,REAL holds MR is diagonal iff for i st
i in dom MR holds Line(MR,i) has_onlyone_value_in i
proof
let MR be Matrix of n,REAL;
A1: width MR = n by MATRIX_0:24;
len MR = n by MATRIX_0:24;
then
A2: dom MR = Seg width MR by A1,FINSEQ_1:def 3;
hereby
assume
A3: MR is diagonal;
now
let i such that
A4: i in dom MR;
A5: len Line(MR,i) = width MR by MATRIX_0:def 7;
A6: now
let j such that
A7: j in dom Line(MR,i) and
A8: j<>i;
j in dom (MR.i) by A4,A7,MATRIX_0:60;
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_0:def 7
.= 0 by A3,A8,A9;
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;
end;
hence for i st i in dom MR holds Line(MR,i) has_onlyone_value_in i;
end;
assume
A10: for i st i in dom MR holds Line(MR,i) has_onlyone_value_in i;
for i,j st [i,j] in Indices MR & MR*(i,j) <> 0 holds i=j
proof
let i,j such that
A11: [i,j] in Indices MR and
A12: MR*(i,j) <> 0;
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_0:60;
assume
A16: i<>j;
len Line(MR,i) = width MR by MATRIX_0: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_0:def 7
.= 0 by A16,A15,A14;
hence thesis by A12;
end;
hence thesis;
end;
definition
let p;
func Vec2DiagMx p -> diagonal Matrix of len p,REAL means
:Def4:
for j st j in dom p holds it*(j,j) = p.j;
existence
proof
defpred P[Nat,Nat,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:] ex x being
Element of REAL st P[i,j,x]
proof
let i,j be Nat;
assume [i,j] in [:Seg len p, Seg len p:];
A2: p.i in REAL by XREAL_0:def 1;
A3: 0 in REAL by XREAL_0:def 1;
i=j implies P[i,j,p.i];
hence thesis by A2,A3;
end;
consider M being Matrix of len p,REAL such that
A4: for i,j being Nat st [i,j] in Indices M holds P[i,j,M*(i,j)] from
MATRIX_0:sch 2(A1);
for i,j st [i,j] in Indices M & M*(i,j) <> 0 holds i=j by A4;
then reconsider M1 = M as diagonal Matrix of len p,REAL by Def3;
take M1;
len M = len p by MATRIX_0:24;
then
A5: Seg len M1 = dom p by FINSEQ_1:def 3;
width M = len p by MATRIX_0:24;
then
A6: Seg width M1 = dom p by FINSEQ_1:def 3;
for j st j in dom p holds M1*(j,j) = p.j
proof
let j;
assume j in dom p;
then [j,j] in Indices M1 by A6,A5,MATRPROB:12;
hence thesis by A4;
end;
hence thesis;
end;
uniqueness
proof
let M1,M2 be diagonal Matrix of len p,REAL such that
A7: for j st j in dom p holds M1*(j,j) = p.j and
A8: for j st j in dom p holds M2*(j,j) = p.j;
width M1 = len p by MATRIX_0:24;
then
A9: Seg width M1 = dom p by FINSEQ_1:def 3;
A10: Indices M1 = Indices M2 by MATRIX_0:26;
now
let i,j being Nat such that
A11: [i,j] in Indices M1;
reconsider i1=i,j1=j as Nat;
A12: [i1,j1] in Indices M1 by A11;
then
A13: j1 in Seg width M1 by MATRPROB:12;
per cases;
suppose
A14: i=j;
hence M1*(i,j) = p.j by A7,A9,A13
.= M2*(i,j) by A8,A9,A13,A14;
end;
suppose
A15: i<>j;
hence M1*(i,j) = 0 by A12,Def3
.= M2*(i,j) by A10,A12,A15,Def3;
end;
end;
hence thesis by MATRIX_0:27;
end;
end;
theorem Th25:
MR=Vec2DiagMx p iff len MR = len p & width MR = len p & for i st
i in dom MR holds Line(MR,i) has_onlyone_value_in i & Line(MR,i).i=p.i
proof
hereby
assume
A1: MR=Vec2DiagMx p;
then reconsider M1=MR as diagonal Matrix of len p,REAL;
A2: len M1 = len p by MATRIX_0:24;
then
A3: dom MR = dom p by FINSEQ_3:29;
thus len MR = len p & width MR = len p by A2,MATRIX_0:24;
width M1 = len p by MATRIX_0:24;
then
A4: Seg width MR = dom p by FINSEQ_1:def 3;
thus for i st i in dom MR holds Line(MR,i) has_onlyone_value_in i & Line(
MR,i).i=p.i
proof
let i such that
A5: i in dom MR;
A6: Line(M1,i) has_onlyone_value_in i by A5,Th24;
Line(MR,i).i = MR*(i,i) by A3,A4,A5,MATRIX_0:def 7
.= p.i by A1,A3,A5,Def4;
hence thesis by A6;
end;
end;
assume that
A7: len MR = len p and
A8: width MR = len p and
A9: for i st i in dom MR holds Line(MR,i) has_onlyone_value_in i & Line
(MR,i).i=p.i;
reconsider MM = MR as Matrix of len p,REAL by A7,A8,MATRIX_0:51;
for i st i in dom MM holds Line(MM,i) has_onlyone_value_in i by A9;
then reconsider MM as diagonal Matrix of len p,REAL by Th24;
for j st j in dom p holds MM*(j,j) = p.j
proof
A10: dom MM = dom p by A7,FINSEQ_3:29;
let j such that
A11: j in dom p;
Seg width MM = dom p by A8,FINSEQ_1:def 3;
hence MM*(j,j) = Line(MM,j).j by A11,MATRIX_0:def 7
.= p.j by A9,A11,A10;
end;
hence thesis by Def4;
end;
theorem Th26:
len p = len MR implies (MR1 = (Vec2DiagMx p) * MR iff len MR1 =
len p & width MR1 = width MR & for i,j st [i,j] in Indices MR1 holds MR1*(i,j)
= p.i * (MR*(i,j)))
proof
set MM = Vec2DiagMx p;
A1: len MM = len p by Th25;
A2: width MM = len p by Th25;
assume
A3: len p = len MR;
then
A4: dom p = dom MR by FINSEQ_3:29;
hereby
assume
A5: MR1 = MM * MR;
hence len MR1 = len p & width MR1 = width MR by A3,A1,A2,MATRPROB:39;
A6: len MR1 = len MM by A3,A2,A5,MATRPROB:39;
then
A7: dom MR1 = dom MM by FINSEQ_3:29;
A8: dom MR1 = dom p by A1,A6,FINSEQ_3:29;
thus for i,j st [i,j] in Indices MR1 holds MR1*(i,j) = p.i *(MR*(i,j))
proof
let i,j such that
A9: [i,j] in Indices MR1;
i in Seg len MR1 by A9,MATRPROB:12;
then
A10: i in dom MR1 by FINSEQ_1:def 3;
then
A11: Line(MM,i).i=p.i by A7,Th25;
set q = mlt(Line(MM,i),Col(MR,j));
A12: len Line(MM,i) = width MM by MATRIX_0:def 7;
A13: len Col(MR,j) = len MR by MATRIX_0:def 8;
A14: Line(MM,i) has_onlyone_value_in i by A7,A10,Th25;
then
A15: q.i = (Line(MM,i).i) * (Col(MR,j).i ) by A3,A2,A12,A13,Th12;
thus MR1*(i,j) = Line(MM,i) "*" Col(MR,j) by A3,A2,A5,A9,MATRPROB:39
.= Sum q 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_0:def 8;
end;
end;
assume that
A16: len MR1 = len p and
A17: width MR1 = width MR and
A18: for i,j st [i,j] in Indices MR1 holds MR1*(i,j) = p.i*(MR*(i,j));
A19: dom MR1 = dom MM by A1,A16,FINSEQ_3:29;
A20: dom MR = dom MR1 by A3,A16,FINSEQ_3:29;
for i,j st [i,j] in Indices MR1 holds MR1*(i,j) = Line(MM,i) "*" Col(MR ,j)
proof
let i,j such that
A21: [i,j] in Indices MR1;
i in Seg len MR1 by A21,MATRPROB:12;
then
A22: i in dom MR1 by FINSEQ_1:def 3;
then
A23: Line(MM,i).i=p.i by A19,Th25;
set q = mlt(Line(MM,i),Col(MR,j));
A24: len Line(MM,i) = width MM by MATRIX_0:def 7;
A25: len Col(MR,j) = len MR by MATRIX_0:def 8;
A26: Line(MM,i) has_onlyone_value_in i by A19,A22,Th25;
then
A27: q.i = (Line(MM,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_0:def 8
.= Sum q by A3,A2,A26,A23,A24,A25,A27,Th12,Th13
.= Line(MM,i) "*" Col(MR,j) by RVSUM_1:def 16;
end;
hence thesis by A3,A1,A2,A16,A17,MATRPROB:39;
end;
theorem Th27:
len p = len MR implies (MR1 = (Vec2DiagMx p) * MR iff len MR1 =
len p & width MR1 = width MR & for i st i in dom MR1 holds Line(MR1,i) = p.i *
Line(MR,i))
proof
set MM = Vec2DiagMx p;
assume
A1: len p = len MR;
hereby
assume
A2: MR1 = MM * MR;
hence len MR1 = len p & width MR1 = width MR by A1,Th26;
A3: width MR1 = width MR by A1,A2,Th26;
thus for i st i in dom MR1 holds Line(MR1,i) = p.i * Line(MR,i)
proof
let i;
assume i in dom MR1;
then
A4: i in Seg len MR1 by FINSEQ_1:def 3;
A5: for j be Nat st j in dom Line(MR1,i) holds (Line(MR1,i)).j = (p.i *
Line(MR,i)).j
proof
let j be Nat;
assume j in dom Line(MR1,i);
then j in Seg len Line(MR1,i) by FINSEQ_1:def 3;
then
A6: j in Seg width MR1 by MATRIX_0:def 7;
then
A7: [i,j] in Indices MR1 by A4,MATRPROB:12;
thus (Line(MR1,i)).j = MR1*(i,j) by A6,MATRIX_0:def 7
.= p.i*(MR*(i,j)) by A1,A2,A7,Th26
.= p.i*(Line(MR,i).j) by A3,A6,MATRIX_0:def 7
.= (p.i * Line(MR,i)).j by RVSUM_1:44;
end;
dom Line(MR1,i) = Seg len Line(MR1,i) by FINSEQ_1:def 3
.= Seg width MR1 by MATRIX_0:def 7
.= Seg len Line(MR,i) by A3,MATRIX_0:def 7
.= dom Line(MR,i) by FINSEQ_1:def 3
.= dom(p.i * Line(MR,i)) by VALUED_1:def 5;
hence thesis by A5,FINSEQ_1:13;
end;
end;
assume that
A8: len MR1 = len p and
A9: width MR1 = width MR and
A10: for i st i in dom MR1 holds Line(MR1,i) = p.i*Line(MR,i);
for i,j st [i,j] in Indices MR1 holds MR1*(i,j) = p.i*(MR*(i,j))
proof
let i,j such that
A11: [i,j] in Indices MR1;
A12: i in dom MR1 by A11,MATRPROB:13;
A13: j in Seg width MR1 by A11,MATRPROB:12;
hence MR1*(i,j) = (Line(MR1,i)).j by MATRIX_0:def 7
.= (p.i*Line(MR,i)).j by A10,A12
.= p.i * Line(MR,i).j by RVSUM_1:44
.= p.i*(MR*(i,j)) by A9,A13,MATRIX_0:def 7;
end;
hence thesis by A1,A8,A9,Th26;
end;
theorem Th28:
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;
let M be non empty-yielding Conditional_Probability Matrix of REAL;
set M1 = (Vec2DiagMx p) * M;
assume
A1: len p = len M;
then
A2: len M1 = len p by Th26;
A3: LineSum M1 = p
proof
set M2=LineSum M1;
A4: len M2 = len M1 by MATRPROB:20;
then
A5: dom M2 = dom M by A1,A2,FINSEQ_3:29;
A6: dom M2 = dom M1 by A4,FINSEQ_3:29;
A7: now
let k be Nat such that
A8: k in dom M2;
k in Seg len M1 by A4,A8,FINSEQ_1:def 3;
hence M2.k = Sum(Line(M1,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_0:60
.= p.k * 1 by A5,A8,MATRPROB:def 9
.= p.k;
end;
dom M2 = dom p by A2,A4,FINSEQ_3:29;
hence thesis by A7,FINSEQ_1:13;
end;
A9: width M1 = width M by A1,Th26;
now
let i,j such that
A10: [i,j] in Indices M1;
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;
M1*(i,j) = p.i *(M*(i,j)) by A1,A10,Th26;
hence M1*(i,j) >= 0 by A12,A13;
end;
then
A14: M1 is m-nonnegative by MATRPROB:def 6;
SumAll M1 = Sum LineSum M1 by MATRPROB:def 3
.= 1 by A3,MATRPROB:def 5;
then M1 is with_sum=1 by MATRPROB:def 7;
hence thesis by A14;
end;
theorem Th29:
for M being Matrix of D for p being FinSequence of D* st len p =
len M & p.1 = M.1 & (for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1
)) holds for k st k in dom p holds len (p.k) = k * width M
proof
let M be Matrix of D;
let p be FinSequence of D* such that
A1: len p = len M and
A2: p.1 = M.1 and
A3: for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1);
defpred P[Nat] means
$1 >= 1 & $1 <= len M implies len (p.$1) =
$1 * width M;
A4: for n being Nat st P[n] holds P[n + 1]
proof
let n be Nat;
assume that
A5: n >= 1 & n <= len M implies len (p.n) = n * width M;
assume that
A6: n + 1 >= 1 and
A7: n + 1 <= len M;
now
per cases;
suppose
A8: n = 0;
then 1 in dom M by A7,FINSEQ_3:25;
hence thesis by A2,A8,MATRIX_0:36;
end;
suppose
A9: n <> 0;
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_0:36,NAT_1:13,14
.= (n + 1) * width M;
hence thesis;
end;
end;
hence thesis;
end;
A11: P[0];
A12: for n being Nat holds P[n] from NAT_1:sch 2(A11,A4);
let k;
assume k in dom p;
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 thesis by A1,A12,A14;
end;
theorem Th30:
for M being Matrix of D for p being FinSequence of D* st len p =
len M & p.1 = M.1 & (for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1
)) holds for i,j st i in dom p & j in dom p & i <= j holds dom (p.i) c= dom (p.
j)
proof
let M be Matrix of D;
let p be FinSequence of D* such that
A1: len p = len M and
A2: p.1 = M.1 and
A3: for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1);
let i,j such that
A4: i in dom p and
A5: j in dom p and
A6: i <= 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 thesis by FINSEQ_1:def 3;
end;
theorem Th31:
for M being Matrix of D for p being FinSequence of D* st len p =
len M & p.1 = M.1 & (for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1
)) holds len (p.1) = width M & for j st [1,j] in Indices M holds j in dom (p.1)
& (p.1).j = M*(1,j)
proof
let M be Matrix of D;
let p be FinSequence of D* such that
A1: len p = len M and
A2: p.1 = M.1 and
A3: for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1);
per cases;
suppose
A4: len M = 0;
then p = {} by A1;
then p.1 = {} by FUNCT_1:def 2,RELAT_1:38;
hence len(p.1)=width M by A4,MATRIX_0:def 3;
let j;
A5: Seg len M = {} by A4;
assume [1,j] in Indices M;
hence thesis by A5,MATRPROB:12;
end;
suppose
len M > 0;
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;
let j such that
A7: [1,j] in Indices M;
j in Seg width M by A7,MATRPROB:12;
hence thesis by A2,A6,A7,FINSEQ_1:def 3,MATRPROB:14;
end;
end;
theorem Th32:
for M being Matrix of D for p being FinSequence of D* st len p =
len M & (for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1)) holds for
j st j >= 1 & j < len p holds for l st l in dom(p.j) holds (p.j).l = (p.(j+1)).
l
proof
let M be Matrix of D;
let p be FinSequence of D* such that
A1: len p = len M and
A2: for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1);
let j such that
A3: j >= 1 and
A4: j < len p;
A5: p.(j+1) = (p.j) ^ M.(j+1) by A1,A2,A3,A4;
let l;
assume l in dom(p.j);
hence thesis by A5,FINSEQ_1:def 7;
end;
theorem Th33:
for M being Matrix of D for p being FinSequence of D* st len p =
len M & p.1 = M.1 & (for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1
)) holds for i,j st i in dom p & j in dom p & i <= j holds for l st l in dom(p.
i) holds (p.i).l = (p.j).l
proof
let M be Matrix of D;
let p be FinSequence of D* such that
A1: len p = len M and
A2: p.1 = M.1 and
A3: for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1);
defpred P[Nat] means
$1 in dom p implies for i st i in dom p & i
<=$1 holds (for l st l in dom(p.i) holds (p.i).l = (p.$1).l);
A4: for j st P[j] holds P[j+1]
proof
let j such that
A5: j in dom p implies for i st i in dom p & i<=j holds for l st l in
dom(p.i) holds(p.i).l=(p.j).l;
assume
A6: j+1 in dom p;
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 such that
A9: i in dom p and
A10: i<=j+1;
i in Seg len p by A9,FINSEQ_1:def 3;
then
A11: i >= 1 by FINSEQ_1:1;
per cases by A8,NAT_1:13;
suppose
j+1 = 1;
hence thesis by A10,A11,XXREAL_0:1;
end;
suppose
A12: j >= 1;
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 st l in dom(p.i) holds (p.i).l=(p.(j+1)).l
proof
let l such that
A16: l in dom(p.i);
per cases by A10,NAT_1:8;
suppose
A17: i <= j;
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;
end;
suppose
i = j+1;
hence thesis;
end;
end;
end;
end;
A19: P[0];
for j holds P[j] from NAT_1:sch 2(A19,A4);
hence thesis;
end;
theorem Th34:
for M being Matrix of D for p being FinSequence of D* st len p =
len M & p.1 = M.1 & (for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1
)) holds for j st j >= 1 & j < len p holds for l 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 M be Matrix of D;
let p be FinSequence of D* such that
A1: len p = len M and
A2: p.1 = M.1 and
A3: for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1);
let j such that
A4: j >= 1 and
A5: j < len p;
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 such that
A8: l in Seg width M;
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;
p.(j+1) = (p.j) ^ M.(j+1) by A1,A3,A4,A5;
hence thesis by A11,A7,FINSEQ_1:def 7;
end;
theorem Th35:
for M being Matrix of D for p being FinSequence of D* st len p =
len M & p.1 = M.1 & (for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1
)) holds for i,j 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 M be Matrix of D;
let p be FinSequence of D* such that
A1: len p = len M and
A2: p.1 = M.1 and
A3: for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1);
let i,j such that
A4: [i,j] in Indices M;
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;
per cases by A7,XXREAL_0:1;
suppose
A9: i > 1;
then reconsider ii = i - 1 as 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 thesis by A1,A2,A3,A4,A5,A11,A10,Th34,MATRPROB:14;
end;
suppose
i = 1;
hence thesis by A1,A2,A3,A4,Th31;
end;
end;
theorem Th36:
for M being Matrix of D for p being FinSequence of D* st len p =
len M & p.1 = M.1 & (for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1
)) holds for i,j 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 M be Matrix of D;
let p be FinSequence of D* such that
A1: len p = len M and
A2: p.1 = M.1 and
A3: for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1);
let i,j such that
A4: [i,j] in Indices M;
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 thesis by A1,A2,A3,A9,A11,A10,A5,A6,Th33;
end;
theorem Th37:
for M being Matrix of REAL for p being FinSequence of REAL* st (
for k st k >= 1 & k < len M holds p.(k+1)=(p.k) ^ M.(k+1)) holds for k 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;
let p be FinSequence of REAL* such that
A1: for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1);
let k such that
A2: k >= 1 and
A3: k < len M;
p.(k+1) = (p.k) ^ M.(k+1) by A1,A2,A3;
hence thesis by RVSUM_1:75;
end;
theorem Th38:
for M being Matrix of REAL for p being FinSequence of REAL* st
len p = len M & p.1 = M.1 & (for k 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;
let p be FinSequence of REAL* such that
A1: len p = len M and
A2: p.1 = M.1 and
A3: for k st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1);
per cases;
suppose
A4: len M = 0;
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;
end;
suppose
A5: len M > 0;
then
A6: len M >= 1 by NAT_1:14;
set q = LineSum M;
A7: len q = len M by MATRPROB:def 1;
then consider qq being FinSequence of REAL such that
A8: len qq = len q and
A9: qq.1 = q.1 and
A10: for k st 0 <> k & k < len q holds qq.(k+1) = qq.k + q.(k+1) and
A11: Sum q = qq.(len q) 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 be Nat st j in dom qq holds qq.j = (Sum p).j
proof
defpred P[Nat] means $1 in dom qq implies qq.$1 = (Sum p).$1;
A16: for k st P[k] holds P[k+1]
proof
let k such that
A17: P[k];
assume
A18: k+1 in dom qq;
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;
per cases by A22,NAT_1:13;
suppose
A23: k+1 = 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_0:60
.= (Sum p).1 by A2,A15,A26,MATRPROB:def 1;
hence thesis by A23;
end;
suppose
A27: 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 + q.(k+1) by A8,A10,A27,A28
.= Sum(p.k) + q.(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_0:60
.= Sum(p.(k+1)) by A3,A27,A29,Th37
.= (Sum p).(k+1) by A20,MATRPROB:def 1;
hence thesis;
end;
end;
A31: P[0] by A13,FINSEQ_1:1;
for j holds P[j] from NAT_1:sch 2(A31,A16);
hence thesis;
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 q by MATRPROB:def 3
.= (Sum p).(len M) by A11,A32,MATRPROB:def 1
.=Sum(p.(len M)) by A33,MATRPROB:def 1;
end;
end;
definition
let D be non empty set;
let M be Matrix of D;
func Mx2FinS(M) -> FinSequence of D means
:Def5:
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 st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1);
existence
proof
thus len M = 0 implies ex z being FinSequence of D st z = {}
proof
assume len M = 0;
<*>D={};
hence thesis;
end;
thus len M <> 0 implies ex z being FinSequence of D st ex p being
FinSequence of D* st z = p.(len M) & len p = len M & p.1 = M.1 & for k st k >=
1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1)
proof
reconsider M1 = M.1 as Element of D* by FINSEQ_1:def 11;
defpred P[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;
A2: for n being Nat st 1 <= n & n < len M for x being Element
of D* ex y being Element of D* st P[n,x,y]
proof
let n be Nat such that
1 <= n and
A3: n < len M;
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*;
set y = x ^ p1;
reconsider y as Element of D* by FINSEQ_1:def 11;
take y, p1, x;
thus thesis;
end;
ex p being FinSequence of D* st len p = len M & (p.1 = M1 or len M =
0) & for n being Nat st 1 <= n & n < len M holds P[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 Nat st 1 <= n & n < len M holds P[n,p.n, p.(n+1)];
reconsider z = p.len M as FinSequence of D;
take z;
for n being Nat st 1 <= n & n < len M holds p.(n+1)= (p.
n) ^ M.(n+1)
proof
let n be Nat such that
A8: 1 <= n and
A9: n < len M;
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 thesis;
end;
hence thesis by A1,A5,A6;
end;
end;
uniqueness
proof
let z1,z2 be FinSequence of D;
thus len M = 0 & z1 ={} & z2={} implies z1=z2;
assume len M <> 0;
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 st k >= 1 & k < len M holds p1.(k+1) = (p1.k) ^ M.(k+1);
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 st k >= 1 & k < len M holds p2.(k+1) = (p2.k) ^ M.(k+1);
for k st k >= 1 & k <= len M holds p1.k = p2.k
proof
defpred P[Nat] means
$1 >= 1 & $1 <= len M implies p1.$1 = p2.$1;
A17: for n being Nat st P[n] holds P[n + 1]
proof
let n being Nat;
assume that
A18: n >= 1 & n <= len M implies p1.n = p2.n;
assume that
n + 1 >= 1 and
A19: n + 1 <= len M;
now
per cases;
suppose
n = 0;
hence thesis by A12,A15;
end;
suppose
A20: n <> 0;
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;
end;
end;
hence thesis;
end;
A22: P[0];
thus for n being Nat holds P[n] from NAT_1:sch 2(A22, A17);
end;
hence thesis by A10,A11,A14;
end;
consistency;
end;
theorem Th39:
for M being Matrix of D holds len Mx2FinS(M) = len M * width M
proof
let M be Matrix of D;
per cases;
suppose
A1: len M = 0;
then Mx2FinS(M) = {} by Def5;
hence thesis by A1;
end;
suppose
A2: len M > 0;
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 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 thesis by A3,A4,A5,A6,Th29;
end;
end;
theorem Th40:
for M being Matrix of D for i,j 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 M be Matrix of D;
let i,j such that
A1: [i,j] in Indices M;
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 st k >= 1 & k < len M holds p.(k+1) = (p.k) ^ M.(k+1) by
Def5;
hence thesis by A1,Th36;
end;
theorem Th41:
for M being Matrix of D for k,l 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 M be Matrix of D;
let k,l such that
A1: k in dom(Mx2FinS(M)) and
A2: l = k - 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: ii <= len M by NAT_1:13;
l mod width M < width M by A7,NAT_D:1;
then
A10: jj <= width M by NAT_1:13;
jj >= 1 by NAT_1:11;
then
A11: jj in Seg width M by A10,FINSEQ_1:1;
ii >= 1 by NAT_1:11;
then ii in Seg len M by A9,FINSEQ_1:1;
hence [ii,jj] in Indices M by A11,MATRPROB:12;
then M*(ii,jj) = (Mx2FinS(M)).((ii-1) * (width M) + jj) by Th40
.= (Mx2FinS(M)).k by A2,A8;
hence thesis;
end;
theorem Th42:
SumAll MR = Sum Mx2FinS MR
proof
per cases;
suppose
A1: len MR = 0;
hence Sum Mx2FinS MR = 0 by Def5,RVSUM_1:72
.= SumAll MR by A1,MATRPROB:23;
end;
suppose
len MR > 0;
then
ex p being FinSequence of REAL* st Mx2FinS(MR) = p.(len MR) & len p
= len MR & p.1 = MR.1 & for k st k >= 1 & k < len MR holds p.(k+ 1) = (p.k) ^
MR.(k+1) by Def5;
hence thesis by Th38;
end;
end;
theorem Th43:
MR is m-nonnegative iff Mx2FinS(MR) is nonnegative
proof
hereby
assume
A1: MR is m-nonnegative;
for k st k in dom(Mx2FinS(MR)) holds (Mx2FinS(MR)).k >= 0
proof
let i such that
A2: i in dom Mx2FinS(MR);
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 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 thesis by A1,A3,MATRPROB:def 6;
end;
hence Mx2FinS(MR) is nonnegative;
end;
assume
A4: Mx2FinS(MR) is nonnegative;
now
let i,j such that
A5: [i,j] in Indices MR;
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;
end;
hence thesis by MATRPROB:def 6;
end;
theorem Th44:
MR is Joint_Probability iff Mx2FinS(MR) is ProbFinS
proof
hereby
assume MR is Joint_Probability;
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 st i in dom Mx2FinS(MR) holds (Mx2FinS(MR)).i >= 0;
Sum Mx2FinS(MR) = SumAll MR by Th42
.= 1 by A1,MATRPROB:def 7;
hence Mx2FinS(MR) is ProbFinS by A2,MATRPROB:def 5;
end;
assume Mx2FinS(MR) is ProbFinS;
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 thesis by A3;
end;
theorem Th45:
for p,q being ProbFinS FinSequence of REAL holds Mx2FinS((
ColVec2Mx p) * (LineVec2Mx q)) is ProbFinS
by Th23,Th44;
theorem
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
by Th28,Th44;
begin :: Information Entropy
definition
let a be Real; let p;
assume that
A1: p is nonnegative;
func FinSeq_log(a,p) -> FinSequence of REAL means
:Def6:
len it = len p &
for k be 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
proof
defpred P[Nat,set] means (p.$1 > 0 implies $2 = log(a,p.$1)) & (p.$1 = 0
implies $2 = 0);
A2: for k be Nat st k in Seg len p ex x being Element of REAL st P[k,x]
proof
let k be Nat;
assume k in Seg len p;
then
A3: k in dom p by FINSEQ_1:def 3;
per cases by A1,A3;
suppose
A4: p.k>0;
reconsider ll= log(a,p.k) as Element of REAL by XREAL_0:def 1;
take ll;
thus thesis by A4;
end;
suppose
A5: p.k=0;
take In(0,REAL);
thus thesis by A5;
end;
end;
consider pp being FinSequence of REAL such that
A6: dom pp = Seg len p & for k be Nat st k in Seg len p holds P[k,pp.k
] from FINSEQ_1:sch 5(A2);
len pp = len p by A6,FINSEQ_1:def 3;
hence thesis by A6;
end;
uniqueness
proof
let p1,p2 be FinSequence of REAL such that
A7: len p1 = len p and
A8: for k be 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 be Nat st k in dom p2 holds (p.k > 0 implies p2.k = log(a,p
.k )) & (p.k = 0 implies p2.k = 0);
A11: for k be Nat st k in dom p1 holds p1.k = p2.k
proof
let k be Nat;
assume
A12: k in dom p1;
then
A13: k in dom p by A7,FINSEQ_3:29;
A14: k in dom p2 by A7,A9,A12,FINSEQ_3:29;
per cases by A1,A13;
suppose
A15: p.k>0;
hence p1.k = log(a,p.k) by A8,A12
.= p2.k by A10,A14,A15;
end;
suppose
A16: p.k=0;
hence p1.k = 0 by A8,A12
.= p2.k by A10,A14,A16;
end;
end;
dom p1 = Seg len p2 by A7,A9,FINSEQ_1:def 3
.= dom p2 by FINSEQ_1:def 3;
hence thesis by A11,FINSEQ_1:13;
end;
end;
definition
let p;
func Infor_FinSeq_of p -> FinSequence of REAL equals
mlt(p,FinSeq_log(2,p));
correctness;
end;
theorem Th47:
for p being nonnegative FinSequence of REAL for q holds q =
Infor_FinSeq_of p iff len q = len p & for k st k in dom q holds q.k = p.k * log
(2,p.k)
proof
let p be nonnegative FinSequence of REAL;
let q;
set pp = mlt(p,FinSeq_log(2,p));
A1: len p = len FinSeq_log(2,p) by Def6;
then
A2: len pp = len p by MATRPROB:30;
hereby
assume
A3: q = Infor_FinSeq_of p;
thus len q = len p & for k st k in dom q holds q.k = p.k * log(2,p.k)
proof
A4: dom p = dom q by A2,A3,FINSEQ_3:29;
thus len q = len p by A1,A3,MATRPROB:30;
let k such that
A5: k in dom q;
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;
per cases by A5,A4,Def1;
suppose
p.k=0;
hence thesis by A6;
end;
suppose
p.k>0;
hence thesis by A6,A7,Def6;
end;
end;
end;
assume that
A8: len q = len p and
A9: for k st k in dom q holds q.k = p.k * log(2,p.k);
A10: dom q = dom p by A8,FINSEQ_3:29;
len q = len pp by A1,A8,MATRPROB:30;
then
A11: dom q = dom pp by FINSEQ_3:29;
A12: dom p = dom FinSeq_log(2,p) by A1,FINSEQ_3:29;
now
let k be Nat such that
A13: k in dom q;
A14: pp.k = p.k * (FinSeq_log(2,p)).k by RVSUM_1:59;
per cases by A10,A13,Def1;
suppose
A15: p.k=0;
hence q.k = 0 * log(2,p.k) by A9,A13
.= pp.k by A14,A15;
end;
suppose
p.k>0;
then (FinSeq_log(2,p)).k = log(2,p.k) by A12,A10,A13,Def6;
hence pp.k = p.k * log(2,p.k) by RVSUM_1:59
.= q.k by A9,A13;
end;
end;
hence thesis by A11,FINSEQ_1:13;
end;
theorem Th48:
for p being nonnegative FinSequence of REAL for k 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;
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 such that
A2: k in dom p;
hereby
assume p.k=0;
hence (Infor_FinSeq_of p).k = 0*log(2,p.k) by A2,A1,Th47
.=0;
end;
thus thesis by A2,A1,Th47;
end;
theorem
for p being nonnegative FinSequence of REAL for q holds q = -
Infor_FinSeq_of p iff (len q = len p & for k st k in dom q holds q.k = p.k *
log(2,1/(p.k)))
proof
let p be nonnegative FinSequence of REAL, q;
set p0 = Infor_FinSeq_of p;
hereby
assume
A1: q = -p0;
then
A2: dom q = dom p0 by VALUED_1:8;
A3: Seg len q = dom q by FINSEQ_1:def 3
.= Seg len p0 by A2,FINSEQ_1:def 3
.= Seg len p by Th47;
for k st k in dom q holds q.k = p.k * log(2,1/(p.k))
proof
let k such that
A4: k in dom q;
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 = -p0.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));
per cases by A5,Def1;
suppose
A8: p.k=0;
then p0.k=0 by A5,Th48;
hence thesis by A6,A8;
end;
suppose
p.k>0;
hence thesis by A7,Th5;
end;
end;
hence len q = len p & for k st k in dom q holds q.k = p.k * log(2,1/(p.k))
by A3,FINSEQ_1:6;
end;
assume that
A9: len q = len p and
A10: for k st k in dom q holds q.k = p.k * log(2,1/(p.k));
A11: dom q = Seg len q by FINSEQ_1:def 3
.= Seg len p0 by A9,Th47
.= dom p0 by FINSEQ_1:def 3;
A12: for k be Nat st k in dom q holds (-p0).k = q.k
proof
let k be Nat;
assume
A13: k in dom q;
then k in Seg len p by A9,FINSEQ_1:def 3;
then
A14: k in dom p by FINSEQ_1:def 3;
per cases by A14,Def1;
suppose
A15: p.k = 0;
thus (-p0).k = -p0.k by RVSUM_1:17
.= -0 by A14,A15,Th48
.= p.k * log(2,1/(p.k)) by A15
.= q.k by A10,A13;
end;
suppose
A16: p.k > 0;
thus (-p0).k = -p0.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;
end;
end;
dom q = dom -p0 by A11,VALUED_1:8;
hence thesis by A12,FINSEQ_1:13;
end;
theorem Th50:
for p being nonnegative FinSequence of REAL st r1>=0 & r2>=0
holds for i 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 p be nonnegative FinSequence of REAL such that
A1: r1>=0 and
A2: r2>=0;
let i such that
A3: i in dom p and
A4: p.i = r1*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;
end;
theorem Th51:
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 p be nonnegative FinSequence of REAL such that
A1: r>=0;
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 qq by Th47;
then
A6: dom q = dom qq by FINSEQ_3:29;
A7: dom FinSeq_log(2,p) = dom p by A4,FINSEQ_3:29;
now
let k be Nat such that
A8: k in dom qq;
A9: q.k = r*p.k by RVSUM_1:44;
p.k>=0 by A2,A6,A8,Def1;
then
A10: qq.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;
per cases by A2,A6,A8,Def1;
suppose
p.k>0;
then
qq.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 qq.k = ((r*log(2,r)*p)+(r*mlt(p,FinSeq_log(2,p)))).k by A2,A6,A3,A5
,A8,VALUED_1:def 1;
end;
suppose
p.k=0;
hence qq.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;
end;
end;
hence thesis by A2,A6,A3,A5,FINSEQ_1:13;
end;
theorem Th52:
for p being non empty ProbFinS FinSequence of REAL for k st k in
dom p holds (Infor_FinSeq_of p).k <= 0
proof
let p be non empty ProbFinS FinSequence of REAL, k such that
A1: k in dom p;
per cases by A1,MATRPROB:53,def 5;
suppose
p.k = 0;
hence thesis by A1,Th48;
end;
suppose
A2: p.k > 0 & p.k <= 1;
then
A3: (Infor_FinSeq_of p).k = p.k * log(2,p.k) by A1,Th48;
thus (Infor_FinSeq_of p).k <= 0
proof
A4: log(2,1) = 0 by POWER:51;
per cases by A2,XXREAL_0:1;
suppose
p.k < 1;
then log(2,p.k) < 0 by A2,A4,POWER:57;
hence thesis by A2,A3;
end;
suppose
p.k = 1;
hence thesis by A3,POWER:51;
end;
end;
end;
end;
definition
let MR;
assume
A1: MR is m-nonnegative;
func Infor_FinSeq_of MR -> Matrix of REAL means
:Def8:
len it = len MR &
width it = width MR & for k st k in dom it holds it.k=mlt(Line(MR,k),FinSeq_log
(2,Line(MR,k)));
existence
proof
deffunc F(Nat) = mlt(Line(MR,$1),FinSeq_log(2,Line(MR,$1)));
consider p be FinSequence such that
A2: len p = len MR and
A3: for k be Nat st k in dom p holds p.k = F(k) from FINSEQ_1:sch 2;
A4: rng p c= REAL*
proof
let x be object;
assume x in rng p;
then consider j be 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 thesis by A6,FINSEQ_1:def 11;
end;
A7: for x being object
st x in rng p ex q being FinSequence st q=x & len q = width MR
proof
let x be object;
assume x in rng p;
then consider j be 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_0: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 thesis by A11;
end;
then reconsider p as Matrix of REAL by A4,FINSEQ_1:def 4,MATRIX_0:def 1;
take p;
width p = width MR
proof
per cases;
suppose
A12: len MR = 0;
then width p = 0 by A2,MATRIX_0:def 3;
hence thesis by A12,MATRIX_0:def 3;
end;
suppose
A13: len MR > 0;
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 thesis by A2,A13,A15,MATRIX_0:def 3;
end;
end;
hence thesis by A2,A3;
end;
uniqueness
proof
let M1,M2 be Matrix of REAL such that
A16: len M1 = len MR and
width M1 = width MR and
A17: for k 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 st k in dom M2 holds M2.k = mlt(Line(MR,k),FinSeq_log(2,
Line( MR,k)));
A20: dom M1 = dom M2 by A16,A18,FINSEQ_3:29;
now
let k be Nat such that
A21: k in dom M1;
thus M1.k = mlt(Line(MR,k),FinSeq_log(2,Line(MR,k))) by A17,A21
.= M2.k by A19,A20,A21;
end;
hence thesis by A20,FINSEQ_1:13;
end;
end;
theorem Th53:
for M being m-nonnegative Matrix of REAL for k 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;
set M1 = Infor_FinSeq_of M;
len M1 = len M by Def8;
then
A1: dom M1 = dom M by FINSEQ_3:29;
let k such that
A2: k in dom M;
thus Line(M1,k) = M1.k by A2,A1,MATRIX_0:60
.= Infor_FinSeq_of Line(M,k) by A2,A1,Def8;
end;
theorem Th54:
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 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;
let M1 be Matrix of REAL;
hereby
assume
A1: M1 = Infor_FinSeq_of M;
then
A2: width M1 = width M by Def8;
A3: len M1 = len M by A1,Def8;
now
let i,j such that
A4: [i,j] in Indices M1;
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_0: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_0:def 7;
thus M1*(i,j) = Line(M1,i).j by A5,MATRIX_0:def 7
.= (Infor_FinSeq_of p).j by A1,A6,Th53
.= M*(i,j)*log(2,M*(i,j)) by A9,A8,Th47;
end;
hence len M1 = len M & width M1 = width M & for i,j st [i,j] in Indices M1
holds M1*(i,j)=M*(i,j)*log(2,M*(i,j)) by A1,Def8;
end;
assume that
A10: len M1 = len M and
A11: width M1 = width M and
A12: for i,j st [i,j] in Indices M1 holds M1*(i,j)=M*(i,j)*log(2,M*(i,j) );
A13: dom M1 = dom M by A10,FINSEQ_3:29;
for k st k in dom M1 holds M1.k = mlt(Line(M,k),FinSeq_log(2,Line(M,k)) )
proof
let k such that
A14: k in dom M1;
A15: len (M1.k) = width M1 by A14,MATRIX_0:36;
reconsider p=Line(M,k) as nonnegative FinSequence of REAL by A13,A14,Th19;
A16: len p = width M by MATRIX_0: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
let j be Nat such that
A20: j in dom (M1.k);
A21: j in Seg width M by A11,A15,A20,FINSEQ_1:def 3;
then
A22: p.j=M*(k,j) by MATRIX_0: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_0:def 7;
A25: j in dom FinSeq_log(2,p) by A16,A17,A21,FINSEQ_1:def 3;
A26: [k,j] in Indices M1 by A14,A20,MATRPROB:13;
then
A27: (M1.k).j = M1*(k,j) by MATRPROB:14
.= M*(k,j)*log(2,M*(k,j)) by A12,A26;
per cases by A23,MATRPROB:def 6;
suppose
M*(k,j)=0;
hence (M1.k).j = (mlt(p,FinSeq_log(2,p))).j by A27,A24;
end;
suppose
M*(k,j)>0;
hence (mlt(p,FinSeq_log(2,p))).j = (M1.k).j by A25,A27,A22,A24,Def6;
end;
end;
hence thesis by A18,FINSEQ_1:13;
end;
hence thesis by A10,A11,Def8;
end;
definition
let p being FinSequence of REAL;
func Entropy p -> Real equals
-Sum Infor_FinSeq_of p;
correctness;
end;
theorem
for p being non empty ProbFinS FinSequence of REAL holds Entropy p >= 0
proof
let p be non empty ProbFinS FinSequence of REAL;
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 be Nat st k in dom p1 holds p1.k >= 0
proof
let k be Nat;
assume k in dom p1;
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 thesis by RVSUM_1:17;
end;
Entropy p = Sum p1 by RVSUM_1:88;
hence thesis by A2,RVSUM_1:84;
end;
theorem
for p being non empty ProbFinS FinSequence of REAL st ex k st k in dom
p & p.k = 1 holds Entropy p = 0
proof
let p be non empty ProbFinS FinSequence of REAL;
assume ex k st k in dom p & p.k = 1;
then consider k1 being Nat such that
A1: k1 in dom p and
A2: p.k1 = 1;
set q = Infor_FinSeq_of p;
len q = len p by Th47;
then
A3: dom q = dom p by FINSEQ_3:29;
A4: p has_onlyone_value_in k1 by A1,A2,Th15;
for k st k in dom q holds q.k = 0
proof
let k such that
A5: k in dom q;
per cases;
suppose
k=k1;
hence q.k = 1*log(2,1) by A2,A5,Th47
.= 0 by POWER:51;
end;
suppose
k<>k1;
then
A6: p.k = 0 by A4,A3,A5;
thus q.k = p.k * log(2,p.k) by A5,Th47
.= 0 by A6;
end;
end;
then for x being object st x in dom q holds q.x = 0;
then q = dom q --> 0 by FUNCOP_1:11;
then q = len q |-> 0 by FINSEQ_1:def 3;
then Sum q = 0 by RVSUM_1:81;
hence thesis;
end;
theorem Th57:
for p,q being non empty ProbFinS FinSequence of REAL, pp,qq
being FinSequence of REAL st len p = len q & len pp = len p & len qq = len q &
(for k 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 st k in dom p holds p.k=q.k)
iff Sum pp = Sum qq) & ((ex k st k in dom p & p.k<>q.k) iff Sum pp < Sum qq)
proof
let p,q be non empty ProbFinS FinSequence of REAL, pp,qq be FinSequence of
REAL such that
A1: len p = len q and
A2: len pp = len p and
A3: len qq = len q and
A4: for k 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);
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 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 st k in dom p holds p1.k = p.k*log(2,number_e)*log(number_e,(q.k)
/(p.k))
proof
let k such that
A11: k in dom p;
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 p1.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;
end;
set n = len p;
deffunc F(Nat) = In(p.$1*log(2,number_e)*(((q.$1)/(p.$1))-1),REAL);
consider p2 be FinSequence of REAL such that
A18: len p2 = n and
A19: for k be Nat st k in dom p2 holds p2.k = F(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 p1 = len p by A1,A2,A3,RVSUM_1:116;
then
A22: p1 is Element of n-tuples_on REAL by FINSEQ_2:92;
A23: dom p2 = Seg n by A18,FINSEQ_1:def 3;
A24: len(q-p)=len q by A1,RVSUM_1:116;
A25: for k st k in dom q holds (q-p).k=q.k-p.k
proof
let k;
assume k in dom q;
then k in dom(q-p) by A24,FINSEQ_3:29;
hence thesis by VALUED_1:13;
end;
A26: dom p = Seg n by FINSEQ_1:def 3;
A27: dom(q-p)=dom p2 by A1,A18,A24,FINSEQ_3:29;
A28: for k be Nat st k in dom p2 holds p2.k=(log(2,number_e)*(q-p)).k
proof
let k be Nat such that
A29: k in dom p2;
A30: p.k>0 by A4,A20,A29;
thus p2.k = F(k) 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;
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 be Nat st k in Seg n holds p1.k <= p2.k
proof
let k be Nat such that
A34: k in Seg n;
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 p1.k <= F(k) by A10,A35;
hence thesis by A19,A23,A34;
end;
A37: p2 is Element of n-tuples_on REAL by A18,FINSEQ_2:92;
hence Sum pp <= Sum qq by A8,A33,A22,A31,RVSUM_1:82,XREAL_1:50;
A38: (ex k st k in Seg n & p.k<>q.k) implies Sum pp < Sum qq
proof
assume ex k st k in Seg n & p.k<>q.k;
then consider k1 being Nat such that
A39: k1 in Seg n 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 p1.k1 < F(k1) by A10,A41;
then p1.k1 < p2.k1 by A19,A23,A39;
then Sum pp - Sum qq < 0 by A8,A33,A22,A37,A31,A39,RVSUM_1:83;
hence thesis by XREAL_1:48;
end;
A45: dom p1 = dom p2 by A21,A18,FINSEQ_3:29;
thus (for k st k in dom p holds p.k=q.k) iff Sum pp = Sum qq
proof
hereby
assume
A46: for k st k in dom p holds p.k=q.k;
for k be Nat st k in dom p holds p1.k = p2.k
proof
let k be Nat such that
A47: k in dom p;
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: p1.k = F(k) by A10,A47;
k in Seg n by A47,FINSEQ_1:def 3;
hence thesis by A19,A23,A49;
end;
then Sum p1 = 0 by A20,A45,A31,FINSEQ_1:13;
hence Sum pp = Sum qq by A8;
end;
assume
A50: Sum pp = Sum qq;
assume not for k st k in dom p holds p.k=q.k;
hence contradiction by A26,A38,A50;
end;
hence thesis by A26,A38;
end;
theorem
for p being non empty ProbFinS FinSequence of REAL st (for k st k in
dom p holds p.k>0) holds Entropy p <= log(2,len p) & ((for k st k in dom p
holds p.k=1/(len p)) iff Entropy p=log(2,len p)) & ((ex k st k in dom p & p.k<>
1/(len p)) iff Entropy p<log(2,len p))
proof
let p be non empty ProbFinS FinSequence of REAL such that
A1: for k st k in dom p holds p.k > 0;
set p3 = - Infor_FinSeq_of p;
set n = len p;
reconsider n1=n as non zero Element of NAT;
reconsider nn=1/n1 as Element of REAL by XREAL_0:def 1;
reconsider p1 = n |-> nn as FinSequence of REAL;
deffunc F(Nat) = In(-p.$1*log(2,p1.$1),REAL);
consider p2 be FinSequence of REAL such that
A2: len p2 = n and
A3: for k be Nat st k in dom p2 holds p2.k = F(k) from FINSEQ_2:sch 1;
A4: dom p2 = Seg n by A2,FINSEQ_1:def 3;
A5: for k be Nat st k in dom p2 holds p2.k = ((-log(2,1/n1))*p).k
proof
let k be Nat such that
A6: k in dom p2;
thus p2.k = F(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;
end;
A7: len p1 = n by CARD_1:def 7;
A8: dom Infor_FinSeq_of p = Seg len Infor_FinSeq_of p by FINSEQ_1:def 3
.= Seg n by Th47;
A9: len p3 = n & for k st k in Seg n holds p3.k=-p.k*log(2,p.k)
proof
dom p3 = Seg n by A8,VALUED_1:8;
hence len p3 = n by FINSEQ_1:def 3;
hereby
let k such that
A10: k in Seg n;
thus p3.k = -((Infor_FinSeq_of p).k) by RVSUM_1:17
.= -p.k*log(2,p.k) by A8,A10,Th47;
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,n);
A12: p1 is non empty ProbFinS FinSequence of REAL by Th16;
A13: dom p = Seg len p by FINSEQ_1:def 3;
A14: for k st k in dom p holds p.k > 0 & p1.k > 0 & p3.k=-p.k*log(2,p.k) &
p2.k = -p.k*log(2,p1.k)
proof let k;
assume
A15: k in dom p;
hence p.k > 0 & p1.k > 0 by A1,FINSEQ_2:57,A13;
thus p3.k=-p.k*log(2,p.k) by A15,A9,A13;
p2.k = F(k) by A15,A3,A4,A13;
hence thesis;
end;
A16: Sum p3 = Entropy p by RVSUM_1:88;
hence Entropy p <= log(2,len p) by A7,A12,A2,A9,A14,A11,Th57;
thus (for k st k in dom p holds p.k=1/(len p)) iff Entropy p=log(2,len p)
proof
hereby
assume
A17: for k st k in dom p holds p.k=1/(len p);
now
let k such that
A18: k in dom p;
thus p.k = 1/n by A17,A18
.= p1.k by A13,A18,FINSEQ_2:57;
end;
hence Entropy p=log(2,n) by A7,A12,A2,A9,A14,A16,A11,Th57;
end;
assume
A19: Entropy p=log(2,n);
hereby
let k;
assume
A20: k in dom p;
hence p.k = p1.k by A7,A12,A2,A9,A14,A16,A11,A19,Th57
.= 1/n by A13,A20,FINSEQ_2:57;
end;
end;
A21: (for k st k in dom p holds p.k=p1.k) iff Sum p3 = Sum p2 by A7,A12,A2,A9
,A14,Th57;
thus (ex k st k in dom p & p.k<>1/(len p)) iff Entropy p<log(2,len p)
proof
hereby
assume ex k st k in dom p & p.k<>1/(len p);
then consider k1 being Nat such that
A22: k1 in dom p and
A23: p.k1<>1/n;
p1.k1 <> p.k1 by A13,A22,A23,FINSEQ_2:57;
hence Entropy p<log(2,n) by A7,A12,A2,A9,A14,A16,A11,A22,Th57;
end;
assume Entropy p<log(2,n);
then consider k1 being Nat such that
A24: k1 in dom p and
A25: p.k1<>p1.k1 by A21,A11,RVSUM_1:88;
p1.k1 = 1/n by A13,A24,FINSEQ_2:57;
hence thesis by A24,A25;
end;
end;
theorem Th59:
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;
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 MM = width M by Def8;
len MM = len M by Def8;
then
A3: len qq = len M * width M by A2,Th39;
len pp = len p by Th47;
then
A4: dom qq = dom pp by A1,A3,FINSEQ_3:29;
A5: dom qq = dom p by A1,A3,FINSEQ_3:29;
now
let k be Nat such that
A6: k in dom qq;
k in Seg len qq by A6,FINSEQ_1:def 3;
then k >= 1 by FINSEQ_1:1;
then reconsider l = k - 1 as Nat by NAT_1:21;
set jj=(l mod width MM)+1;
set ii=(l div width MM)+1;
A7: [ii,jj] in Indices MM by A6,Th41;
A8: qq.k = MM*(ii,jj) by A6,Th41;
A9: p.k = M*(ii,jj) by A2,A5,A6,Th41;
thus pp.k = p.k *log(2,p.k) by A4,A6,Th47
.= qq.k by A7,A8,A9,Th54;
end;
hence thesis by A4,FINSEQ_1:13;
end;
theorem Th60:
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;
set p1= Infor_FinSeq_of p;
set p2= (Sum Infor_FinSeq_of q)*p;
A1: len p1 = len p by Th47;
dom p2 = dom p by VALUED_1:def 5;
then
A2: len p1 = len p2 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 such that
A4: M=(ColVec2Mx p)*(LineVec2Mx q);
reconsider M as Joint_Probability Matrix of REAL by A4,Th23;
set M1 = Infor_FinSeq_of M;
set L = LineSum M1;
A5: len L = len M1 by MATRPROB:def 1;
then
A6: dom L = dom M1 by FINSEQ_3:29;
A7: len M1 = len M by Def8;
then
A8: dom M1 = 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
let k such that
A12: k in dom L;
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 L.k = Sum(M1.k) by A12,MATRPROB:def 1
.= Sum(Line(M1,k)) by A6,A12,MATRIX_0:60
.= 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;
end;
A17: dom p1 = dom L by A9,A7,A5,A1,FINSEQ_3:29;
now
let k such that
A18: k in dom p1;
thus L.k = p.k*log(2,p.k)+p.k*Sum Infor_FinSeq_of q by A11,A17,A18
.= p1.k + p.k*Sum Infor_FinSeq_of q by A18,Th47
.= p1.k + p2.k by RVSUM_1:44;
end;
then Sum L = Sum p1 + Sum p2 by A9,A7,A5,A1,A2,Th7
.= Sum p1 + (Sum Infor_FinSeq_of q)*Sum p by RVSUM_1:87
.= Sum p1 + (Sum Infor_FinSeq_of q)*1 by MATRPROB:def 5
.= Sum Infor_FinSeq_of p+Sum Infor_FinSeq_of q;
hence thesis by MATRPROB:def 3;
end;
definition
let MR;
func Entropy_of_Joint_Prob MR -> Real equals
Entropy Mx2FinS MR;
coherence;
end;
theorem
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;
set M = (ColVec2Mx p) * (LineVec2Mx q);
reconsider M as Joint_Probability Matrix of REAL by Th23;
set pp = Mx2FinS((ColVec2Mx p) * (LineVec2Mx q));
reconsider pp 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 thesis;
end;
definition
let MR;
func Entropy_of_Cond_Prob MR -> FinSequence of REAL means
:Def11:
len it = len MR & for k st k in dom it holds it.k = Entropy Line(MR,k);
existence
proof
deffunc F(Nat) = In(Entropy Line(MR,$1),REAL);
consider p be FinSequence of REAL such that
A1: len p = len MR and
A2: for k be Nat st k in dom p holds p.k = F(k) from FINSEQ_2:sch 1;
take p;
thus len p = len MR by A1;
let k;
assume k in dom p;
then p.k = F(k) by A2;
hence thesis;
end;
uniqueness
proof
let p1,p2 be FinSequence of REAL such that
A3: len p1 = len MR and
A4: for k st k in dom p1 holds p1.k = Entropy Line(MR,k) and
A5: len p2 = len MR and
A6: for k st k in dom p2 holds p2.k = Entropy Line(MR,k);
A7: dom p1 = dom p2 by A3,A5,FINSEQ_3:29;
now
let k be Nat such that
A8: k in dom p1;
thus p1.k = Entropy Line(MR,k) by A4,A8
.= p2.k by A6,A7,A8;
end;
hence thesis by A7,FINSEQ_1:13;
end;
end;
theorem Th62:
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 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;
let p be FinSequence of REAL;
A1: len Infor_FinSeq_of M = len M by Def8;
hereby
assume
A2: p = Entropy_of_Cond_Prob M;
then
A3: len p = len M by Def11;
then
A4: dom p = dom M by FINSEQ_3:29;
now
let k such that
A5: k in dom p;
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_0:60;
end;
hence len p = len M & for k st k in dom p holds p.k = -Sum ((
Infor_FinSeq_of M).k) by A2,Def11;
end;
assume that
A7: len p = len M and
A8: for k st k in dom p holds p.k = -Sum ((Infor_FinSeq_of M).k);
A9: dom p = dom M by A7,FINSEQ_3:29;
A10: dom Infor_FinSeq_of M = dom M by A1,FINSEQ_3:29;
now
let k such that
A11: k in dom p;
thus p.k = -Sum ((Infor_FinSeq_of M).k) by A8,A11
.= -Sum Line(Infor_FinSeq_of M,k) by A10,A9,A11,MATRIX_0:60
.= Entropy Line(M,k) by A9,A11,Th53;
end;
hence thesis by A7,Def11;
end;
theorem Th63:
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;
set p=Entropy_of_Cond_Prob M;
set q=-LineSum Infor_FinSeq_of M;
A1: dom q = dom LineSum Infor_FinSeq_of M by VALUED_1:8;
then len q = len LineSum Infor_FinSeq_of M by FINSEQ_3:29;
then len q = len Infor_FinSeq_of M by MATRPROB:def 1;
then
A2: len q = len M by Def8;
len p = len M by Th62;
then
A3: dom p = dom q by A2,FINSEQ_3:29;
now
let k be Nat such that
A4: k in dom p;
thus p.k = -Sum ((Infor_FinSeq_of M).k) by A4,Th62
.= -(Sum Infor_FinSeq_of M).k by A1,A3,A4,MATRPROB:def 1
.= q.k by RVSUM_1:17;
end;
hence thesis by A3,FINSEQ_1:13;
end;
theorem Th64:
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;
let M be non empty-yielding Conditional_Probability Matrix of REAL;
assume
A1: len p = len M;
let M1 be Matrix of REAL such that
A2: M1=(Vec2DiagMx p)*M;
reconsider 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 M2;
A5: len L = len M2 by MATRPROB:def 1;
then
A6: dom L = dom M2 by FINSEQ_3:29;
A7: len M2 = len M1 by Def8;
then
A8: dom M2 = dom M1 by FINSEQ_3:29;
A9: dom p = dom M by A1,FINSEQ_3:29;
A10: for k st k in dom L holds L.k = p.k*log(2,p.k)+p.k*Sum Infor_FinSeq_of
Line(M,k)
proof
let k such that
A11: k in dom L;
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;
L.k = Sum(M2.k) by A11,MATRPROB:def 1
.= Sum(Line(M2,k)) by A6,A11,MATRIX_0:60
.= 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 thesis;
end;
set M3 = Infor_FinSeq_of M;
set L2 = LineSum M3;
set p2 = mlt(p,L2);
set p1 = Infor_FinSeq_of p;
A17: len p1 = len p by Th47;
then
A18: dom p1 = dom M by A1,FINSEQ_3:29;
A19: len M3 = len M by Def8;
then
A20: len L2 = len p by A1,MATRPROB:def 1;
then
A21: len p2 = len p by MATRPROB:30;
A22: dom p1 = dom M3 by A1,A19,A17,FINSEQ_3:29;
A23: dom L2 = dom p1 by A20,A17,FINSEQ_3:29;
A24: dom p1 = dom L by A3,A7,A5,A17,FINSEQ_3:29;
now
let k such that
A25: k in dom p1;
A26: p2.k = p.k*L2.k by RVSUM_1:59
.= p.k*Sum (M3.k) by A23,A25,MATRPROB:def 1
.= p.k*Sum (Line(M3,k)) by A22,A25,MATRIX_0:60
.= p.k*Sum (Infor_FinSeq_of Line(M,k)) by A18,A25,Th53;
thus L.k = p.k*log(2,p.k)+p.k*Sum Infor_FinSeq_of Line(M,k) by A10,A24,A25
.= p1.k + p2.k by A25,A26,Th47;
end;
then Sum L = Sum Infor_FinSeq_of p+Sum mlt(p,LineSum(Infor_FinSeq_of M)) by
A3,A7,A5,A17,A21,Th7;
hence thesis by MATRPROB:def 3;
end;
theorem
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;
let M be non empty-yielding Conditional_Probability Matrix of REAL;
set M1 = (Vec2DiagMx p) * M;
assume
A1: len p = len M;
then reconsider M1 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 thesis by A2;
end;