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 * (Complement A))) . 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 * (Complement A))) . 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 * (Complement A))) . n <= (Partial_Product (JSum (Prob * A))) . n
let A be SetSequence of Sigma; :: thesis: for n being Nat holds (Partial_Product (Prob * (Complement A))) . n <= (Partial_Product (JSum (Prob * A))) . n
let n be Nat; :: thesis: (Partial_Product (Prob * (Complement A))) . n <= (Partial_Product (JSum (Prob * A))) . n
defpred S₁[ Nat] means (Partial_Product (Prob * (Complement A))) . $1 <= (Partial_Product (JSum (Prob * A))) . $1;
A1: (Partial_Product (Prob * (Complement A))) . 0 = (Prob * (Complement A)) . 0 by SERIES_3:def 1;
dom (Prob * (Complement A)) = NAT by FUNCT_2:def 1;
then A2: (Prob * (Complement A)) . 0 = Prob . ((Complement A) . 0) by FUNCT_1:12;
A3: (Partial_Product (Prob * (Complement A))) . 0 = Prob . ((A . 0) `) by A2, A1, PROB_1:def 2;
Prob . ((A . 0) `) = Prob . (([#] Sigma) \ (A . 0)) by SUBSET_1:def 4;
then A4: (Partial_Product (Prob * (Complement A))) . 0 = 1 - (Prob . (A . 0)) by A3, PROB_1:32;
(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: S₁[ 0 ] by A4, A6, A5, FUNCT_1:12;
A8: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A9: S₁[k] ; :: thesis: S₁[k + 1]
( Prob . ((Complement A) . (k + 1)) = Prob . ((A . (k + 1)) `) & (A . (k + 1)) ` = ([#] Sigma) \ (A . (k + 1)) ) by PROB_1:def 2, SUBSET_1:def 4;
then A10: Prob . ((Complement A) . (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 * (Complement A)) = NAT by FUNCT_2:def 1;
then A12: (Prob * (Complement A)) . (k + 1) <= exp_R . (- (Prob . (A . (k + 1)))) by A11, A10, FUNCT_1:12;
A13: ((Prob * (Complement A)) . (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 A14, SIN_COS:def 22; :: thesis: verum

end;

then (Partial_Product (JSum (Prob * A))) . k > 0 by SERIES_3:43;
hence ((Prob * (Complement A)) . (k + 1)) * ((Partial_Product (JSum (Prob * A))) . k) <= (exp_R . (- (Prob . (A . (k + 1))))) * ((Partial_Product (JSum (Prob * A))) . k) by A12, XREAL_1:64; :: thesis: verum

end;

A15: ((Partial_Product (Prob * (Complement A))) . k) * ((Prob * (Complement A)) . (k + 1)) <= ((Partial_Product (JSum (Prob * A))) . k) * ((Prob * (Complement A)) . (k + 1))

proof

for n being Element of NAT holds (Prob * (Complement A)) . n >= 0

proof

let n be Element of NAT ; :: thesis: (Prob * (Complement A)) . n >= 0
A16: Prob . ((Complement A) . n) >= 0 by PROB_1:def 8;
dom (Prob * (Complement A)) = NAT by FUNCT_2:def 1;
hence (Prob * (Complement A)) . n >= 0 by A16, FUNCT_1:12; :: thesis: verum

end;

then (Prob * (Complement A)) . (k + 1) >= 0 ;
hence ((Partial_Product (Prob * (Complement A))) . k) * ((Prob * (Complement A)) . (k + 1)) <= ((Partial_Product (JSum (Prob * A))) . k) * ((Prob * (Complement A)) . (k + 1)) by A9, XREAL_1:64; :: thesis: verum

end;

((Partial_Product (Prob * (Complement A))) . k) * ((Prob * (Complement A)) . (k + 1)) <= (exp_R . (- (Prob . (A . (k + 1))))) * ((Partial_Product (JSum (Prob * A))) . k) by A15, A13, XXREAL_0:2;
then (Partial_Product (Prob * (Complement A))) . (k + 1) <= (exp_R . (- (Prob . (A . (k + 1))))) * ((Partial_Product (JSum (Prob * A))) . k) by SERIES_3:def 1;
then (Partial_Product (Prob * (Complement A))) . (k + 1) <= (Sum ((- (Prob . (A . (k + 1)))) rExpSeq)) * ((Partial_Product (JSum (Prob * A))) . k) by SIN_COS:def 22;
then (Partial_Product (Prob * (Complement A))) . (k + 1) <= (Sum ((- (Prob . (A . (k + 1)))) rExpSeq)) * (exp_R . (- ((Partial_Sums (Prob * A)) . k))) by Th3;
then (Partial_Product (Prob * (Complement A))) . (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 * (Complement A))) . (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 * (Complement A))) . (k + 1) <= exp_R . (- ((Partial_Sums (Prob * A)) . (k + 1))) by A17, SERIES_1:def 1;
hence S₁[k + 1] by Th3; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A7, A8);
hence (Partial_Product (Prob * (Complement A))) . n <= (Partial_Product (JSum (Prob * A))) . n ; :: thesis: verum