let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma
for n being Nat holds (Partial_Product (Prob * ())) . n <= (Partial_Product (JSum (Prob * A))) . n

let Sigma be SigmaField of Omega; :: thesis: for Prob being Probability of Sigma
for A being SetSequence of Sigma
for n being Nat holds (Partial_Product (Prob * ())) . n <= (Partial_Product (JSum (Prob * A))) . n

let Prob be Probability of Sigma; :: thesis: for A being SetSequence of Sigma
for n being Nat holds (Partial_Product (Prob * ())) . n <= (Partial_Product (JSum (Prob * A))) . n

let A be SetSequence of Sigma; :: thesis: for n being Nat holds (Partial_Product (Prob * ())) . n <= (Partial_Product (JSum (Prob * A))) . n
let n be Nat; :: thesis: (Partial_Product (Prob * ())) . n <= (Partial_Product (JSum (Prob * A))) . n
defpred S1[ Nat] means (Partial_Product (Prob * ())) . \$1 <= (Partial_Product (JSum (Prob * A))) . \$1;
A1: (Partial_Product (Prob * ())) . 0 = (Prob * ()) . 0 by SERIES_3:def 1;
dom (Prob * ()) = NAT by FUNCT_2:def 1;
then A2: (Prob * ()) . 0 = Prob . (() . 0) by FUNCT_1:12;
A3: (Partial_Product (Prob * ())) . 0 = Prob . ((A . 0) `) by ;
Prob . ((A . 0) `) = Prob . (([#] Sigma) \ (A . 0)) by SUBSET_1:def 4;
then A4: (Partial_Product (Prob * ())) . 0 = 1 - (Prob . (A . 0)) by ;
(Partial_Product (JSum (Prob * A))) . 0 = (JSum (Prob * A)) . 0 by SERIES_3:def 1;
then (Partial_Product (JSum (Prob * A))) . 0 = Sum ((- ((Prob * A) . 0)) rExpSeq) by Def1;
then A5: (Partial_Product (JSum (Prob * A))) . 0 = exp_R . (- ((Prob * A) . 0)) by SIN_COS:def 22;
A6: dom (Prob * A) = NAT by FUNCT_2:def 1;
1 + (- (Prob . (A . 0))) <= exp_R . (- (Prob . (A . 0))) by Th2;
then A7: S1[ 0 ] by ;
A8: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A9: S1[k] ; :: thesis: S1[k + 1]
( Prob . (() . (k + 1)) = Prob . ((A . (k + 1)) `) & (A . (k + 1)) ` = ([#] Sigma) \ (A . (k + 1)) ) by ;
then A10: Prob . (() . (k + 1)) = 1 - (Prob . (A . (k + 1))) by PROB_1:32;
A11: 1 + (- (Prob . (A . (k + 1)))) <= exp_R . (- (Prob . (A . (k + 1)))) by Th2;
dom (Prob * ()) = NAT by FUNCT_2:def 1;
then A12: (Prob * ()) . (k + 1) <= exp_R . (- (Prob . (A . (k + 1)))) by ;
A13: ((Prob * ()) . (k + 1)) * ((Partial_Product (JSum (Prob * A))) . k) <= (exp_R . (- (Prob . (A . (k + 1))))) * ((Partial_Product (JSum (Prob * A))) . k)
proof
for n being Nat holds (JSum (Prob * A)) . n > 0
proof
let n be Nat; :: thesis: (JSum (Prob * A)) . n > 0
A14: exp_R . (- ((Prob * A) . n)) > 0 by SIN_COS:54;
(JSum (Prob * A)) . n = Sum ((- ((Prob * A) . n)) rExpSeq) by Def1;
hence (JSum (Prob * A)) . n > 0 by ; :: thesis: verum
end;
then (Partial_Product (JSum (Prob * A))) . k > 0 by SERIES_3:43;
hence ((Prob * ()) . (k + 1)) * ((Partial_Product (JSum (Prob * A))) . k) <= (exp_R . (- (Prob . (A . (k + 1))))) * ((Partial_Product (JSum (Prob * A))) . k) by ; :: thesis: verum
end;
A15: ((Partial_Product (Prob * ())) . k) * ((Prob * ()) . (k + 1)) <= ((Partial_Product (JSum (Prob * A))) . k) * ((Prob * ()) . (k + 1))
proof
for n being Element of NAT holds (Prob * ()) . n >= 0
proof
let n be Element of NAT ; :: thesis: (Prob * ()) . n >= 0
A16: Prob . (() . n) >= 0 by PROB_1:def 8;
dom (Prob * ()) = NAT by FUNCT_2:def 1;
hence (Prob * ()) . n >= 0 by ; :: thesis: verum
end;
then (Prob * ()) . (k + 1) >= 0 ;
hence ((Partial_Product (Prob * ())) . k) * ((Prob * ()) . (k + 1)) <= ((Partial_Product (JSum (Prob * A))) . k) * ((Prob * ()) . (k + 1)) by ; :: thesis: verum
end;
((Partial_Product (Prob * ())) . k) * ((Prob * ()) . (k + 1)) <= (exp_R . (- (Prob . (A . (k + 1))))) * ((Partial_Product (JSum (Prob * A))) . k) by ;
then (Partial_Product (Prob * ())) . (k + 1) <= (exp_R . (- (Prob . (A . (k + 1))))) * ((Partial_Product (JSum (Prob * A))) . k) by SERIES_3:def 1;
then (Partial_Product (Prob * ())) . (k + 1) <= (Sum ((- (Prob . (A . (k + 1)))) rExpSeq)) * ((Partial_Product (JSum (Prob * A))) . k) by SIN_COS:def 22;
then (Partial_Product (Prob * ())) . (k + 1) <= (Sum ((- (Prob . (A . (k + 1)))) rExpSeq)) * (exp_R . (- ((Partial_Sums (Prob * A)) . k))) by Th3;
then (Partial_Product (Prob * ())) . (k + 1) <= (exp_R (- (Prob . (A . (k + 1))))) * (exp_R (- ((Partial_Sums (Prob * A)) . k))) by SIN_COS:def 22;
then A17: (Partial_Product (Prob * ())) . (k + 1) <= exp_R ((- (Prob . (A . (k + 1)))) + (- ((Partial_Sums (Prob * A)) . k))) by SIN_COS:50;
dom (Prob * A) = NAT by FUNCT_2:def 1;
then (Prob * A) . (k + 1) = Prob . (A . (k + 1)) by FUNCT_1:12;
then (- (Prob . (A . (k + 1)))) + (- ((Partial_Sums (Prob * A)) . k)) = - (((Prob * A) . (k + 1)) + ((Partial_Sums (Prob * A)) . k)) ;
then (Partial_Product (Prob * ())) . (k + 1) <= exp_R . (- ((Partial_Sums (Prob * A)) . (k + 1))) by ;
hence S1[k + 1] by Th3; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A7, A8);
hence (Partial_Product (Prob * ())) . n <= (Partial_Product (JSum (Prob * A))) . n ; :: thesis: verum