let p be non empty ProbFinS FinSequence of REAL ; :: thesis: ( ( for k being Element of NAT st k in dom p holds
p . k > 0 ) implies ( Entropy p <= log 2,(len p) & ( ( for k being Element of 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 Element of NAT st k in dom p holds
p . k = 1 / (len p) ) & ( ex k being Element of 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 Element of NAT st
( k in dom p & p . k <> 1 / (len p) ) ) ) )
assume A1: for k being Element of NAT st k in dom p holds
p . k > 0 ; :: thesis: ( Entropy p <= log 2,(len p) & ( ( for k being Element of 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 Element of NAT st k in dom p holds
p . k = 1 / (len p) ) & ( ex k being Element of 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 Element of NAT st
( k in dom p & p . k <> 1 / (len p) ) ) )
set n = len p;
reconsider n1 = len p as non empty Element of NAT ;
A2: dom p = Seg (len p) by FINSEQ_1:def 3;
reconsider nn = 1 / n1 as Element of REAL ;
reconsider p1 = (len p) |-> nn as FinSequence of REAL ;
A3: len p1 = len p by FINSEQ_1:def 18;
A7: p1 is non empty ProbFinS FinSequence of REAL by Th16;
deffunc H₁( Nat) -> Element of REAL = - ((p . $1) * (log 2,(p1 . $1)));
consider p2 being FinSequence of REAL such that
A8: len p2 = len p and
A9: for k being Nat st k in dom p2 holds
p2 . k = H₁(k) from FINSEQ_2:sch 1();
A10: dom p2 = Seg (len p) by A8, FINSEQ_1:def 3;
set p3 = - (Infor_FinSeq_of p);
A12: dom (Infor_FinSeq_of p) = Seg (len (Infor_FinSeq_of p)) by FINSEQ_1:def 3
.= Seg (len p) by Th47 ;
A13: ( len (- (Infor_FinSeq_of p)) = len p & ( for k being Element of NAT st k in Seg (len p) holds
(- (Infor_FinSeq_of p)) . k = - ((p . k) * (log 2,(p . k))) ) )

proof

dom (- (Infor_FinSeq_of p)) = Seg (len p) by A12, VALUED_1:8;
hence len (- (Infor_FinSeq_of p)) = len p by FINSEQ_1:def 3; :: thesis: for k being Element of NAT st k in Seg (len p) holds
(- (Infor_FinSeq_of p)) . k = - ((p . k) * (log 2,(p . k)))

hereby :: thesis: verum

let k be Element of NAT ; :: thesis: ( k in Seg (len p) implies (- (Infor_FinSeq_of p)) . k = - ((p . k) * (log 2,(p . k))) )
assume A14: k in Seg (len p) ; :: thesis: (- (Infor_FinSeq_of p)) . k = - ((p . k) * (log 2,(p . k)))
thus (- (Infor_FinSeq_of p)) . k = - ((Infor_FinSeq_of p) . k) by RVSUM_1:35
.= - ((p . k) * (log 2,(p . k))) by A12, A14, Th47 ; :: thesis: verum

end;

end;

then A15: for k being Element of 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))) ) by A1, A2, A9, A10, FINSEQ_2:71;
then A16: ( Sum (- (Infor_FinSeq_of p)) <= Sum p2 & ( ( for k being Element of NAT st k in dom p holds
p . k = p1 . k ) implies Sum (- (Infor_FinSeq_of p)) = Sum p2 ) & ( Sum (- (Infor_FinSeq_of p)) = Sum p2 implies for k being Element of NAT st k in dom p holds
p . k = p1 . k ) & ( ex k being Element of NAT st
( k in dom p & p . k <> p1 . k ) implies Sum (- (Infor_FinSeq_of p)) < Sum p2 ) & ( Sum (- (Infor_FinSeq_of p)) < Sum p2 implies ex k being Element of NAT st
( k in dom p & p . k <> p1 . k ) ) ) by A3, A7, A8, A13, Th57;
A17: Sum (- (Infor_FinSeq_of p)) = Entropy p by RVSUM_1:118;
A18: dom p2 = dom p by A8, FINSEQ_3:31;
p2 = (- (log 2,(1 / n1))) * p

proof

A19: dom p2 = dom ((- (log 2,(1 / n1))) * p) by A18, VALUED_1:def 5;
for k being Nat st k in dom p2 holds
p2 . k = ((- (log 2,(1 / n1))) * p) . k

proof

let k be Nat; :: thesis: ( k in dom p2 implies p2 . k = ((- (log 2,(1 / n1))) * p) . k )
assume A20: k in dom p2 ; :: thesis: p2 . k = ((- (log 2,(1 / n1))) * p) . k
thus p2 . k = - ((p . k) * (log 2,(p1 . k))) by A9, A20
.= - ((p . k) * (log 2,(1 / n1))) by A20, A10, FINSEQ_2:71
.= (- (log 2,(1 / n1))) * (p . k)
.= ((- (log 2,(1 / n1))) * p) . k by RVSUM_1:66 ; :: thesis: verum

end;

hence p2 = (- (log 2,(1 / n1))) * p by A19, FINSEQ_1:17; :: thesis: verum

end;

then A21: Sum p2 = (- (log 2,(1 / n1))) * (Sum p) by RVSUM_1:117
.= (- (log 2,(1 / n1))) * 1 by MATRPROB:def 5
.= log 2,(1 / (1 / n1)) by Th5
.= log 2,(len p) ;
hence Entropy p <= log 2,(len p) by A3, A7, A8, A13, A15, A17, Th57; :: thesis: ( ( ( for k being Element of 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 Element of NAT st k in dom p holds
p . k = 1 / (len p) ) & ( ex k being Element of 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 Element of NAT st
( k in dom p & p . k <> 1 / (len p) ) ) )
thus ( ( for k being Element of NAT st k in dom p holds
p . k = 1 / (len p) ) iff Entropy p = log 2,(len p) ) :: thesis: ( ex k being Element of NAT st
( k in dom p & p . k <> 1 / (len p) ) iff Entropy p < log 2,(len p) )

proof

hereby :: thesis: ( Entropy p = log 2,(len p) implies for k being Element of NAT st k in dom p holds
p . k = 1 / (len p) )

assume A22: for k being Element of NAT st k in dom p holds
p . k = 1 / (len p) ; :: thesis: Entropy p = log 2,(len p)

now

let k be Element of NAT ; :: thesis: ( k in dom p implies p . k = p1 . k )
assume A23: k in dom p ; :: thesis: p . k = p1 . k
thus p . k = 1 / (len p) by A22, A23
.= p1 . k by A2, A23, FINSEQ_2:71 ; :: thesis: verum

end;

hence Entropy p = log 2,(len p) by A3, A7, A8, A13, A15, A17, A21, Th57; :: thesis: verum

end;

assume A24: Entropy p = log 2,(len p) ; :: thesis: for k being Element of NAT st k in dom p holds
p . k = 1 / (len p)

hereby :: thesis: verum

let k be Element of NAT ; :: thesis: ( k in dom p implies p . k = 1 / (len p) )
assume A25: k in dom p ; :: thesis: p . k = 1 / (len p)
hence p . k = p1 . k by A3, A7, A8, A13, A15, A17, A21, A24, Th57
.= 1 / (len p) by A2, A25, FINSEQ_2:71 ;
:: thesis: verum

end;

end;

thus ( ex k being Element of NAT st
( k in dom p & p . k <> 1 / (len p) ) iff Entropy p < log 2,(len p) ) :: thesis: verum

proof

hereby :: thesis: ( Entropy p < log 2,(len p) implies ex k being Element of NAT st
( k in dom p & p . k <> 1 / (len p) ) )

assume ex k being Element of NAT st
( k in dom p & p . k <> 1 / (len p) ) ; :: thesis: Entropy p < log 2,(len p)
then consider k1 being Nat such that
A26: ( k1 in dom p & p . k1 <> 1 / (len p) ) ;
p1 . k1 <> p . k1 by A2, A26, FINSEQ_2:71;
hence Entropy p < log 2,(len p) by A3, A7, A8, A13, A15, A17, A21, A26, Th57; :: thesis: verum

end;

assume Entropy p < log 2,(len p) ; :: thesis: ex k being Element of NAT st
( k in dom p & p . k <> 1 / (len p) )
then consider k1 being Nat such that
A27: ( k1 in dom p & p . k1 <> p1 . k1 ) by A16, A21, RVSUM_1:118;
p1 . k1 = 1 / (len p) by A2, A27, FINSEQ_2:71;
hence ex k being Element of NAT st
( k in dom p & p . k <> 1 / (len p) ) by A27; :: thesis: verum

end;