let p be non empty ProbFinS FinSequence of REAL ; :: thesis: ( ( 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 ; :: thesis: ( 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 H₁( 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 = H₁(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

proof

let k be Nat; :: thesis: ( k in dom p2 implies p2 . k = ((- (log (2,(1 / n1)))) * p) . k )
assume A6: k in dom p2 ; :: thesis: p2 . k = ((- (log (2,(1 / n1)))) * p) . k
thus p2 . k = H₁(k) by A3, A6
.= - ((p . k) * (log (2,(1 / n1)))) by A4, A6, FINSEQ_2:57
.= (- (log (2,(1 / n1)))) * (p . k)
.= ((- (log (2,(1 / n1)))) * p) . k by RVSUM_1:44 ; :: thesis: verum

end;

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)))) ) )

proof

dom (- (Infor_FinSeq_of p)) = Seg (len p) by A8, VALUED_1:8;
hence len (- (Infor_FinSeq_of p)) = len p by FINSEQ_1:def 3; :: thesis: for k being 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 Nat; :: thesis: ( k in Seg (len p) implies (- (Infor_FinSeq_of p)) . k = - ((p . k) * (log (2,(p . k)))) )
assume A10: 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:17
.= - ((p . k) * (log (2,(p . k)))) by A8, A10, Th47 ; :: thesis: verum

end;

end;

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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: ( (- (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; :: thesis: p2 . k = - ((p . k) * (log (2,(p1 . k))))
p2 . k = H₁(k) by A15, A3, A4, A13;
hence p2 . k = - ((p . k) * (log (2,(p1 . k)))) ; :: thesis: 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; :: thesis: ( ( ( 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)) ) :: thesis: ( ex k being 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 Nat st k in dom p holds
p . k = 1 / (len p) )

assume A17: for k being Nat st k in dom p holds
p . k = 1 / (len p) ; :: thesis: Entropy p = log (2,(len p))

now :: thesis: for k being Nat st k in dom p holds
p . k = p1 . k

let k be Nat; :: thesis: ( k in dom p implies p . k = p1 . k )
assume A18: k in dom p ; :: thesis: p . k = p1 . k
thus p . k = 1 / (len p) by A17, A18
.= p1 . k by A13, A18, FINSEQ_2:57 ; :: thesis: verum

end;

hence Entropy p = log (2,(len p)) by A7, A12, A2, A9, A14, A16, A11, Th57; :: thesis: verum

end;

assume A19: Entropy p = log (2,(len p)) ; :: thesis: for k being Nat st k in dom p holds
p . k = 1 / (len p)

hereby :: thesis: verum

let k be Nat; :: thesis: ( k in dom p implies p . k = 1 / (len p) )
assume A20: k in dom p ; :: thesis: 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 ;
:: thesis: 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)) ) :: thesis: verum

proof

hereby :: thesis: ( 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) ) ; :: thesis: 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; :: thesis: verum

end;

assume Entropy p < log (2,(len p)) ; :: thesis: 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; :: thesis: verum

end;