:: Product Pre-Measure
:: by Noboru Endou
::
:: Received December 31, 2015
:: Copyright (c) 2015-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, CARD_3, FUNCT_1, RELAT_1, FINSEQ_1, XBOOLE_0,
ARYTM_3, XXREAL_0, CARD_1, TARSKI, NAT_1, ZFMISC_1, ORDINAL4, PROB_1,
FINSUB_1, SETFAM_1, PROB_2, MEASURE9, MSSUBFAM, FUNCOP_1, SUPINF_2,
VALUED_0, FUNCT_2, PARTFUN1, MEASURE1, ORDINAL2, SERIES_1, MESFUNC5,
SUPINF_1, SEQ_2, MEASURE6, SEQFUNC, REAL_1, XCMPLX_0, PBOOLE, MESFUNC9,
VALUED_1, SIMPLEX0, SRINGS_3, MEASURE3, MEASURE5, XXREAL_1, MEASUR10,
SRINGS_1, SRINGS_4, MESFUNC8, MESFUNC1, FUNCT_3, INTEGRA5, RFUNCT_3,
REWRITE1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSUB_1, CARD_1,
CARD_3, NUMBERS, FUNCT_3, XXREAL_1, XXREAL_3, BINOP_1, XTUPLE_0, PROB_1,
XCMPLX_0, XREAL_0, XXREAL_0, SIMPLEX0, NAT_1, VALUED_0, SUPINF_1,
FINSEQ_1, FINSEQOP, SUPINF_2, PROB_2, SEQFUNC, MEASURE1, MEASURE3,
MEASURE5, MESFUNC1, MESFUNC2, MESFUNC5, MESFUNC8, MESFUNC9, RINFSUP2,
EXTREAL1, SRINGS_3, MEASURE9, SRINGS_1, SRINGS_4, MESFUNC6;
constructors TOPMETR, PROB_2, MESFUNC5, EXTREAL1, SUPINF_1, MESFUNC1,
MESFUNC9, RINFSUP2, FINSEQOP, SEQFUNC, MEASURE3, INTEGRA1, SRINGS_1,
MEASURE9, SEQ_4, SRINGS_4, MESFUNC2, MESFUNC8, MESFUNC6;
registrations XREAL_0, MEMBERED, FUNCT_1, XBOOLE_0, FINSEQ_1, RELAT_1,
SUBSET_1, XXREAL_0, ROUGHS_1, NUMBERS, VALUED_0, FUNCT_2, ORDINAL1,
MESFUNC9, RELSET_1, PROB_1, MEASURE1, MESFUNC5, NAT_1, PARTFUN1,
XXREAL_3, CARD_1, XXREAL_2, SIMPLEX0, SRINGS_3, DBLSEQ_3, MEASURE3,
MEASURE9, SRINGS_2, SRINGS_1, SRINGS_4;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities FINSEQ_1, BINOP_1;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, XBOOLE_0, XREAL_0, FINSEQ_1, NAT_1, FUNCT_1, CARD_3,
XXREAL_0, ZFMISC_1, FINSEQ_3, XBOOLE_1, PROB_2, XREAL_1, PROB_1,
FINSUB_1, SETFAM_1, FUNCOP_1, XXREAL_3, MEASURE1, VALUED_0, FUNCT_2,
RELAT_1, MESFUNC5, EXTREAL1, MESFUNC9, FINSEQ_2, PARTFUN1, ORDINAL1,
ABCMIZ_1, RINFSUP2, MEASURE8, MESFUNC1, SUPINF_2, XTUPLE_0, SRINGS_3,
MEASURE3, CARD_1, MEASURE9, MEASURE5, SRINGS_2, XXREAL_1, FINANCE1,
FINANCE2, SRINGS_4, FUNCT_5, MESFUNC8, FUNCT_3, MESFUNC2, MESFUNC6,
MESFUNC7, RELSET_1;
schemes FINSEQ_1, NAT_1, FUNCT_2, FUNCT_1, SEQFUNC;
begin :: Preliminaries
theorem Th23:
for A,A1,A2,B,B1,B2 be non empty set holds
[:A1,B1:] misses [:A2,B2:] & [:A,B:] = [:A1,B1:] \/ [:A2,B2:]
iff
(A1 misses A2 & A = A1 \/ A2 & B = B1 & B = B2)
or (B1 misses B2 & B = B1 \/ B2 & A = A1 & A = A2)
proof
let A,A1,A2,B,B1,B2 be non empty set;
hereby assume
A2: [:A1,B1:] misses [:A2,B2:] & [:A,B:] = [:A1,B1:] \/ [:A2,B2:];
[:A1,B1:] c= [:A,B:] & [:A2,B2:] c= [:A,B:] by A2,XBOOLE_1:7; then
A3: A1 c= A & B1 c= B & A2 c= A & B2 c= B by ZFMISC_1:114;
[:A1 \/ A2,B1 \/ B2:]
= [:A1,B1:] \/ [:A1,B2:] \/ [:A2,B1:] \/ [:A2,B2:] by ZFMISC_1:98
.= ([:A1,B1:] \/ [:A1,B2:]) \/ [:A2,B2:] \/ [:A2,B1:] by XBOOLE_1:4
.= [:A1,B1:] \/ ([:A2,B2:] \/ [:A1,B2:]) \/ [:A2,B1:] by XBOOLE_1:4
.= [:A1,B1:] \/ [:A2,B2:] \/ [:A1,B2:] \/ [:A2,B1:] by XBOOLE_1:4
.= [:A1,B1:] \/ [:A2,B2:] \/ ([:A1,B2:] \/ [:A2,B1:]) by XBOOLE_1:4; then
A5: [:A1,B1:] \/ [:A2,B2:] c= [:A1 \/ A2, B1 \/ B2:] by XBOOLE_1:7;
A6: [:A1 /\ A2, B1 /\ B2:] = {} by A2,ZFMISC_1:100;
per cases by A6;
suppose A7: A1 /\ A2 = {}; then
B7: A1 misses A2;
A12: now assume B \ B1 <> {}; then
consider y be object such that
A8: y in B \ B1 by XBOOLE_0:def 1;
A9: y in B & not y in B1 by A8,XBOOLE_0:def 5;
consider x be object such that
A10: x in A1 by XBOOLE_0:def 1;
A11: [x,y] in [:A,B:] by A3,A10,A8,ZFMISC_1:def 2;
not x in A2 by B7,A10,XBOOLE_0:3; then
not [x,y] in [:A1,B1:] & not [x,y] in [:A2,B2:] by A9,ZFMISC_1:87;
hence contradiction by A11,A2,XBOOLE_0:def 3;
end;
now assume B \ B2 <> {}; then
consider y be object such that
A14: y in B \ B2 by XBOOLE_0:def 1;
A15: y in B & not y in B2 by A14,XBOOLE_0:def 5;
consider x be object such that
A16: x in A2 by XBOOLE_0:def 1;
A17: [x,y] in [:A,B:] by A3,A16,A14,ZFMISC_1:def 2;
not x in A1 by B7,A16,XBOOLE_0:3; then
not [x,y] in [:A1,B1:] & not [x,y] in [:A2,B2:] by A15,ZFMISC_1:87;
hence contradiction by A17,A2,XBOOLE_0:def 3;
end;
hence (A1 misses A2 & A = A1 \/ A2 & B = B1 & B = B2)
or (B1 misses B2 & B = B1 \/ B2 & A = A1 & A = A2)
by A3,A5,A7,A12,XBOOLE_1:8,37,A2,ZFMISC_1:114;
end;
suppose A18: B1 /\ B2 = {}; then
B18: B1 misses B2;
A19: now assume A \ A1 <> {}; then
consider x be object such that
A20: x in A \ A1 by XBOOLE_0:def 1;
A21: x in A & not x in A1 by A20,XBOOLE_0:def 5;
consider y be object such that
A22: y in B1 by XBOOLE_0:def 1;
A23: [x,y] in [:A,B:] by A3,A22,A20,ZFMISC_1:def 2;
not y in B2 by B18,A22,XBOOLE_0:3; then
not [x,y] in [:A1,B1:] & not [x,y] in [:A2,B2:] by A21,ZFMISC_1:87;
hence contradiction by A23,A2,XBOOLE_0:def 3;
end;
now assume A \ A2 <> {}; then
consider x be object such that
A24: x in A \ A2 by XBOOLE_0:def 1;
A25: x in A & not x in A2 by A24,XBOOLE_0:def 5;
consider y be object such that
A26: y in B2 by XBOOLE_0:def 1;
A27: [x,y] in [:A,B:] by A3,A26,A24,ZFMISC_1:def 2;
not y in B1 by B18,A26,XBOOLE_0:3; then
not [x,y] in [:A1,B1:] & not [x,y] in [:A2,B2:] by A25,ZFMISC_1:87;
hence contradiction by A27,A2,XBOOLE_0:def 3;
end;
hence (A1 misses A2 & A = A1 \/ A2 & B = B1 & B = B2)
or (B1 misses B2 & B = B1 \/ B2 & A = A1 & A = A2)
by A3,A5,A18,A19,XBOOLE_1:8,37,A2,ZFMISC_1:114;
end;
end;
assume A28: (A1 misses A2 & A = A1 \/ A2 & B = B1 & B = B2)
or (B1 misses B2 & B = B1 \/ B2 & A = A1 & A = A2);
per cases by A28;
suppose A29: A1 misses A2 & A = A1 \/ A2 & B = B1 & B = B2;
for z be object holds not z in [:A1,B1:] /\ [:A2,B2:]
proof
let z be object;
assume z in [:A1,B1:] /\ [:A2,B2:]; then
A31: z in [:A1,B1:] & z in [:A2,B2:] by XBOOLE_0:def 4; then
consider x,y be object such that
A32: x in A1 & y in B1 & z = [x,y] by ZFMISC_1:84;
x in A2 & y in B2 by A31,A32,ZFMISC_1:87;
hence contradiction by A32,A29,XBOOLE_0:3;
end;
hence [:A1,B1:] misses [:A2,B2:] & [:A,B:] = [:A1,B1:] \/ [:A2,B2:]
by A29,ZFMISC_1:97,XBOOLE_0:4;
end;
suppose A33: B1 misses B2 & B = B1 \/ B2 & A = A1 & A = A2;
for z be object holds not z in [:A1,B1:] /\ [:A2,B2:]
proof
let z be object;
assume z in [:A1,B1:] /\ [:A2,B2:]; then
A35: z in [:A1,B1:] & z in [:A2,B2:] by XBOOLE_0:def 4; then
consider x,y be object such that
A36: x in A1 & y in B1 & z = [x,y] by ZFMISC_1:84;
x in A2 & y in B2 by A35,A36,ZFMISC_1:87;
hence contradiction by A36,A33,XBOOLE_0:3;
end;
hence [:A1,B1:] misses [:A2,B2:] & [:A,B:] = [:A1,B1:] \/ [:A2,B2:]
by A33,ZFMISC_1:97,XBOOLE_0:4;
end;
end;
definition
let C,D be non empty set, F be sequence of Funcs(C,D), n be Nat;
redefine func F.n -> Function of C,D; :: redefines . (FUNCT_1, definition)
correctness
proof
F.n in Funcs(C,D);
hence thesis by FUNCT_2:66;
end;
end;
theorem Th26:
for X,Y,A,B being set, x,y being object st x in X & y in Y holds
chi(A,X).x * chi(B,Y).y = chi([:A,B:],[:X,Y:]).(x,y)
proof
let X,Y,A,B be set, x,y be object;
assume A1: x in X & y in Y;
per cases;
suppose A2: x in A & y in B; then
A3: [x,y] in [:X,Y:] & [x,y] in [:A,B:] by A1,ZFMISC_1:87;
chi(A,X).x = 1 & chi(B,Y).y = 1 by A1,A2,FUNCT_3:def 3; then
chi(A,X).x * chi(B,Y).y = 1 * 1 by XXREAL_3:def 5;
hence chi(A,X).x * chi(B,Y).y = chi([:A,B:],[:X,Y:]).(x,y)
by A3,FUNCT_3:def 3;
end;
suppose A4: not x in A or not y in B; then
not [x,y] in [:A,B:] & [x,y] in [:X,Y:] by A1,ZFMISC_1:87; then
A5: chi([:A,B:],[:X,Y:]).(x,y) = 0 by FUNCT_3:def 3;
per cases by A4;
suppose not x in A; then
chi(A,X).x = 0 by A1,FUNCT_3:def 3;
hence chi(A,X).x * chi(B,Y).y = chi([:A,B:],[:X,Y:]).(x,y) by A5;
end;
suppose not y in B; then
chi(B,Y).y = 0 by A1,FUNCT_3:def 3;
hence chi(A,X).x * chi(B,Y).y = chi([:A,B:],[:X,Y:]).(x,y) by A5;
end;
end;
end;
registration
let A, B be set;
cluster chi (A,B) -> nonnegative;
coherence
proof
for x be object holds chi(A,B).x >= 0
proof
let x be object;
per cases;
suppose x in B & x in A;
hence chi(A,B).x >= 0 by FUNCT_3:def 3;
end;
suppose x in B & not x in A;
hence chi(A,B).x >= 0 by FUNCT_3:def 3;
end;
suppose not x in B; then
not x in dom(chi(A,B));
hence chi(A,B).x >= 0 by FUNCT_1:def 2;
end;
end;
hence chi(A,B) is nonnegative by SUPINF_2:51;
end;
end;
theorem :: Construction of complete sigma measure from pre-measure
for X be non empty set, S be semialgebra_of_sets of X,
P be pre-Measure of S, m be induced_Measure of S,P,
M be induced_sigma_Measure of S,m holds
COM(M) is complete by MEASURE3:20;
definition
func Family_of_Intervals -> semialgebra_of_sets of REAL equals
the set of all I where I is Interval;
correctness by SRINGS_3:28;
end;
theorem Th02:
Family_of_halflines c= Family_of_Intervals
proof
now let A be object;
assume A in Family_of_halflines; then
consider r be Element of REAL such that
A1: A = halfline r by PROB_1:def 11;
A = ].-infty,r.[ by A1,PROB_1:def 10;
hence A in Family_of_Intervals by A1;
end;
hence thesis;
end;
Lm01:
for I be Subset of REAL st I is open_interval holds I in Borel_Sets
proof
let I be Subset of REAL;
assume I is open_interval; then
consider a,b be R_eal such that
A1: I = ].a,b.[ by MEASURE5:def 2;
A2:Family_of_halflines c= Borel_Sets by PROB_1:def 9,def 12;
per cases by XXREAL_0:14;
suppose a = +infty; then
I = {} by A1,XXREAL_0:3,XXREAL_1:28;
hence I in Borel_Sets by MEASURE1:7;
end;
suppose A3: a = -infty;
per cases by XXREAL_0:14;
suppose b = +infty;
hence I in Borel_Sets by A1,A3,XXREAL_1:224,FINANCE2:11;
end;
suppose b = -infty; then
I = {} by A1,A3,XXREAL_1:20;
hence I in Borel_Sets by MEASURE1:7;
end;
suppose A4: b in REAL;
I = halfline(b) by A1,A3,PROB_1:def 10; then
I in Family_of_halflines by A4,PROB_1:def 11;
hence I in Borel_Sets by A2;
end;
end;
suppose A8: a in REAL; then
reconsider a1=a as Real;
per cases by XXREAL_0:14;
suppose A6: b = +infty; then
[.a1,b.[ is Element of Borel_Sets by FINANCE1:3; then
A7: {a} in Borel_Sets & [.a,b.[ in Borel_Sets by FINANCE2:5;
I = [.a,b.[ \ {a} by A1,A6,A8,XXREAL_0:9,XXREAL_1:136;
hence I in Borel_Sets by A7,MEASURE1:6;
end;
suppose b = -infty; then
I = {} by A1,XXREAL_1:210;
hence I in Borel_Sets by MEASURE1:7;
end;
suppose b in REAL; then
A9: ].a,b.] is Element of Borel_Sets & {b} is Element of Borel_Sets
by A8,FINANCE2:5,6;
per cases;
suppose a < b; then
I = ].a,b.] \ {b} by A1,XXREAL_1:137;
hence I in Borel_Sets by A9,MEASURE1:6;
end;
suppose a >= b; then
I = {} by A1,XXREAL_1:28;
hence I in Borel_Sets by MEASURE1:7;
end;
end;
end;
end;
Lm02:
for I be Subset of REAL st I is closed_interval holds I in Borel_Sets
proof
let I be Subset of REAL;
assume I is closed_interval; then
consider a,b be Real such that
A1: I = [.a,b.] by MEASURE5:def 3;
A2: ].a,b.] is Element of Borel_Sets & {a} is Element of Borel_Sets
by FINANCE2:5,6;
per cases;
suppose a <= b; then
I = ].a,b.] \/ {a} by A1,XXREAL_1:130;
hence I in Borel_Sets by A2,MEASURE1:11;
end;
suppose a > b; then
I = {} by A1,XXREAL_1:29;
hence I in Borel_Sets by MEASURE1:7;
end;
end;
Lm03:
for I be Subset of REAL st I is right_open_interval holds I in Borel_Sets
proof
let I be Subset of REAL;
assume I is right_open_interval; then
consider a be Real, b be R_eal such that
A1: I = [.a,b.[ by MEASURE5:def 4;
per cases by XXREAL_0:14;
suppose b = +infty; then
I is Element of Borel_Sets by A1,FINANCE1:3;
hence I in Borel_Sets;
end;
suppose b = -infty; then
I = {} by A1,XXREAL_0:5,XXREAL_1:27;
hence I in Borel_Sets by MEASURE1:7;
end;
suppose b in REAL; then
I is Element of Borel_Sets by A1,FINANCE1:4;
hence I in Borel_Sets;
end;
end;
Lm04:
for I be Subset of REAL st I is left_open_interval holds I in Borel_Sets
proof
let I be Subset of REAL;
assume I is left_open_interval; then
consider a be R_eal, b be Real such that
A1: I = ].a,b.] by MEASURE5:def 5;
per cases by XXREAL_0:14;
suppose a = +infty; then
I = {} by A1,XXREAL_0:3,XXREAL_1:26;
hence I in Borel_Sets by MEASURE1:7;
end;
suppose A2: a = -infty; then
A3: a < b by XREAL_0:def 1,XXREAL_0:12;
].a,b.[ is Element of Borel_Sets by A2,FINANCE1:3; then
].a,b.[ in Borel_Sets & {b} in Borel_Sets by FINANCE2:5; then
].a,b.[ \/ {b} in Borel_Sets by MEASURE1:11;
hence I in Borel_Sets by A1,A3,XXREAL_1:132;
end;
suppose a in REAL; then
I is Element of Borel_Sets by A1,FINANCE2:6;
hence I in Borel_Sets;
end;
end;
theorem Th03:
for I be Subset of REAL st I is Interval holds I in Borel_Sets
proof
let I be Subset of REAL;
assume I is Interval; then
I is open_interval or I is closed_interval or
I is right_open_interval or I is left_open_interval by MEASURE5:1;
hence thesis by Lm01,Lm02,Lm03,Lm04;
end;
theorem
sigma Family_of_Intervals = Borel_Sets &
sigma(Field_generated_by Family_of_Intervals) = Borel_Sets
proof
Family_of_Intervals c= sigma(Family_of_Intervals) by PROB_1:def 9; then
A1:Family_of_halflines c= sigma(Family_of_Intervals) by Th02;
now let x be object;
assume x in Family_of_Intervals; then
ex I be Interval st x = I;
hence x in Borel_Sets by Th03;
end; then
Family_of_Intervals c= Borel_Sets;
hence sigma Family_of_Intervals = Borel_Sets by A1,PROB_1:def 9,def 12;
hence thesis by SRINGS_3:23;
end;
begin :: Family of semialgebras, fields and measures
theorem Th05:
for X1,X2 be set, S1 be non empty Subset-Family of X1,
S2 be non empty Subset-Family of X2
holds the set of all [:a,b:] where a is Element of S1, b is Element of S2
is non empty Subset-Family of [:X1,X2:]
proof
let X1,X2 be set;
let S1 be non empty Subset-Family of X1;
let S2 be non empty Subset-Family of X2;
set L = the set of all [:a,b:] where a is Element of S1, b is Element of S2;
A1:L = {s where s is Subset of [:X1,X2:]: ex x1,x2 be set
st x1 in S1 & x2 in S2 & s=[:x1,x2:]} by SRINGS_2:2;
consider a be object such that
A2: a in S1 by XBOOLE_0:def 1;
consider b be object such that
A3: b in S2 by XBOOLE_0:def 1;
reconsider a as Element of S1 by A2;
reconsider b as Element of S2 by A3;
A4:[:a,b:] in L;
now let z be object;
assume z in L; then
ex s be Subset of [:X1,X2:] st
z = s & ex x1,x2 be set st x1 in S1 & x2 in S2 & s = [:x1,x2:] by A1;
hence z in bool [:X1,X2:];
end; then
L c= bool [:X1,X2:];
hence thesis by A4;
end;
theorem
for X,Y be set, M be with_empty_element Subset-Family of X,
N be with_empty_element Subset-Family of Y
holds the set of all [:A,B:] where A is Element of M, B is Element of N
is with_empty_element Subset-Family of [:X,Y:]
proof
let X,Y be set;
let M be with_empty_element Subset-Family of X,
N be with_empty_element Subset-Family of Y;
set L = the set of all [:A,B:] where A is Element of M, B is Element of N;
reconsider E1 = {} as Element of M by SETFAM_1:def 8;
reconsider E2 = {} as Element of N by SETFAM_1:def 8;
{} = [:E1,E2:] by ZFMISC_1:90; then
{} in L;
hence thesis by Th05;
end;
theorem Th07:
for X be set, F1,F2 be disjoint_valued FinSequence of X
st union rng F1 misses union rng F2 holds
F1^F2 is disjoint_valued FinSequence of X
proof
let X be set;
let F1,F2 be disjoint_valued FinSequence of X;
assume A1: union rng F1 misses union rng F2;
now let x,y be object;
assume A2: x <> y;
per cases;
suppose A3: x in dom(F1^F2) & y in dom(F1^F2); then
reconsider i=x, j=y as Nat;
per cases;
suppose A4: i in dom F1; then
A5: (F1^F2).x = F1.i by FINSEQ_1:def 7;
per cases;
suppose j in dom F1; then
(F1^F2).y = F1.j by FINSEQ_1:def 7;
hence (F1^F2).x misses (F1^F2).y by A2,A5,PROB_2:def 2;
end;
suppose not j in dom F1; then
consider j1 be Nat such that
A6: j1 in dom F2 & j = len F1 + j1 by A3,FINSEQ_1:25;
(F1^F2).y = F2.j1 by A6,FINSEQ_1:def 7; then
(F1^F2).x c= union rng F1 & (F1^F2).y c= union rng F2
by A4,A5,A6,FUNCT_1:3,ZFMISC_1:74;
hence (F1^F2).x misses (F1^F2).y by A1,XBOOLE_1:64;
end;
end;
suppose not i in dom F1; then
consider i1 be Nat such that
A7: i1 in dom F2 & i = len F1 + i1 by A3,FINSEQ_1:25;
A8: (F1^F2).x = F2.i1 by A7,FINSEQ_1:def 7;
per cases;
suppose A9: j in dom F1; then
(F1^F2).y = F1.j by FINSEQ_1:def 7; then
(F1^F2).x c= union rng F2 & (F1^F2).y c= union rng F1
by A7,A8,A9,FUNCT_1:3,ZFMISC_1:74;
hence (F1^F2).x misses (F1^F2).y by A1,XBOOLE_1:64;
end;
suppose not j in dom F1; then
consider j1 be Nat such that
A10: j1 in dom F2 & j = len F1 + j1 by A3,FINSEQ_1:25;
(F1^F2).y = F2.j1 by A10,FINSEQ_1:def 7;
hence (F1^F2).x misses (F1^F2).y by A2,A7,A10,A8,PROB_2:def 2;
end;
end;
end;
suppose not x in dom(F1^F2) or not y in dom(F1^F2); then
(F1^F2).x = {} or (F1^F2).y = {} by FUNCT_1:def 2;
hence (F1^F2).x misses (F1^F2).y;
end;
end;
hence thesis by PROB_2:def 2;
end;
theorem Th08:
for X1,X2 be set, S1 be Semiring of X1, S2 be Semiring of X2 holds
the set of all [:A,B:] where A is Element of S1, B is Element of S2
is Semiring of [:X1,X2:]
proof
let X1,X2 be set, S1 be Semiring of X1, S2 be Semiring of X2;
A1:S1 is semiring_of_sets of X1 by SRINGS_3:9;
S2 is diff-c=-finite-partition-closed by SRINGS_3:9; then
the set of all [:A,B:] where A is Element of S1, B is Element of S2
is cap-closed semiring_of_sets of [:X1,X2:] by A1,SRINGS_4:36;
hence thesis by SRINGS_3:10;
end;
theorem Th09:
for X1,X2 be set, S1 be semialgebra_of_sets of X1,
S2 be semialgebra_of_sets of X2 holds
the set of all [:A,B:] where A is Element of S1, B is Element of S2
is semialgebra_of_sets of [:X1,X2:]
proof
let X1,X2 be set,
S1 be semialgebra_of_sets of X1, S2 be semialgebra_of_sets of X2;
set S = the set of all [:A,B:] where A is Element of S1, B is Element of S2;
A1:S is Semiring of [:X1,X2:] by Th08;
X1 in S1 & X2 in S2 by SRINGS_3:def 6; then
[:X1,X2:] in S;
hence thesis by A1,SRINGS_3:def 6;
end;
theorem
for X1,X2 be set, F1 be Field_Subset of X1, F2 be Field_Subset of X2
holds the set of all [:A,B:] where A is Element of F1, B is Element of F2
is semialgebra_of_sets of [:X1,X2:]
proof
let X1,X2 be set, F1 be Field_Subset of X1, F2 be Field_Subset of X2;
set S = the set of all [:A,B:] where A is Element of F1, B is Element of F2;
F1 is semialgebra_of_sets of X1 & F2 is semialgebra_of_sets of X2
by SRINGS_3:20;
hence thesis by Th09;
end;
definition
let n be non zero Nat, X be non-empty n-element FinSequence;
mode SemialgebraFamily of X -> n-element FinSequence means
:Def2:
for i being Nat st i in Seg n holds
it.i is semialgebra_of_sets of X.i;
existence
proof
deffunc F(set)=bool (X.$1);
consider p being FinSequence such that
A1: len p = n and
A2: for i being Nat st i in dom p holds p.i=F(i) from FINSEQ_1:sch 2;
reconsider p as n-element FinSequence by A1,CARD_1:def 7;
take p;
hereby
let i be Nat;
assume
A3: i in Seg n;
reconsider Xi=X.i as set;
reconsider BXi=bool Xi as Subset-Family of Xi;
A4: BXi is cap-finite-partition-closed diff-c=-finite-partition-closed
with_countable_Cover with_empty_element Subset-Family of Xi;
A5: i in dom p by A3,A1,FINSEQ_1:def 3; then
A6: p.i is with_empty_element semi-diff-closed
cap-closed Subset-Family of X.i by A2,A4;
X.i in bool(X.i) by ZFMISC_1:def 1; then
X.i in p.i by A2,A5;
hence p.i is semialgebra_of_sets of X.i by A6,SRINGS_3:def 6;
end;
end;
end;
Lm05:
for n be non zero Nat, X be non-empty n-element FinSequence,
S be SemialgebraFamily of X
holds S is cap-closed-yielding SemiringFamily of X
proof
let n be non zero Nat, X be non-empty n-element FinSequence,
S be SemialgebraFamily of X;
A1:now let i be Nat;
assume i in Seg n; then
S.i is semialgebra_of_sets of X.i by Def2;
hence S.i is semiring_of_sets of X.i by SRINGS_3:9;
end;
for i be Nat st i in Seg n holds S.i is cap-closed by Def2;
hence thesis by A1,SRINGS_4:def 3,def 5;
end;
definition
let n be non zero Nat, X be non-empty n-element FinSequence;
redefine mode SemialgebraFamily of X :: redefines SemialgebraFamily (MEASUR10, definition)
-> cap-closed-yielding SemiringFamily of X;
correctness by Lm05;
end;
theorem Th11:
for n be non zero Nat, X be non-empty n-element FinSequence,
S be SemialgebraFamily of X
holds for i be Nat st i in Seg n holds X.i in S.i
proof
let n be non zero Nat, X be non-empty n-element FinSequence,
S be SemialgebraFamily of X;
hereby let i be Nat;
assume i in Seg n; then
S.i is semialgebra_of_sets of X.i by Def2;
hence X.i in S.i by SRINGS_3:def 6;
end;
end;
theorem Th12:
for X be non-empty 1-element FinSequence,
S be SemialgebraFamily of X holds
the set of all product <*s*> where s is Element of S.1 is
semialgebra_of_sets of the set of all <*x*> where x is Element of X.1
proof
let X be non-empty 1-element FinSequence,
S be SemialgebraFamily of X;
set S1 = the set of all product <*s*> where s is Element of S.1;
set X1 = the set of all <*x*> where x is Element of X.1;
A1:1 in Seg 1; then
X.1 in S.1 by Th11; then
A3:product <*X.1*> in S1;
S1 is cap-closed semiring_of_sets of X1 by SRINGS_4:34; then
A5:S1 is with_empty_element semi-diff-closed cap-closed Subset-Family of X1
by SRINGS_3:10;
1 in dom X by A1,FINSEQ_1:89; then
product <*X.1*> = the set of all <*y*> where y is Element of X.1
by SRINGS_4:24;
hence thesis by A3,A5,SRINGS_3:def 6;
end;
theorem Th13:
for X be non-empty 1-element FinSequence, S be SemialgebraFamily of X
holds SemiringProduct(S) is semialgebra_of_sets of product X
proof
let X be non-empty 1-element FinSequence, S be SemialgebraFamily of X;
set S1=the set of all product <*s*> where s is Element of S.1;
set X1=the set of all <*x*> where x is Element of X.1;
S1 = SemiringProduct(S) & X1 = product X by SRINGS_4:23,25;
hence thesis by Th12;
end;
theorem Th14:
for X1,X2 be set, S1 be semialgebra_of_sets of X1,
S2 be semialgebra_of_sets of X2 holds
the set of all [:s1,s2:] where s1 is Element of S1,
s2 is Element of S2 is semialgebra_of_sets of [:X1,X2:]
proof
let X1,X2 be set, S1 be semialgebra_of_sets of X1,
S2 be semialgebra_of_sets of X2;
set S = the set of all [:s1,s2:] where s1 is Element of S1,
s2 is Element of S2;
S1 is cap-closed semiring_of_sets of X1 &
S2 is cap-closed semiring_of_sets of X2 by SRINGS_3:9; then
S is cap-closed semiring_of_sets of [:X1,X2:] by SRINGS_4:36; then
A1:S is with_empty_element semi-diff-closed cap-closed
Subset-Family of [:X1,X2:] by SRINGS_3:10;
X1 in S1 & X2 in S2 by SRINGS_3:def 6; then
[:X1,X2:] in S;
hence thesis by A1,SRINGS_3:def 6;
end;
theorem Th15:
for n be non zero Nat, X be non-empty n-element FinSequence,
S be SemialgebraFamily of X holds
SemiringProduct(S) is semialgebra_of_sets of product X
proof
let n be non zero Nat, X be non-empty n-element FinSequence,
S be SemialgebraFamily of X;
defpred P[non zero Nat] means
for X be non-empty $1-element FinSequence,
S be SemialgebraFamily of X holds
SemiringProduct(S) is semialgebra_of_sets of product X;
A1:P[1] by Th13;
A2:now let k be non zero Nat;
assume P[k];
now let Xn1 be non-empty (k+1)-element FinSequence,
Sn1 be SemialgebraFamily of Xn1;
A3: SemiringProduct(Sn1) is cap-closed semiring_of_sets of product Xn1
by SRINGS_4:38; then
A4: SemiringProduct(Sn1) is semi-diff-closed by SRINGS_3:10;
A6: dom Xn1 = dom Sn1 by SRINGS_4:18;
now let x be object;
assume x in dom Sn1; then
x in Seg(k+1) by FINSEQ_1:89;
hence Xn1.x in Sn1.x by Th11;
end; then
Xn1 in product Sn1 by A6,CARD_3:9; then
product Xn1 in SemiringProduct(Sn1) by SRINGS_4:def 4;
hence SemiringProduct(Sn1) is semialgebra_of_sets of product Xn1
by A3,A4,SRINGS_3:def 6;
end;
hence P[k+1];
end;
for k be non zero Nat holds P[k] from NAT_1:sch 10(A1,A2);
hence thesis;
end;
theorem
for n be non zero Nat, Xn be non-empty n-element FinSequence,
X1 be non-empty 1-element FinSequence,
Sn be SemialgebraFamily of Xn, S1 be SemialgebraFamily of X1 holds
SemiringProduct(Sn^S1) is semialgebra_of_sets of product(Xn^X1)
proof
let n be non zero Nat, Xn be non-empty n-element FinSequence,
X1 be non-empty 1-element FinSequence,
Sn be SemialgebraFamily of Xn, S1 be SemialgebraFamily of X1;
A1:SemiringProduct(Sn) is semialgebra_of_sets of product Xn &
SemiringProduct(S1) is semialgebra_of_sets of product X1 by Th15;
reconsider S12 = the set of all [:s1,s2:] where
s1 is Element of SemiringProduct(Sn),
s2 is Element of SemiringProduct(S1) as
semialgebra_of_sets of [:product Xn,product X1:] by A1,Th14;
SemiringProduct(Sn) is cap-closed semiring_of_sets of product Xn &
SemiringProduct(S1) is cap-closed semiring_of_sets of product X1
by SRINGS_4:38; then
A5:SemiringProduct(Sn^S1) is cap-closed semiring_of_sets of product (Xn^X1)
by SRINGS_4:37; then
A6:SemiringProduct(Sn^S1) is semi-diff-closed by SRINGS_3:10;
A11:dom Xn = dom Sn & dom X1 = dom S1 by SRINGS_4:18; then
A8:len Xn = len Sn & len X1 = len S1 by FINSEQ_3:29;
len(Xn^X1) = len Xn + len X1 & len(Sn^S1) = len Sn + len S1
by FINSEQ_1:22; then
A7:dom (Xn^X1) = dom (Sn^S1) by A8,FINSEQ_3:29;
now let x be object;
assume A9: x in dom(Sn^S1);
per cases by A9,FINSEQ_1:25;
suppose A10: x in dom Sn; then
x in Seg n by FINSEQ_1:89; then
Xn.x in Sn.x by Th11; then
(Xn^X1).x in Sn.x by A10,A11,FINSEQ_1:def 7;
hence (Xn^X1).x in (Sn^S1).x by A10,FINSEQ_1:def 7;
end;
suppose ex k be Nat st k in dom S1 & x = len Sn + k; then
consider k be Nat such that
A12: k in dom S1 & x = len Sn + k;
k in Seg 1 by A12,FINSEQ_1:89; then
X1.k in S1.k by Th11; then
(Xn^X1).x in S1.k by A12,A11,A8,FINSEQ_1:def 7;
hence (Xn^X1).x in (Sn^S1).x by A12,FINSEQ_1:def 7;
end;
end; then
Xn^X1 in product(Sn^S1) by A7,CARD_3:9; then
product(Xn^X1) in SemiringProduct(Sn^S1) by SRINGS_4:def 4;
hence thesis by A5,A6,SRINGS_3:def 6;
end;
definition
let n be non zero Nat, X be non-empty n-element FinSequence;
mode FieldFamily of X -> n-element FinSequence means
:Def3:
for i being Nat st i in Seg n holds it.i is Field_Subset of X.i;
existence
proof
deffunc F(set)=bool (X.$1);
consider p being FinSequence such that
A1: len p = n and
A2: for i being Nat st i in dom p holds p.i=F(i) from FINSEQ_1:sch 2;
reconsider p as n-element FinSequence by A1,CARD_1:def 7;
take p;
hereby
let i be Nat;
assume i in Seg n; then
i in dom p by A1,FINSEQ_1:def 3; then
p.i = bool (X.i) by A2;
hence p.i is Field_Subset of X.i;
end;
end;
end;
Lm06:
for n be non zero Nat, X be non-empty n-element FinSequence,
S be FieldFamily of X
holds S is SemialgebraFamily of X
proof
let n be non zero Nat, X be non-empty n-element FinSequence,
S be FieldFamily of X;
for i be Nat st i in Seg n holds S.i is semialgebra_of_sets of X.i
proof
let i be Nat;
assume i in Seg n;
then S.i is Field_Subset of X.i by Def3;
hence thesis by SRINGS_3:20;
end;
hence thesis by Def2;
end;
definition
let n be non zero Nat, X be non-empty n-element FinSequence;
redefine mode FieldFamily of X -> SemialgebraFamily of X; :: redefines FieldFamily (MEASUR10, definition)
correctness by Lm06;
end;
theorem Th17:
for X be non-empty 1-element FinSequence,
S be FieldFamily of X holds
the set of all product <*s*> where s is Element of S.1 is
Field_Subset of the set of all <*x*> where x is Element of X.1
proof
let X be non-empty 1-element FinSequence, S be FieldFamily of X;
set S1 = the set of all product <*s*> where s is Element of S.1;
set X1 = the set of all <*x*> where x is Element of X.1;
dom X = Seg 1 by FINSEQ_1:89; then
A1:len X = 1 by FINSEQ_1:def 3;
A2: 1 in Seg 1; then
1 in dom X by FINSEQ_1:89; then
A4:X1 = product <*X.1*> by SRINGS_4:24;
A5:X = <*X.1*> by A1,FINSEQ_1:40;
reconsider F = S.1 as Field_Subset of X.1 by A2,Def3;
F is non empty;
then consider s be object such that
A7: s in F;
reconsider s as Element of S.1 by A7;
S1 = SemiringProduct(S) by SRINGS_4:25; then
reconsider S1 as Subset-Family of product X by SRINGS_4:22;
now let A be set;
assume A in S1; then
consider s be Element of S.1 such that
A8: A = product <*s*>;
(X.1) \ s in F by MEASURE1:def 1; then
product <* (X.1) \ s *> in S1;
hence (product X) \ A in S1 by A5,A8,SRINGS_4:27;
end;
hence thesis by A4,A5,Th12,MEASURE1:def 1;
end;
theorem
for X be non-empty 1-element FinSequence, S be FieldFamily of X
holds SemiringProduct(S) is Field_Subset of product X
proof
let X be non-empty 1-element FinSequence, S be SemialgebraFamily of X;
set S1=the set of all product <*s*> where s is Element of S.1;
set X1=the set of all <*x*> where x is Element of X.1;
S1 = SemiringProduct(S) & X1 = product X by SRINGS_4:23,25;
hence thesis by Th17;
end;
definition
let n be non zero Nat, X be non-empty n-element FinSequence,
S be FieldFamily of X;
mode MeasureFamily of S -> n-element FinSequence means
for i being Nat st i in Seg n
ex F being Field_Subset of X.i st F = S.i & it.i is Measure of F;
existence
proof
defpred P[Nat, object] means
ex F being Field_Subset of X.$1 st F = S.$1 & $2 is Measure of F;
A0:now let i be Nat;
assume i in Seg n;
then reconsider F = S.i as Field_Subset of X.i by Def3;
reconsider M = F --> 0. as Function of F,ExtREAL;
A1: for A,B being Element of F st A misses B holds M.(A \/ B) = M.A + M.B
proof
let A,B be Element of F;
assume A misses B;
A2: M.A = 0. & M.B = 0. by FUNCOP_1:7;
reconsider A,B as Element of S.i;
0.= M.A + M.B by A2;
hence thesis by FUNCOP_1:7;
end;
(for x being Element of S.i holds 0.<= M.x) & M.{} = 0.
by FUNCOP_1:7,PROB_1:4; then
M is nonnegative additive zeroed Function of F,ExtREAL
by A1,VALUED_0:def 19,MEASURE1:def 8,SUPINF_2:39;
hence ex M be object st P[i,M];
end;
consider M be FinSequence such that
A4: dom M = Seg n & for i be Nat st i in Seg n holds P[i,M.i]
from FINSEQ_1:sch 1(A0);
Seg len M = Seg n by A4,FINSEQ_1:def 3; then
reconsider M as n-element FinSequence by CARD_1:def 7,FINSEQ_1:6;
take M;
thus thesis by A4;
end;
end;
begin :: Product of two measures
definition
let X1,X2 be set, S1 be Field_Subset of X1, S2 be Field_Subset of X2;
func measurable_rectangles(S1,S2) -> semialgebra_of_sets of [:X1,X2:]
equals
the set of all [:A,B:] where A is Element of S1, B is Element of S2;
correctness
proof
S1 is semialgebra_of_sets of X1 & S2 is semialgebra_of_sets of X2
by SRINGS_3:20;
hence thesis by Th09;
end;
end;
theorem
for X being set, F being Field_Subset of X
ex S being semialgebra_of_sets of X
st F = S & F = Field_generated_by S
proof
let X be set, F be Field_Subset of X;
reconsider S = F as semialgebra_of_sets of X by SRINGS_3:20;
take S;
now let x be object;
assume x in Field_generated_by S; then
A2: x in meet{Z where Z is Field_Subset of X : S c= Z} by SRINGS_3:def 7;
F in {Z where Z is Field_Subset of X: S c= Z};
hence x in S by A2,SETFAM_1:def 1;
end; then
Field_generated_by S c= S;
hence thesis by SRINGS_3:21;
end;
definition
let X1,X2 be set, S1 be Field_Subset of X1, S2 be Field_Subset of X2,
m1 be Measure of S1, m2 be Measure of S2;
func product-pre-Measure(m1,m2) -> nonnegative zeroed Function
of measurable_rectangles(S1,S2),ExtREAL means :Def6:
for C be Element of measurable_rectangles(S1,S2)
ex A be Element of S1, B be Element of S2 st
C = [:A,B:] & it.C = m1.A * m2.B;
existence
proof
defpred P[Element of measurable_rectangles(S1,S2),Element of ExtREAL] means
ex A be Element of S1, B be Element of S2 st
$1 = [:A,B:] & $2 = m1.A * m2.B;
A1:for C be Element of measurable_rectangles(S1,S2)
ex y be Element of ExtREAL st P[C,y]
proof
let C be Element of measurable_rectangles(S1,S2);
C in the set of all [:A,B:] where A is Element of S1, B is Element of S2;
then consider A be Element of S1, B be Element of S2 such that
A2: C = [:A,B:];
set y = m1.A * m2.B;
take y;
thus thesis by A2;
end;
consider IT be Function of measurable_rectangles(S1,S2),ExtREAL such that
A3: for C be Element of measurable_rectangles(S1,S2) holds P[C,IT.C]
from FUNCT_2:sch 3(A1);
A6:now let x be object;
assume x in dom IT; then
reconsider C = x as Element of measurable_rectangles(S1,S2);
consider A be Element of S1, B be Element of S2 such that
A5: C = [:A,B:] & IT.C = m1.A * m2.B by A3;
0 <= m1.A & 0 <= m2.B by SUPINF_2:51;
hence 0 <= IT.x by A5;
end;
reconsider Z = {} as Element of measurable_rectangles(S1,S2)
by SETFAM_1:def 8;
consider A0 be Element of S1, B0 be Element of S2 such that
A7: Z = [:A0,B0:] & IT.Z = m1.A0 * m2.B0 by A3;
A0 = {} or B0 = {} by A7; then
m1.A0 = 0 or m2.B0 = 0 by VALUED_0:def 19; then
IT.{} = 0 by A7; then
reconsider IT as nonnegative zeroed Function of
measurable_rectangles(S1,S2),ExtREAL by A6,SUPINF_2:52,VALUED_0:def 19;
take IT;
thus for C be Element of measurable_rectangles(S1,S2) holds
ex A be Element of S1, B be Element of S2 st
C = [:A,B:] & IT.C = m1.A * m2.B by A3;
end;
uniqueness
proof
let F1,F2 be nonnegative zeroed Function
of measurable_rectangles(S1,S2),ExtREAL;
assume that
A1: for C be Element of measurable_rectangles(S1,S2)
ex A be Element of S1, B be Element of S2
st C = [:A,B:] & F1.C = m1.A * m2.B and
A2: for C be Element of measurable_rectangles(S1,S2)
ex A be Element of S1, B be Element of S2
st C = [:A,B:] & F2.C = m1.A * m2.B;
now let C be Element of measurable_rectangles(S1,S2);
consider A1 be Element of S1, B1 be Element of S2 such that
A3: C = [:A1,B1:] & F1.C = m1.A1 * m2.B1 by A1;
consider A2 be Element of S1, B2 be Element of S2 such that
A4: C = [:A2,B2:] & F2.C = m1.A2 * m2.B2 by A2;
per cases;
suppose A5: A1 = {} or B1 = {}; then
A2 = {} or B2 = {} by A3,A4; then
(m1.A1 = 0 or m2.B1 = 0) & (m1.A2 = 0 or m2.B2 = 0) by A5,VALUED_0:def 19;
hence F1.C = F2.C by A3,A4;
end;
suppose A1 <> {} & B1 <> {}; then
A1 = A2 & B1 = B2 by A3,A4,ZFMISC_1:110;
hence F1.C = F2.C by A3,A4;
end;
end;
hence F1 = F2 by FUNCT_2:def 8;
end;
end;
theorem Th20:
for X1,X2 be set, S1 be Field_Subset of X1, S2 be Field_Subset of X2,
m1 be Measure of S1, m2 be Measure of S2, A,B be set
st A in S1 & B in S2 holds
product-pre-Measure(m1,m2).([:A,B:]) = m1.A * m2.B
proof
let X1,X2 be set, S1 be Field_Subset of X1, S2 be Field_Subset of X2,
m1 be Measure of S1, m2 be Measure of S2, A,B be set;
assume A in S1 & B in S2; then
[:A,B:] in measurable_rectangles(S1,S2); then
consider A1 be Element of S1, B1 be Element of S2 such that
A2: [:A,B:] = [:A1,B1:] & product-pre-Measure(m1,m2).([:A,B:]) = m1.A1 * m2.B1
by Def6;
per cases;
suppose A3: A = {} or B = {}; then
[:A,B:] = {} by ZFMISC_1:90; then
A4: product-pre-Measure(m1,m2).([:A,B:]) = 0 by VALUED_0:def 19;
m1.A = 0 or m2.B = 0 by A3,VALUED_0:def 19;
hence thesis by A4;
end;
suppose A <> {} & B <> {}; then
A = A1 & B = B1 by A2,ZFMISC_1:110;
hence thesis by A2;
end;
end;
theorem
for X1,X2 be set, S1 be non empty Subset-Family of X1,
S2 be non empty Subset-Family of X2,
S be non empty Subset-Family of [:X1,X2:], H be FinSequence of S
st S = the set of all [:A,B:] where A is Element of S1, B is Element of S2
ex F be FinSequence of S1, G be FinSequence of S2 st
len H = len F & len H = len G &
for k be Nat st k in dom H & H.k <> {} holds H.k = [:F.k,G.k:]
proof
let X1,X2 be set, S1 be non empty Subset-Family of X1,
S2 be non empty Subset-Family of X2,
S be non empty Subset-Family of [:X1,X2:], H be FinSequence of S;
assume AS: S = the set of all [:A,B:]
where A is Element of S1, B is Element of S2;
A1:for k be Nat st k in dom H
ex A be Element of S1, B be Element of S2 st H.k = [:A,B:]
proof
let k be Nat;
assume A2: k in dom H;
H/.k in S; then
H.k in S by A2,PARTFUN1:def 6;
hence thesis by AS;
end;
defpred P1[Nat,set] means
ex B be Element of S2 st H.$1 = [:$2,B:];
Seg len H = dom H by FINSEQ_1:def 3; then
A3:for k be Nat st k in Seg len H ex A be Element of S1 st P1[k,A] by A1;
consider F be FinSequence of S1 such that
A4: dom F = Seg len H
& for k be Nat st k in Seg len H holds P1[k,F.k] from FINSEQ_1:sch 5(A3);
defpred P2[Nat,set] means
ex A be Element of S1 st H.$1 = [:A,$2:];
A5:for k be Nat st k in Seg len H ex B be Element of S2 st P2[k,B]
proof
let k be Nat;
assume k in Seg len H; then
k in dom H by FINSEQ_1:def 3; then
ex A be Element of S1, B be Element of S2 st H.k = [:A,B:] by A1;
hence thesis;
end;
consider G be FinSequence of S2 such that
A6: dom G = Seg len H
& for k be Nat st k in Seg len H holds P2[k,G.k] from FINSEQ_1:sch 5(A5);
take F,G;
thus len H = len F & len H = len G by A4,A6,FINSEQ_1:def 3;
hereby let k be Nat;
assume A8: k in dom H & H.k <> {}; then
A9: k in Seg len H by FINSEQ_1:def 3; then
consider B be Element of S2 such that
A10: H.k = [:F.k,B:] by A4;
consider A be Element of S1 such that
A11: H.k = [:A,G.k:] by A9,A6;
F.k <> {} & B <> {} by A8,A10;
hence H.k = [:F.k,G.k:] by A10,A11,ZFMISC_1:110;
end;
end;
theorem
for X be set,
S be non empty semi-diff-closed cap-closed Subset-Family of X,
E1,E2 be Element of S
ex F1,F2,F3 be disjoint_valued FinSequence of S
st union rng F1 = E1 \ E2
& union rng F2 = E2 \ E1 & union rng F3 = E1 /\ E2
& F1^F2^F3 is disjoint_valued FinSequence of S
proof
let X be set, S be non empty semi-diff-closed cap-closed Subset-Family of X,
E1,E2 be Element of S;
consider F1 be disjoint_valued FinSequence of S such that
A2: E1 \ E2 = Union F1 by SRINGS_3:def 1;
consider F2 be disjoint_valued FinSequence of S such that
A3: E2 \ E1 = Union F2 by SRINGS_3:def 1;
E1 \ E2 misses E2 \ E1 by XBOOLE_1:82; then
union rng F1 misses Union F2 by A2,A3,CARD_3:def 4; then
union rng F1 misses union rng F2 by CARD_3:def 4; then
reconsider G = F1^F2 as disjoint_valued FinSequence of S by Th07;
rng G = rng F1 \/ rng F2 by FINSEQ_1:31; then
A4:union rng G = union rng F1 \/ union rng F2 by ZFMISC_1:78;
Union F1 = union rng F1 & Union F2 = union rng F2 by CARD_3:def 4; then
Union G = (E1 \ E2) \/ (E2 \ E1) by A2,A3,A4,CARD_3:def 4; then
A5:Union G = E1 \+\ E2 by XBOOLE_0:def 6;
reconsider E = E1 /\ E2 as Element of S by FINSUB_1:def 2;
reconsider F3 = <*E*> as FinSequence of S;
reconsider F3 as disjoint_valued FinSequence of S;
take F1,F2,F3;
reconsider F = G^<*E*> as FinSequence of S;
thus union rng F1 = E1 \ E2 & union rng F2 = E2 \ E1 by A2,A3,CARD_3:def 4;
rng F3 = {E} by FINSEQ_1:38;
hence union rng F3 = E1 /\ E2 by ZFMISC_1:25;
A6:Union G misses E by A5,XBOOLE_1:103;
B1:len F = len G + 1 by FINSEQ_2:16;
A7:now let i,j be Nat;
assume A8: i in dom G & j = len F; then
A9: F.j = E by B1,FINSEQ_1:42;
F.i = G.i by A8,FINSEQ_1:def 7; then
F.i c= union rng G by A8,FUNCT_1:3,ZFMISC_1:74; then
F.i c= Union G by CARD_3:def 4;
hence F.i misses F.j by A6,A9,XBOOLE_1:63;
end;
now let x,y be object;
assume A10: x <> y;
per cases;
suppose A11: x in dom F & y in dom F; then
reconsider x1=x, y1=y as Nat;
A12: 1 <= x1 & x1 <= len F & 1 <= y1 & y1 <= len F by A11,FINSEQ_3:25;
per cases;
suppose A13: x1 = len F; then
y1 < len F by A10,A12,XXREAL_0:1; then
y1 <= len G by B1,NAT_1:13;
hence F.x misses F.y by A7,A13,A12,FINSEQ_3:25;
end;
suppose A11: y1 = len F; then
x1 < len F by A10,A12,XXREAL_0:1; then
x1 <= len G by B1,NAT_1:13;
hence F.x misses F.y by A7,A11,A12,FINSEQ_3:25;
end;
suppose x1 <> len F & y1 <> len F; then
x1 < len F & y1 < len F by A12,XXREAL_0:1; then
x1 <= len G & y1 <= len G by B1,NAT_1:13; then
x1 in dom G & y1 in dom G by A12,FINSEQ_3:25; then
F.x = G.x & F.y = G.y by FINSEQ_1:def 7;
hence F.x misses F.y by A10,PROB_2:def 2;
end;
end;
suppose not x in dom F or not y in dom F; then
F.x = {} or F.y = {} by FUNCT_1:def 2;
hence F.x misses F.y;
end;
end;
hence thesis by PROB_2:def 2;
end;
theorem
for X1,X2 be set, S1 be Field_Subset of X1, S2 be Field_Subset of X2,
m1 be Measure of S1, m2 be Measure of S2,
E1,E2 be Element of measurable_rectangles(S1,S2)
st E1 misses E2 & E1 \/ E2 in measurable_rectangles(S1,S2)
holds product-pre-Measure(m1,m2).(E1 \/ E2)
= product-pre-Measure(m1,m2).E1 + product-pre-Measure(m1,m2).E2
proof
let X1,X2 be set, S1 be Field_Subset of X1, S2 be Field_Subset of X2,
m1 be Measure of S1, m2 be Measure of S2,
E1,E2 be Element of measurable_rectangles(S1,S2);
assume that
A1:E1 misses E2 and
A2:E1 \/ E2 in measurable_rectangles(S1,S2);
set S = measurable_rectangles(S1,S2);
set P = product-pre-Measure(m1,m2);
reconsider E = E1 \/ E2 as Element of S by A2;
consider A be Element of S1, B be Element of S2 such that
A3: E = [:A,B:] & P.E = m1.A * m2.B by Def6;
consider A1 be Element of S1, B1 be Element of S2 such that
A4: E1 = [:A1,B1:] & P.E1 = m1.A1 * m2.B1 by Def6;
consider A2 be Element of S1, B2 be Element of S2 such that
A5: E2 = [:A2,B2:] & P.E2 = m1.A2 * m2.B2 by Def6;
per cases;
suppose E1 = {} or E2 = {}; then
(P.E1 = 0 & P.E = P.E2) or (P.E2 = 0 & P.E = P.E1) by VALUED_0:def 19;
hence P.(E1 \/ E2) = P.E1 + P.E2 by XXREAL_3:4;
end;
suppose E1 <> {} & E2 <> {}; then
A11:A <> {} & B <> {} & A1 <> {} & B1 <> {} & A2 <> {} & B2 <> {}
by A3,A4,A5;
per cases by A1,A4,A5,A3,A11,Th23;
suppose A13: A1 misses A2 & A = A1 \/ A2 & B = B1 & B = B2; then
[:A1,B1:] \/ [:A2,B2:] = [:A1 \/ A2,B:] by ZFMISC_1:97; then
P.(E1 \/ E2) = m1.(A1\/A2) * m2.B by A4,A5,Th20; then
A14: P.(E1 \/ E2) = (m1.A1 + m1.A2) * m2.B by A13,MEASURE1:def 3;
m1.A1 >= 0 & m1.A2 >= 0 by MEASURE1:def 2;
hence P.(E1 \/ E2) = P.E1 + P.E2 by A4,A5,A13,A14,XXREAL_3:96;
end;
suppose A15: B1 misses B2 & B = B1 \/ B2 & A = A1 & A = A2; then
[:A1,B1:] \/ [:A2,B2:] = [:A, B1 \/ B2:] by ZFMISC_1:97; then
P.(E1 \/ E2) = m1.A * m2.(B1\/B2) by A4,A5,Th20; then
A16: P.(E1 \/ E2) = m1.A * (m2.B1 + m2.B2) by A15,MEASURE1:def 3;
m2.B1 >= 0 & m2.B2 >= 0 by MEASURE1:def 2;
hence P.(E1 \/ E2) = P.E1 + P.E2 by A4,A5,A15,A16,XXREAL_3:96;
end;
end;
end;
theorem Th25:
for X be non empty set, S be non empty Subset-Family of X,
f be Function of NAT,S, F be Functional_Sequence of X,ExtREAL st
f is disjoint_valued & (for n be Nat holds F.n = chi(f.n,X))
holds (for x be object st x in X holds
chi(Union f,X).x = (lim Partial_Sums F).x)
proof
let X be non empty set, S be non empty Subset-Family of X,
f be Function of NAT,S, F be Functional_Sequence of X,ExtREAL;
assume A0: f is disjoint_valued;
assume A1: for n be Nat holds F.n = chi(f.n,X);
let x be object;
assume A2: x in X; then
reconsider x1=x as Element of X;
A3:now let n,m be Nat;
assume n <> m;
hereby let x be set;
assume x in dom(F.n) /\ dom(F.m); then
A5: x in dom(F.n) & x in dom(F.m) by XBOOLE_0:def 4;
F.n = chi(f.n,X) & F.m = chi(f.m,X) by A1; then
rng(F.n) c= {0,1} & rng(F.m) c= {0,1} by FUNCT_3:39; then
not +infty in rng(F.n) & not -infty in rng(F.m);
hence (F.n).x <> +infty or (F.m).x <> -infty by A5,FUNCT_1:3;
end;
end;
now let n,m be Nat;
F.n = chi(f.n,X) & F.m = chi(f.m,X) by A1; then
dom(F.n) = X & dom(F.m) = X by FUNCT_3:def 3;
hence dom(F.n) = dom(F.m);
end; then
A9:F is with_the_same_dom by MESFUNC8:def 2;
F.0 = chi(f.0,X) by A1; then
A20:dom(F.0) = X by FUNCT_3:def 3; then
dom((Partial_Sums F).0) = X by MESFUNC9:def 4; then
x in dom(lim Partial_Sums F) by A2,MESFUNC8:def 9; then
A14: (lim Partial_Sums F).x = lim((Partial_Sums F)#x1) by MESFUNC8:def 9;
per cases;
suppose A10: x in Union f; then
x in union rng f by CARD_3:def 4; then
consider V be set such that
A11: x in V & V in rng f by TARSKI:def 4;
consider n be Element of NAT such that
A12: V = f.n by A11,FUNCT_2:113;
A15:for m be Nat st m <> n holds (F.m).x1 = 0
proof
let m be Nat;
assume m <> n; then
not x in f.m by A0,PROB_2:def 2,A11,A12,XBOOLE_0:3; then
chi(f.m,X).x = 0 by A2,FUNCT_3:def 3;
hence (F.m).x1 = 0 by A1;
end;
defpred P1[Nat] means $1 < n implies ((Partial_Sums F)#x1).$1 = 0;
now assume A16: 0 < n;
((Partial_Sums F)#x1).0 = ((Partial_Sums F).0).x1 by MESFUNC5:def 13
.= (F.0).x1 by MESFUNC9:def 4;
hence ((Partial_Sums F)#x1).0 = 0 by A15,A16;
end; then
A17:P1[0];
A18:for k be Nat st P1[k] holds P1[k+1]
proof
let k be Nat;
assume A19: P1[k];
assume A21: k+1 < n; then
A22: (Partial_Sums(F#x1)).k = 0 by A9,A19,A20,A3,MESFUNC9:def 5,32,NAT_1:13;
((Partial_Sums F)#x1).(k+1)
= (Partial_Sums(F#x1)).(k+1) by A3,A9,A20,MESFUNC9:def 5,32
.= (Partial_Sums(F#x1)).k + (F#x1).(k+1) by MESFUNC9:def 1
.= (F#x1).(k+1) by A22,XXREAL_3:4
.= (F.(k+1)).x1 by MESFUNC5:def 13;
hence ((Partial_Sums F)#x1).(k+1) = 0 by A15,A21;
end;
A23:for k be Nat holds P1[k] from NAT_1:sch 2(A17,A18);
defpred P2[Nat] means $1 >= n implies ((Partial_Sums F)#x1).$1 = 1;
now assume 0 >= n; then
A24: n = 0;
A25: ((Partial_Sums F)#x1).0 = ((Partial_Sums F).0).x1 by MESFUNC5:def 13
.= (F.0).x1 by MESFUNC9:def 4;
F.0 = chi(f.n,X) by A24,A1;
hence ((Partial_Sums F)#x1).0 = 1 by A25,A11,A12,FUNCT_3:def 3;
end; then
A26:P2[0];
A27:for k be Nat st P2[k] holds P2[k+1]
proof
let k be Nat;
assume A28: P2[k];
assume A29: k+1 >= n;
A30: ((Partial_Sums F)#x1).(k+1)
= (Partial_Sums(F#x1)).(k+1) by A3,A9,A20,MESFUNC9:def 5,32
.= (Partial_Sums(F#x1)).k + (F#x1).(k+1) by MESFUNC9:def 1;
per cases;
suppose A31: k >= n; then
k+1 > n by NAT_1:13; then
(F.(k+1)).x1 = 0 by A15; then
(F#x1).(k+1) = 0 by MESFUNC5:def 13; then
((Partial_Sums F)#x1).(k+1) = (Partial_Sums(F#x1)).k by A30,XXREAL_3:4;
hence ((Partial_Sums F)#x1).(k+1) = 1
by A28,A31,A3,A9,A20,MESFUNC9:def 5,32;
end;
suppose A33: k < n; then
A34: k+1 = n by A29,NAT_1:8;
((Partial_Sums F)#x1).k = 0 by A23,A33; then
(Partial_Sums(F#x1)).k = 0 by A3,A9,A20,MESFUNC9:def 5,32; then
((Partial_Sums F)#x1).(k+1) = (F#x1).(k+1) by A30,XXREAL_3:4
.= (F.(k+1)).x1 by MESFUNC5:def 13
.= (chi(f.(k+1),X)).x by A1;
hence ((Partial_Sums F)#x1).(k+1) = 1 by A34,A11,A12,FUNCT_3:def 3;
end;
end;
A35:for k be Nat holds P2[k] from NAT_1:sch 2(A26,A27);
for k be Nat holds (((Partial_Sums F)#x1)^\n).k = 1
proof
let k be Nat;
(((Partial_Sums F)#x1)^\n).k = ((Partial_Sums F)#x1).(n+k) by NAT_1:def 3;
hence thesis by A35,NAT_1:12;
end; then
((Partial_Sums F)#x1)^\n is convergent_to_finite_number
& lim (((Partial_Sums F)#x1)^\n) = 1 by MESFUNC5:52; then
(lim Partial_Sums F).x = 1 by A14,RINFSUP2:16;
hence chi(Union f,X).x = (lim Partial_Sums F).x by A10,A2,FUNCT_3:def 3;
end;
suppose A37: not x in Union f; then
not x in union rng f by CARD_3:def 4; then
A38:for V be set st V in rng f holds not x in V by TARSKI:def 4;
defpred P3[Nat] means ((Partial_Sums F)#x1).$1 = 0;
A39:((Partial_Sums F)#x1).0 = ((Partial_Sums F).0).x1 by MESFUNC5:def 13
.= (F.0).x1 by MESFUNC9:def 4
.= chi(f.0,X).x1 by A1;
not x in f.0 by A38,FUNCT_2:4; then
A40:P3[0] by A39,FUNCT_3:def 3;
A41:for k be Nat st P3[k] holds P3[k+1]
proof
let k be Nat;
assume P3[k]; then
A42: (Partial_Sums(F#x1)).k = 0 by A3,A9,A20,MESFUNC9:def 5,32;
A43: ((Partial_Sums F)#x1).(k+1)
= (Partial_Sums(F#x1)).(k+1) by A3,A9,A20,MESFUNC9:def 5,32
.= (Partial_Sums(F#x1)).k + (F#x1).(k+1) by MESFUNC9:def 1
.= (F#x1).(k+1) by A42,XXREAL_3:4
.= (F.(k+1)).x1 by MESFUNC5:def 13
.= chi(f.(k+1),X).x by A1;
not x in f.(k+1) by A38,FUNCT_2:4;
hence P3[k+1] by A43,FUNCT_3:def 3;
end;
for k be Nat holds P3[k] from NAT_1:sch 2(A40,A41); then
(Partial_Sums F)#x1 is convergent_to_finite_number
& lim ((Partial_Sums F)#x1) = 0 by MESFUNC5:52;
hence chi(Union f,X).x = (lim Partial_Sums F).x
by A37,A14,FUNCT_3:def 3;
end;
end;
theorem Th27:
for X being non empty set,
S being SigmaField of X, M being sigma_Measure of S,
f being PartFunc of X,ExtREAL, r being Real
st dom f in S & 0 <= r & (for x be object st x in dom f holds f.x = r)
holds Integral(M,f) = r * M.(dom f)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, r be Real;
assume that
A1: dom f in S & 0 <= r and
A2: for x be object st x in dom f holds f.x = r;
now let y be object;
assume y in rng f; then
consider x be object such that
A3: x in dom f & y = f.x by FUNCT_1:def 3;
y = r by A2,A3;
hence y in REAL by XREAL_0:def 1;
end; then
rng f c= REAL; then
reconsider g = f as PartFunc of X,REAL by RELSET_1:6;
A4:Integral(M,g) = r * M.(dom g) by A1,A2,MESFUNC6:97;
f = R_EAL g by MESFUNC5:def 7;
hence thesis by A4,MESFUNC6:def 3;
end;
theorem Th28:
for X being non empty set,
S being SigmaField of X, M being sigma_Measure of S,
f being PartFunc of X,ExtREAL, A being Element of S
st (ex E being Element of S st E = dom f & f is E-measurable) &
(for x being object st x in dom f \ A holds f.x = 0) &
f is nonnegative
holds Integral(M,f) = Integral(M,f|A)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, A be Element of S;
assume that
A1: ex E be Element of S st E = dom f & f is E-measurable and
A2: for x be object st x in dom f \ A holds f.x = 0 and
A3: f is nonnegative;
consider E be Element of S such that
A4: E = dom f & f is E-measurable by A1;
reconsider B = E\A as Element of S;
A6:Integral(M,f|(A\/B)) = Integral(M,f|A) + Integral(M,f|B)
by A1,A3,MESFUNC5:91,XBOOLE_1:79;
A \/ B = dom f \/ A by A4,XBOOLE_1:39; then
A7:f|(A\/B) = f by RELAT_1:68,XBOOLE_1:7;
A8:B c= dom f by A4,XBOOLE_1:36;
dom(f|B) = dom f /\ B by RELAT_1:61; then
A9:dom(f|B) = B by A4,XBOOLE_1:28,36;
now let x be object;
assume A10: x in dom(f|B); then
(f|B).x = (f|B)/.x by PARTFUN1:def 6 .= f/.x by A10,PARTFUN1:80
.= f.x by A10,A8,A9,PARTFUN1:def 6;
hence (f|B).x = 0 by A2,A10,A9,A4;
end; then
Integral(M,f|B) = 0 * M.(dom(f|B)) by A9,Th27 .= 0;
hence thesis by A6,A7,XXREAL_3:4;
end;
theorem
for X being non empty set,
S being SigmaField of X, M being sigma_Measure of S,
f being PartFunc of X,ExtREAL, A being Element of S
st f is_integrable_on M &
(for x being object st x in dom f \ A holds f.x = 0)
holds Integral(M,f) = Integral(M,f|A)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, A be Element of S;
assume that
A1: f is_integrable_on M and
A2: for x being object st x in dom f \ A holds f.x = 0;
consider E be Element of S such that
A3: E = dom f & f is E-measurable by A1,MESFUNC5:def 17;
reconsider B = E\A as Element of S;
A4:Integral(M,f|(A\/B)) = Integral(M,f|A) + Integral(M,f|B)
by A1,MESFUNC5:98,XBOOLE_1:79;
A \/ B = dom f \/ A by A3,XBOOLE_1:39; then
A5:f|(A\/B) = f by RELAT_1:68,XBOOLE_1:7;
A6:B c= dom f by A3,XBOOLE_1:36;
dom(f|B) = dom f /\ B by RELAT_1:61; then
A7:dom(f|B) = B by A3,XBOOLE_1:28,36;
now let x be object;
assume A9: x in dom(f|B); then
(f|B).x = (f|B)/.x by PARTFUN1:def 6 .= f/.x by A9,PARTFUN1:80
.= f.x by A9,A7,A6,PARTFUN1:def 6;
hence (f|B).x = 0 by A2,A9,A7,A3;
end; then
Integral(M,f|B) = 0 * M.(dom(f|B)) by A7,Th27 .= 0;
hence Integral(M,f) = Integral(M,f|A) by A4,A5,XXREAL_3:4;
end;
theorem Th30:
for X1,X2 being non empty set,
S1 being SigmaField of X1,
S2 being SigmaField of X2,
M2 being sigma_Measure of S2,
D being Function of NAT,S1, E being Function of NAT,S2,
A being Element of S1, B being Element of S2,
F being Functional_Sequence of X2,ExtREAL,
RD being sequence of Funcs(X1,REAL),
x being Element of X1 st
(for n being Nat holds RD.n = chi(D.n,X1))
& (for n being Nat holds F.n = ((RD.n).x)(#)(chi(E.n,X2)))
& (for n being Nat holds E.n c= B)
holds
ex I be ExtREAL_sequence st
(for n be Nat holds I.n = M2.(E.n) * (chi(D.n,X1).x)) &
I is summable & Integral(M2,lim Partial_Sums F) = Sum I
proof
let X1,X2 be non empty set, S1 being SigmaField of X1,
S2 be SigmaField of X2, M2 be sigma_Measure of S2,
D be Function of NAT,S1, E be Function of NAT,S2,
A be Element of S1, B be Element of S2,
F be Functional_Sequence of X2,ExtREAL,
RD be sequence of Funcs(X1,REAL),
x be Element of X1;
assume that
A7: (for n being Nat holds RD.n = chi(D.n,X1)) and
A8: (for n being Nat holds F.n = ((RD.n).x)(#)(chi(E.n,X2))) and
A9: (for n being Nat holds E.n c= B);
B1:for n be Nat holds dom(F.n) = X2
proof
let n be Nat;
dom(F.n) = dom( ((RD.n).x)(#)(chi(E.n,X2)) ) by A8; then
dom(F.n) = dom(chi(E.n,X2)) by MESFUNC1:def 6;
hence dom(F.n) = X2 by FUNCT_3:def 3;
end;
reconsider SX2 = X2 as Element of S2 by PROB_1:5;
P1:dom(F.0) = X2 by B1;
B2:for n be Nat, y be set st y in E.n holds (F.n).y = 0 or (F.n).y = 1
proof
let n be Nat, y be set;
assume B3: y in E.n;
B4: E.n in S2; then
y in X2 by B3; then
B5: y in dom(F.n) by B1; then
B6: (F.n).y in rng(F.n) by FUNCT_1:3;
reconsider y1=y as Element of X2 by B3,B4;
B7: now assume x in D.n; then
chi(D.n,X1).x = 1 by FUNCT_3:def 3; then
(RD.n).x = 1 by A7; then
F.n = 1(#)(chi(E.n,X2)) by A8; then
F.n = chi(E.n,X2) by MESFUNC2:1; then
rng(F.n) c= {0,1} by FUNCT_3:39;
hence (F.n).y = 0 or (F.n).y = 1 by B6,TARSKI:def 2;
end;
now assume not x in D.n; then
chi(D.n,X1).x = 0 by FUNCT_3:def 3; then
(RD.n).x = 0 by A7; then
F.n = ( 0(#)(chi(E.n,X2)) ) by A8; then
(F.n).y = 0 * chi(E.n,X2).y1 by B5,MESFUNC1:def 6;
hence (F.n).y = 0;
end;
hence (F.n).y =0 or (F.n).y = 1 by B7;
end;
B8:for n be Nat, y be set st not y in E.n holds (F.n).y = 0
proof
let n be Nat, y be set;
assume B9: not y in E.n;
B10:now assume B11: y in X2; then
reconsider y1=y as Element of X2;
B12: chi(E.n,X2).y1 = 0 by B9,FUNCT_3:def 3;
B13: y in dom(F.n) by B1,B11;
(F.n) = ((RD.n).x)(#)(chi(E.n,X2)) by A8; then
(F.n).y = (RD.n).x * (chi(E.n,X2)).y1 by B13,MESFUNC1:def 6;
hence (F.n).y = 0 by B12;
end;
now assume not y in X2; then
not y in dom(F.n);
hence (F.n).y = 0 by FUNCT_1:def 2;
end;
hence (F.n).y = 0 by B10;
end;
P2:now let n,m be Nat;
assume n <> m;
thus for y be set st y in dom(F.n) /\ dom(F.m) holds
(F.n).y <> +infty or (F.m).y <> -infty
proof
let y be set;
assume y in dom(F.n) /\ dom(F.m);
y in E.n implies (F.n).y <> +infty or (F.m).y <> -infty by B2;
hence (F.n).y <> +infty or (F.m).y <> -infty by B8;
end;
end; then
S2:F is additive by MESFUNC9:def 5;
now let n,m be Nat;
dom(F.n) = X2 & dom(F.m) = X2 by B1;
hence dom(F.n) = dom(F.m);
end; then
P3:F is with_the_same_dom by MESFUNC8:def 2;
P4:for n be Nat holds F.n is nonnegative & F.n is B-measurable
proof
let n be Nat;
now let y be object;
per cases;
suppose not y in dom(F.n);
hence (F.n).y >= 0 by FUNCT_1:def 2;
end;
suppose y in dom(F.n) & y in E.n;
hence (F.n).y >= 0 by B2;
end;
suppose y in dom(F.n) & not y in E.n;
hence (F.n).y >= 0 by B8;
end;
end;
hence F.n is nonnegative by SUPINF_2:51;
thus F.n is B-measurable
proof
B14: dom(chi(E.n,X2)) = X2 by FUNCT_3:def 3;
per cases;
suppose x in D.n; then
chi(D.n,X1).x = 1 by FUNCT_3:def 3; then
(RD.n).x = 1 by A7; then
F.n = 1 (#) (chi(E.n,X2)) by A8;
hence F.n is B-measurable by B14,MESFUNC1:37,MESFUNC2:29;
end;
suppose not x in D.n; then
chi(D.n,X1).x = 0 by FUNCT_3:def 3; then
(RD.n).x = 0 by A7; then
F.n = 0 (#) (chi(E.n,X2)) by A8;
hence F.n is B-measurable by B14,MESFUNC1:37,MESFUNC2:29;
end;
end;
end;
for y be Element of X2 st y in B holds F#y is summable
proof
let y be Element of X2;
assume y in B;
for n be Element of NAT holds 0 <= (F#y).n
proof
let n be Element of NAT;
(F#y).n = (F.n).y by MESFUNC5:def 13;
hence 0 <= (F#y).n by P4,SUPINF_2:51;
end; then
F#y is nonnegative by SUPINF_2:39; then
Partial_Sums (F#y) is non-decreasing by MESFUNC9:16;
hence F#y is summable by RINFSUP2:37,MESFUNC9:def 2;
end; then
consider I be ExtREAL_sequence such that
Q1: (for n be Nat holds I.n = Integral(M2,(F.n)|B))
& I is summable & Integral(M2,(lim(Partial_Sums F))|B) = Sum I
by P1,P2,P3,P4,MESFUNC9:def 5,51;
take I;
R1:for n be Nat holds chi(E.n,X2) is SX2-measurable by MESFUNC2:29;
Q2:for n be Nat holds I.n = M2.(E.n) * chi(D.n,X1).x
proof
let n be Nat;
B16:I.n = Integral(M2,(F.n)|B) by Q1;
B17:dom((F.n)|B) = dom(F.n) /\ B by RELAT_1:61; then
B18:dom((F.n)|B) = X2 /\ B by B1;
B19:dom((RD.n).x(#)(chi(E.n,X2)|B)) = dom(chi(E.n,X2)|B) by MESFUNC1:def 6
.= dom(chi(E.n,X2)) /\ B by RELAT_1:61
.= X2 /\ B by FUNCT_3:def 3;
now let y be object;
assume B20: y in dom((F.n)|B); then
reconsider y1=y as Element of X2;
B22: y in X2 & y in B by B17,B20,XBOOLE_0:def 4;
dom(chi(E.n,X2)) = X2 by FUNCT_3:def 3; then
B23: y in dom(((RD.n).x)(#)(chi(E.n,X2))) by B22,MESFUNC1:def 6;
B21: ((F.n)|B).y = (F.n).y1 by B20,FUNCT_1:47
.= (((RD.n).x)(#)(chi(E.n,X2))).y1 by A8
.= ((RD.n).x) * (chi(E.n,X2).y) by B23,MESFUNC1:def 6;
( (RD.n).x (#) (chi(E.n,X2)|B) ).y
= ((RD.n).x) * (chi(E.n,X2)|B).y by B20,B18,B19,MESFUNC1:def 6
.= ((RD.n).x) * (chi(E.n,X2).y) by B22,FUNCT_1:49;
hence ((F.n)|B).y = ( (RD.n).x (#) (chi(E.n,X2)|B) ).y by B21;
end; then
B24:I.n = Integral(M2,(RD.n).x(#)(chi(E.n,X2)|B))
by B16,B18,B19,FUNCT_1:def 11;
C0: B = dom( (RD.n).x (#) (chi(E.n,X2)|B) ) by B19,XBOOLE_1:28;
C4: dom(chi(E.n,X2)|B) = dom(chi(E.n,X2)) /\ B by RELAT_1:61;
dom(chi(E.n,X2)) /\ B = X2 /\ B by FUNCT_3:def 3; then
C3: dom(chi(E.n,X2)) /\ B = B by XBOOLE_1:28; then
C8: chi(E.n,X2)|B is B-measurable by MESFUNC2:29,MESFUNC5:42;
C5a: chi(E.n,X2)|B is nonnegative by MESFUNC5:15;
C6: now assume x in D.n; then
chi(D.n,X1).x = 1 by FUNCT_3:def 3;
hence (RD.n).x = 1 by A7;
end;
C7: now assume not x in D.n; then
chi(D.n,X1).x = 0 by FUNCT_3:def 3;
hence (RD.n).x = 0 by A7;
end; then
(RD.n).x (#) (chi(E.n,X2)|B) is nonnegative by C5a,C6,MESFUNC5:20; then
I.n = integral+(M2,(RD.n).x(#)(chi(E.n,X2)|B))
by B24,C0,C8,C3,C4,MESFUNC1:37,MESFUNC5:88;
then
I.n = (RD.n).x * integral+(M2,(chi(E.n,X2)|B))
by C3,C4,C6,C7,C8,MESFUNC5:15,86; then
D2: I.n = (RD.n).x * Integral(M2,(chi(E.n,X2)|B))
by C3,C4,C8,MESFUNC5:15,88;
E1: dom(chi(E.n,X2)) = X2 by FUNCT_3:def 3;
for y being object st y in dom(chi(E.n,X2)) \ B holds chi(E.n,X2).y = 0
proof
let y be object;
assume E4: y in dom(chi(E.n,X2)) \ B; then
reconsider y1=y as Element of X2;
E.n c= B by A9; then
not y1 in E.n by E4,XBOOLE_0:def 5;
hence chi(E.n,X2).y = 0 by FUNCT_3:def 3;
end; then
Integral(M2,chi(E.n,X2)) = Integral(M2,chi(E.n,X2)|B)
by E1,R1,Th28; then
I.n = M2.(E.n) * (RD.n).x by D2,MESFUNC9:14;
hence I.n = M2.(E.n) * (chi(D.n,X1).x) by A7;
end;
F1:dom(lim Partial_Sums F) = dom((Partial_Sums F).0) by MESFUNC8:def 9
.= dom(F.0) by MESFUNC9:def 4; then
F4:dom(lim Partial_Sums F) = SX2 by B1;
G0:Partial_Sums F is with_the_same_dom Functional_Sequence of X2,ExtREAL
by P2,P3,MESFUNC9:def 5,43;
G1:dom((Partial_Sums F).0) = dom(F.0) by MESFUNC9:def 4 .= SX2 by B1;
R2:for n be Nat holds F.n is SX2-measurable
proof
let n be Nat;
chi(E.n,X2) is SX2-measurable & dom(chi(E.n,X2)) = SX2
by MESFUNC2:29,FUNCT_3:def 3; then
((RD.n).x)(#)(chi(E.n,X2)) is SX2-measurable by MESFUNC1:37;
hence F.n is SX2-measurable by A8;
end;
for n be Nat holds F.n is without-infty
proof
let n be Nat;
F.n is nonnegative by P4;
hence F.n is without-infty;
end; then
G2:for n be Nat holds (Partial_Sums F).n is SX2-measurable
by R2,MESFUNC9:41;
for y be Element of X2 st y in SX2 holds
(Partial_Sums F)#y is convergent
proof
let y be Element of X2;
assume y in SX2; then
y in dom(F.0) by B1;
hence (Partial_Sums F)#y is convergent by P3,P4,MESFUNC9:38;
end; then
F2: (lim Partial_Sums F) is SX2-measurable by G0,G1,G2,MESFUNC8:25;
F3:for y being object st y in dom(lim Partial_Sums F) \ B
holds (lim Partial_Sums F).y = 0
proof
let y be object;
assume K0: y in dom(lim Partial_Sums F) \ B; then
K1: y in dom(lim Partial_Sums F) & not y in B by XBOOLE_0:def 5; then
y in dom((Partial_Sums F).0) by MESFUNC8:def 9; then
J1: y in dom(F.0) by MESFUNC9:def 4;
reconsider y1 = y as Element of X2 by K0;
K2: (lim Partial_Sums F).y = lim((Partial_Sums F)#y1)
by K1,MESFUNC8:def 9;
for n be Nat holds ((Partial_Sums F)#y1).n = 0
proof
let n be Nat;
K6: ((Partial_Sums F)#y1).n = ((Partial_Sums F).n).y1 by MESFUNC5:def 13;
defpred P[Nat] means ((Partial_Sums F).$1).y1 = 0;
K3: ((Partial_Sums F).0).y1 = (F.0).y1 by MESFUNC9:def 4;
E.0 c= B by A9; then
K4: P[0] by K1,K3,B8;
K5: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume J2: P[k];
J3: dom((Partial_Sums F).(k+1)) = dom((Partial_Sums F).0)
by S2,P3,MESFUNC9:43,MESFUNC8:def 2
.= dom(F.0) by MESFUNC9:def 4;
J4: E.(k+1) c= B by A9;
(Partial_Sums F).(k+1) = (Partial_Sums F).k + F.(k+1)
by MESFUNC9:def 4; then
((Partial_Sums F).(k+1)).y1
= ((Partial_Sums F).k).y1 + (F.(k+1)).y1 by J1,J3,MESFUNC1:def 3
.= (F.(k+1)).y1 by J2,XXREAL_3:4;
hence P[k+1] by J4,B8,K1;
end;
for k be Nat holds P[k] from NAT_1:sch 2(K4,K5);
hence ((Partial_Sums F)#y1).n = 0 by K6;
end;
hence (lim Partial_Sums F).y = 0 by K2,MESFUNC5:52;
end;
for y be object st y in dom(lim Partial_Sums F) holds
(lim Partial_Sums F).y >= 0
proof
let y be object;
assume L1: y in dom(lim Partial_Sums F); then
reconsider y1=y as Element of X2;
L2: for n be Nat holds ((Partial_Sums F)#y1).n >= 0
proof
let n be Nat;
((Partial_Sums F).n).y1 >= 0 by P4,MESFUNC9:36,SUPINF_2:51;
hence ((Partial_Sums F)#y1).n >= 0 by MESFUNC5:def 13;
end;
lim((Partial_Sums F)#y1) >= 0 by L1,F1,L2,P3,P4,MESFUNC9:10,38;
hence (lim Partial_Sums F).y >= 0 by L1,MESFUNC8:def 9;
end;
hence thesis by Q1,Q2,F4,F2,F3,Th28,SUPINF_2:52;
end;
theorem
for X being non empty set, S being SigmaField of X, A being Element of S,
p being R_eal holds
X --> p is A-measurable
proof
let X be non empty set, S be SigmaField of X, A be Element of S,
p be R_eal;
A0:dom(X --> p) = X by FUNCOP_1:13;
for r be Real holds A /\ great_eq_dom(X --> p, r) in S
proof
let r be Real;
per cases;
suppose A2: r > p;
for x be object holds not x in great_eq_dom(X --> p,r)
proof
let x be object;
hereby assume x in great_eq_dom(X-->p, r); then
x in dom(X-->p) & r <= (X-->p).x by MESFUNC1:def 14;
hence contradiction by A2,FUNCOP_1:7;
end;
end; then
great_eq_dom(X --> p, r) = {} by XBOOLE_0:def 1;
hence A /\ great_eq_dom(X --> p, r) in S by MEASURE1:7;
end;
suppose A4: r <= p;
now let x be object;
assume A6: x in X; then
(X-->p).x = p by FUNCOP_1:7;
hence x in great_eq_dom(X-->p,r) by A0,A4,A6,MESFUNC1:def 14;
end; then
X c= great_eq_dom(X-->p,r); then
great_eq_dom(X --> p, r) = X; then
A /\ great_eq_dom(X --> p, r) = A by XBOOLE_1:28;
hence A /\ great_eq_dom(X --> p, r) in S;
end;
end;
hence thesis by A0,MESFUNC1:27;
end;
definition
let A,X be set;
func Xchi(A,X) -> Function of X,ExtREAL means :DefXchi:
for x being object st x in X holds
(x in A implies it.x = +infty) & (not x in A implies it.x = 0);
existence
proof
defpred P[object,object] means ($1 in A implies $2 = +infty) &
(not $1 in A implies $2 = 0);
A1: for x being object st x in X ex y being object st P[x,y]
proof
let x be object;
assume x in X;
not x in A implies ex y be object st y = {} & (x in A implies y = +infty)
& (not x in A implies y = {});
hence thesis;
end;
A2: for x,y1,y2 being object st x in X & P[x,y1] & P[x,y2] holds y1 = y2;
consider f being Function such that
A3: dom f = X &
for x being object st x in X holds P[x,f.x] from FUNCT_1:sch 2(A2,A1);
for x being object st x in X holds f.x in ExtREAL
proof
let x be object;
assume A4: x in X;
per cases;
suppose x in A; then
f.x = +infty by A3,A4;
hence f.x in ExtREAL;
end;
suppose not x in A; then
f.x = 0. by A3,A4;
hence f.x in ExtREAL;
end;
end; then
reconsider f as Function of X,ExtREAL by A3,FUNCT_2:3;
take f;
thus thesis by A3;
end;
uniqueness
proof
let f1,f2 be Function of X,ExtREAL such that
A4: for x being object st x in X holds (x in A implies f1.x = +infty) &
(not x in A implies f1.x = 0) and
A6: for x being object st x in X holds (x in A implies f2.x = +infty) &
(not x in A implies f2.x = 0);
for x being object st x in X holds f1.x=f2.x
proof
let x be object;
assume
A7: x in X;
then
A8: not x in A implies f1.x = 0 & f2.x = 0 by A4,A6;
x in A implies f1.x = +infty & f2.x = +infty by A4,A6,A7;
hence thesis by A8;
end;
hence thesis by FUNCT_2:12;
end;
end;
Lm08:
for X being non empty set, S being SigmaField of X, A being Element of S,
r be Real st r > 0 holds great_eq_dom(Xchi(A,X),r) = A
proof
let X be non empty set, S be SigmaField of X, A be Element of S, r be Real;
assume A1: r > 0;
now let x be object;
assume A2: x in A; then
x in X; then
A4: x in dom(Xchi(A,X)) by FUNCT_2:def 1;
Xchi(A,X).x = +infty by A2,DefXchi; then
r <= Xchi(A,X).x by XXREAL_0:3;
hence x in great_eq_dom(Xchi(A,X),r) by A4,MESFUNC1:def 14;
end; then
A5:A c= great_eq_dom(Xchi(A,X),r);
now let x be object;
assume x in great_eq_dom(Xchi(A,X),r); then
x in dom(Xchi(A,X)) & r <= Xchi(A,X).x by MESFUNC1:def 14;
hence x in A by A1,DefXchi;
end; then
great_eq_dom(Xchi(A,X),r) c= A;
hence thesis by A5;
end;
Lm09:
for X being non empty set, S being SigmaField of X, A being Element of S,
r be Real st r <= 0 holds great_eq_dom(Xchi(A,X),r) = X
proof
let X be non empty set, S be SigmaField of X, A be Element of S,
r be Real;
assume A1: r <= 0;
now let x be object;
assume A2: x in X; then
A3: x in dom(Xchi(A,X)) by FUNCT_2:def 1;
per cases;
suppose x in A; then
Xchi(A,X).x = +infty by DefXchi; then
r <= Xchi(A,X).x by XXREAL_0:3;
hence x in great_eq_dom(Xchi(A,X),r) by A3,MESFUNC1:def 14;
end;
suppose not x in A; then
Xchi(A,X).x = 0 by A2,DefXchi;
hence x in great_eq_dom(Xchi(A,X),r) by A1,A3,MESFUNC1:def 14;
end;
end; then
X c= great_eq_dom(Xchi(A,X),r);
hence thesis;
end;
theorem Th32:
for X being non empty set, S being SigmaField of X, A,B being Element of S
holds Xchi(A,X) is B-measurable
proof
let X be non empty set, S be SigmaField of X, A,B be Element of S;
A1:dom(Xchi(A,X)) = X by FUNCT_2:def 1;
for r be Real holds B /\ great_eq_dom(Xchi(A,X),r) in S
proof
let r be Real;
per cases;
suppose r > 0; then
B /\ great_eq_dom(Xchi(A,X), r) = B /\ A by Lm08;
hence B /\ great_eq_dom(Xchi(A,X), r) in S;
end;
suppose r <= 0; then
great_eq_dom(Xchi(A,X),r) = X by Lm09; then
B /\ great_eq_dom(Xchi(A,X), r) = B by XBOOLE_1:28;
hence B /\ great_eq_dom(Xchi(A,X), r) in S;
end;
end;
hence thesis by A1,MESFUNC1:27;
end;
registration
let X be non empty set;
let S be SigmaField of X;
let A be Element of S;
cluster Xchi(A,X) -> A-measurable;
coherence by Th32;
end;
registration
let X,A be set;
cluster Xchi(A,X) -> nonnegative;
coherence
proof
for x be object holds Xchi(A,X).x >= 0
proof
let x be object;
per cases;
suppose L1: x in X;
per cases;
suppose x in A;
hence Xchi(A,X).x >= 0 by L1,DefXchi;
end;
suppose not x in A;
hence Xchi(A,X).x >= 0 by L1,DefXchi;
end;
end;
suppose not x in X; then
not x in dom(Xchi(A,X));
hence Xchi(A,X).x >= 0 by FUNCT_1:def 2;
end;
end;
hence Xchi(A,X) is nonnegative by SUPINF_2:51;
end;
end;
theorem Th34:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
A be Element of S holds
(M.A <> 0 implies Integral(M,Xchi(A,X)) = +infty) &
(M.A = 0 implies Integral(M,Xchi(A,X)) = 0)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
A be Element of S;
reconsider XX = X as Element of S by MEASURE1:7;
N6:XX = dom(Xchi(A,X)) by FUNCT_2:def 1;
hereby assume
Q1: M.A <> 0;
now let x be object;
assume x in eq_dom(Xchi(A,X),+infty); then
x in dom(Xchi(A,X)) & Xchi(A,X).x = +infty by MESFUNC1:def 15;
hence x in A by DefXchi;
end; then
Q3: eq_dom(Xchi(A,X),+infty) c= A;
now let x be object;
assume Q4: x in A; then
x in X; then
Q6: x in dom(Xchi(A,X)) by FUNCT_2:def 1;
Xchi(A,X).x = +infty by Q4,DefXchi;
hence x in eq_dom(Xchi(A,X),+infty) by Q6,MESFUNC1:def 15;
end; then
A c= eq_dom(Xchi(A,X),+infty); then
WW: XX /\ eq_dom(Xchi(A,X),+infty) = A by Q3,XBOOLE_1:28;
Xchi(A,X) is XX-measurable by Th32;
hence Integral(M,Xchi(A,X)) = +infty by Q1,N6,MESFUNC9:13,WW;
end;
assume M5: M.A = 0;
reconsider XDn = XX \ A as Element of S;
reconsider F = Xchi(A,X)|A as PartFunc of X,ExtREAL by PARTFUN1:11;
reconsider F1 = Xchi(A,X)|XDn as PartFunc of X,ExtREAL by PARTFUN1:11;
reconsider F2 = Xchi(A,X)|(XDn \/ A) as PartFunc of X,ExtREAL
by PARTFUN1:11;
ZZ: ex E be Element of S st E = dom Xchi(A,X) & Xchi(A,X)
is E-measurable
proof
take XX;
thus thesis by N6,Th32;
end; then
M4:Integral(M,F) = 0 by M5,MESFUNC5:94;
N1:XDn = dom((Xchi(A,X))|XDn) by FUNCT_2:def 1;
MM:XDn = dom(Xchi(A,X)) /\ XDn by N6,XBOOLE_1:28;
Xchi(A,X) is XDn-measurable by Th32; then
N2:F1 is XDn-measurable by MM,MESFUNC5:42;
for x be Element of X st x in dom((Xchi(A,X))|XDn)
holds ((Xchi(A,X))|XDn).x = 0
proof
let x be Element of X;
assume N31: x in dom((Xchi(A,X))|XDn); then
not x in A by XBOOLE_0:def 5; then
Xchi(A,X).x = 0 by DefXchi;
hence (Xchi(A,X)|XDn).x = 0 by N31,FUNCT_1:47;
end; then
N4:integral+(M,F1) = 0 by N1,N2,MESFUNC5:87;
N5:Integral(M,F1) = 0 by N1,N2,N4,MESFUNC5:15,88;
XDn \/ A = XX \/ A by XBOOLE_1:39; then
N10:XDn \/ A = XX by XBOOLE_1:12;
XDn misses A by XBOOLE_1:79; then
Integral(M,F2) = Integral(M,F1) + Integral(M,F) by ZZ,MESFUNC5:91; then
Integral(M,F2) = Integral(M,F1) + 0 by M4;
hence Integral(M,Xchi(A,X)) = 0 by N5,N10;
end;
theorem Th35:
for X1,X2 being non empty set, S1 being SigmaField of X1,
S2 being SigmaField of X2,
M1 being sigma_Measure of S1, M2 being sigma_Measure of S2,
K being disjoint_valued Function of NAT,measurable_rectangles(S1,S2) st
Union K in measurable_rectangles(S1,S2) holds
product-pre-Measure(M1,M2).(Union K) = SUM(product-pre-Measure(M1,M2)*K)
proof
let X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2,
K be disjoint_valued Function of NAT,measurable_rectangles(S1,S2);
assume A1: Union K in measurable_rectangles(S1,S2); then
consider A being Element of S1, B being Element of S2 such that
A2: Union K = [:A,B:];
consider P be Element of S1, Q be Element of S2 such that
Q1: Union K = [:P,Q:]
& product-pre-Measure(M1,M2).(Union K) = M1.P * M2.Q by A1,Def6;
A10:A c= X1 & B c= X2;
deffunc F0(object) = chi(K.$1,[:X1,X2:]);
consider XK being Functional_Sequence of [:X1,X2:],ExtREAL such that
A3: for n being Nat holds XK.n = F0(n) from SEQFUNC:sch 1;
K1:dom XK = NAT by FUNCT_2:def 1;
now let n be object;
assume n in NAT; then
reconsider n1=n as Nat;
K2: XK.n = chi(K.n1,[:X1,X2:]) by A3;
K3: dom (chi(K.n1,[:X1,X2:])) = [:X1,X2:] by FUNCT_3:def 3;
rng (chi(K.n1,[:X1,X2:])) c= ExtREAL;
hence XK.n in Funcs([:X1,X2:],ExtREAL) by K2,K3,FUNCT_2:def 2;
end; then
reconsider XXK = XK as sequence of Funcs([:X1,X2:],ExtREAL) by K1,FUNCT_2:3;
defpred P1[Nat,object] means $2 = proj1 (K.$1);
B0:for i be Element of NAT ex A being Element of S1 st P1[i,A]
proof
let i be Element of NAT;
K.i in measurable_rectangles(S1,S2); then
consider Ai be Element of S1, Bi be Element of S2 such that
B1: K.i = [:Ai,Bi:];
per cases;
suppose B2: Bi <> {};
take Ai;
thus proj1(K.i) = Ai by B1,B2,FUNCT_5:9;
end;
suppose B3: Bi = {};
reconsider Ai = {} as Element of S1 by MEASURE1:7;
take Ai;
thus proj1(K.i) = Ai by B3,B1;
end;
end;
consider D being Function of NAT,S1 such that
B4: for i be Element of NAT holds P1[i,D.i] from FUNCT_2:sch 3(B0);
defpred P2[Nat,object] means $2 = proj2 (K.$1);
C0:for i be Element of NAT ex B being Element of S2 st P2[i,B]
proof
let i be Element of NAT;
K.i in measurable_rectangles(S1,S2); then
consider Ai be Element of S1, Bi be Element of S2 such that
C1: K.i = [:Ai,Bi:];
per cases;
suppose C2: Ai <> {};
take Bi;
thus proj2(K.i) = Bi by C1,C2,FUNCT_5:9;
end;
suppose C3: Ai = {};
reconsider Bi = {} as Element of S2 by MEASURE1:7;
take Bi;
thus proj2(K.i) = Bi by C1,C3;
end;
end;
consider E be Function of NAT,S2 such that
C4: for i be Element of NAT holds P2[i,E.i] from FUNCT_2:sch 3(C0);
deffunc F1(object) = chi(D.$1,X1);
consider XD being Functional_Sequence of X1,ExtREAL such that
B5: for n being Nat holds XD.n = F1(n) from SEQFUNC:sch 1;
deffunc F2(object) = chi(E.$1,X2);
consider XE being Functional_Sequence of X2,ExtREAL such that
C5: for n being Nat holds XE.n = F2(n) from SEQFUNC:sch 1;
E0:for n be Nat, x,y be object st x in X1 & y in X2 holds
(XK.n).(x,y) = (XD.n).x * (XE.n).y
proof
let n be Nat, x,y be object;
assume E1: x in X1 & y in X2; then
E7: [x,y] in [:X1,X2:] by ZFMISC_1:87;
E5: XK.n = chi(K.n,[:X1,X2:]) & XD.n = chi(D.n,X1) & XE.n = chi(E.n,X2)
by A3,B5,C5;
E2: n in NAT by ORDINAL1:def 12;
K.n in measurable_rectangles(S1,S2); then
consider An be Element of S1, Bn be Element of S2 such that
E3: K.n = [:An,Bn:];
E4: D.n = proj1(K.n) & E.n = proj2(K.n) by B4,C4,E2;
per cases;
suppose x in An & y in Bn; then
D.n = An & E.n = Bn by E4,E3,FUNCT_5:9;
hence (XK.n).(x,y) = (XD.n).x * (XE.n).y by E5,E3,E1,Th26;
end;
suppose not x in An or not y in Bn; then
not [x,y] in [:An,Bn:] by ZFMISC_1:87; then
E8: (XK.n).(x,y) = 0 by E7,E5,E3,FUNCT_3:def 3;
per cases;
suppose [:An,Bn:] = {}; then
(XD.n).x = 0 & (XE.n).y = 0 by E4,E3,E5,E1,FUNCT_3:def 3;
hence (XK.n).(x,y) = (XD.n).x * (XE.n).y by E8;
end;
suppose [:An,Bn:] <> {}; then
D.n = An & E.n = Bn by E4,E3,FUNCT_5:9;
hence (XK.n).(x,y) = (XD.n).x * (XE.n).y by E3,E5,E1,Th26;
end;
end;
end;
HH2:product-pre-Measure(M1,M2).(Union K) = M1.A * M2.B
proof
per cases;
suppose A <> {} & B <> {}; then
A = P & B = Q by A2,Q1,ZFMISC_1:110;
hence product-pre-Measure(M1,M2).(Union K) = M1.A * M2.B by Q1;
end;
suppose HA: A = {} or B = {}; then
P = {} or Q = {} by A2,Q1; then
(M1.A = 0 or M2.B = 0) & (M1.P = 0 or M2.Q = 0)
by HA,VALUED_0:def 19;
hence product-pre-Measure(M1,M2).(Union K) = M1.A * M2.B by Q1;
end;
end;
T1:rng chi([:A,B:],[:X1,X2:]) c= ExtREAL;
dom chi([:A,B:],[:X1,X2:]) = [:X1,X2:] by FUNCT_3:def 3; then
reconsider CAB = chi([:A,B:],[:X1,X2:]) as Function of [:X1,X2:],ExtREAL
by T1,FUNCT_2:2;
QQ:for x be Element of X1 holds
M2.B * chi(A,X1).x = Integral(M2,ProjMap1(CAB,x))
proof
let x be Element of X1;
QQ1:for y be Element of X2 holds
ProjMap1(CAB,x).y = chi(A,X1).x * chi(B,X2).y
proof
let y be Element of X2;
ProjMap1(CAB,x).y
= chi(Union K,[:X1,X2:]).(x,y) by A2,MESFUNC9:def 6;
hence thesis by A2,Th26;
end;
per cases;
suppose x in A; then
QQ2: chi(A,X1).x = 1 by FUNCT_3:def 3; then
QQ4: M2.B * chi(A,X1).x = M2.B by XXREAL_3:81;
QQ3: dom (ProjMap1(CAB,x)) = X2 by FUNCT_2:def 1
.= dom chi(B,X2) by FUNCT_3:def 3;
for y be Element of X2 st y in dom(ProjMap1(CAB,x)) holds
ProjMap1(CAB,x).y = chi(B,X2).y
proof
let y be Element of X2;
assume y in dom(ProjMap1(CAB,x));
ProjMap1(CAB,x).y = chi(A,X1).x * chi(B,X2).y by QQ1;
hence ProjMap1(CAB,x).y = chi(B,X2).y by QQ2,XXREAL_3:81;
end; then
ProjMap1(CAB,x) = chi(B,X2) by QQ3,PARTFUN1:5;
hence M2.B * chi(A,X1).x = Integral(M2,ProjMap1(CAB,x))
by QQ4,MESFUNC9:14;
end;
suppose not x in A; then
QQ5: chi(A,X1).x = 0 by FUNCT_3:def 3; then
QQ9: M2.B * chi(A,X1).x = 0;
QQ8: {} is Element of S2 by PROB_1:4;
QQ6: dom(ProjMap1(CAB,x)) = X2 by FUNCT_2:def 1
.= dom chi({},X2) by FUNCT_3:def 3;
for y be Element of X2 st y in dom(ProjMap1(CAB,x)) holds
ProjMap1(CAB,x).y = chi({},X2).y
proof
let y be Element of X2;
assume y in dom(ProjMap1(CAB,x));
ProjMap1(CAB,x).y = chi(A,X1).x * chi(B,X2).y by QQ1; then
ProjMap1(CAB,x).y = 0 by QQ5;
hence ProjMap1(CAB,x).y = chi({},X2).y by FUNCT_3:def 3;
end; then
ProjMap1(CAB,x) = chi({},X2) by QQ6,PARTFUN1:5; then
Integral(M2,ProjMap1(CAB,x)) = M2.{} by QQ8,MESFUNC9:14;
hence M2.B * chi(A,X1).x = Integral(M2,ProjMap1(CAB,x))
by QQ9,VALUED_0:def 19;
end;
end;
RB1:dom XD = NAT by FUNCT_2:def 1;
for n be object st n in NAT holds XD.n in Funcs(X1,REAL)
proof
let n be object;
assume n in NAT; then
reconsider n1=n as Element of NAT;
RB2:XD.n = chi(D.n1,X1) by B5; then
RB3:dom(XD.n) = X1 by FUNCT_3:def 3;
rng(XD.n) c= {0,1} & {0,1} c= REAL by RB2,FUNCT_3:39,XREAL_0:def 1; then
rng(XD.n) c= REAL;
hence XD.n in Funcs(X1,REAL) by RB3,FUNCT_2:def 2;
end; then
reconsider RXD = XD as sequence of Funcs(X1,REAL) by RB1,FUNCT_2:3;
Y3:for n be Nat holds D.n c= A & E.n c= B
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 12; then
YY1:D.n = proj1(K.n) & E.n = proj2(K.n) by B4,C4;
proj1(K.n) c= proj1(Union K) & proj1(Union K) c= A &
proj2(K.n) c= proj2(Union K) & proj2(Union K) c= B
by A2,XTUPLE_0:8,9,FUNCT_5:10,ABCMIZ_1:1;
hence D.n c= A & E.n c= B by YY1;
end;
Z1:for x be Element of X1
ex XF be Functional_Sequence of X2,ExtREAL, I be ExtREAL_sequence st
( for n be Nat holds XF.n = ((RXD.n).x)(#)(chi(E.n,X2)) ) &
( for n be Nat holds I.n = M2.(E.n) * (chi(D.n,X1).x)) &
I is summable &
Integral(M2,lim Partial_Sums XF) = Sum I
proof
let x be Element of X1;
deffunc FF(Nat) = ((RXD.$1).x)(#)(chi(E.$1,X2));
defpred FP[Nat,object] means $2 = FF($1);
W1: for n be Element of NAT ex y be Element of PFuncs(X2,ExtREAL) st FP[n,y]
proof
let n be Element of NAT;
reconsider r = (RXD.n).x as Real;
reconsider y = FF(n) as Element of PFuncs(X2,ExtREAL) by PARTFUN1:45;
take y;
thus FP[n,y];
end;
consider XF be Function of NAT,PFuncs(X2,ExtREAL) such that
W2: for n be Element of NAT holds FP[n,XF.n] from FUNCT_2:sch 3(W1);
reconsider XF as Functional_Sequence of X2,ExtREAL;
Y2: for n be Nat holds XF.n = ((RXD.n).x)(#)(chi(E.n,X2))
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 12;
hence thesis by W2;
end;
consider I be ExtREAL_sequence such that
Y4: (for n be Nat holds I.n = M2.(E.n)*(chi(D.n,X1).x)) &
I is summable & Integral(M2,lim Partial_Sums XF) = Sum I
by B5,Y2,Y3,Th30;
thus
ex XF be Functional_Sequence of X2,ExtREAL, I be ExtREAL_sequence st
( for n be Nat holds XF.n = ((RXD.n).x)(#)(chi(E.n,X2)) ) &
( for n be Nat holds I.n = M2.(E.n) * (chi(D.n,X1).x)) &
I is summable &
Integral(M2,lim Partial_Sums XF) = Sum I by Y2,Y4;
end;
dom(lim Partial_Sums XK) = dom((Partial_Sums XK).0) by MESFUNC8:def 9; then
dom(lim Partial_Sums XK) = dom(XK.0) by MESFUNC9:def 4; then
dom(lim Partial_Sums XK) = dom(chi(K.0,[:X1,X2:])) by A3; then
QR0: dom(lim Partial_Sums XK) = [:X1,X2:] by FUNCT_3:def 3; then
reconsider LPSXK = lim Partial_Sums XK as Function of [:X1,X2:],ExtREAL
by FUNCT_2:67;
QR:for x be Element of X1, y be Element of X2 holds
ProjMap1(CAB,x).y = ProjMap1(LPSXK,x).y
proof
let x be Element of X1, y be Element of X2;
QR1: [x,y] in [:X1,X2:] by ZFMISC_1:def 2;
ProjMap1(CAB,x).y
= chi([:A,B:],[:X1,X2:]).(x,y) by MESFUNC9:def 6
.= LPSXK.(x,y) by A3,Th25,QR1,A2;
hence ProjMap1(CAB,x).y = ProjMap1(LPSXK,x).y by MESFUNC9:def 6;
end;
QS:for x be Element of X1 holds ProjMap1(CAB,x) = ProjMap1(LPSXK,x)
proof
let x be Element of X1;
for y be Element of X2 holds ProjMap1(CAB,x).y = ProjMap1(LPSXK,x).y by QR;
hence thesis by FUNCT_2:def 8;
end;
QT:for x be Element of X1 holds
M2.B * chi(A,X1).x = Integral(M2,ProjMap1(LPSXK,x))
proof
let x be Element of X1;
ProjMap1(CAB,x) = ProjMap1(LPSXK,x) by QS;
hence thesis by QQ;
end;
ZZ:for x be Element of X1 ex I be ExtREAL_sequence st
( for n be Nat holds I.n = M2.(E.n) * (chi(D.n,X1).x) ) &
M2.B * chi(A,X1).x = Sum I
proof
let x be Element of X1;
consider XF be Functional_Sequence of X2,ExtREAL,
I be ExtREAL_sequence such that
Z3: ( for n be Nat holds XF.n = ((RXD.n).x)(#)(chi(E.n,X2)) ) &
( for n be Nat holds I.n = M2.(E.n) * (chi(D.n,X1).x) ) &
I is summable &
Integral(M2,lim Partial_Sums XF) = Sum I by Z1;
dom(lim Partial_Sums XF) = dom((Partial_Sums XF).0) by MESFUNC8:def 9; then
Z31:dom(lim Partial_Sums XF) = dom(XF.0) by MESFUNC9:def 4; then
dom(lim Partial_Sums XF) = dom(((RXD.0).x)(#)(chi(E.0,X2))) by Z3; then
dom(lim Partial_Sums XF) = dom(chi(E.0,X2)) by MESFUNC1:def 6; then
Z4A:dom(lim Partial_Sums XF) = X2 by FUNCT_3:def 3; then
Z4: dom(ProjMap1(LPSXK,x)) = dom(lim Partial_Sums XF) by FUNCT_2:def 1;
now let y be Element of X2;
assume Z41: y in dom(ProjMap1(LPSXK,x));
Z42: (ProjMap1(LPSXK,x)).y = LPSXK.(x,y) by MESFUNC9:def 6;
reconsider z = [x,y] as Element of [:X1,X2:] by ZFMISC_1:def 2;
Z46: for n be Nat holds dom(XK.n) = [:X1,X2:]
proof
let n be Nat;
XK.n = chi(K.n,[:X1,X2:]) by A3;
hence dom(XK.n) = [:X1,X2:] by FUNCT_3:def 3;
end;
Z49: for n be Nat holds XK.n is nonnegative
proof
let n be Nat;
for z be object holds 0 <= (XK.n).z
proof
let z be object;
Z45: XK.n = chi(K.n,[:X1,X2:]) by A3;
Z44: dom(XK.n) = [:X1,X2:] by Z46;
per cases;
suppose not z in [:X1,X2:];
hence (XK.n).z >= 0 by Z44,FUNCT_1:def 2;
end;
suppose z in [:X1,X2:] & z in K.n;
hence (XK.n).z >= 0 by Z45,FUNCT_3:def 3;
end;
suppose z in [:X1,X2:] & not z in K.n;
hence (XK.n).z >= 0 by Z45,FUNCT_3:def 3;
end;
end;
hence XK.n is nonnegative by SUPINF_2:51;
end;
for n,m be Nat holds dom(XK.n) = dom(XK.m)
proof
let n,m be Nat;
dom(XK.n) = [:X1,X2:] by Z46;
hence dom(XK.n) = dom(XK.m) by Z46;
end; then
Z48: XK is with_the_same_dom by MESFUNC8:def 2;
ZZ1: dom(XK.0) = [:X1,X2:] by Z46; then
ZP1: (Partial_Sums XK)#z is convergent by Z49,Z48,MESFUNC9:38;
Z50: for n be Nat holds dom(XF.n) = X2
proof
let n be Nat;
XF.n = ((RXD.n).x)(#)(chi(E.n,X2)) by Z3; then
dom(XF.n) = dom(chi(E.n,X2)) by MESFUNC1:def 6;
hence dom(XF.n) = X2 by FUNCT_3:def 3;
end;
ZZ5: for n,m be Nat holds dom(XF.n) = dom(XF.m)
proof
let n,m be Nat;
dom(XF.n) = X2 by Z50;
hence dom(XF.n) = dom(XF.m) by Z50;
end; then
Z51: XF is with_the_same_dom by MESFUNC8:def 2;
ZX1: for n be Nat holds XF.n is nonnegative
proof
let n be Nat;
for y be object holds 0 <= (XF.n).y
proof
let y be object;
Z53: XF.n = ((RXD.n).x)(#)(chi(E.n,X2)) by Z3;
Z54: dom(XF.n) = X2 by Z50;
per cases;
suppose not y in X2;
hence (XF.n).y >= 0 by Z54,FUNCT_1:def 2;
end;
suppose Z55: y in X2 & y in E.n; then
reconsider y1 = y as Element of X2;
Z56: (XF.n).y = ((RXD.n).x) * (chi(E.n,X2)).y1
by Z53,Z54,MESFUNC1:def 6;
(chi(E.n,X2)).y1 = 1 by Z55,FUNCT_3:def 3; then
(XF.n).y = (RXD.n).x by Z56,XXREAL_3:81; then
(XF.n).y = (chi(D.n,X1)).x by B5;
hence (XF.n).y >= 0 by SUPINF_2:51;
end;
suppose Z57: y in X2 & not y in E.n; then
reconsider y1 = y as Element of X2;
Z58: (XF.n).y = ((RXD.n).x) * (chi(E.n,X2)).y1
by Z53,Z54,MESFUNC1:def 6;
(chi(E.n,X2)).y1 = 0 by Z57,FUNCT_3:def 3;
hence (XF.n).y >= 0 by Z58;
end;
end;
hence XF.n is nonnegative by SUPINF_2:51;
end; then
ZP2: (Partial_Sums XF)#y is convergent
by Z51,Z31,Z4A,MESFUNC9:38;
X20: for n be Nat holds ((Partial_Sums XK)#z).n = ((Partial_Sums XF)#y).n
proof
let n be Nat;
X17: ((Partial_Sums XK)#z).n = ((Partial_Sums XK).n).z &
((Partial_Sums XF)#y).n = ((Partial_Sums XF).n).y by MESFUNC5:def 13;
defpred P1[Nat] means
((Partial_Sums XK).$1).z = ((Partial_Sums XF).$1).y;
((Partial_Sums XK).0).z = (XK.0).(x,y) by MESFUNC9:def 4; then
X14: ((Partial_Sums XK).0).z = (XD.0).x * (XE.0).y by E0;
X13: y in dom(((RXD.0).x)(#)(chi(E.0,X2))) by Z3,Z31,Z4,Z41;
(Partial_Sums XF).0 = XF.0 by MESFUNC9:def 4; then
((Partial_Sums XF).0).y = (((RXD.0).x)(#)(chi(E.0,X2))).y by Z3; then
((Partial_Sums XF).0).y = (XD.0).x * (chi(E.0,X2)).y
by X13,MESFUNC1:def 6; then
X15: P1[0] by C5,X14;
X16: for n be Nat st P1[n] holds P1[n+1]
proof
let n be Nat;
assume X18: P1[n];
X30: dom((Partial_Sums XK).(n+1)) = dom(XK.0) by Z49,Z48,MESFUNC9:29,30;
(Partial_Sums XK).(n+1)
= (Partial_Sums XK).n + XK.(n+1) by MESFUNC9:def 4; then
X31: ((Partial_Sums XK).(n+1)).z
= ((Partial_Sums XK).n).z + (XK.(n+1)).z by ZZ1,X30,MESFUNC1:def 3;
X32: dom((Partial_Sums XF).(n+1)) = dom(XF.0) by Z51,ZX1,MESFUNC9:30,29;
(Partial_Sums XF).(n+1)
= (Partial_Sums XF).n + XF.(n+1) by MESFUNC9:def 4; then
X33: ((Partial_Sums XF).(n+1)).y
= ((Partial_Sums XF).n).y + (XF.(n+1)).y
by Z31,Z4A,X32,MESFUNC1:def 3;
(XK.(n+1)).z = (XK.(n+1)).(x,y); then
X35: (XK.(n+1)).z = (XD.(n+1)).x * (XE.(n+1)).y by E0;
dom(XF.(n+1)) = dom(XF.0) by ZZ5; then
X34: y in dom( ((RXD.(n+1)).x)(#)(chi(E.(n+1),X2)) ) by Z3,Z31,Z4,Z41;
(XF.(n+1)).y = (((RXD.(n+1)).x)(#)(chi(E.(n+1),X2))).y by Z3; then
(XF.(n+1)).y = (RXD.(n+1)).x * (chi(E.(n+1),X2)).y
by X34,MESFUNC1:def 6;
hence P1[n+1] by C5,X35,X33,X31,X18;
end;
for n be Nat holds P1[n] from NAT_1:sch 2(X15,X16);
hence ((Partial_Sums XK)#z).n = ((Partial_Sums XF)#y).n by X17;
end;
for n be Nat holds ((Partial_Sums XK)#z).n <= ((Partial_Sums XF)#y).n
by X20;
then
ZP3: lim((Partial_Sums XK)#z) <= lim((Partial_Sums XF)#y)
by ZP1,ZP2,RINFSUP2:38;
for n be Nat holds ((Partial_Sums XF)#y).n <= ((Partial_Sums XK)#z).n
by X20;
then lim((Partial_Sums XF)#y) <= lim((Partial_Sums XK)#z)
by ZP1,ZP2,RINFSUP2:38; then
lim((Partial_Sums XK)#z) = lim((Partial_Sums XF)#y)
by ZP3,XXREAL_0:1; then
(lim Partial_Sums XK).z = lim((Partial_Sums XF)#y)
by QR0,MESFUNC8:def 9;
hence (ProjMap1(LPSXK,x)).y = (lim Partial_Sums XF).y
by Z42,Z4A,MESFUNC8:def 9;
end; then
ProjMap1(LPSXK,x) = lim Partial_Sums XF by Z4,PARTFUN1:5;
hence thesis by Z3,QT;
end;
defpred PI[Nat,object] means
(M2.(E.$1) = +infty implies $2 = Xchi(D.$1,X1)) &
(M2.(E.$1) <> +infty implies
ex m2 be Real st m2 = M2.(E.$1) & $2 = m2(#)(chi(D.$1,X1)));
H1:for n be Element of NAT ex y be Element of PFuncs(X1,ExtREAL) st PI[n,y]
proof
let n be Element of NAT;
per cases;
suppose HA1: M2.(E.n) = +infty;
set y = Xchi(D.n,X1);
reconsider y as Element of PFuncs(X1,ExtREAL) by PARTFUN1:45;
PI[n,y] by HA1;
hence ex y be Element of PFuncs(X1,ExtREAL) st PI[n,y];
end;
suppose HA2: M2.(E.n) <> +infty;
M2.(E.n) >= 0 by SUPINF_2:51; then
M2.(E.n) in REAL by HA2,XXREAL_0:14; then
reconsider m2 = M2.(E.n) as Real;
set y = m2(#)(chi(D.n,X1));
reconsider y as Element of PFuncs(X1,ExtREAL) by PARTFUN1:45;
PI[n,y];
hence ex y be Element of PFuncs(X1,ExtREAL) st PI[n,y];
end;
end;
consider FI be Function of NAT,PFuncs(X1,ExtREAL) such that
H2: for n be Element of NAT holds PI[n,FI.n] from FUNCT_2:sch 3(H1);
H3:for n be Nat holds dom(FI.n) = X1
proof
let n be Nat;
HA3:n is Element of NAT by ORDINAL1:def 12;
per cases;
suppose M2.(E.n) = +infty; then
FI.n = Xchi(D.n,X1) by H2,HA3;
hence dom(FI.n) = X1 by FUNCT_2:def 1;
end;
suppose M2.(E.n) <> +infty; then
consider m2 be Real such that
HA4: m2 = M2.(E.n) & FI.n = m2(#)(chi(D.n,X1)) by H2,HA3;
dom(FI.n) = dom(chi(D.n,X1)) by HA4,MESFUNC1:def 6;
hence dom(FI.n) = X1 by FUNCT_3:def 3;
end;
end;
F1:A c= dom(FI.0) by H3,A10;
F2A:for n be Nat holds FI.n is nonnegative
proof
let n be Nat;
HA5:n is Element of NAT by ORDINAL1:def 12;
per cases;
suppose M2.(E.n) = +infty; then
FI.n = Xchi(D.n,X1) by H2,HA5;
hence FI.n is nonnegative;
end;
suppose M2.(E.n) <> +infty; then
consider m2 be Real such that
HA6: m2 = M2.(E.n) & FI.n = m2(#)(chi(D.n,X1)) by H2,HA5;
for x be object holds (FI.n).x >= 0
proof
let x be object;
per cases;
suppose HA7: x in X1; then
reconsider x1 = x as Element of X1;
x1 in dom(chi(D.n,X1)) by HA7,FUNCT_3:def 3; then
x1 in dom(FI.n) by HA6,MESFUNC1:def 6; then
HA8: (FI.n).x = m2 * chi(D.n,X1).x1 by HA6,MESFUNC1:def 6;
m2 >= 0 & chi(D.n,X1).x1 >= 0 by HA6,SUPINF_2:51;
hence (FI.n).x >= 0 by HA8;
end;
suppose not x in X1; then
not x in dom(FI.n);
hence (FI.n).x >= 0 by FUNCT_1:def 2;
end;
end;
hence FI.n is nonnegative by SUPINF_2:51;
end;
end;
for n,m be Nat holds dom(FI.n) = dom(FI.m)
proof
let n,m be Nat;
dom(FI.n) = X1 & dom(FI.m) = X1 by H3;
hence dom(FI.n) = dom(FI.m);
end; then
F3:FI is with_the_same_dom by MESFUNC8:def 2;
reconsider XX = X1 as Element of S1 by MEASURE1:7;
F4:for n be Nat holds FI.n is nonnegative & FI.n is A-measurable
& FI.n is XX-measurable
proof
let n be Nat;
F4A:n is Element of NAT by ORDINAL1:def 12;
thus FI.n is nonnegative by F2A;
per cases;
suppose M2.(E.n) = +infty; then
FI.n = Xchi(D.n,X1) by H2,F4A;
hence FI.n is A-measurable & FI.n is XX-measurable by Th32;
end;
suppose M2.(E.n) <> +infty; then
consider m2 being Real such that
F4B: m2 = M2.(E.n) & FI.n = m2(#)(chi(D.n,X1)) by H2,F4A;
dom(chi(D.n,X1)) = X1 by FUNCT_3:def 3;
hence FI.n is A-measurable & FI.n is XX-measurable
by F4B,MESFUNC2:29,MESFUNC1:37;
end;
end;
F5:for x be Element of X1 st x in A holds FI#x is summable
proof
let x be Element of X1;
assume x in A;
for n be Element of NAT holds (FI#x).n >= 0
proof
let n be Element of NAT;
(FI#x).n = (FI.n).x by MESFUNC5:def 13;
hence (FI#x).n >= 0 by F4,SUPINF_2:51;
end; then
FI#x is nonnegative by SUPINF_2:39;
hence FI#x is summable by MEASURE8:2;
end;
consider J be ExtREAL_sequence such that
F6: ( for n be Nat holds J.n = Integral(M1,(FI.n)|A) ) &
J is summable &
Integral(M1,(lim Partial_Sums FI)|A) = Sum J
by F1,F3,F4,F5,MESFUNC9:30,51;
G1:for n be Nat holds J.n = Integral(M1,FI.n)
proof
let n be Nat;
F4A:n is Element of NAT by ORDINAL1:def 12;
FF: XX = dom(FI.n) by H3;
T1: ex E be Element of S1 st E = dom(FI.n) & (FI.n) is E-measurable
proof
take XX;
thus thesis by FF,F4;
end;
for x be object st x in dom(FI.n) \ A holds (FI.n).x = 0
proof
let x be object;
assume T3: x in dom(FI.n) \ A;
then
T3A: x in dom(FI.n) & not x in A by XBOOLE_0:def 5;
D.n c= A by Y3; then
T6: not x in D.n by T3,XBOOLE_0:def 5;
per cases;
suppose M2.(E.n) = +infty; then
FI.n = Xchi(D.n,X1) by H2,F4A;
hence (FI.n).x = 0 by T6,T3,DefXchi;
end;
suppose M2.(E.n) <> +infty; then
consider m2 being Real such that
F4B: m2 = M2.(E.n) & FI.n = m2(#)(chi(D.n,X1)) by H2,F4A;
T5: (FI.n).x = m2 * chi(D.n,X1).x by F4B,T3A,MESFUNC1:def 6;
chi(D.n,X1).x = 0 by T3,T6,FUNCT_3:def 3;
hence (FI.n).x = 0 by T5;
end;
end; then
Integral(M1,FI.n) = Integral(M1,(FI.n)|A) by F4,T1,Th28;
hence J.n = Integral(M1,FI.n) by F6;
end;
reconsider XX = X1 as Element of S1 by MEASURE1:7;
for n be Element of NAT holds J.n = (product-pre-Measure(M1,M2)*K).n
proof
let n be Element of NAT;
Integral(M1,FI.n) = M2.(E.n) * M1.(D.n)
proof
M2: XX = dom(FI.n) by H3;
M3b: FI.n is nonnegative by F4;
per cases;
suppose M0: M2.(E.n) = +infty; then
M1: FI.n = Xchi(D.n,X1) by H2;
per cases;
suppose M5: M1.(D.n) = 0; then
Integral(M1,FI.n) = 0 by M1,Th34;
hence Integral(M1,FI.n) = M2.(E.n) * M1.(D.n) by M5;
end;
suppose Q1: M1.(D.n) <> 0; then
M1.(D.n) > 0 by SUPINF_2:51; then
M2.(E.n) * M1.(D.n) = +infty by M0,XXREAL_3:def 5;
hence Integral(M1,FI.n) = M2.(E.n) * M1.(D.n) by M1,Q1,Th34;
end;
end;
suppose M2.(E.n) <> +infty; then
consider m2 be Real such that
R2: m2 = M2.(E.n) & FI.n = m2(#)(chi(D.n,X1)) by H2;
R3: m2 >= 0 by R2,SUPINF_2:51;
R4: XX = dom(chi(D.n,X1)) by FUNCT_3:def 3;
R5: chi(D.n,X1) is XX-measurable by MESFUNC2:29;
integral+(M1,m2(#)chi(D.n,X1)) = m2 * integral+(M1,chi(D.n,X1))
by R4,MESFUNC2:29,R3,MESFUNC5:86; then
integral+(M1,m2(#)chi(D.n,X1)) = m2 * Integral(M1,chi(D.n,X1))
by R4,MESFUNC2:29,MESFUNC5:88; then
integral+(M1,m2(#)chi(D.n,X1)) = m2 * M1.(D.n) by MESFUNC9:14;
hence Integral(M1,FI.n) = M2.(E.n) * M1.(D.n)
by R2,M2,R4,R5,MESFUNC1:37,M3b,MESFUNC5:88;
end;
end; then
Q9: J.n = M2.(E.n) * M1.(D.n) by G1;
Q17:dom K = NAT by FUNCT_2:def 1;
consider Dn be Element of S1, En be Element of S2 such that
Q10: K.n = [:Dn,En:] &
product-pre-Measure(M1,M2).(K.n) = M1.Dn * M2.En by Def6;
Q13:D.n = proj1(K.n) & E.n = proj2(K.n) by B4,C4;
M1.Dn * M2.En = M1.(D.n) * M2.(E.n)
proof
per cases;
suppose Q14: Dn = {} or En = {}; then
M1.Dn = 0 or M2.En = 0 by VALUED_0:def 19; then
Q15: M1.Dn * M2.En = 0;
D.n = {} & E.n = {} by Q13,Q10,Q14; then
M1.(D.n) = 0 & M2.(E.n) = 0 by VALUED_0:def 19;
hence M1.Dn * M2.En = M1.(D.n) * M2.(E.n) by Q15;
end;
suppose Dn <> {} & En <> {}; then
Dn = D.n & En = E.n by Q10,Q13,FUNCT_5:9;
hence M1.Dn * M2.En = M1.(D.n) * M2.(E.n);
end;
end;
hence J.n = (product-pre-Measure(M1,M2)*K).n by Q9,Q17,Q10,FUNCT_1:13;
end; then
F7:J = product-pre-Measure(M1,M2)*K by FUNCT_2:def 8;
V5:dom(lim Partial_Sums FI) = dom((Partial_Sums FI).0) by MESFUNC8:def 9; then
V0:dom(lim Partial_Sums FI) = dom(FI.0) by MESFUNC9:def 4; then
V1:XX = dom (lim Partial_Sums FI) by H3;
for x be Element of X1 holds (lim Partial_Sums FI).x >= 0
proof
let x be Element of X1;
(Partial_Sums FI)#x is non-decreasing by V0,V1,F3,F2A,MESFUNC9:38; then
lim((Partial_Sums FI)#x) = sup((Partial_Sums FI)#x) by RINFSUP2:37; then
((Partial_Sums FI)#x).0 <= lim((Partial_Sums FI)#x) by RINFSUP2:23; then
((Partial_Sums FI).0).x <= lim((Partial_Sums FI)#x)
by MESFUNC5:def 13; then
(FI.0).x <= lim((Partial_Sums FI)#x) by MESFUNC9:def 4; then
0 <= lim((Partial_Sums FI)#x) by F2A,SUPINF_2:51;
hence 0 <= (lim Partial_Sums FI).x by V1,MESFUNC8:def 9;
end; then
V4:(lim Partial_Sums FI) is nonnegative by SUPINF_2:39;
W4:Partial_Sums FI is with_the_same_dom by F2A,F3,MESFUNC9:30,43;
for n be Nat holds FI.n is XX-measurable & FI.n is without-infty
proof
let n be Nat;
thus FI.n is XX-measurable by F4;
FI.n is nonnegative by F4;
hence FI.n is without-infty;
end; then
W1:for n be Nat holds (Partial_Sums FI).n is XX-measurable by MESFUNC9:41;
V2:for x be Element of X1 st x in XX holds (Partial_Sums FI)#x is convergent
by V0,V1,F3,F2A,MESFUNC9:38;
V3:for x be object st x in dom (lim Partial_Sums FI) \ A
holds (lim Partial_Sums FI).x = 0
proof
let x be object;
assume VV1: x in dom(lim Partial_Sums FI) \ A; then
reconsider x1 = x as Element of X1;
for n be Nat holds ((Partial_Sums FI)#x1).n = 0
proof
let n be Nat;
VV4: x1 in X1; then
x1 in dom(FI.0) by H3; then
VV7: ((Partial_Sums FI)#x1).n = (Partial_Sums (FI#x1)).n
by F2A,F3,MESFUNC9:30,32;
VV8: for k be Nat holds (FI#x1).k = 0
proof
let k be Nat;
F4A: k is Element of NAT by ORDINAL1:def 12;
D.k c= A by Y3; then
VV2: not x1 in D.k by VV1,XBOOLE_0:def 5;
per cases;
suppose M2.(E.k) = +infty; then
FI.k = Xchi(D.k,X1) by H2,F4A; then
(FI.k).x1 = 0 by VV2,DefXchi;
hence (FI#x1).k = 0 by MESFUNC5:def 13;
end;
suppose M2.(E.k) <> +infty; then
consider m2 be Real such that
VV3: m2 = M2.(E.k) & FI.k = m2(#)(chi(D.k,X1)) by H2,F4A;
VV5: chi(D.k,X1).x1 = 0 by VV2,FUNCT_3:def 3;
x1 in dom(FI.k) by VV4,H3; then
(FI.k).x1 = m2 * chi(D.k,X1).x1 by VV3,MESFUNC1:def 6;
hence (FI#x1).k = 0 by VV5,MESFUNC5:def 13;
end;
end;
defpred P[Nat] means (Partial_Sums(FI#x1)).$1 = 0;
(Partial_Sums(FI#x1)).0 = (FI#x1).0 by MESFUNC9:def 1; then
VV9: P[0] by VV8;
VV10:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume VV11: P[k];
(Partial_Sums(FI#x1)).(k+1)
= (Partial_Sums(FI#x1)).k + (FI#x1).(k+1) by MESFUNC9:def 1
.= (Partial_Sums(FI#x1)).k + 0 by VV8
.= (Partial_Sums(FI#x1)).k by XXREAL_3:4;
hence P[k+1] by VV11;
end;
for k be Nat holds P[k] from NAT_1:sch 2(VV9,VV10);
hence ((Partial_Sums FI)#x1).n = 0 by VV7;
end; then
lim((Partial_Sums FI)#x1) = 0 by MESFUNC5:52;
hence (lim Partial_Sums FI).x = 0 by V1,MESFUNC8:def 9;
end;
F9:Integral(M1,lim Partial_Sums FI) = Integral(M1,(lim Partial_Sums FI)|A)
by V1,V2,V3,V4,Th28,V5,W1,W4,MESFUNC8:25;
Integral(M1,lim Partial_Sums FI) = M1.A * M2.B
proof
J1: lim Partial_Sums FI is Function of X1,ExtREAL by V1,FUNCT_2:def 1;
per cases;
suppose I0: M2.B = +infty;
for x be Element of X1 holds (lim Partial_Sums FI).x = Xchi(A,X1).x
proof
let x be Element of X1;
JJ: x in X1;
J2: dom(FI.0) = X1 by H3;
J4: (lim Partial_Sums FI).x = lim((Partial_Sums FI)#x)
by V1,MESFUNC8:def 9;
consider I be ExtREAL_sequence such that
J5: for n be Nat holds I.n = M2.(E.n)*(chi(D.n,X1).x) &
M2.B * chi(A,X1).x = Sum I by ZZ;
J6: lim Partial_Sums I = M2.B * chi(A,X1).x by J5,MESFUNC9:def 3;
for n be Element of NAT holds (FI#x).n = I.n
proof
let n be Element of NAT;
per cases;
suppose J8: M2.(E.n) = +infty; then
FI.n = Xchi(D.n,X1) by H2; then
J9: (FI#x).n = Xchi(D.n,X1).x by MESFUNC5:def 13;
per cases;
suppose J10: x in D.n; then
J11: (FI#x).n = +infty by J9,DefXchi;
chi(D.n,X1).x = 1 by J10,FUNCT_3:def 3; then
M2.(E.n) * chi(D.n,X1).x = +infty by J8,XXREAL_3:81;
hence (FI#x).n = I.n by J5,J11;
end;
suppose J12: not x in D.n; then
J13: (FI#x).n = 0 by J9,DefXchi;
chi(D.n,X1).x = 0 by J12,FUNCT_3:def 3; then
M2.(E.n) * chi(D.n,X1).x = 0;
hence (FI#x).n = I.n by J5,J13;
end;
end;
suppose M2.(E.n) <> +infty; then
consider m2 be Real such that
J15: m2 = M2.(E.n) & FI.n = m2(#)(chi(D.n,X1)) by H2;
x in dom(FI.n) by JJ,H3; then
(FI.n).x = m2 * chi(D.n,X1).x by J15,MESFUNC1:def 6; then
(FI#x).n = m2 * chi(D.n,X1).x by MESFUNC5:def 13;
hence (FI#x).n = I.n by J15,J5;
end;
end; then
(FI#x) = I by FUNCT_2:63; then
J17: for n be Element of NAT holds
((Partial_Sums FI)#x).n = (Partial_Sums I).n
by F2A,F3,J2,MESFUNC9:30,32;
Xchi(A,X1).x = M2.B * chi(A,X1).x
proof
per cases;
suppose J18: x in A; then
J19: Xchi(A,X1).x = +infty by DefXchi;
chi(A,X1).x = 1 by J18,FUNCT_3:def 3;
hence Xchi(A,X1).x = M2.B * chi(A,X1).x by J19,I0,XXREAL_3:81;
end;
suppose J20: not x in A; then
J21: Xchi(A,X1).x = 0 by DefXchi;
chi(A,X1).x = 0 by J20,FUNCT_3:def 3;
hence Xchi(A,X1).x = M2.B * chi(A,X1).x by J21;
end;
end;
hence (lim Partial_Sums FI).x = Xchi(A,X1).x by J17,J4,J6,FUNCT_2:63;
end; then
I1: lim Partial_Sums FI = Xchi(A,X1) by J1,FUNCT_2:63;
per cases;
suppose I2: M1.A <> 0; then
M1.A > 0 by SUPINF_2:51; then
M1.A * M2.B = +infty by I0,XXREAL_3:def 5;
hence Integral(M1,lim Partial_Sums FI) = M1.A * M2.B by I1,I2,Th34;
end;
suppose I3: M1.A = 0; then
M1.A * M2.B = 0;
hence Integral(M1,lim Partial_Sums FI) = M1.A * M2.B by I1,I3,Th34;
end;
end;
suppose J22: M2.B <> +infty;
M2.B >= 0 by SUPINF_2:51; then
M2.B in REAL by J22,XXREAL_0:14; then
reconsider M2B = M2.B as Real;
G3: X1 = dom(chi(A,X1)) by FUNCT_3:def 3;
dom(M2B(#)chi(A,X1)) = dom(chi(A,X1)) by MESFUNC1:def 6; then
G0: dom(M2B(#)chi(A,X1)) = X1 by FUNCT_3:def 3; then
G1: M2B(#)chi(A,X1) is Function of X1,ExtREAL by FUNCT_2:def 1;
R5: chi(A,X1) is XX-measurable by MESFUNC2:29;
for x be Element of X1 holds
(lim Partial_Sums FI).x = (M2B(#)chi(A,X1)).x
proof
let x be Element of X1;
JJ: x in X1;
J2: dom(FI.0) = X1 by H3;
J4: (lim Partial_Sums FI).x = lim((Partial_Sums FI)#x)
by V1,MESFUNC8:def 9;
consider I be ExtREAL_sequence such that
J5: for n be Nat holds I.n = M2.(E.n)*(chi(D.n,X1).x) &
M2.B * chi(A,X1).x = Sum I by ZZ;
J6: lim Partial_Sums I = M2.B * chi(A,X1).x by J5,MESFUNC9:def 3;
for n be Element of NAT holds (FI#x).n = I.n
proof
let n be Element of NAT;
M2.(E.n) <= M2.B & M2.B < +infty by Y3,MEASURE1:8,J22,XXREAL_0:4; then
consider m2 be Real such that
J15: m2 = M2.(E.n) & FI.n = m2(#)(chi(D.n,X1)) by H2;
x in dom(FI.n) by JJ,H3; then
(FI.n).x = m2 * chi(D.n,X1).x by J15,MESFUNC1:def 6; then
(FI#x).n = m2 * chi(D.n,X1).x by MESFUNC5:def 13;
hence (FI#x).n = I.n by J15,J5;
end; then
(FI#x) = I by FUNCT_2:63; then
for n be Element of NAT holds
((Partial_Sums FI)#x).n = (Partial_Sums I).n
by F2A,F3,J2,MESFUNC9:30,32; then
lim((Partial_Sums FI)#x) = lim Partial_Sums I by FUNCT_2:63;
hence (lim Partial_Sums FI).x = (M2B(#)chi(A,X1)).x
by J4,J6,G0,MESFUNC1:def 6;
end; then
lim Partial_Sums FI = M2B(#)chi(A,X1) by J1,G1,FUNCT_2:63; then
integral+(M1,lim Partial_Sums FI) = M2B * integral+(M1,chi(A,X1))
by SUPINF_2:51,G3,R5,MESFUNC5:86; then
Integral(M1,lim Partial_Sums FI) = M2B * integral+(M1,chi(A,X1))
by V1,V2,V4,V5,W1,W4,MESFUNC8:25,MESFUNC5:88; then
Integral(M1,lim Partial_Sums FI) = M2B * Integral(M1,chi(A,X1))
by G3,R5,MESFUNC5:88;
hence Integral(M1,lim Partial_Sums FI) = M1.A * M2.B by MESFUNC9:14;
end;
end;
hence thesis by F9,HH2,F6,F7,MEASURE8:2;
end;
theorem Th36:
for f be without-infty FinSequence of ExtREAL,
s be without-infty ExtREAL_sequence
st (for n be object st n in dom f holds f.n = s.n) holds
Sum f + s.0 = (Partial_Sums s).(len f)
proof
let f be without-infty FinSequence of ExtREAL,
s be without-infty ExtREAL_sequence;
assume A1: for n be object st n in dom f holds f.n = s.n;
consider F be sequence of ExtREAL such that
A2: Sum f = F.(len f) & F.0 = 0 &
for i be Nat st i < len f holds F.(i+1) = F.i + f.(i+1) by EXTREAL1:def 2;
defpred P[Nat] means
$1 <= len f implies F.$1 + s.0 = (Partial_Sums s).$1 & F.$1 <> -infty;
F.0 + s.0 = s.0 by A2,XXREAL_3:4; then
a3:P[0] by A2,MESFUNC9:def 1;
a4:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume a5: P[k];
hereby assume a7: k+1 <= len f; then
b0: k+1 in dom f by NAT_1:11,FINSEQ_3:25; then
a8: f.(k+1) <> -infty by MESFUNC5:10;
dom s = NAT by FUNCT_2:def 1; then
a9: s.0 <> -infty by MESFUNC5:10;
d1: F.(k+1) = F.k + f.(k+1) by A2,a7,NAT_1:13; then
F.(k+1) + s.0
= F.k + s.0 + f.(k+1) by a5,a7,NAT_1:13,a8,a9,XXREAL_3:29
.= (Partial_Sums s).k + s.(k+1) by b0,A1,a5,a7,NAT_1:13;
hence F.(k+1) + s.0 = (Partial_Sums s).(k+1) by MESFUNC9:def 1;
thus F.(k+1) <> -infty by d1,a5,a7,NAT_1:13,a8,XXREAL_3:17;
end;
end;
for k be Nat holds P[k] from NAT_1:sch 2(a3,a4);
hence Sum f + s.0 = (Partial_Sums s).(len f) by A2;
end;
theorem Th37:
for f be nonnegative FinSequence of ExtREAL, s be ExtREAL_sequence
st (for n be object st n in dom f holds f.n = s.n) &
(for n be Element of NAT st not n in dom f holds s.n = 0) holds
Sum f = Sum s & Sum f = SUM s
proof
let f be nonnegative FinSequence of ExtREAL, s be ExtREAL_sequence;
assume that
a1: for n be object st n in dom f holds f.n = s.n and
a2: for n be Element of NAT st not n in dom f holds s.n = 0;
for n be object st n in dom s holds 0 <= s.n
proof
let n be object;
assume L1: n in dom s;
per cases;
suppose n in dom f; then
f.n = s.n by a1;
hence 0 <= s.n by SUPINF_2:51;
end;
suppose not n in dom f;
hence 0 <= s.n by a2,L1;
end;
end; then
a7:s is nonnegative by SUPINF_2:52; then
a5:Sum f + s.0 = (Partial_Sums s).(len f) by a1,Th36;
not 0 in dom f by FINSEQ_3:24; then
s.0 = 0 by a2; then
a6:Sum f = (Partial_Sums s).(len f) by a5,XXREAL_3:4;
Partial_Sums s is nonnegative & Partial_Sums s is non-decreasing
by a7,MESFUNC9:16; then
Partial_Sums s is convergent by RINFSUP2:37; then
a9:(Partial_Sums s)^\(len f) is convergent &
lim (Partial_Sums s) = lim ((Partial_Sums s)^\(len f))
by RINFSUP2:21;
defpred P[Nat] means
(Partial_Sums s).(len f) = ((Partial_Sums s)^\(len f)).$1;
(Partial_Sums s).(len f) = (Partial_Sums s).(len f + 0); then
b1:P[0] by NAT_1:def 3;
b2:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume b3: P[k];
len f + 0 < len f + (k+1) by XREAL_1:6; then
not len f + (k+1) in dom f by FINSEQ_3:25; then
b4: s.(len f + (k+1)) = 0 by a2;
((Partial_Sums s)^\(len f)).(k+1)
= (Partial_Sums s).(len f + (k+1)) by NAT_1:def 3
.= (Partial_Sums s).(len f + k) + s.(len f + k + 1) by MESFUNC9:def 1
.= ((Partial_Sums s)^\(len f)).k + 0 by b4,NAT_1:def 3;
hence P[k+1] by b3,XXREAL_3:4;
end;
b5:for k be Nat holds P[k] from NAT_1:sch 2(b1,b2);
c1:(Partial_Sums s).(len f) >= 0 by a7,SUPINF_2:51;
per cases;
suppose c2: (Partial_Sums s).(len f) = +infty; then
for k be Element of NAT holds
((Partial_Sums s)^\(len f)).k >= +infty by b5; then
(Partial_Sums s)^\(len f) is convergent_to_+infty by RINFSUP2:32; then
lim ((Partial_Sums s)^\(len f)) = +infty by MESFUNC5:def 12;
hence Sum s = Sum f by a6,c2,a9,MESFUNC9:def 3;
hence SUM s = Sum f by a7,MEASURE8:2;
end;
suppose (Partial_Sums s).(len f) <> +infty; then
(Partial_Sums s).(len f) in REAL by c1,XXREAL_0:14; then
reconsider r = (Partial_Sums s).(len f) as Real;
for k be Nat holds ((Partial_Sums s)^\(len f)).k = r by b5; then
lim (Partial_Sums s) = Sum f by a6,a9,MESFUNC5:52;
hence Sum s = Sum f by MESFUNC9:def 3;
hence SUM s = Sum f by a7,MEASURE8:2;
end;
end;
theorem Th38:
for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2 holds
for F be disjoint_valued FinSequence of measurable_rectangles(S1,S2)
st Union F in measurable_rectangles(S1,S2) holds
product-pre-Measure(M1,M2).(Union F)
= Sum(product-pre-Measure(M1,M2)*F)
proof
let X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2;
set S = measurable_rectangles(S1,S2);
set P = product-pre-Measure(M1,M2);
let F be disjoint_valued FinSequence of S;
assume A1: Union F in S;
defpred P[object,object] means
($1 in dom F implies $2 = F.$1) & (not $1 in dom F implies $2 = {});
A2:for n be Element of NAT ex y be Element of S st P[n,y]
proof
let n be Element of NAT;
per cases;
suppose A3: n in dom F; then
F.n in rng F by FUNCT_1:3;
hence ex y be Element of S st P[n,y] by A3;
end;
suppose A4: not n in dom F;
{} in S by SETFAM_1:def 8;
hence ex y be Element of S st P[n,y] by A4;
end;
end;
consider G be Function of NAT,S such that
A5: for n be Element of NAT holds P[n,G.n] from FUNCT_2:sch 3(A2);
A6:for x be object st not x in dom F holds G.x = {}
proof
let x be object;
assume A7: not x in dom F;
per cases;
suppose x in dom G;
hence G.x = {} by A5,A7;
end;
suppose not x in dom G;
hence G.x = {} by FUNCT_1:def 2;
end;
end;
for x,y be object st x <> y holds G.x misses G.y
proof
let x,y be object;
assume A7: x <> y;
per cases;
suppose x in dom F & y in dom F; then
G.x = F.x & G.y = F.y by A5;
hence G.x misses G.y by A7,PROB_2:def 2;
end;
suppose not x in dom F or not y in dom F; then
G.x = {} or G.y = {} by A6;
hence G.x misses G.y;
end;
end; then
reconsider G as disjoint_valued Function of
NAT,measurable_rectangles(S1,S2) by PROB_2:def 2;
now let y be object;
assume B1: y in rng F \/ {{}};
per cases by B1,XBOOLE_0:def 3;
suppose y in rng F; then
consider x be object such that
A8: x in dom F & y = F.x by FUNCT_1:def 3;
y = G.x by A8,A5;
hence y in rng G by A8,FUNCT_2:4;
end;
suppose y in {{}}; then
B3: y = {} by TARSKI:def 1;
not 0 in dom F by FINSEQ_3:24; then
G.0 = {} by A5;
hence y in rng G by B3,FUNCT_2:4;
end;
end; then
A10:rng F \/ {{}} c= rng G;
now let y be object;
assume y in rng G; then
consider x be Element of NAT such that
A11: y = G.x by FUNCT_2:113;
per cases;
suppose A12: x in dom F; then
y = F.x by A5,A11; then
y in rng F by A12,FUNCT_1:3;
hence y in rng F \/ {{}} by XBOOLE_0:def 3;
end;
suppose not x in dom F; then
y = {} by A5,A11; then
y in {{}} by TARSKI:def 1;
hence y in rng F \/ {{}} by XBOOLE_0:def 3;
end;
end; then
rng G c= rng F \/ {{}}; then
rng F \/ {{}} = rng G by A10; then
union rng F \/ union {{}} = union rng G by ZFMISC_1:78; then
union rng F \/ {} = union rng G by ZFMISC_1:25; then
Union F = union rng G by CARD_3:def 4; then
Union F = Union G by CARD_3:def 4; then
P2:product-pre-Measure(M1,M2).(Union F) = SUM(product-pre-Measure(M1,M2)*G)
by A1,Th35;
P3:product-pre-Measure(M1,M2)*F is nonnegative FinSequence of ExtREAL
by MEASURE9:47;
P4:for n be object st n in dom(product-pre-Measure(M1,M2)*F) holds
(product-pre-Measure(M1,M2)*F).n = (product-pre-Measure(M1,M2)*G).n
proof
let n be object;
assume Q1: n in dom(product-pre-Measure(M1,M2)*F);
Q5: dom G = NAT by FUNCT_2:def 1;
F.n = G.n by A5,Q1,FUNCT_1:11; then
(product-pre-Measure(M1,M2)*F).n
= product-pre-Measure(M1,M2).(G.n) by Q1,FUNCT_1:12;
hence thesis by Q5,Q1,FUNCT_1:13;
end;
for n be Element of NAT st not n in dom(product-pre-Measure(M1,M2)*F) holds
(product-pre-Measure(M1,M2)*G).n = 0
proof
let n be Element of NAT;
assume L1: not n in dom(product-pre-Measure(M1,M2)*F);
L2: dom(product-pre-Measure(M1,M2)) = measurable_rectangles(S1,S2)
by FUNCT_2:def 1;
n in NAT; then
L4: n in dom G by FUNCT_2:def 1;
now assume not F.n in dom(product-pre-Measure(M1,M2)); then
not F.n in rng F by L2;
hence not n in dom F by FUNCT_1:3;
end; then
G.n = {} by A5,L1,FUNCT_1:11; then
(product-pre-Measure(M1,M2)*G).n = (product-pre-Measure(M1,M2)).{}
by L4,FUNCT_1:13;
hence thesis by VALUED_0:def 19;
end;
hence thesis by P2,P3,P4,Th37;
end;
theorem Th39:
for X1,X2 be non empty set,
S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2 holds
product-pre-Measure(M1,M2) is pre-Measure of measurable_rectangles(S1,S2)
proof
let X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2;
set P = measurable_rectangles(S1,S2);
set M = product-pre-Measure(M1,M2);
A2: for F be disjoint_valued FinSequence of P st Union F in P
holds M.(Union F) = Sum(M*F) by Th38;
for K be disjoint_valued Function of NAT,P st Union K in P
holds M.(Union K) <= SUM(M*K) by Th35;
hence thesis by A2,MEASURE9:def 7;
end;
definition
let X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2,
M1 be sigma_Measure of S1, M2 be sigma_Measure of S2;
redefine func product-pre-Measure(M1,M2) -> pre-Measure of :: redefines product-pre-Measure (MEASUR10, definition)
measurable_rectangles(S1,S2);
correctness by Th39;
end;