let p be non empty ProbFinS FinSequence of REAL ; ( ( for k being Nat st k in dom p holds
p . k > 0 ) implies ( Entropy p <= log (2,(len p)) & ( ( for k being Nat st k in dom p holds
p . k = 1 / (len p) ) implies Entropy p = log (2,(len p)) ) & ( Entropy p = log (2,(len p)) implies for k being Nat st k in dom p holds
p . k = 1 / (len p) ) & ( ex k being Nat st
( k in dom p & p . k <> 1 / (len p) ) implies Entropy p < log (2,(len p)) ) & ( Entropy p < log (2,(len p)) implies ex k being Nat st
( k in dom p & p . k <> 1 / (len p) ) ) ) )
assume A1:
for k being Nat st k in dom p holds
p . k > 0
; ( Entropy p <= log (2,(len p)) & ( ( for k being Nat st k in dom p holds
p . k = 1 / (len p) ) implies Entropy p = log (2,(len p)) ) & ( Entropy p = log (2,(len p)) implies for k being Nat st k in dom p holds
p . k = 1 / (len p) ) & ( ex k being Nat st
( k in dom p & p . k <> 1 / (len p) ) implies Entropy p < log (2,(len p)) ) & ( Entropy p < log (2,(len p)) implies ex k being Nat st
( k in dom p & p . k <> 1 / (len p) ) ) )
set p3 = - (Infor_FinSeq_of p);
set n = len p;
reconsider n1 = len p as non zero Element of NAT ;
reconsider nn = 1 / n1 as Element of REAL by XREAL_0:def 1;
reconsider p1 = (len p) |-> nn as FinSequence of REAL ;
deffunc H1( Nat) -> Element of REAL = In ((- ((p . $1) * (log (2,(p1 . $1))))),REAL);
consider p2 being FinSequence of REAL such that
A2:
len p2 = len p
and
A3:
for k being Nat st k in dom p2 holds
p2 . k = H1(k)
from FINSEQ_2:sch 1();
A4:
dom p2 = Seg (len p)
by A2, FINSEQ_1:def 3;
A5:
for k being Nat st k in dom p2 holds
p2 . k = ((- (log (2,(1 / n1)))) * p) . k
A7:
len p1 = len p
by CARD_1:def 7;
A8: dom (Infor_FinSeq_of p) =
Seg (len (Infor_FinSeq_of p))
by FINSEQ_1:def 3
.=
Seg (len p)
by Th47
;
A9:
( len (- (Infor_FinSeq_of p)) = len p & ( for k being Nat st k in Seg (len p) holds
(- (Infor_FinSeq_of p)) . k = - ((p . k) * (log (2,(p . k)))) ) )
dom p2 = dom p
by A2, FINSEQ_3:29;
then
dom p2 = dom ((- (log (2,(1 / n1)))) * p)
by VALUED_1:def 5;
then
p2 = (- (log (2,(1 / n1)))) * p
by A5, FINSEQ_1:13;
then A11: Sum p2 =
(- (log (2,(1 / n1)))) * (Sum p)
by RVSUM_1:87
.=
(- (log (2,(1 / n1)))) * 1
by MATRPROB:def 5
.=
log (2,(1 / (1 / n1)))
by Th5
.=
log (2,(len p))
;
A12:
p1 is non empty ProbFinS FinSequence of REAL
by Th16;
A13:
dom p = Seg (len p)
by FINSEQ_1:def 3;
A14:
for k being Nat st k in dom p holds
( p . k > 0 & p1 . k > 0 & (- (Infor_FinSeq_of p)) . k = - ((p . k) * (log (2,(p . k)))) & p2 . k = - ((p . k) * (log (2,(p1 . k)))) )
proof
let k be
Nat;
( k in dom p implies ( p . k > 0 & p1 . k > 0 & (- (Infor_FinSeq_of p)) . k = - ((p . k) * (log (2,(p . k)))) & p2 . k = - ((p . k) * (log (2,(p1 . k)))) ) )
assume A15:
k in dom p
;
( p . k > 0 & p1 . k > 0 & (- (Infor_FinSeq_of p)) . k = - ((p . k) * (log (2,(p . k)))) & p2 . k = - ((p . k) * (log (2,(p1 . k)))) )
hence
(
p . k > 0 &
p1 . k > 0 )
by A1, FINSEQ_2:57, A13;
( (- (Infor_FinSeq_of p)) . k = - ((p . k) * (log (2,(p . k)))) & p2 . k = - ((p . k) * (log (2,(p1 . k)))) )
thus
(- (Infor_FinSeq_of p)) . k = - ((p . k) * (log (2,(p . k))))
by A15, A9, A13;
p2 . k = - ((p . k) * (log (2,(p1 . k))))
p2 . k = H1(
k)
by A15, A3, A4, A13;
hence
p2 . k = - ((p . k) * (log (2,(p1 . k))))
;
verum
end;
A16:
Sum (- (Infor_FinSeq_of p)) = Entropy p
by RVSUM_1:88;
hence
Entropy p <= log (2,(len p))
by A7, A12, A2, A9, A14, A11, Th57; ( ( ( for k being Nat st k in dom p holds
p . k = 1 / (len p) ) implies Entropy p = log (2,(len p)) ) & ( Entropy p = log (2,(len p)) implies for k being Nat st k in dom p holds
p . k = 1 / (len p) ) & ( ex k being Nat st
( k in dom p & p . k <> 1 / (len p) ) implies Entropy p < log (2,(len p)) ) & ( Entropy p < log (2,(len p)) implies ex k being Nat st
( k in dom p & p . k <> 1 / (len p) ) ) )
thus
( ( for k being Nat st k in dom p holds
p . k = 1 / (len p) ) iff Entropy p = log (2,(len p)) )
( ex k being Nat st
( k in dom p & p . k <> 1 / (len p) ) iff Entropy p < log (2,(len p)) )proof
assume A19:
Entropy p = log (2,
(len p))
;
for k being Nat st k in dom p holds
p . k = 1 / (len p)
hereby verum
let k be
Nat;
( k in dom p implies p . k = 1 / (len p) )assume A20:
k in dom p
;
p . k = 1 / (len p)hence p . k =
p1 . k
by A7, A12, A2, A9, A14, A16, A11, A19, Th57
.=
1
/ (len p)
by A13, A20, FINSEQ_2:57
;
verum
end;
end;
A21:
( ( for k being Nat st k in dom p holds
p . k = p1 . k ) iff Sum (- (Infor_FinSeq_of p)) = Sum p2 )
by A7, A12, A2, A9, A14, Th57;
thus
( ex k being Nat st
( k in dom p & p . k <> 1 / (len p) ) iff Entropy p < log (2,(len p)) )
verumproof
hereby ( Entropy p < log (2,(len p)) implies ex k being Nat st
( k in dom p & p . k <> 1 / (len p) ) )
assume
ex
k being
Nat st
(
k in dom p &
p . k <> 1
/ (len p) )
;
Entropy p < log (2,(len p))then consider k1 being
Nat such that A22:
k1 in dom p
and A23:
p . k1 <> 1
/ (len p)
;
p1 . k1 <> p . k1
by A13, A22, A23, FINSEQ_2:57;
hence
Entropy p < log (2,
(len p))
by A7, A12, A2, A9, A14, A16, A11, A22, Th57;
verum
end;
assume
Entropy p < log (2,
(len p))
;
ex k being Nat st
( k in dom p & p . k <> 1 / (len p) )
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
/ (len p)
by A13, A24, FINSEQ_2:57;
hence
ex
k being
Nat st
(
k in dom p &
p . k <> 1
/ (len p) )
by A24, A25;
verum
end;