let p be non empty ProbFinS FinSequence of REAL ; :: thesis: ( ex k being Nat st
( k in dom p & p . k = 1 ) implies Entropy p = 0 )
assume ex k being Nat st
( k in dom p & p . k = 1 ) ; :: thesis: Entropy p = 0
then consider k1 being Nat such that
A1: k1 in dom p and
A2: p . k1 = 1 ;
set q = Infor_FinSeq_of p;
len (Infor_FinSeq_of p) = len p by Th47;
then A3: dom (Infor_FinSeq_of p) = dom p by FINSEQ_3:29;
A4: p has_onlyone_value_in k1 by A1, A2, Th15;
for k being Nat st k in dom (Infor_FinSeq_of p) holds
(Infor_FinSeq_of p) . k = 0
proof
let k be Nat; :: thesis: ( k in dom (Infor_FinSeq_of p) implies (Infor_FinSeq_of p) . k = 0 )
assume A5: k in dom (Infor_FinSeq_of p) ; :: thesis: (Infor_FinSeq_of p) . k = 0
per cases ( k = k1 or k <> k1 ) ;
suppose k = k1 ; :: thesis: (Infor_FinSeq_of p) . k = 0
hence (Infor_FinSeq_of p) . k = 1 * (log (2,1)) by A2, A5, Th47
.= 0 by POWER:51 ;
:: thesis: verum
end;
suppose k <> k1 ; :: thesis: (Infor_FinSeq_of p) . k = 0
then A6: p . k = 0 by A4, A3, A5;
thus (Infor_FinSeq_of p) . k = (p . k) * (log (2,(p . k))) by A5, Th47
.= 0 by A6 ; :: thesis: verum
end;
end;
end;
then for x being object st x in dom (Infor_FinSeq_of p) holds
(Infor_FinSeq_of p) . x = 0 ;
then Infor_FinSeq_of p = (dom (Infor_FinSeq_of p)) --> 0 by FUNCOP_1:11;
then Infor_FinSeq_of p = (len (Infor_FinSeq_of p)) |-> 0 by FINSEQ_1:def 3;
then Sum (Infor_FinSeq_of p) = 0 by RVSUM_1:81;
hence Entropy p = 0 ; :: thesis: verum