let p, q be 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))
set p1 = Infor_FinSeq_of p;
set p2 = (Sum (Infor_FinSeq_of q)) * p;
A1:
len (Infor_FinSeq_of p) = len p
by Th47;
dom ((Sum (Infor_FinSeq_of q)) * p) = dom p
by VALUED_1:def 5;
then A2:
len (Infor_FinSeq_of p) = len ((Sum (Infor_FinSeq_of q)) * p)
by A1, FINSEQ_3:29;
len (FinSeq_log (2,q)) = len q
by Def6;
then A3:
len (mlt (q,(FinSeq_log (2,q)))) = len q
by MATRPROB:30;
let M be Matrix of REAL; ( M = (ColVec2Mx p) * (LineVec2Mx q) implies SumAll (Infor_FinSeq_of M) = (Sum (Infor_FinSeq_of p)) + (Sum (Infor_FinSeq_of q)) )
assume A4:
M = (ColVec2Mx p) * (LineVec2Mx q)
; SumAll (Infor_FinSeq_of M) = (Sum (Infor_FinSeq_of p)) + (Sum (Infor_FinSeq_of q))
reconsider M = M as Joint_Probability Matrix of REAL by A4, Th23;
set M1 = Infor_FinSeq_of M;
set L = LineSum (Infor_FinSeq_of M);
A5:
len (LineSum (Infor_FinSeq_of M)) = len (Infor_FinSeq_of M)
by MATRPROB:def 1;
then A6:
dom (LineSum (Infor_FinSeq_of M)) = dom (Infor_FinSeq_of M)
by FINSEQ_3:29;
A7:
len (Infor_FinSeq_of M) = len M
by Def8;
then A8:
dom (Infor_FinSeq_of M) = dom M
by FINSEQ_3:29;
A9:
len M = len p
by A4, Th22;
then A10:
dom M = dom p
by FINSEQ_3:29;
A11:
now for k being Nat st k in dom (LineSum (Infor_FinSeq_of M)) holds
(LineSum (Infor_FinSeq_of M)) . k = ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of q)))let k be
Nat;
( k in dom (LineSum (Infor_FinSeq_of M)) implies (LineSum (Infor_FinSeq_of M)) . k = ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of q))) )assume A12:
k in dom (LineSum (Infor_FinSeq_of M))
;
(LineSum (Infor_FinSeq_of M)) . k = ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of q)))reconsider pp =
Line (
M,
k) as
nonnegative FinSequence of
REAL by A6, A8, A12, Th19;
A13:
pp = (p . k) * q
by A4, A6, A8, A12, Th22;
dom (((p . k) * (log (2,(p . k)))) * q) = dom q
by VALUED_1:def 5;
then A14:
len (((p . k) * (log (2,(p . k)))) * q) = len q
by FINSEQ_3:29;
dom ((p . k) * (mlt (q,(FinSeq_log (2,q))))) = dom (mlt (q,(FinSeq_log (2,q))))
by VALUED_1:def 5;
then A15:
len (((p . k) * (log (2,(p . k)))) * q) = len ((p . k) * (mlt (q,(FinSeq_log (2,q)))))
by A3, A14, FINSEQ_3:29;
A16:
p . k >= 0
by A6, A8, A10, A12, Def1;
thus (LineSum (Infor_FinSeq_of M)) . k =
Sum ((Infor_FinSeq_of M) . k)
by A12, MATRPROB:def 1
.=
Sum (Line ((Infor_FinSeq_of M),k))
by A6, A12, MATRIX_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
;
verum end;
A17:
dom (Infor_FinSeq_of p) = dom (LineSum (Infor_FinSeq_of M))
by A9, A7, A5, A1, FINSEQ_3:29;
then Sum (LineSum (Infor_FinSeq_of M)) =
(Sum (Infor_FinSeq_of p)) + (Sum ((Sum (Infor_FinSeq_of q)) * p))
by A9, A7, A5, A1, A2, Th7
.=
(Sum (Infor_FinSeq_of p)) + ((Sum (Infor_FinSeq_of q)) * (Sum p))
by RVSUM_1:87
.=
(Sum (Infor_FinSeq_of p)) + ((Sum (Infor_FinSeq_of q)) * 1)
by MATRPROB:def 5
.=
(Sum (Infor_FinSeq_of p)) + (Sum (Infor_FinSeq_of q))
;
hence
SumAll (Infor_FinSeq_of M) = (Sum (Infor_FinSeq_of p)) + (Sum (Infor_FinSeq_of q))
by MATRPROB:def 3; verum