let G be sequence of ExtREAL; :: thesis: ( G is nonnegative implies for S being non empty Subset of NAT
for H being Function of S,NAT st H is one-to-one holds
SUM (On (G * H)) <= SUM G )
assume A1: G is nonnegative ; :: thesis: for S being non empty Subset of NAT
for H being Function of S,NAT st H is one-to-one holds
SUM (On (G * H)) <= SUM G
let S be non empty Subset of NAT; :: thesis: for H being Function of S,NAT st H is one-to-one holds
SUM (On (G * H)) <= SUM G
let H be Function of S,NAT; :: thesis: ( H is one-to-one implies SUM (On (G * H)) <= SUM G )
defpred S1[ Nat] means ex m being Element of NAT st
for F being sequence of ExtREAL st F is nonnegative holds
(Ser (On (F * H))) . $1 <= (Ser F) . m;
assume A2: H is one-to-one ; :: thesis: SUM (On (G * H)) <= SUM G
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
given m0 being Element of NAT such that A4: for F being sequence of ExtREAL st F is nonnegative holds
(Ser (On (F * H))) . k <= (Ser F) . m0 ; :: thesis: S1[k + 1]
per cases ( k + 1 in S or not k + 1 in S ) ;
suppose A5: k + 1 in S ; :: thesis: S1[k + 1]
reconsider m1 = H . (k + 1) as Element of NAT ;
set m = m0 + m1;
take m0 + m1 ; :: thesis: for F being sequence of ExtREAL st F is nonnegative holds
(Ser (On (F * H))) . (k + 1) <= (Ser F) . (m0 + m1)
let F be sequence of ExtREAL; :: thesis: ( F is nonnegative implies (Ser (On (F * H))) . (k + 1) <= (Ser F) . (m0 + m1) )
defpred S2[ Element of NAT , Element of ExtREAL ] means ( ( $1 = H . (k + 1) implies $2 = F . $1 ) & ( $1 <> H . (k + 1) implies $2 = 0. ) );
A6: for n being Element of NAT ex y being Element of ExtREAL st S2[n,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of ExtREAL st S2[n,y]
per cases ( n = H . (k + 1) or n <> H . (k + 1) ) ;
suppose A7: n = H . (k + 1) ; :: thesis: ex y being Element of ExtREAL st S2[n,y]
take F . n ; :: thesis: S2[n,F . n]
thus S2[n,F . n] by A7; :: thesis: verum
end;
suppose A8: n <> H . (k + 1) ; :: thesis: ex y being Element of ExtREAL st S2[n,y]
take 0. ; :: thesis: S2[n, 0. ]
thus S2[n, 0. ] by A8; :: thesis: verum
end;
end;
end;
consider G0 being sequence of ExtREAL such that
A9: for n being Element of NAT holds S2[n,G0 . n] from FUNCT_2:sch 3(A6);
reconsider GG0 = On (G0 * H) as sequence of ExtREAL ;
A10: for n being Element of NAT st n <> k + 1 holds
GG0 . n = 0.
proof
let n be Element of NAT ; :: thesis: ( n <> k + 1 implies GG0 . n = 0. )
assume A11: n <> k + 1 ; :: thesis: GG0 . n = 0.
per cases ( n in S or not n in S ) ;
suppose A12: n in S ; :: thesis: GG0 . n = 0.
then A13: GG0 . n = (G0 * H) . n by Def1
.= G0 . (H . n) by A12, FUNCT_2:15 ;
reconsider n = n as Element of S by A12;
not H . n = H . (k + 1) by A2, A5, A11, FUNCT_2:19;
hence GG0 . n = 0. by A9, A13; :: thesis: verum
end;
end;
end;
assume A14: F is nonnegative ; :: thesis: (Ser (On (F * H))) . (k + 1) <= (Ser F) . (m0 + m1)
for n being Element of NAT holds 0. <= G0 . n
proof
let n be Element of NAT ; :: thesis: 0. <= G0 . n
per cases ( n = H . (k + 1) or not n = H . (k + 1) ) ;
suppose n = H . (k + 1) ; :: thesis: 0. <= G0 . n
then G0 . n = F . n by A9;
hence 0. <= G0 . n by A14, SUPINF_2:39; :: thesis: verum
end;
suppose not n = H . (k + 1) ; :: thesis: 0. <= G0 . n
hence 0. <= G0 . n by A9; :: thesis: verum
end;
end;
end;
then A15: G0 is nonnegative by SUPINF_2:39;
reconsider n = k + 1 as Element of S by A5;
defpred S3[ Element of NAT , Element of ExtREAL ] means ( ( $1 <> H . (k + 1) implies $2 = F . $1 ) & ( $1 = H . (k + 1) implies $2 = 0. ) );
A16: for n being Element of NAT ex y being Element of ExtREAL st S3[n,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of ExtREAL st S3[n,y]
per cases ( n <> H . (k + 1) or n = H . (k + 1) ) ;
suppose A17: n <> H . (k + 1) ; :: thesis: ex y being Element of ExtREAL st S3[n,y]
take F . n ; :: thesis: S3[n,F . n]
thus S3[n,F . n] by A17; :: thesis: verum
end;
suppose A18: n = H . (k + 1) ; :: thesis: ex y being Element of ExtREAL st S3[n,y]
take 0. ; :: thesis: S3[n, 0. ]
thus S3[n, 0. ] by A18; :: thesis: verum
end;
end;
end;
consider G1 being sequence of ExtREAL such that
A19: for n being Element of NAT holds S3[n,G1 . n] from FUNCT_2:sch 3(A16);
set GG1 = On (G1 * H);
A20: (On (G1 * H)) . (k + 1) = (G1 * H) . n by Def1
.= G1 . (H . n) by FUNCT_2:15
.= 0. by A19 ;
A21: GG0 . n = (G0 * H) . n by Def1
.= G0 . (H . n) by FUNCT_2:15
.= F . (H . n) by A9 ;
then A22: (Ser GG0) . (k + 1) = F . (H . (k + 1)) by A10, Th9;
A23: for n being Element of NAT st n <> k + 1 & n in S holds
(On (G1 * H)) . n = F . (H . n)
proof
let n be Element of NAT ; :: thesis: ( n <> k + 1 & n in S implies (On (G1 * H)) . n = F . (H . n) )
assume that
A24: n <> k + 1 and
A25: n in S ; :: thesis: (On (G1 * H)) . n = F . (H . n)
A26: (On (G1 * H)) . n = (G1 * H) . n by A25, Def1
.= G1 . (H . n) by A25, FUNCT_2:15 ;
reconsider n = n as Element of S by A25;
not H . n = H . (k + 1) by A2, A5, A24, FUNCT_2:19;
hence (On (G1 * H)) . n = F . (H . n) by A19, A26; :: thesis: verum
end;
A27: for n being Element of NAT holds (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n)
proof
let n be Element of NAT ; :: thesis: (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n)
per cases ( n = k + 1 or n <> k + 1 ) ;
suppose A28: n = k + 1 ; :: thesis: (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n)
then (On (F * H)) . n = (F * H) . n by A5, Def1
.= F . (H . n) by A5, A28, FUNCT_2:15
.= (GG0 . n) + ((On (G1 * H)) . n) by A21, A20, A28, XXREAL_3:4 ;
hence (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) ; :: thesis: verum
end;
suppose A29: n <> k + 1 ; :: thesis: (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n)
now :: thesis: (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n)
per cases ( n in S or not n in S ) ;
suppose A30: n in S ; :: thesis: (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n)
then A31: (On (G1 * H)) . n = F . (H . n) by A23, A29;
A32: GG0 . n = 0. by A10, A29;
(On (F * H)) . n = (F * H) . n by A30, Def1
.= F . (H . n) by A30, FUNCT_2:15
.= (GG0 . n) + ((On (G1 * H)) . n) by A32, A31, XXREAL_3:4 ;
hence (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) ; :: thesis: verum
end;
suppose A33: not n in S ; :: thesis: (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n)
then A34: (On (G1 * H)) . n = 0. by Def1;
A35: GG0 . n = 0. by A10, A29;
(On (F * H)) . n = 0. by A33, Def1
.= (GG0 . n) + ((On (G1 * H)) . n) by A35, A34 ;
hence (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) ; :: thesis: verum
end;
end;
end;
hence (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) ; :: thesis: verum
end;
end;
end;
m1 <= m0 + m1 by NAT_1:11;
then A36: (Ser G0) . (m0 + m1) = G0 . (H . (k + 1)) by A9, Th9;
set v = H . n;
A37: (Ser (On (G1 * H))) . (k + 1) = ((Ser (On (G1 * H))) . k) + ((On (G1 * H)) . (k + 1)) by SUPINF_2:def 11
.= (Ser (On (G1 * H))) . k by A20, XXREAL_3:4 ;
A38: G0 . (H . n) = F . (H . n) by A9;
for n being Element of NAT holds 0. <= G1 . n
proof
let n be Element of NAT ; :: thesis: 0. <= G1 . n
per cases ( n <> H . (k + 1) or n = H . (k + 1) ) ;
suppose n <> H . (k + 1) ; :: thesis: 0. <= G1 . n
then G1 . n = F . n by A19;
hence 0. <= G1 . n by A14, SUPINF_2:39; :: thesis: verum
end;
suppose n = H . (k + 1) ; :: thesis: 0. <= G1 . n
hence 0. <= G1 . n by A19; :: thesis: verum
end;
end;
end;
then A39: G1 is nonnegative by SUPINF_2:39;
then G1 * H is nonnegative by MEASURE1:25;
then A40: On (G1 * H) is nonnegative by Th7;
G0 * H is nonnegative by A15, MEASURE1:25;
then GG0 is nonnegative by Th7;
then A41: (Ser (On (F * H))) . (k + 1) = ((Ser GG0) . (k + 1)) + ((Ser (On (G1 * H))) . (k + 1)) by A40, A27, Th3;
( (Ser (On (G1 * H))) . k <= (Ser G1) . m0 & (Ser G1) . m0 <= (Ser G1) . (m0 + m1) ) by A4, A39, Th8, NAT_1:11;
then A42: (Ser (On (G1 * H))) . (k + 1) <= (Ser G1) . (m0 + m1) by A37, XXREAL_0:2;
for m being Element of NAT holds F . m = (G0 . m) + (G1 . m)
proof
let m be Element of NAT ; :: thesis: F . m = (G0 . m) + (G1 . m)
per cases ( m = H . (k + 1) or m <> H . (k + 1) ) ;
suppose m = H . (k + 1) ; :: thesis: F . m = (G0 . m) + (G1 . m)
then ( G0 . m = F . m & G1 . m = 0. ) by A9, A19;
hence F . m = (G0 . m) + (G1 . m) by XXREAL_3:4; :: thesis: verum
end;
suppose m <> H . (k + 1) ; :: thesis: F . m = (G0 . m) + (G1 . m)
then ( G0 . m = 0. & G1 . m = F . m ) by A9, A19;
hence F . m = (G0 . m) + (G1 . m) by XXREAL_3:4; :: thesis: verum
end;
end;
end;
then (Ser F) . (m0 + m1) = ((Ser G0) . (m0 + m1)) + ((Ser G1) . (m0 + m1)) by A15, A39, Th3;
hence (Ser (On (F * H))) . (k + 1) <= (Ser F) . (m0 + m1) by A22, A36, A38, A42, A41, XXREAL_3:36; :: thesis: verum
end;
suppose A43: not k + 1 in S ; :: thesis: S1[k + 1]
take m0 ; :: thesis: for F being sequence of ExtREAL st F is nonnegative holds
(Ser (On (F * H))) . (k + 1) <= (Ser F) . m0
let F be sequence of ExtREAL; :: thesis: ( F is nonnegative implies (Ser (On (F * H))) . (k + 1) <= (Ser F) . m0 )
A44: (On (F * H)) . (k + 1) = 0. by A43, Def1;
assume A45: F is nonnegative ; :: thesis: (Ser (On (F * H))) . (k + 1) <= (Ser F) . m0
(Ser (On (F * H))) . (k + 1) = ((Ser (On (F * H))) . k) + ((On (F * H)) . (k + 1)) by SUPINF_2:def 11
.= (Ser (On (F * H))) . k by A44, XXREAL_3:4 ;
hence (Ser (On (F * H))) . (k + 1) <= (Ser F) . m0 by A4, A45; :: thesis: verum
end;
end;
end;
A46: S1[ 0 ]
proof
per cases ( 0 in S or not 0 in S ) ;
suppose A47: 0 in S ; :: thesis: S1[ 0 ]
reconsider m = H . 0 as Element of NAT ;
take m ; :: thesis: for F being sequence of ExtREAL st F is nonnegative holds
(Ser (On (F * H))) . 0 <= (Ser F) . m
let F be sequence of ExtREAL; :: thesis: ( F is nonnegative implies (Ser (On (F * H))) . 0 <= (Ser F) . m )
(Ser (On (F * H))) . 0 = (On (F * H)) . 0 by SUPINF_2:def 11;
then A48: (Ser (On (F * H))) . 0 = (F * H) . 0 by A47, Def1
.= F . (H . 0) by A47, FUNCT_2:15 ;
assume F is nonnegative ; :: thesis: (Ser (On (F * H))) . 0 <= (Ser F) . m
hence (Ser (On (F * H))) . 0 <= (Ser F) . m by A48, Th2; :: thesis: verum
end;
suppose A49: not 0 in S ; :: thesis: S1[ 0 ]
take m = 0 ; :: thesis: for F being sequence of ExtREAL st F is nonnegative holds
(Ser (On (F * H))) . 0 <= (Ser F) . m
let F be sequence of ExtREAL; :: thesis: ( F is nonnegative implies (Ser (On (F * H))) . 0 <= (Ser F) . m )
assume F is nonnegative ; :: thesis: (Ser (On (F * H))) . 0 <= (Ser F) . m
then A50: ( 0. <= F . 0 & F . 0 <= (Ser F) . m ) by Th2, SUPINF_2:39;
(Ser (On (F * H))) . 0 = (On (F * H)) . 0 by SUPINF_2:def 11;
then (Ser (On (F * H))) . 0 = 0. by A49, Def1;
hence (Ser (On (F * H))) . 0 <= (Ser F) . m by A50, XXREAL_0:2; :: thesis: verum
end;
end;
end;
A51: for k being Nat holds S1[k] from NAT_1:sch 2(A46, A3);
 for x being ExtReal st x in rng (Ser (On (G * H))) holds
ex y being ExtReal st
( y in rng (Ser G) & x <= y )
proof
let x be ExtReal; :: thesis: ( x in rng (Ser (On (G * H))) implies ex y being ExtReal st
( y in rng (Ser G) & x <= y ) )
assume A52: x in rng (Ser (On (G * H))) ; :: thesis: ex y being ExtReal st
( y in rng (Ser G) & x <= y )
ex y being ExtReal st
( y in rng (Ser G) & x <= y )
proof
consider n being object such that
A53: n in dom (Ser (On (G * H))) and
A54: x = (Ser (On (G * H))) . n by A52, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A53;
consider m being Element of NAT such that
A55: for F being sequence of ExtREAL st F is nonnegative holds
(Ser (On (F * H))) . n <= (Ser F) . m by A51;
take (Ser G) . m ; :: thesis: ( (Ser G) . m in rng (Ser G) & x <= (Ser G) . m )
dom (Ser G) = NAT by FUNCT_2:def 1;
hence ( (Ser G) . m in rng (Ser G) & x <= (Ser G) . m ) by A1, A54, A55, FUNCT_1:def 3; :: thesis: verum
end;
hence ex y being ExtReal st
( y in rng (Ser G) & x <= y ) ; :: thesis: verum
end;
then sup (rng (Ser (On (G * H)))) <= sup (rng (Ser G)) by XXREAL_2:63;
hence SUM (On (G * H)) <= SUM G ; :: thesis: verum