let p be ProbFinS FinSequence of REAL ; for M being V3() Conditional_Probability Matrix of REAL st len p = len M holds
for M1 being Matrix of REAL st M1 = (Vec2DiagMx p) * M holds
SumAll (Infor_FinSeq_of M1) = (Sum (Infor_FinSeq_of p)) + (Sum (mlt (p,(LineSum (Infor_FinSeq_of M)))))
let M be V3() Conditional_Probability Matrix of REAL; ( len p = len M implies for M1 being Matrix of REAL st M1 = (Vec2DiagMx p) * M holds
SumAll (Infor_FinSeq_of M1) = (Sum (Infor_FinSeq_of p)) + (Sum (mlt (p,(LineSum (Infor_FinSeq_of M))))) )
assume A1:
len p = len M
; for M1 being Matrix of REAL st M1 = (Vec2DiagMx p) * M holds
SumAll (Infor_FinSeq_of M1) = (Sum (Infor_FinSeq_of p)) + (Sum (mlt (p,(LineSum (Infor_FinSeq_of M)))))
let M1 be Matrix of REAL; ( M1 = (Vec2DiagMx p) * M implies SumAll (Infor_FinSeq_of M1) = (Sum (Infor_FinSeq_of p)) + (Sum (mlt (p,(LineSum (Infor_FinSeq_of M))))) )
assume A2:
M1 = (Vec2DiagMx p) * M
; SumAll (Infor_FinSeq_of M1) = (Sum (Infor_FinSeq_of p)) + (Sum (mlt (p,(LineSum (Infor_FinSeq_of M)))))
reconsider M1 = M1 as Joint_Probability Matrix of REAL by A1, A2, Th28;
A3:
len M1 = len p
by A1, A2, Th26;
then A4:
dom M1 = dom p
by FINSEQ_3:29;
set M2 = Infor_FinSeq_of M1;
set L = LineSum (Infor_FinSeq_of M1);
A5:
len (LineSum (Infor_FinSeq_of M1)) = len (Infor_FinSeq_of M1)
by MATRPROB:def 1;
then A6:
dom (LineSum (Infor_FinSeq_of M1)) = dom (Infor_FinSeq_of M1)
by FINSEQ_3:29;
A7:
len (Infor_FinSeq_of M1) = len M1
by Def8;
then A8:
dom (Infor_FinSeq_of M1) = dom M1
by FINSEQ_3:29;
A9:
dom p = dom M
by A1, FINSEQ_3:29;
A10:
for k being Nat st k in dom (LineSum (Infor_FinSeq_of M1)) holds
(LineSum (Infor_FinSeq_of M1)) . k = ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of (Line (M,k)))))
proof
let k be
Nat;
( k in dom (LineSum (Infor_FinSeq_of M1)) implies (LineSum (Infor_FinSeq_of M1)) . k = ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of (Line (M,k))))) )
assume A11:
k in dom (LineSum (Infor_FinSeq_of M1))
;
(LineSum (Infor_FinSeq_of M1)) . k = ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of (Line (M,k)))))
reconsider pp =
Line (
M1,
k) as
nonnegative FinSequence of
REAL by A6, A8, A11, Th19;
A12:
p . k >= 0
by A6, A8, A4, A11, Def1;
reconsider q =
Line (
M,
k) as non
empty ProbFinS FinSequence of
REAL by A6, A8, A4, A9, A11, MATRPROB:60;
A13:
pp = (p . k) * q
by A1, A2, A6, A8, A11, Th27;
dom (((p . k) * (log (2,(p . k)))) * q) = dom q
by VALUED_1:def 5;
then A14:
len (((p . k) * (log (2,(p . k)))) * q) = len q
by FINSEQ_3:29;
len (FinSeq_log (2,q)) = len q
by Def6;
then A15:
len (mlt (q,(FinSeq_log (2,q)))) = len q
by MATRPROB:30;
dom ((p . k) * (mlt (q,(FinSeq_log (2,q))))) = dom (mlt (q,(FinSeq_log (2,q))))
by VALUED_1:def 5;
then A16:
len ((p . k) * (mlt (q,(FinSeq_log (2,q))))) = len (mlt (q,(FinSeq_log (2,q))))
by FINSEQ_3:29;
(LineSum (Infor_FinSeq_of M1)) . k =
Sum ((Infor_FinSeq_of M1) . k)
by A11, MATRPROB:def 1
.=
Sum (Line ((Infor_FinSeq_of M1),k))
by A6, A11, MATRIX_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
(LineSum (Infor_FinSeq_of M1)) . k = ((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of (Line (M,k)))))
;
verum
end;
set M3 = Infor_FinSeq_of M;
set L2 = LineSum (Infor_FinSeq_of M);
set p2 = mlt (p,(LineSum (Infor_FinSeq_of M)));
set p1 = Infor_FinSeq_of p;
A17:
len (Infor_FinSeq_of p) = len p
by Th47;
then A18:
dom (Infor_FinSeq_of p) = dom M
by A1, FINSEQ_3:29;
A19:
len (Infor_FinSeq_of M) = len M
by Def8;
then A20:
len (LineSum (Infor_FinSeq_of M)) = len p
by A1, MATRPROB:def 1;
then A21:
len (mlt (p,(LineSum (Infor_FinSeq_of M)))) = len p
by MATRPROB:30;
A22:
dom (Infor_FinSeq_of p) = dom (Infor_FinSeq_of M)
by A1, A19, A17, FINSEQ_3:29;
A23:
dom (LineSum (Infor_FinSeq_of M)) = dom (Infor_FinSeq_of p)
by A20, A17, FINSEQ_3:29;
A24:
dom (Infor_FinSeq_of p) = dom (LineSum (Infor_FinSeq_of M1))
by A3, A7, A5, A17, FINSEQ_3:29;
now for k being Nat st k in dom (Infor_FinSeq_of p) holds
(LineSum (Infor_FinSeq_of M1)) . k = ((Infor_FinSeq_of p) . k) + ((mlt (p,(LineSum (Infor_FinSeq_of M)))) . k)let k be
Nat;
( k in dom (Infor_FinSeq_of p) implies (LineSum (Infor_FinSeq_of M1)) . k = ((Infor_FinSeq_of p) . k) + ((mlt (p,(LineSum (Infor_FinSeq_of M)))) . k) )assume A25:
k in dom (Infor_FinSeq_of p)
;
(LineSum (Infor_FinSeq_of M1)) . k = ((Infor_FinSeq_of p) . k) + ((mlt (p,(LineSum (Infor_FinSeq_of M)))) . k)A26:
(mlt (p,(LineSum (Infor_FinSeq_of M)))) . k =
(p . k) * ((LineSum (Infor_FinSeq_of M)) . k)
by RVSUM_1:59
.=
(p . k) * (Sum ((Infor_FinSeq_of M) . k))
by A23, A25, MATRPROB:def 1
.=
(p . k) * (Sum (Line ((Infor_FinSeq_of M),k)))
by A22, A25, MATRIX_0:60
.=
(p . k) * (Sum (Infor_FinSeq_of (Line (M,k))))
by A18, A25, Th53
;
thus (LineSum (Infor_FinSeq_of M1)) . k =
((p . k) * (log (2,(p . k)))) + ((p . k) * (Sum (Infor_FinSeq_of (Line (M,k)))))
by A10, A24, A25
.=
((Infor_FinSeq_of p) . k) + ((mlt (p,(LineSum (Infor_FinSeq_of M)))) . k)
by A25, A26, Th47
;
verum end;
then
Sum (LineSum (Infor_FinSeq_of M1)) = (Sum (Infor_FinSeq_of p)) + (Sum (mlt (p,(LineSum (Infor_FinSeq_of M)))))
by A3, A7, A5, A17, A21, Th7;
hence
SumAll (Infor_FinSeq_of M1) = (Sum (Infor_FinSeq_of p)) + (Sum (mlt (p,(LineSum (Infor_FinSeq_of M)))))
by MATRPROB:def 3; verum