let X be set ; :: thesis: for S being SigmaField of X
for M being Measure of S
for F being Sep_Sequence of S holds SUM (M * F) <= M . (union (rng F))
let S be SigmaField of X; :: thesis: for M being Measure of S
for F being Sep_Sequence of S holds SUM (M * F) <= M . (union (rng F))
let M be Measure of S; :: thesis: for F being Sep_Sequence of S holds SUM (M * F) <= M . (union (rng F))
let F be Sep_Sequence of S; :: thesis: SUM (M * F) <= M . (union (rng F))
set T = rng F;
( union (rng F) is Subset of X & {} is Subset of X ) by XBOOLE_1:2;
then consider H being Function of NAT ,(bool X) such that
A1: ( rng H = {(union (rng F)),{} } & H . 0 = union (rng F) & ( for n being Element of NAT st 0 < n holds
H . n = {} ) ) by MEASURE1:40;
rng H c= S
proof
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in rng H or a in S )
assume a in rng H ; :: thesis: a in S
then ( a = union (rng F) or a = {} ) by A1, TARSKI:def 2;
hence a in S by PROB_1:10; :: thesis: verum
end;
then reconsider H = H as Function of NAT ,S by FUNCT_2:8;
A2: ( M * F is nonnegative & M * H is nonnegative ) by MEASURE1:54;
consider G being Function of NAT ,S such that
A3: ( G . 0 = F . 0 & ( for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \/ (G . n) ) ) by MEASURE2:5;
A4: for n being Element of NAT holds (G . n) /\ (F . (n + 1)) = {}
proof
let n be Element of NAT ; :: thesis: (G . n) /\ (F . (n + 1)) = {}
A5: for n, k being Element of NAT st n < k holds
(G . n) /\ (F . k) = {}
proof
defpred S1[ Element of NAT ] means for k being Element of NAT st $1 < k holds
(G . $1) /\ (F . k) = {} ;
A6: S1[ 0 ]
proof
let k be Element of NAT ; :: thesis: ( 0 < k implies (G . 0 ) /\ (F . k) = {} )
assume 0 < k ; :: thesis: (G . 0 ) /\ (F . k) = {}
then F . 0 misses F . k by PROB_2:def 3;
hence (G . 0 ) /\ (F . k) = {} by A3, XBOOLE_0:def 7; :: thesis: verum
end;
A7: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
assume A8: for k being Element of NAT st n < k holds
(G . n) /\ (F . k) = {} ; :: thesis: S1[n + 1]
let k be Element of NAT ; :: thesis: ( n + 1 < k implies (G . (n + 1)) /\ (F . k) = {} )
assume A9: n + 1 < k ; :: thesis: (G . (n + 1)) /\ (F . k) = {}
A10: (G . (n + 1)) /\ (F . k) = ((F . (n + 1)) \/ (G . n)) /\ (F . k) by A3
.= ((F . (n + 1)) /\ (F . k)) \/ ((G . n) /\ (F . k)) by XBOOLE_1:23 ;
A11: n < k by A9, NAT_1:13;
F . (n + 1) misses F . k by A9, PROB_2:def 3;
then (F . (n + 1)) /\ (F . k) = {} by XBOOLE_0:def 7;
hence (G . (n + 1)) /\ (F . k) = {} by A8, A10, A11; :: thesis: verum
end;
thus for n being Element of NAT holds S1[n] from NAT_1:sch 1(A6, A7); :: thesis: verum
end;
n < n + 1 by NAT_1:13;
hence (G . n) /\ (F . (n + 1)) = {} by A5; :: thesis: verum
end;
A12: (Ser (M * F)) . 0 = (M * F) . 0 by SUPINF_2:63;
defpred S1[ Element of NAT ] means (Ser (M * F)) . $1 = M . (G . $1);
A13: ( dom F = NAT & dom (M * F) = NAT ) by FUNCT_2:def 1;
then A14: S1[ 0 ] by A3, A12, FUNCT_1:22;
A15: for n being Element of NAT holds (Ser (M * F)) . n = M . (G . n)
proof
A16: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume (Ser (M * F)) . k = M . (G . k) ; :: thesis: S1[k + 1]
then A17: (Ser (M * F)) . (k + 1) = (M . (G . k)) + ((M * F) . (k + 1)) by SUPINF_2:63;
(G . k) /\ (F . (k + 1)) = {} by A4;
then A18: G . k misses F . (k + 1) by XBOOLE_0:def 7;
(Ser (M * F)) . (k + 1) = (M . (G . k)) + (M . (F . (k + 1))) by A13, A17, FUNCT_1:22
.= M . ((F . (k + 1)) \/ (G . k)) by A18, MEASURE1:def 5
.= M . (G . (k + 1)) by A3 ;
hence S1[k + 1] ; :: thesis: verum
end;
thus for n being Element of NAT holds S1[n] from NAT_1:sch 1(A14, A16); :: thesis: verum
end;
A19: for n being Element of NAT holds G . n c= union (rng F)
proof
defpred S2[ Element of NAT ] means G . $1 c= union (rng F);
A20: S2[ 0 ] by A3, FUNCT_2:6, ZFMISC_1:92;
A21: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; :: thesis: ( S2[n] implies S2[n + 1] )
assume A22: G . n c= union (rng F) ; :: thesis: S2[n + 1]
A23: G . (n + 1) = (F . (n + 1)) \/ (G . n) by A3;
F . (n + 1) c= union (rng F) by FUNCT_2:6, ZFMISC_1:92;
hence S2[n + 1] by A22, A23, XBOOLE_1:8; :: thesis: verum
end;
thus for n being Element of NAT holds S2[n] from NAT_1:sch 1(A20, A21); :: thesis: verum
end;
defpred S2[ Element of NAT ] means (Ser (M * H)) . $1 = M . (union (rng F));
A24: S2[ 0 ]
proof
A25: (Ser (M * H)) . 0 = (M * H) . 0 by SUPINF_2:63;
dom (M * H) = NAT by FUNCT_2:def 1;
hence S2[ 0 ] by A1, A25, FUNCT_1:22; :: thesis: verum
end;
A26: for n being Element of NAT holds (Ser (M * H)) . n = M . (union (rng F))
proof
A27: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; :: thesis: ( S2[n] implies S2[n + 1] )
assume (Ser (M * H)) . n = M . (union (rng F)) ; :: thesis: S2[n + 1]
then A28: (Ser (M * H)) . (n + 1) = (M . (union (rng F))) + ((M * H) . (n + 1)) by SUPINF_2:63;
0 <= n by NAT_1:2;
then 0 < n + 1 by NAT_1:13;
then A29: H . (n + 1) = {} by A1;
dom (M * H) = NAT by FUNCT_2:def 1;
then (M * H) . (n + 1) = M . {} by A29, FUNCT_1:22;
then (M * H) . (n + 1) = 0. by VALUED_0:def 19;
hence S2[n + 1] by A28, XXREAL_3:4; :: thesis: verum
end;
thus for n being Element of NAT holds S2[n] from NAT_1:sch 1(A24, A27); :: thesis: verum
end;
A30: for n being Element of NAT holds (Ser (M * F)) . n <= (Ser (M * H)) . n
proof
let n be Element of NAT ; :: thesis: (Ser (M * F)) . n <= (Ser (M * H)) . n
(Ser (M * F)) . n = M . (G . n) by A15;
then (Ser (M * F)) . n <= M . (union (rng F)) by A19, MEASURE1:25;
hence (Ser (M * F)) . n <= (Ser (M * H)) . n by A26; :: thesis: verum
end;
for r being Element of NAT st 1 <= r holds
(M * H) . r = 0.
proof
let r be Element of NAT ; :: thesis: ( 1 <= r implies (M * H) . r = 0. )
assume 1 <= r ; :: thesis: (M * H) . r = 0.
then 0 + 1 <= r ;
then 0 < r by NAT_1:13;
then A31: H . r = {} by A1;
dom (M * H) = NAT by FUNCT_2:def 1;
then (M * H) . r = M . {} by A31, FUNCT_1:22;
hence (M * H) . r = 0. by VALUED_0:def 19; :: thesis: verum
end;
then SUM (M * H) = (Ser (M * H)) . 1 by A2, SUPINF_2:67;
then SUM (M * H) = M . (union (rng F)) by A26;
hence SUM (M * F) <= M . (union (rng F)) by A30, Th3; :: thesis: verum