let X be set ; for C being C_Measure of X
for seq being Sep_Sequence of (sigma_Field C) holds
( union (rng seq) in sigma_Field C & C . (union (rng seq)) = Sum (C * seq) )
let C be C_Measure of X; for seq being Sep_Sequence of (sigma_Field C) holds
( union (rng seq) in sigma_Field C & C . (union (rng seq)) = Sum (C * seq) )
let seq be Sep_Sequence of (sigma_Field C); ( union (rng seq) in sigma_Field C & C . (union (rng seq)) = Sum (C * seq) )
A1:
rng seq c= sigma_Field C
by RELAT_1:def 19;
then reconsider seq1 = seq as sequence of (bool X) by FUNCT_2:6;
A2:
for A being Subset of X
for n being Element of NAT holds ((Ser (C * (A (/\) seq1))) . n) + (C . (A /\ (X \ (union (rng seq))))) <= C . A
proof
defpred S1[
Nat]
means for
A being
Subset of
X holds
C . A >= ((Ser (C * (A (/\) seq1))) . $1) + (C . (A /\ (X \ (union (rng seq)))));
let A be
Subset of
X;
for n being Element of NAT holds ((Ser (C * (A (/\) seq1))) . n) + (C . (A /\ (X \ (union (rng seq))))) <= C . Alet n be
Element of
NAT ;
((Ser (C * (A (/\) seq1))) . n) + (C . (A /\ (X \ (union (rng seq))))) <= C . A
A3:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
S1[k + 1]
let A be
Subset of
X;
C . A >= ((Ser (C * (A (/\) seq1))) . (k + 1)) + (C . (A /\ (X \ (union (rng seq)))))
A /\ (X \ (seq1 . (k + 1))) =
(A /\ X) \ (seq1 . (k + 1))
by XBOOLE_1:49
.=
A \ (seq1 . (k + 1))
by XBOOLE_1:28
;
then A9:
C . (A \ (seq1 . (k + 1))) >= ((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ (union (rng seq)))))
by A5;
A10:
A \ (seq1 . (k + 1)) c= X \ (seq1 . (k + 1))
by XBOOLE_1:33;
A11:
A \/ (A \ (seq1 . (k + 1))) = A
by XBOOLE_1:12, XBOOLE_1:36;
(
seq1 . (k + 1) in rng seq &
A /\ (seq1 . (k + 1)) c= seq1 . (k + 1) )
by FUNCT_2:4, XBOOLE_1:17;
then (C . (A /\ (seq1 . (k + 1)))) + (C . (A \ (seq1 . (k + 1)))) =
C . ((A /\ (seq1 . (k + 1))) \/ (A \ (seq1 . (k + 1))))
by A1, A10, MEASURE4:5
.=
C . ((A \/ (A \ (seq1 . (k + 1)))) /\ ((seq1 . (k + 1)) \/ (A \ (seq1 . (k + 1)))))
by XBOOLE_1:24
.=
C . ((A \/ (A \ (seq1 . (k + 1)))) /\ ((seq1 . (k + 1)) \/ A))
by XBOOLE_1:39
;
then
(C . (A /\ (seq1 . (k + 1)))) + (C . (A \ (seq1 . (k + 1)))) = C . A
by A11, XBOOLE_1:7, XBOOLE_1:28;
then A12:
C . A >= (((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ (union (rng seq)))))) + (C . (A /\ (seq1 . (k + 1))))
by A9, XXREAL_3:36;
A13:
((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (seq1 . (k + 1)))) =
((Ser (C * (A (/\) seq1))) . k) + (C . ((A (/\) seq1) . (k + 1)))
by SETLIM_2:def 5
.=
((Ser (C * (A (/\) seq1))) . k) + ((C * (A (/\) seq1)) . (k + 1))
by FUNCT_2:15
.=
(Ser (C * (A (/\) seq1))) . (k + 1)
by SUPINF_2:def 11
;
A14:
C is
nonnegative
by MEASURE4:def 1;
then A15:
C * (A (/\) seq1) is
nonnegative
by MEASURE1:25;
then
(C * (A (/\) seq1)) . k >= 0
by SUPINF_2:51;
then A16:
(Ser (C * (A (/\) seq1))) . k > -infty
by A15, MEASURE7:2;
(
C . (A /\ (X \ (union (rng seq)))) > -infty &
C . (A /\ (seq1 . (k + 1))) > -infty )
by A14, SUPINF_2:51;
hence
C . A >= ((Ser (C * (A (/\) seq1))) . (k + 1)) + (C . (A /\ (X \ (union (rng seq)))))
by A16, A12, A13, XXREAL_3:29;
verum
end;
A17:
seq . 0 in sigma_Field C
;
then A20:
S1[
0 ]
;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A20, A3);
hence
((Ser (C * (A (/\) seq1))) . n) + (C . (A /\ (X \ (union (rng seq))))) <= C . A
;
verum
end;
A21:
for A being Subset of X holds
( (SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ (union (rng seq))))) <= C . A & C . (A /\ (Union seq1)) <= SUM (C * (A (/\) seq1)) )
then A30:
C . ((union (rng seq)) /\ (Union seq1)) <= SUM (C * ((union (rng seq)) (/\) seq1))
;
for W, Z being Subset of X st W c= Union seq1 & Z c= X \ (Union seq1) holds
(C . W) + (C . Z) <= C . (W \/ Z)
then
Union seq1 in sigma_Field C
by MEASURE4:def 2;
hence
union (rng seq) in sigma_Field C
by CARD_3:def 4; C . (union (rng seq)) = Sum (C * seq)
set Sseq = Ser (C * seq1);
union (rng seq) misses X \ (union (rng seq))
by XBOOLE_1:79;
then A38:
(union (rng seq)) /\ (X \ (union (rng seq))) = {}
by XBOOLE_0:def 7;
C is zeroed
by MEASURE4:def 1;
then A39:
C . ((union (rng seq)) /\ (X \ (union (rng seq)))) = 0
by A38, VALUED_0:def 19;
for n being object st n in NAT holds
((union (rng seq)) (/\) seq1) . n = seq . n
then A40:
SUM (C * ((union (rng seq)) (/\) seq1)) = sup (Ser (C * seq1))
by FUNCT_2:12;
C is nonnegative
by MEASURE4:def 1;
then
C * seq1 is nonnegative
by MEASURE1:25;
then
for m, n being ExtReal st m in dom (Ser (C * seq1)) & n in dom (Ser (C * seq1)) & m <= n holds
(Ser (C * seq1)) . m <= (Ser (C * seq1)) . n
by MEASURE7:8;
then
Ser (C * seq1) is non-decreasing
by VALUED_0:def 15;
then
SUM (C * ((union (rng seq)) (/\) seq1)) = lim (Ser (C * seq1))
by A40, RINFSUP2:37;
then A41:
SUM (C * ((union (rng seq)) (/\) seq1)) = lim (Partial_Sums (C * seq1))
by Th1;
(SUM (C * ((union (rng seq)) (/\) seq1))) + (C . ((union (rng seq)) /\ (X \ (union (rng seq))))) <= C . (union (rng seq))
by A21;
then
( union (rng seq) = Union seq1 & C . (union (rng seq)) >= Sum (C * seq) )
by A39, A41, CARD_3:def 4, XXREAL_3:4;
hence
C . (union (rng seq)) = Sum (C * seq)
by A30, A41, XXREAL_0:1; verum