:: Fubini's Theorem
:: by Noboru Endou
::
:: Received March 11, 2019
:: Copyright (c) 2019-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, XXREAL_0, SUBSET_1, CARD_1, ARYTM_3, ARYTM_1, RELAT_1,
REAL_1, FUNCT_1, XBOOLE_0, TARSKI, ZFMISC_1, PROB_1, SUPINF_2, VALUED_0,
PARTFUN1, MEASURE1, MESFUNC5, MESFUNC1, MEASUR10, FUNCT_3, MEASUR11,
COMPLEX1, MESFUN12, RFUNCT_3, INTEGRA5, MESFUN13, MEASURE6, LPSPACE1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XXREAL_3, XXREAL_0, XREAL_0,
NUMBERS, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, PARTFUN1, PROB_1, SUPINF_2,
MEASURE1, MESFUNC1, MESFUNC2, MESFUNC5, EXTREAL1, MEASUR10, MEASUR11,
MESFUN12, MESFUNC6, LPSPACE1;
constructors EXTREAL1, SUPINF_1, MESFUNC2, MEASUR11, MESFUN12, MESFUNC6,
LPSPACE1;
registrations ORDINAL1, XBOOLE_0, RELAT_1, SUBSET_1, XXREAL_0, XREAL_0, NAT_1,
NUMBERS, VALUED_0, RELSET_1, MEASURE1, XXREAL_3, MESFUNC7;
requirements BOOLE, SUBSET, NUMERALS, REAL;
definitions MESFUNC1;
expansions TARSKI, XBOOLE_0, MESFUNC1;
theorems XBOOLE_0, FUNCT_1, XXREAL_0, XBOOLE_1, XXREAL_3, MEASURE1, VALUED_0,
FUNCT_2, RELAT_1, MESFUNC5, EXTREAL1, PARTFUN1, MESFUNC1, SUPINF_2,
MESFUNC2, MEASUR10, SUBSET_1, MEASUR11, MESFUN11, MESFUN12, MESFUN10,
RELSET_1, MESFUNC6, LPSPACE1;
schemes PARTFUN1;
begin :: Preliminaries
reserve X for set;
theorem Th15:
for A being Subset of X, f being X-defined Relation holds
f|A` = f|(dom f \ A)
proof
let A be Subset of X, f be X-defined Relation;
f|A` = (f|dom f)|A`
.= f|(dom f /\ A`) by RELAT_1:71
.= f|(dom f /\ (X \ A)) by SUBSET_1:def 4
.= f|((dom f /\ X) \ A) by XBOOLE_1:49;
hence f|A` = f|(dom f \ A) by XBOOLE_1:28;
end;
theorem Th10:
for f being PartFunc of X,ExtREAL holds
great_eq_dom(f,+infty) = eq_dom(f,+infty)
proof
let f be PartFunc of X,ExtREAL;
now let x be object;
assume x in great_eq_dom(f,+infty); then
A1: x in dom f & +infty <= f.x by MESFUNC1:def 14; then
f.x = +infty by XXREAL_0:4;
hence x in eq_dom(f,+infty) by A1,MESFUNC1:def 15;
end; then
A2:great_eq_dom(f,+infty) c= eq_dom(f,+infty);
now let x be object;
assume x in eq_dom(f,+infty); then
x in dom f & +infty = f.x by MESFUNC1:def 15;
hence x in great_eq_dom(f,+infty) by MESFUNC1:def 14;
end; then
eq_dom(f,+infty) c= great_eq_dom(f,+infty);
hence great_eq_dom(f,+infty) = eq_dom(f,+infty) by A2;
end;
theorem
for f being PartFunc of X,ExtREAL holds
less_eq_dom(f,-infty) = eq_dom(f,-infty)
proof
let f be PartFunc of X,ExtREAL;
now let x be object;
assume x in less_eq_dom(f,-infty); then
A1: x in dom f & -infty >= f.x by MESFUNC1:def 12; then
f.x = -infty by XXREAL_0:6;
hence x in eq_dom(f,-infty) by A1,MESFUNC1:def 15;
end; then
A2:less_eq_dom(f,-infty) c= eq_dom(f,-infty);
now let x be object;
assume x in eq_dom(f,-infty); then
x in dom f & -infty = f.x by MESFUNC1:def 15;
hence x in less_eq_dom(f,-infty) by MESFUNC1:def 12;
end; then
eq_dom(f,-infty) c= less_eq_dom(f,-infty);
hence less_eq_dom(f,-infty) = eq_dom(f,-infty) by A2;
end;
theorem
for f being PartFunc of X,ExtREAL, er being ExtReal
holds great_eq_dom(f,er) misses less_dom(f,er)
proof
let f be PartFunc of X,ExtREAL, er be ExtReal;
now let x be object;
assume x in great_eq_dom(f,er) /\ less_dom(f,er); then
x in great_eq_dom(f,er) & x in less_dom(f,er) by XBOOLE_0:def 4; then
f.x >= er & f.x < er by MESFUNC1:def 11,def 14;
hence contradiction;
end;
hence thesis by XBOOLE_0:def 1;
end;
theorem
for f being PartFunc of X,ExtREAL holds
dom f = eq_dom(f,-infty) \/ (great_dom(f,-infty) /\ less_dom(f,+infty))
\/ eq_dom(f,+infty)
proof
let f be PartFunc of X,ExtREAL;
set A1 = eq_dom(f,-infty), A2 = great_dom(f,-infty) /\ less_dom(f,+infty),
A3 = eq_dom(f,+infty);
now let x be object;
assume A1: x in dom f;
per cases by XXREAL_0:14;
suppose f.x in REAL; then
f.x > -infty & f.x < +infty by XXREAL_0:9,12; then
x in great_dom(f,-infty) & x in less_dom(f,+infty)
by A1,MESFUNC1:def 11,def 13; then
A2: x in A2 by XBOOLE_0:def 4;
A2 c= A1 \/ A2 & A1 \/ A2 c= A1 \/ A2 \/ A3 by XBOOLE_1:7;
hence x in A1 \/ A2 \/ A3 by A2;
end;
suppose f.x = +infty; then
A3: x in A3 by A1,MESFUNC1:def 15;
A3 c= A1 \/ A2 \/ A3 by XBOOLE_1:7;
hence x in A1 \/ A2 \/ A3 by A3;
end;
suppose f.x = -infty; then
A4: x in A1 by A1,MESFUNC1:def 15;
A1 c= A1 \/ A2 & A1 \/ A2 c= A1 \/ A2 \/ A3 by XBOOLE_1:7;
hence x in A1 \/ A2 \/ A3 by A4;
end;
end; then
A5:dom f c= A1 \/ A2 \/ A3;
now let x be object;
assume x in A1 \/ A2 \/ A3; then
A6: x in A1 \/ A2 or x in A3 by XBOOLE_0:def 3;
per cases by A6,XBOOLE_0:def 3;
suppose x in A1;
hence x in dom f by MESFUNC1:def 15;
end;
suppose x in A2; then
x in great_dom(f,-infty) by XBOOLE_0:def 4;
hence x in dom f by MESFUNC1:def 13;
end;
suppose x in A3;
hence x in dom f by MESFUNC1:def 15;
end;
end; then
A1 \/ A2 \/ A3 c= dom f;
hence thesis by A5;
end;
reserve X,X1,X2 for non empty set;
theorem Th29:
for f being PartFunc of X,ExtREAL, x being Element of X
holds (max+f).x <= (|.f.|).x & (max-f).x <= (|.f.|).x
proof
let f be PartFunc of X,ExtREAL, x be Element of X;
A1: -(f.x) <= --|. f.x .| by XXREAL_3:38,EXTREAL1:20;
((max+f).x = f.x or (max+f).x = 0)
& ((max-f).x = -(f.x) or (max-f).x = 0) by MESFUNC2:18; then
A2: (max+f).x <= |. f.x .| & (max-f).x <= |. f.x .| by A1,EXTREAL1:14,20;
per cases;
suppose x in dom |.f.|;
hence (max+f).x <= (|.f.|).x & (max-f).x <= (|.f.|).x
by A2,MESFUNC1:def 10;
end;
suppose A3: not x in dom |.f.|; then
not x in dom f by MESFUNC1:def 10; then
f.x = 0 & (|.f.|).x = 0 by A3,FUNCT_1:def 2;
hence (max+f).x <= (|.f.|).x & (max-f).x <= (|.f.|).x by A1,MESFUNC2:18;
end;
end;
theorem Th27:
for f being PartFunc of [:X1,X2:],ExtREAL,
x being Element of X1, y being Element of X2
holds ProjPMap1(|.f.|,x) = |.ProjPMap1(f,x).|
& ProjPMap2(|.f.|,y) = |.ProjPMap2(f,y).|
proof
let f be PartFunc of [:X1,X2:],ExtREAL,
x be Element of X1, y be Element of X2;
A1: |.f.| = max+f + max-f by MESFUNC2:24; then
ProjPMap1(|.f.|,x)
= ProjPMap1(max+f,x) + ProjPMap1(max-f,x) by MESFUN12:44
.= max+(ProjPMap1(f,x)) + ProjPMap1(max-f,x) by MESFUN12:45
.= max+(ProjPMap1(f,x)) + max-(ProjPMap1(f,x)) by MESFUN12:45;
hence ProjPMap1(|.f.|,x) = |.ProjPMap1(f,x).| by MESFUNC2:24;
ProjPMap2(|.f.|,y)
= ProjPMap2(max+f,y) + ProjPMap2(max-f,y) by A1,MESFUN12:44
.= max+(ProjPMap2(f,y)) + ProjPMap2(max-f,y) by MESFUN12:46
.= max+(ProjPMap2(f,y)) + max-(ProjPMap2(f,y)) by MESFUN12:46;
hence ProjPMap2(|.f.|,y) = |.ProjPMap2(f,y).| by MESFUNC2:24;
end;
begin :: Markov's inequality and Misc.
reserve S for SigmaField of X;
reserve S1 for SigmaField of X1;
reserve S2 for SigmaField of X2;
reserve M for sigma_Measure of S;
reserve M1 for sigma_Measure of S1;
reserve M2 for sigma_Measure of S2;
registration
let X be non empty set, S be SigmaField of X, E be Element of S;
cluster E-measurable for PartFunc of X,ExtREAL;
existence
proof
reconsider f = chi(E,X) as PartFunc of X,ExtREAL;
take f;
thus f is E-measurable by MESFUNC2:29;
end;
end;
theorem Th9:
for E being Element of S, f be E-measurable PartFunc of X,ExtREAL
st dom f = E holds eq_dom(f,+infty) in S & eq_dom(f,-infty) in S
proof
let E be Element of S, f be E-measurable PartFunc of X,ExtREAL;
assume A1: dom f = E; then
A2:eq_dom(f,+infty) c= E & eq_dom(f,-infty) c= E by MESFUNC1:def 15;
E /\ eq_dom(f,+infty) in S & E /\ eq_dom(f,-infty) in S
by A1,MESFUNC1:33,34;
hence thesis by A2,XBOOLE_1:28;
end;
theorem Th1:
for E being Element of sigma measurable_rectangles(S1,S2),
f being E-measurable PartFunc of [:X1,X2:],ExtREAL
st M1 is sigma_finite & M2 is sigma_finite & dom f = E
holds Integral(M1,Integral2(M2,|.f.|)) = Integral(Prod_Measure(M1,M2),|.f.|)
& Integral(M2,Integral1(M1,|.f.|)) = Integral(Prod_Measure(M1,M2),|.f.|)
proof
let E be Element of sigma measurable_rectangles(S1,S2),
f be E-measurable PartFunc of [:X1,X2:],ExtREAL;
assume that
A1: M1 is sigma_finite and
A2: M2 is sigma_finite and
A3: dom f = E;
E = dom |.f.| & |.f.| is E-measurable by A3,MESFUNC1:def 10,MESFUNC2:27;
hence thesis by A1,A2,MESFUN12:84;
end;
Lm1:
for f being PartFunc of [:X1,X2:],ExtREAL
st M1 is sigma_finite & M2 is sigma_finite
& f is_integrable_on Prod_Measure(M1,M2)
holds Integral(M1,Integral2(M2,|.f.|)) < +infty
& Integral(M2,Integral1(M1,|.f.|)) < +infty
proof
let f be PartFunc of [:X1,X2:],ExtREAL;
assume that
A1: M1 is sigma_finite and
A2: M2 is sigma_finite and
A3: f is_integrable_on Prod_Measure(M1,M2);
consider E be Element of sigma measurable_rectangles(S1,S2) such that
A4: E = dom f & f is E-measurable by A3,MESFUNC5:def 17;
A5: |.f.| is_integrable_on Prod_Measure(M1,M2) by A3,A4,MESFUNC5:100;
E = dom |.f.| by A4,MESFUNC1:def 10; then
Integral(Prod_Measure(M1,M2),|.f.|)
= integral+(Prod_Measure(M1,M2),|.f.|) by A4,MESFUNC2:27,MESFUNC5:88
.= integral+(Prod_Measure(M1,M2),max+|.f.|) by MESFUN11:31; then
Integral(Prod_Measure(M1,M2),|.f.|) < +infty by A5,MESFUNC5:def 17;
hence thesis by A1,A2,A4,Th1;
end;
Lm2:
for E being Element of sigma measurable_rectangles(S1,S2),
f being E-measurable PartFunc of [:X1,X2:],ExtREAL
st M1 is sigma_finite & M2 is sigma_finite & E = dom f
& (Integral(M2,Integral1(M1,|.f.|)) < +infty or
Integral(M1,Integral2(M2,|.f.|)) < +infty)
holds f is_integrable_on Prod_Measure(M1,M2)
proof
let E be Element of sigma measurable_rectangles(S1,S2),
f be E-measurable PartFunc of [:X1,X2:],ExtREAL;
assume that
A1: M1 is sigma_finite and
A2: M2 is sigma_finite and
A3: E = dom f;
set M = Prod_Measure(M1,M2);
A5: E = dom |.f.| by A3,MESFUNC1:def 10; then
A6: E = dom(max-(|.f.|)) by MESFUNC2:def 3;
A7: |.f.| is E-measurable by A3,MESFUNC2:27;
assume Integral(M2,Integral1(M1,|.f.|)) < +infty
or Integral(M1,Integral2(M2,|.f.|)) < +infty; then
Integral(M,|.f.|) < +infty by A1,A2,A5,A7,MESFUN12:84; then
integral+(M,|.f.|) < +infty by A3,A5,MESFUNC2:27,MESFUNC5:88; then
A8: integral+(M,max+(|.f.|)) < +infty by MESFUN11:31;
now let z be Element of [:X1,X2:];
assume z in dom(max-(|.f.|));
max+(|.f.|).z = |.f.| .z by MESFUN11:31;
hence max-(|.f.|).z = 0 by MESFUNC2:19;
end; then
integral+(M,max-(|.f.|)) = 0 by A5,A6,A7,MESFUNC2:26,MESFUNC5:87; then
|.f.| is_integrable_on M by A3,A5,A8,MESFUNC2:27,MESFUNC5:def 17;
hence f is_integrable_on M by A3,MESFUNC5:100;
end;
theorem
for E being Element of sigma measurable_rectangles(S1,S2),
f being E-measurable PartFunc of [:X1,X2:],ExtREAL
st M1 is sigma_finite & M2 is sigma_finite & E = dom f
holds f is_integrable_on Prod_Measure(M1,M2)
iff Integral(M2,Integral1(M1,|.f.|)) < +infty by Lm1,Lm2;
theorem
for E being Element of sigma measurable_rectangles(S1,S2),
f being E-measurable PartFunc of [:X1,X2:],ExtREAL
st M1 is sigma_finite & M2 is sigma_finite & E = dom f
holds f is_integrable_on Prod_Measure(M1,M2)
iff Integral(M1,Integral2(M2,|.f.|)) < +infty by Lm1,Lm2;
theorem Th4:
for E being Element of sigma measurable_rectangles(S1,S2),
U being Element of S1, f be E-measurable PartFunc of [:X1,X2:],ExtREAL
st M2 is sigma_finite & E = dom f
holds Integral2(M2,|.f.|) is U-measurable
proof
let E be Element of sigma measurable_rectangles(S1,S2),
U be Element of S1, f be E-measurable PartFunc of [:X1,X2:],ExtREAL;
assume that
A1: M2 is sigma_finite and
A2: E = dom f;
A3: E = dom |.f.| by A2,MESFUNC1:def 10;
|.f.| is E-measurable by A2,MESFUNC2:27;
hence Integral2(M2,|.f.|) is U-measurable by A1,A3,MESFUN12:60;
end;
theorem Th5:
for E being Element of sigma measurable_rectangles(S1,S2),
V being Element of S2, f being E-measurable PartFunc of [:X1,X2:],ExtREAL
st M1 is sigma_finite & E = dom f
holds Integral1(M1,|.f.|) is V-measurable
proof
let E be Element of sigma measurable_rectangles(S1,S2),
V be Element of S2, f be E-measurable PartFunc of [:X1,X2:],ExtREAL;
assume that
A1: M1 is sigma_finite and
A2: E = dom f;
A3: E = dom |.f.| by A2,MESFUNC1:def 10;
|.f.| is E-measurable by A2,MESFUNC2:27;
hence Integral1(M1,|.f.|) is V-measurable by A1,A3,MESFUN12:59;
end;
theorem
for f being PartFunc of [:X1,X2:],ExtREAL
st M2 is sigma_finite & f is_integrable_on Prod_Measure(M1,M2)
holds
Integral(M1,max+(Integral2(M2,|.f.|))) = Integral(M1,Integral2(M2,|.f.|))
& Integral(M1,max-(Integral2(M2,|.f.|))) = 0
proof
let f be PartFunc of [:X1,X2:],ExtREAL;
assume that
A1: M2 is sigma_finite and
A2: f is_integrable_on Prod_Measure(M1,M2);
consider A be Element of sigma measurable_rectangles(S1,S2) such that
A3: A = dom f & f is A-measurable by A2,MESFUNC5:def 17;
reconsider SX1 = X1 as Element of S1 by MEASURE1:7;
A4: Integral2(M2,|.f.|) is SX1-measurable by A1,A3,Th4;
A = dom |.f.| & |.f.| is A-measurable
by A3,MESFUNC1:def 10,MESFUNC2:27; then
A5: Integral2(M2,|.f.|) is nonnegative by MESFUN12:66;
hence Integral(M1,max+(Integral2(M2,|.f.|)))
= Integral(M1,Integral2(M2,|.f.|)) by MESFUN11:31;
SX1 = dom(Integral2(M2,|.f.|)) by FUNCT_2:def 1;
hence Integral(M1,max-(Integral2(M2,|.f.|))) = 0 by A4,A5,MESFUN11:53;
end;
theorem
for f being PartFunc of [:X1,X2:],ExtREAL
st M1 is sigma_finite
& f is_integrable_on Prod_Measure(M1,M2) holds
Integral(M2,max+(Integral1(M1,|.f.|))) = Integral(M2,Integral1(M1,|.f.|))
& Integral(M2,max-(Integral1(M1,|.f.|))) = 0
proof
let f be PartFunc of [:X1,X2:],ExtREAL;
assume that
A1: M1 is sigma_finite and
A2: f is_integrable_on Prod_Measure(M1,M2);
consider E be Element of sigma measurable_rectangles(S1,S2) such that
A3: E = dom f & f is E-measurable by A2,MESFUNC5:def 17;
reconsider SX2 = X2 as Element of S2 by MEASURE1:7;
A4: Integral1(M1,|.f.|) is SX2-measurable by A1,A3,Th5;
E = dom |.f.| & |.f.| is E-measurable
by A3,MESFUNC1:def 10,MESFUNC2:27; then
A5: Integral1(M1,|.f.|) is nonnegative by MESFUN12:66;
hence Integral(M2,max+(Integral1(M1,|.f.|)))
= Integral(M2,Integral1(M1,|.f.|)) by MESFUN11:31;
SX2 = dom(Integral1(M1,|.f.|)) by FUNCT_2:def 1;
hence Integral(M2,max-(Integral1(M1,|.f.|))) = 0 by A4,A5,MESFUN11:53;
end;
::$N Markov's inequality
theorem Th14: :: extension of RANDOM_1:36
for E being Element of S, f being E-measurable PartFunc of X,ExtREAL,
er being ExtReal st dom f = E & f is nonnegative & er >= 0
holds er*M.(great_eq_dom(f,er)) <= Integral(M,f)
proof
let E be Element of S, f be E-measurable PartFunc of X,ExtREAL,
er be ExtReal;
assume that
A1: dom f = E and
A2: f is nonnegative and
A3: er >= 0;
A4: great_eq_dom(f,er) c= E by A1,MESFUNC1:def 14;
A5: great_eq_dom(f,+infty) = eq_dom(f,+infty) by Th10;
er in REAL or er = +infty by A3,XXREAL_0:14; then
E /\ great_eq_dom(f,er) is Element of S by A1,A5,MESFUNC1:27,33; then
reconsider Er = great_eq_dom(f,er) as Element of S by A4,XBOOLE_1:28;
dom(chi(er,Er,X)) = X by FUNCT_2:def 1; then
A6: Er = dom(f|Er) & Er = dom(chi(er,Er,X)|Er) by A1,A4,RELAT_1:62;
f is Er-measurable & Er = Er /\ dom f
by A1,A4,XBOOLE_1:28,MESFUNC1:30; then
A7: f|Er is Er-measurable by MESFUNC5:42;
A8: f|Er is nonnegative by A2,MESFUNC5:15;
A9: chi(er,Er,X)|Er is Er-measurable by MESFUN12:15;
chi(er,Er,X) is nonnegative by A3,MESFUN12:17; then
A10:chi(er,Er,X)|Er is nonnegative by MESFUNC5:15;
for x be Element of X st x in dom(chi(er,Er,X)|Er) holds
(chi(er,Er,X)|Er).x <= (f|Er).x
proof
let x be Element of X;
assume A11: x in dom(chi(er,Er,X)|Er); then
(chi(er,Er,X)|Er).x = chi(er,Er,X).x by FUNCT_1:47; then
A12: (chi(er,Er,X)|Er).x = er by A6,A11,MESFUN12:def 1;
A13: (f|Er).x = f.x by A6,A11,FUNCT_1:47;
x in great_eq_dom(f,er) by A11,RELAT_1:57;
hence (chi(er,Er,X)|Er).x <= (f|Er).x by A12,A13,MESFUNC1:def 14;
end; then
integral+(M,chi(er,Er,X)|Er) <= integral+(M,f|Er)
by A6,A7,A8,A9,A10,MESFUNC5:85; then
Integral(M,chi(er,Er,X)|Er) <= integral+(M,f|Er)
by A6,A10,MESFUNC5:88,MESFUN12:15; then
A14:er*M.Er <= integral+(M,f|Er) by MESFUN12:50;
integral+(M,f|Er) <= integral+(M,f|E) by A1,A2,A4,MESFUNC5:83; then
integral+(M,f|Er) <= Integral(M,f) by A1,A2,MESFUNC5:88;
hence er*M.(great_eq_dom(f,er)) <= Integral(M,f) by A14,XXREAL_0:2;
end;
begin :: Fubini's Theorem
theorem Th21:
for f,g being PartFunc of X,ExtREAL
st f is_integrable_on M & g is_integrable_on M
holds Integral(M,f+g)
= Integral(M,f|(dom f /\ dom g)) + Integral(M,g|(dom f /\ dom g))
& Integral(M,f-g)
= Integral(M,f|(dom f /\ dom g)) - Integral(M,g|(dom f /\ dom g))
proof
let f,g be PartFunc of X,ExtREAL;
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M;
consider E be Element of S such that
A3: E = dom f /\ dom g & Integral(M,f+g)=Integral(M,f|E)+Integral(M,g|E)
by A1,A2,MESFUNC5:109;
thus Integral(M,f+g)
= Integral(M,f|(dom f /\ dom g)) + Integral(M,g|(dom f /\ dom g)) by A3;
ex E0 be Element of S st
E0 = dom g & g is E0-measurable by A2,MESFUNC5:def 17; then
A4:g is E-measurable by A3,XBOOLE_1:17,MESFUNC1:30;
ex E be Element of S st
E = dom f /\ dom g & Integral(M,f-g)=Integral(M,f|E)+Integral(M,(-g)|E)
by A1,A2,MESFUN10:13; then
Integral(M,f-g)
= Integral(M,f|E) + -(Integral(M,g|E)) by A3,A4,XBOOLE_1:17,MESFUN11:55;
hence Integral(M,f-g)
= Integral(M,f|(dom f /\ dom g)) - Integral(M,g|(dom f /\ dom g))
by A3,XXREAL_3:def 4;
end;
theorem
for f being PartFunc of X,ExtREAL holds f is_integrable_on M iff
max+f is_integrable_on M & max-f is_integrable_on M
proof
let f be PartFunc of X,ExtREAL;
hereby assume A1: f is_integrable_on M; then
consider E be Element of S such that
A2: E = dom f & f is E-measurable by MESFUNC5:def 17;
A3: integral+(M,max+f) < +infty & integral+(M,max-f) < +infty
by A1,MESFUNC5:def 17;
A4: E = dom(max+f) & E = dom(max-f) by A2,MESFUNC2:def 2,def 3;
A5: max+f is E-measurable & max-f is E-measurable by A2,MESFUN11:10;
A6: max+f is nonnegative & max-f is nonnegative by MESFUN11:5; then
A7: integral+(M,max+(max+f)) < +infty
& integral+(M,max+(max-f)) < +infty by A3,MESFUN11:31;
integral+(M,max-(max+f)) < +infty
& integral+(M,max-(max-f)) < +infty by A4,A5,A6,MESFUN11:53;
hence max+f is_integrable_on M & max-f is_integrable_on M
by A4,A5,A7,MESFUNC5:def 17;
end;
assume that
A8: max+f is_integrable_on M and
A9: max-f is_integrable_on M;
consider E1 be Element of S such that
A10: E1 = dom(max+f) & max+f is E1-measurable by A8,MESFUNC5:def 17;
consider E2 be Element of S such that
A11: E2 = dom(max-f) & max-f is E2-measurable by A9,MESFUNC5:def 17;
A12:E1 = dom f by A10,MESFUNC2:def 2; then
E1 = E2 by A11,MESFUNC2:def 3; then
A13:f is E1-measurable by A10,A11,A12,MESFUN11:10;
max+f is nonnegative & max-f is nonnegative by MESFUN11:5; then
max+(max+f) = max+f & max+(max-f) = max-f by MESFUN11:31; then
integral+(M,max+f) < +infty & integral+(M,max-f) < +infty
by A8,A9,MESFUNC5:def 17;
hence f is_integrable_on M by A12,A13,MESFUNC5:def 17;
end;
theorem
for A,B being Element of S, f being PartFunc of X,ExtREAL
st B c= A & f|A is B-measurable holds f is B-measurable
proof
let A,B be Element of S, f be PartFunc of X,ExtREAL;
assume that
A1: B c= A and
A2: f|A is B-measurable;
let r be Real;
now let x be object;
assume x in B /\ less_dom(f|A,r); then
A3: x in B & x in less_dom(f|A,r) by XBOOLE_0:def 4; then
x in dom(f|A) & (f|A).x < r by MESFUNC1:def 11; then
x in dom f & f.x < r by RELAT_1:57,FUNCT_1:47; then
x in less_dom(f,r) by MESFUNC1:def 11;
hence x in B /\ less_dom(f,r) by A3,XBOOLE_0:def 4;
end; then
A4: B /\ less_dom(f|A,r) c= B /\ less_dom(f,r);
now let x be object;
assume x in B /\ less_dom(f,r); then
A5: x in B & x in less_dom(f,r) by XBOOLE_0:def 4; then
x in dom f & f.x < r by MESFUNC1:def 11; then
x in dom(f|A) & (f|A).x < r by A1,A5,RELAT_1:57,FUNCT_1:49; then
x in less_dom(f|A,r) by MESFUNC1:def 11;
hence x in B /\ less_dom(f|A,r) by A5,XBOOLE_0:def 4;
end; then
B /\ less_dom(f,r) c= B /\ less_dom(f|A,r); then
B /\ less_dom(f|A,r) = B /\ less_dom(f,r) by A4;
hence B /\ less_dom(f,r) in S by A2;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL;
pred f is_a.e.integrable_on M means
ex A be Element of S st M.A = 0 & A c= dom f & f|A` is_integrable_on M;
end;
theorem Th16:
for f being PartFunc of X,ExtREAL
st f is_a.e.integrable_on M holds dom f in S
proof
let f be PartFunc of X,ExtREAL;
assume f is_a.e.integrable_on M; then
consider A be Element of S such that
A1: M.A = 0 & A c= dom f & f|A` is_integrable_on M;
consider B be Element of S such that
A2: B = dom(f|A`) & f|A` is B-measurable by A1,MESFUNC5:def 17;
dom(f|A`) = dom f /\ A` by RELAT_1:61
.= dom f /\ (X \ A) by SUBSET_1:def 4
.= (dom f /\ X) \ A by XBOOLE_1:49
.= dom f \ A by XBOOLE_1:28; then
dom f = A \/ B by A1,A2,XBOOLE_1:45;
hence dom f in S;
end;
theorem
for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
f is_a.e.integrable_on M
proof
let f be PartFunc of X,ExtREAL;
assume A1: f is_integrable_on M;
reconsider A = {}, XX = X as Element of S by MEASURE1:7;
A2:M.A = 0 & A c= dom f & f|(dom f \ A) is_integrable_on M
by A1,VALUED_0:def 19; then
f|A` is_integrable_on M by Th15;
hence thesis by A2;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL;
pred f is_a.e.finite M means
ex A be Element of S st M.A = 0 & A c= dom f & f|A` is PartFunc of X,REAL;
end;
theorem
for E being Element of S, f being E-measurable PartFunc of X,ExtREAL
st dom f = E holds
f is_a.e.finite M iff M.(eq_dom(f,+infty) \/ eq_dom(f,-infty)) = 0
proof
let E be Element of S, f be E-measurable PartFunc of X,ExtREAL;
assume dom f = E; then
reconsider E01 = eq_dom(f,+infty), E02 = eq_dom(f,-infty) as Element of S
by Th9;
A1: E01 c= dom f & E02 c= dom f by MESFUNC1:def 15;
hereby assume f is_a.e.finite M; then
consider A be Element of S such that
A2: M.A = 0 & A c= dom f & f|A` is PartFunc of X,REAL;
now assume ex x be object st x in E01 \/ E02 & not x in A; then
consider x be object such that
A3: x in E01 \/ E02 & not x in A;
x in E01 or x in E02 by A3,XBOOLE_0:def 3; then
A4: x in dom f & (f.x = +infty or f.x = -infty) by MESFUNC1:def 15;
x in X \ A by A3,XBOOLE_0:def 5; then
A5: x in A` by SUBSET_1:def 4; then
x in dom(f|A`) by A4,RELAT_1:57; then
(f|A`).x in REAL by A2,PARTFUN1:4;
hence contradiction by A4,A5,FUNCT_1:49;
end; then
E01 \/ E02 c= A; then
M.(E01 \/ E02) <= 0 by A2,MEASURE1:8;
hence M.(eq_dom(f,+infty) \/ eq_dom(f,-infty)) = 0 by MEASURE1:def 2;
end;
assume
A6: M.(eq_dom(f,+infty) \/ eq_dom(f,-infty)) = 0;
now let y be object;
assume y in rng(f|(E01 \/ E02)`); then
consider x be object such that
A7: x in dom(f|(E01 \/ E02)`) & (f|(E01 \/ E02)`).x = y by FUNCT_1:def 3;
dom(f|(E01 \/ E02)`) c= (E01 \/ E02)` by RELAT_1:58; then
x in (E01 \/ E02)` by A7; then
x in X \ (E01 \/ E02) by SUBSET_1:def 4; then
not x in (E01 \/ E02) by XBOOLE_0:def 5; then
A8: not x in E01 & not x in E02 by XBOOLE_0:def 3;
dom(f|(E01 \/ E02)`) c= dom f by RELAT_1:60; then
f.x <> +infty & f.x <> -infty by A7,A8,MESFUNC1:def 15; then
f.x in REAL by XXREAL_0:14;
hence y in REAL by A7,FUNCT_1:47;
end; then
rng (f|(E01 \/ E02)`) c= REAL; then
f|(E01 \/ E02)` is PartFunc of X,REAL by RELSET_1:6;
hence f is_a.e.finite M by A1,A6,XBOOLE_1:8;
end;
theorem Th19:
for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
M.(eq_dom(f,+infty)) = 0 & M.(eq_dom(f,-infty)) = 0 & f is_a.e.finite M
& for r being Real st r > 0 holds M.(great_eq_dom(|.f.|,r)) < +infty
proof
let f be PartFunc of X,ExtREAL;
assume
A2: f is_integrable_on M;
consider E be Element of S such that
A3: E = dom f & f is E-measurable by A2,MESFUNC5:def 17;
eq_dom(f,+infty) c= E by A3,MESFUNC1:def 15; then
eq_dom(f,+infty) = E /\ eq_dom(f,+infty) by XBOOLE_1:28; then
reconsider E0 = eq_dom(f,+infty) as Element of S by A3,MESFUNC1:33;
eq_dom(f,-infty) c= E by A3,MESFUNC1:def 15; then
eq_dom(f,-infty) = E /\ eq_dom(f,-infty) by XBOOLE_1:28; then
reconsider E1 = eq_dom(f,-infty) as Element of S by A3,MESFUNC1:34;
A4: E0 c= E & E1 c= E by A3,MESFUNC1:def 15; then
A5: E0 = E /\ E0 & E1 = E /\ E1 & E0 \/ E1 c= E by XBOOLE_1:8,28;
A6: dom(max+f) = E & dom(max-f) = E & dom |.f.| = E
by A3,MESFUNC1:def 10,MESFUNC2:def 2,def 3; then
A7: dom(f|E0) = E0 & dom(max+f|E0) = E0
& dom(f|E1) = E1 & dom(max-f|E1) = E1 by A3,A4,RELAT_1:62;
A8: max+f is E-measurable & max-f is E-measurable & |.f.| is E-measurable
by A3,MESFUNC2:25,26,27; then
A9: max+f is E0-measurable & max-f is E1-measurable by A4,MESFUNC1:30;
A10:(max+f)|E0 is nonnegative & (max-f)|E1 is nonnegative
by MESFUNC5:15,MESFUN11:5;
A11:max+f is nonnegative & max-f is nonnegative by MESFUN11:5; then
integral+(M,max+f|E0) <= integral+(M,max+f|E)
by A3,A4,A6,MESFUNC2:25,MESFUNC5:83; then
integral+(M,max+f|E0) < +infty by A2,A6,MESFUNC5:def 17,XXREAL_0:2; then
A12:Integral(M,max+f|E0) < +infty by A5,A6,A7,A9,A10,MESFUNC5:42,88;
A13:now let x be Element of X;
assume A14: x in dom(f|E0); then
x in E0 by RELAT_1:57; then
x in dom f & f.x = +infty by MESFUNC1:def 15;
hence (f|E0).x = +infty by A14,FUNCT_1:47;
end;
now let x be Element of X;
assume A15: x in dom(f|E0); then
A16: (f|E0).x = +infty by A13; then
A17: x in dom f & f.x = +infty by A15,RELAT_1:57,FUNCT_1:47; then
x in dom(max+f) by MESFUNC2:def 2; then
(max+f).x = max(+infty,0) by A17,MESFUNC2:def 2; then
(max+f).x = +infty by XXREAL_0:def 10;
hence (f|E0).x = (max+f|E0).x by A7,A15,A16,FUNCT_1:47;
end; then
A18:Integral(M,f|E0) < +infty by A7,A12,PARTFUN1:5;
dom(chi(+infty,E0,X)) = X by FUNCT_2:def 1; then
A19:dom(chi(+infty,E0,X)|E0) = E0 by RELAT_1:62;
now let x be Element of X;
assume A20: x in dom(f|E0); then
A21: x in E0 by RELAT_1:57; then
(chi(+infty,E0,X)|E0).x = chi(+infty,E0,X).x by FUNCT_1:49; then
(chi(+infty,E0,X)|E0).x = +infty by A21,MESFUN12:def 1;
hence (f|E0).x = (chi(+infty,E0,X)|E0).x by A13,A20;
end; then
f|E0 = chi(+infty,E0,X)|E0 by A3,A4,A19,RELAT_1:62,PARTFUN1:5; then
A22:Integral(M,f|E0) = +infty * M.E0 by MESFUN12:50;
A23:now assume M.E0 <> 0; then
M.E0 > 0 by SUPINF_2:51;
hence contradiction by A18,A22,XXREAL_3:def 5;
end;
hence M.(eq_dom(f,+infty)) = 0;
A24:Integral(M,-(max-f|E1)) = - Integral(M,max-f|E1)
by A5,A6,A7,A9,MESFUNC5:42,MESFUN11:52;
integral+(M,max-f|E1) <= integral+(M,max-f|E)
by A3,A4,A6,A11,MESFUNC2:26,MESFUNC5:83; then
integral+(M,max-f|E1) < +infty by A2,A6,MESFUNC5:def 17,XXREAL_0:2; then
Integral(M,max-f|E1) < +infty by A5,A6,A7,A9,A10,MESFUNC5:42,88; then
A25:Integral(M,-(max-f|E1)) > -infty by A24,XXREAL_3:6,38;
A26:now let x be Element of X;
assume d7: x in dom(f|E1); then
x in E1 by RELAT_1:57; then
x in dom f & f.x = -infty by MESFUNC1:def 15;
hence (f|E1).x = -infty by d7,FUNCT_1:47;
end;
A27:dom(-(max-f|E1)) = E1 by A7,MESFUNC1:def 7;
now let x be Element of X;
assume A28: x in dom(f|E1); then
x in E1 by RELAT_1:57; then
A29: x in dom f & f.x = -infty by MESFUNC1:def 15; then
A30: (f|E1).x = -(+infty) by A28,FUNCT_1:47,XXREAL_3:6;
x in dom(max-f) by A29,MESFUNC2:def 3; then
(max-f).x = max(-(-infty),0) by A29,MESFUNC2:def 3; then
(max-f).x = +infty by XXREAL_0:def 10,XXREAL_3:5; then
(f|E1).x = -((max-f|E1).x) by A7,A28,A30,FUNCT_1:47;
hence (f|E1).x = (-(max-f|E1)).x by A7,A27,A28,MESFUNC1:def 7;
end; then
A31:Integral(M,f|E1) > -infty by A3,A4,A25,A27,RELAT_1:62,PARTFUN1:5;
dom(chi(-infty,E1,X)) = X by FUNCT_2:def 1; then
A32:dom(chi(-infty,E1,X)|E1) = E1 by RELAT_1:62;
now let x be Element of X;
assume A33: x in dom(f|E1); then
A34: x in E1 by RELAT_1:57; then
(chi(-infty,E1,X)|E1).x = chi(-infty,E1,X).x by FUNCT_1:49; then
(chi(-infty,E1,X)|E1).x = -infty by A34,MESFUN12:def 1;
hence (f|E1).x = (chi(-infty,E1,X)|E1).x by A26,A33;
end; then
f|E1 = chi(-infty,E1,X)|E1 by A3,A4,A32,RELAT_1:62,PARTFUN1:5; then
A35:Integral(M,f|E1) = -infty * M.E1 by MESFUN12:50;
A36:now assume M.E1 <> 0; then
M.E1 > 0 by SUPINF_2:51;
hence contradiction by A31,A35,XXREAL_3:def 5;
end;
hence M.(eq_dom(f,-infty)) = 0;
set E2 = E0 \/ E1;
M.E2 <= M.E0 + M.E1 by MEASURE1:33; then
M.E2 <= 0 & M.E2 >= 0 by A23,A36,SUPINF_2:51; then
A37:M.E2 = 0;
now let r be ExtReal;
assume r in rng(f|E2`); then
consider x be object such that
A38: x in dom(f|E2`) & r = (f|E2`).x by FUNCT_1:def 3;
A39: x in dom f & x in E2` by A38,RELAT_1:57; then
x in X \ E2 by SUBSET_1:def 4; then
x in X & not x in E2 by XBOOLE_0:def 5; then
not x in E0 & not x in E1 by XBOOLE_0:def 3; then
f.x <> +infty & f.x <> -infty by A39,MESFUNC1:def 15; then
r <> +infty & r <> -infty by A38,FUNCT_1:47;
hence r in REAL by XXREAL_0:14;
end; then
rng(f|E2`) c= REAL; then
f|E2` is PartFunc of X,REAL by RELSET_1:6;
hence f is_a.e.finite M by A3,A4,A37,XBOOLE_1:8;
|.f.| is_integrable_on M by A2,A3,MESFUNC5:100; then
A40:Integral(M,|.f.|) < +infty by MESFUNC5:96;
thus for r be Real st r > 0 holds M.(great_eq_dom(|.f.|,r)) < +infty
proof
let r be Real;
assume A41: r > 0; then
r * M.(great_eq_dom(|.f.|,r)) <= Integral(M,|.f.|) by A6,A8,Th14; then
r * M.(great_eq_dom(|.f.|,r)) < +infty by A40,XXREAL_0:2; then
(r * M.(great_eq_dom(|.f.|,r))) / r < +infty /r by A41,XXREAL_3:80; then
M.(great_eq_dom(|.f.|,r)) < +infty / r by A41,XXREAL_3:88;
hence M.(great_eq_dom(|.f.|,r)) < +infty by A41,XXREAL_3:83;
end;
end;
theorem Th20:
for f being PartFunc of [:X1,X2:],ExtREAL
st M1 is sigma_finite & M2 is sigma_finite
& f is_integrable_on Prod_Measure(M1,M2)
holds Integral1(M1,max+f) is_integrable_on M2
& Integral2(M2,max+f) is_integrable_on M1
& Integral1(M1,max-f) is_integrable_on M2
& Integral2(M2,max-f) is_integrable_on M1
& Integral1(M1,|.f.|) is_integrable_on M2
& Integral2(M2,|.f.|) is_integrable_on M1
proof
let f be PartFunc of [:X1,X2:],ExtREAL;
assume that
A1: M1 is sigma_finite and
A2: M2 is sigma_finite and
A3: f is_integrable_on Prod_Measure(M1,M2);
reconsider XX1 = X1 as Element of S1 by MEASURE1:7;
reconsider XX2 = X2 as Element of S2 by MEASURE1:7;
set PM = Prod_Measure(M1,M2);
consider E be Element of sigma measurable_rectangles(S1,S2) such that
A4: E = dom f & f is E-measurable by A3,MESFUNC5:def 17;
A5: max+f is E-measurable & max-f is E-measurable & |.f.| is E-measurable
by A4,MESFUNC2:27,MESFUN11:10;
A6: dom(max+f) = E & dom(max-f) = E & dom(|.f.|) = E
by A4,MESFUNC1:def 10,MESFUNC2:def 2,def 3;
A7: max+f is nonnegative & max-f is nonnegative & |.f.| is nonnegative
by MESFUN11:5; then
A8: Integral1(M1,max+f) is nonnegative & Integral2(M2,max+f) is nonnegative
& Integral1(M1,max-f) is nonnegative & Integral2(M2,max-f) is nonnegative
& Integral1(M1,|.f.|) is nonnegative & Integral2(M2,|.f.|) is nonnegative
by A5,A6,MESFUN12:66;
A9: Integral1(M1,max+f) is XX2-measurable
& Integral1(M1,max-f) is XX2-measurable
& Integral1(M1,|.f.|) is XX2-measurable
& Integral2(M2,max+f) is XX1-measurable
& Integral2(M2,max-f) is XX1-measurable
& Integral2(M2,|.f.|) is XX1-measurable
by A1,A2,A5,A6,MESFUN11:5,MESFUN12:59,60;
A10:dom(Integral1(M1,max+f)) = XX2 & dom(Integral2(M2,max+f)) = XX1
& dom(Integral1(M1,max-f)) = XX2 & dom(Integral2(M2,max-f)) = XX1
& dom(Integral1(M1,|.f.|)) = XX2 & dom(Integral2(M2,|.f.|)) = XX1
by FUNCT_2:def 1;
integral+(PM,max+f) = Integral(PM,max+f)
& integral+(PM,max-f) = Integral(PM,max-f)
by A5,A6,MESFUN11:5,MESFUNC5:88; then
integral+(PM,max+f) = Integral(M2,Integral1(M1,max+f))
& integral+(PM,max+f) = Integral(M1,Integral2(M2,max+f))
& integral+(PM,max-f) = Integral(M2,Integral1(M1,max-f))
& integral+(PM,max-f) = Integral(M1,Integral2(M2,max-f))
by A1,A2,A5,A6,A7,MESFUN12:84; then
A11:Integral(M2,Integral1(M1,max+f)) < +infty
& Integral(M1,Integral2(M2,max+f)) < +infty
& Integral(M2,Integral1(M1,max-f)) < +infty
& Integral(M1,Integral2(M2,max-f)) < +infty by A3,MESFUNC5:def 17;
Integral1(M1,max+f) = max+(Integral1(M1,max+f))
& Integral2(M2,max+f) = max+(Integral2(M2,max+f))
& Integral1(M1,max-f) = max+(Integral1(M1,max-f))
& Integral2(M2,max-f) = max+(Integral2(M2,max-f)) by A8,MESFUN11:31; then
A12:integral+(M2,max+(Integral1(M1,max+f))) <+infty
& integral+(M1,max+(Integral2(M2,max+f))) <+infty
& integral+(M2,max+(Integral1(M1,max-f))) <+infty
& integral+(M1,max+(Integral2(M2,max-f))) <+infty
by A8,A9,A10,A11,MESFUNC5:88;
integral+(M2,max-(Integral1(M1,max+f))) = 0
& integral+(M1,max-(Integral2(M2,max+f))) = 0
& integral+(M2,max-(Integral1(M1,max-f))) = 0
& integral+(M1,max-(Integral2(M2,max-f))) = 0 by A8,A9,A10,MESFUN11:53;
hence Integral1(M1,max+f) is_integrable_on M2
& Integral2(M2,max+f) is_integrable_on M1
& Integral1(M1,max-f) is_integrable_on M2
& Integral2(M2,max-f) is_integrable_on M1
by A9,A10,A12,MESFUNC5:def 17;
A13:|.f.| is_integrable_on Prod_Measure(M1,M2) by A3,A4,MESFUNC5:100;
max+(|.f.|) = |.f.| by MESFUN11:31; then
integral+(PM,max+(|.f.|))
= Integral(PM,|.f.|) by A6,A4,MESFUNC2:27,MESFUNC5:88; then
integral+(PM,max+(|.f.|)) = Integral(M2,Integral1(M1,|.f.|))
& integral+(PM,max+(|.f.|)) = Integral(M1,Integral2(M2,|.f.|))
by A1,A2,A5,A6,MESFUN12:84; then
A15:Integral(M2,Integral1(M1,|.f.|)) < +infty
& Integral(M1,Integral2(M2,|.f.|)) < +infty by A13,MESFUNC5:def 17;
Integral1(M1,|.f.|) = max+(Integral1(M1,|.f.|))
& Integral2(M2,|.f.|) = max+(Integral2(M2,|.f.|)) by A8,MESFUN11:31; then
A16:integral+(M2,max+(Integral1(M1,|.f.|))) <+infty
& integral+(M1,max+(Integral2(M2,|.f.|))) <+infty
by A8,A9,A10,A15,MESFUNC5:88;
integral+(M2,max-(Integral1(M1,|.f.|))) = 0
& integral+(M1,max-(Integral2(M2,|.f.|))) = 0 by A8,A9,A10,MESFUN11:53;
hence Integral1(M1,|.f.|) is_integrable_on M2
& Integral2(M2,|.f.|) is_integrable_on M1 by A9,A10,A16,MESFUNC5:def 17;
end;
theorem
for E being Element of S, f being E-measurable PartFunc of X,ExtREAL
st dom f c= E & f is_a.e.integrable_on M holds f is_integrable_on M
proof
let E be Element of S, f be E-measurable PartFunc of X,ExtREAL;
assume that
A1: dom f c= E and
A2: f is_a.e.integrable_on M;
reconsider E1 = dom f as Element of S by A2,Th16;
consider A be Element of S such that
A3: M.A = 0 & A c= dom f & f|A` is_integrable_on M by A2;
A4:f|A` = f|(dom f \ A) by Th15; then
A5:dom(f|A`) = dom f /\ (dom f \ A) by RELAT_1:61; then
A6:dom(f|A`) = (E1 /\ E1) \ A by XBOOLE_1:49 .= E1 \ A; then
A7:dom(max+(f|A`)) = E1\A & dom(max-(f|A`)) = E1\A by MESFUNC2:def 2,def 3;
A8:f is E1-measurable by A1,MESFUNC1:30; then
f is (E1\A)-measurable by XBOOLE_1:36,MESFUNC1:30; then
f|A` is (E1\A)-measurable by A4,A5,A6,MESFUNC5:42; then
A9:max+(f|A`) is (E1\A)-measurable & max-(f|A`) is (E1\A)-measurable
by A6,MESFUNC2:25,26;
A10:E1 = dom(max+f) & E1 = dom(max-f) by MESFUNC2:def 2,def 3;
A11:max+f is nonnegative & max-f is nonnegative by MESFUN11:5;
Integral(M,max+f|(dom f \ A)) = Integral(M,max+f)
& Integral(M,max-f|(dom f \ A)) = Integral(M,max-f)
by A3,A8,A10,MESFUNC2:25,26,MESFUNC5:95; then
Integral(M,max+(f|A`)) = Integral(M,max+f)
& Integral(M,max-(f|A`)) = Integral(M,max-f) by A4,MESFUNC5:28; then
integral+(M,max+(f|A`)) = Integral(M,max+f)
& integral+(M,max-(f|A`)) = Integral(M,max-f)
by A7,A9,MESFUNC5:88,MESFUN11:5; then
A12:integral+(M,max+(f|A`)) = integral+(M,max+f)
& integral+(M,max-(f|A`)) = integral+(M,max-f)
by A8,A10,A11,MESFUNC2:25,26,MESFUNC5:88;
integral+(M,max+(f|A`)) < +infty & integral+(M,max-(f|A`)) < +infty
by A3,MESFUNC5:def 17;
hence f is_integrable_on M by A8,A12,MESFUNC5:def 17;
end;
theorem Th23:
for A being Element of S, f being PartFunc of X,ExtREAL st
M.A = 0 & A c= dom f & f|A` is_integrable_on M holds
ex g be PartFunc of X,ExtREAL st dom g = dom f &
f|A` = g|A` & g is_integrable_on M & Integral(M,f|A`) = Integral(M,g)
proof
let A be Element of S, f be PartFunc of X,ExtREAL;
assume that
A2: M.A = 0 and
A1: A c= dom f and
A3: f|A` is_integrable_on M;
consider B be Element of S such that
A4: B = dom(f|A`) & f|A` is B-measurable by A3,MESFUNC5:def 17;
A5: f|A` = f|(dom f \ A) by Th15; then
A6: B = dom f /\ (dom f \ A) by A4,RELAT_1:61
.= (dom f /\ dom f) \ A by XBOOLE_1:49
.= dom f \ A; then
A7: dom f = A \/ B by A1,XBOOLE_1:45;
A8: (ex E be Element of S st E = dom(f|B) & f|B is E-measurable)
& integral+(M,max+(f|B)) < +infty & integral+(M,max-(f|B)) < +infty
by A3,A5,A6,MESFUNC5:def 17;
defpred C[object] means $1 in A;
deffunc F(object) = +infty;
deffunc G(object) = f.$1;
consider g be Function such that
A9: dom g = dom f &
for x be object st x in dom f holds
(C[x] implies g.x = F(x)) & (not C[x] implies g.x = G(x))
from PARTFUN1:sch 1;
now let y be object;
assume y in rng g; then
consider x be object such that
A10: x in dom g & y = g.x by FUNCT_1:def 3;
per cases;
suppose x in A; then
g.x = +infty by A9,A10;
hence y in ExtREAL by A10,XXREAL_0:def 1;
end;
suppose not x in A; then
g.x = f.x by A9,A10; then
g.x in rng f by A9,A10,FUNCT_1:3;
hence y in ExtREAL by A10;
end;
end; then
rng g c= ExtREAL; then
reconsider g as PartFunc of X,ExtREAL by A9,RELSET_1:4;
take g;
thus dom g = dom f by A9;
dom(f|A`) = dom f /\ A` by RELAT_1:61; then
A11:dom(f|A`) = dom(g|A`) by A9,RELAT_1:61;
now let x be Element of X;
assume x in dom(f|A`); then
A12: x in dom f & x in A` by RELAT_1:57; then
x in X \ A by SUBSET_1:def 4; then
A13: not x in A by XBOOLE_0:def 5;
(f|A`).x = f.x by A12,FUNCT_1:49; then
(f|A`).x = g.x by A9,A12,A13;
hence (f|A`).x = (g|A`).x by A12,FUNCT_1:49;
end;
hence
A14: f|A` = g|A` by A11,PARTFUN1:5;
A15:A` = X \ A by SUBSET_1:def 4; then
f|B = (g|A`)|B by A6,A14,XBOOLE_1:33,RELAT_1:74; then
f|B = g|B by A6,A15,XBOOLE_1:33,RELAT_1:74; then
A16:(max+g)|B = max+(f|B) & (max-g)|B = max-(f|B) by MESFUNC5:28;
A17:for r be Real holds (A \/ B) /\ less_dom(g,r) in S
proof
let r be Real;
now let x be object;
assume x in (A \/ B) /\ less_dom(g,r); then
A18: x in dom f & x in less_dom(g,r) by A7,XBOOLE_0:def 4; then
A19: x in dom g & g.x < r by MESFUNC1:def 11;
A20: now assume x in A; then
g.x = +infty by A9,A18;
hence contradiction by A19,XXREAL_0:3;
end; then
A21: x in B by A7,A18,XBOOLE_0:def 3;
g.x = f.x by A9,A18,A20; then
(f|B).x < r by A19,A21,FUNCT_1:49; then
x in less_dom(f|B,r) by A4,A5,A6,A21,MESFUNC1:def 11;
hence x in B /\ less_dom(f|B,r) by A21,XBOOLE_0:def 4;
end; then
A22: (A \/ B) /\ less_dom(g,r) c= B /\ less_dom(f|B,r);
now let x be object;
assume x in B /\ less_dom(f|B,r); then
A23: x in B & x in less_dom(f|B,r) by XBOOLE_0:def 4; then
A24: x in dom(f|B) & (f|B).x < r by MESFUNC1:def 11;
A25: x in dom f & not x in A by A23,A6,XBOOLE_0:def 5; then
g.x = f.x by A9; then
g.x < r by A24,FUNCT_1:47; then
x in less_dom(g,r) by A9,A25,MESFUNC1:def 11;
hence x in (A \/ B) /\ less_dom(g,r) by A7,A25,XBOOLE_0:def 4;
end; then
B /\ less_dom(f|B,r) c= (A \/ B) /\ less_dom(g,r); then
(A \/ B) /\ less_dom(g,r) = B /\ less_dom(f|B,r) by A22;
hence (A \/ B) /\ less_dom(g,r) in S by A4,A5,A6;
end; then
A26:max+g is (A\/B)-measurable & max-g is (A\/B)-measurable
by A7,A9,MESFUNC1:def 16,MESFUNC2:25,26;
A27:(max+g)|B is nonnegative & (max-g)|B is nonnegative
by MESFUNC5:15,MESFUN11:5;
A28:dom(max+g) = A \/ B & dom(max-g) = A \/ B by A7,A9,MESFUNC2:def 2,def 3;
A29:B = (A \/ B) /\ B by XBOOLE_1:7,28; then
A30:dom((max+g)|B) = B & dom((max-g)|B) = B by A28,RELAT_1:61;
A31:max+g is B-measurable & max-g is B-measurable
by A26,XBOOLE_1:7,MESFUNC1:30;
Integral(M,(max+g)|B) = Integral(M,max+g)
& Integral(M,(max-g)|B) = Integral(M,max-g)
by A2,A6,A7,A26,A28,MESFUNC5:95; then
integral+(M,(max+g)|B) = Integral(M,max+g)
& integral+(M,(max-g)|B) = Integral(M,max-g)
by A27,A28,A29,A30,A31,MESFUNC5:42,88; then
integral+(M,max+g) < +infty & integral+(M,max-g) < +infty
by A8,A16,A26,A28,MESFUNC5:88,MESFUN11:5;
hence g is_integrable_on M by A7,A9,A17,MESFUNC5:def 17,MESFUNC1:def 16;
f is_a.e.integrable_on M by A1,A2,A3; then
reconsider E = dom f as Element of S by Th16;
Integral(M,f|A`) = Integral(M,g|(dom g \ A)) by A14,Th15;
hence Integral(M,f|A`) = Integral(M,g)
by A2,A7,A9,A17,MESFUNC5:95,MESFUNC1:def 16;
end;
theorem
for f being PartFunc of [:X1,X2:],ExtREAL
st M1 is sigma_finite & M2 is sigma_finite
& f is_integrable_on Prod_Measure(M1,M2)
holds
Integral(Prod_Measure(M1,M2),f)
= Integral(M2,Integral1(M1,max+f)) - Integral(M2,Integral1(M1,max-f))
& Integral(Prod_Measure(M1,M2),f)
= Integral(M1,Integral2(M2,max+f)) - Integral(M1,Integral2(M2,max-f))
proof
let f be PartFunc of [:X1,X2:],ExtREAL;
assume that
A1: M1 is sigma_finite and
A2: M2 is sigma_finite and
A3: f is_integrable_on Prod_Measure(M1,M2);
set M = Prod_Measure(M1,M2);
consider E be Element of sigma measurable_rectangles(S1,S2) such that
A4: E = dom f & f is E-measurable by A3,MESFUNC5:def 17;
A5: max+f is nonnegative & max-f is nonnegative by MESFUN11:5;
A6: dom(max+f) = E & dom(max-f) = E by A4,MESFUNC2:def 2,def 3;
max+f is E-measurable & max-f is E-measurable by A4,MESFUNC2:25,26; then
A7: Integral(M,max+f) = Integral(M2,Integral1(M1,max+f))
& Integral(M,max-f) = Integral(M2,Integral1(M1,max-f))
& Integral(M,max+f) = Integral(M1,Integral2(M2,max+f))
& Integral(M,max-f) = Integral(M1,Integral2(M2,max-f))
by A1,A2,A5,A6,MESFUN12:84;
integral+(M,max+f) = Integral(M,max+f)
& integral+(M,max-f) = Integral(M,max-f)
by A4,A5,A6,MESFUNC2:25,26,MESFUNC5:88;
hence thesis by A7,MESFUNC5:def 16;
end;
theorem
for E being Element of sigma measurable_rectangles(S1,S2), y be Element of X2
holds
( M1.Measurable-Y-section(E,y) <> 0
implies Integral1(M1,Xchi(E,[:X1,X2:])).y = +infty ) &
( M1.Measurable-Y-section(E,y) = 0
implies Integral1(M1,Xchi(E,[:X1,X2:])).y = 0 )
proof
let E be Element of sigma measurable_rectangles(S1,S2),
y be Element of X2;
ProjPMap2(Xchi(E,[:X1,X2:]),y) = Xchi(Y-section(E,y),X1)
by MESFUN12:35; then
A1: Integral1(M1,Xchi(E,[:X1,X2:])).y
= Integral(M1,Xchi(Y-section(E,y),X1)) by MESFUN12:def 7;
A2: Measurable-Y-section(E,y) = Y-section(E,y) by MEASUR11:def 7;
hence M1.Measurable-Y-section(E,y) <> 0 implies
Integral1(M1,Xchi(E,[:X1,X2:])).y = +infty by A1,MEASUR10:33;
assume M1.Measurable-Y-section(E,y) = 0;
hence thesis by A1,A2,MEASUR10:33;
end;
theorem
for E being Element of sigma measurable_rectangles(S1,S2), x be Element of X1
holds
( M2.Measurable-X-section(E,x) <> 0
implies Integral2(M2,Xchi(E,[:X1,X2:])).x = +infty ) &
( M2.Measurable-X-section(E,x) = 0
implies Integral2(M2,Xchi(E,[:X1,X2:])).x = 0 )
proof
let E be Element of sigma measurable_rectangles(S1,S2),
x be Element of X1;
ProjPMap1(Xchi(E,[:X1,X2:]),x) = Xchi(X-section(E,x),X2)
by MESFUN12:35; then
A1: Integral2(M2,Xchi(E,[:X1,X2:])).x
= Integral(M2,Xchi(X-section(E,x),X2)) by MESFUN12:def 8;
A2: Measurable-X-section(E,x) = X-section(E,x) by MEASUR11:def 6;
hence M2.Measurable-X-section(E,x) <> 0 implies
Integral2(M2,Xchi(E,[:X1,X2:])).x = +infty by A1,MEASUR10:33;
assume M2.Measurable-X-section(E,x) = 0;
hence thesis by A1,A2,MEASUR10:33;
end;
::$N Fubini`s theorem
theorem
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, f being PartFunc of [:X1,X2:],ExtREAL,
SX1 being Element of S1
st M1 is sigma_finite & M2 is sigma_finite
& f is_integrable_on Prod_Measure(M1,M2) & X1 = SX1
holds
ex U be Element of S1 st M1.U = 0
& (for x being Element of X1 st x in U` holds
ProjPMap1(f,x) is_integrable_on M2)
& Integral2(M2,|.f.|)|U` is PartFunc of X1,REAL
& Integral2(M2,f) is (SX1\U)-measurable
& Integral2(M2,f)|U` is_integrable_on M1
& Integral2(M2,f)|U` in L1_Functions M1
& (ex g be Function of X1,ExtREAL st
g is_integrable_on M1 & g|U` = Integral2(M2,f)|U`
& Integral(Prod_Measure(M1,M2),f) = Integral(M1,g))
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,
f be PartFunc of [:X1,X2:],ExtREAL, SX1 be Element of S1;
assume that
A1: M1 is sigma_finite and
A2: M2 is sigma_finite and
A3: f is_integrable_on Prod_Measure(M1,M2) and
A4: X1 = SX1;
consider A be Element of sigma measurable_rectangles(S1,S2) such that
A5: A = dom f & f is A-measurable by A3,MESFUNC5:def 17;
A6: A = dom |.f.| & A = dom (max+f) & A = dom (max-f)
by A5,MESFUNC1:def 10,MESFUNC2:def 2,def 3;
A7: |.f.| is A-measurable & max+f is A-measurable & max-f is A-measurable
by A5,MESFUNC2:25,26,27;
A8: Integral2(M2,|.f.|) is_integrable_on M1
& Integral2(M2,max+f) is_integrable_on M1
& Integral2(M2,max-f) is_integrable_on M1 by A1,A2,A3,Th20;
A9: max+f is nonnegative & max-f is nonnegative by MESFUN11:5;
Integral2(M2,|.f.|) is_a.e.finite M1 by A8,Th19; then
consider U be Element of S1 such that
A10: M1.U = 0 & Integral2(M2,|.f.|)|U` is PartFunc of X1,REAL;
A11:U` = SX1 \ U by A4,SUBSET_1:def 4; then
A12:Integral2(M2,|.f.|)|U` is_integrable_on M1
& Integral2(M2,max+f)|U` is_integrable_on M1
& Integral2(M2,max-f)|U` is_integrable_on M1 by A8,MESFUNC5:97;
A13:dom Integral2(M2,f) = X1 & dom Integral2(M2,max+f) = X1
& dom Integral2(M2,max-f) = X1 & dom Integral2(M2,|.f.|) = X1
by FUNCT_2:def 1;
take U;
thus M1.U = 0 by A10;
thus
A14: for x be Element of X1 st x in U` holds ProjPMap1(f,x) is_integrable_on M2
proof
let x be Element of X1;
assume
A15: x in U`; then
A16: x in dom(Integral2(M2,|.f.|)|U`) by A13,RELAT_1:57;
X-section(A,x) = Measurable-X-section(A,x) by MEASUR11:def 6; then
A17: dom ProjPMap1(|.f.|,x) = Measurable-X-section(A,x)
& dom ProjPMap1(f,x) = Measurable-X-section(A,x) by A5,A6,MESFUN12:def 3;
A18: ProjPMap1(|.f.|,x) is (Measurable-X-section(A,x))-measurable
& ProjPMap1(f,x) is (Measurable-X-section(A,x))-measurable
by A5,A6,A7,MESFUN12:47;
A19: ProjPMap1(|.f.|,x) = |.ProjPMap1(f,x).| by Th27; then
integral+(M2,max+ ProjPMap1(|.f.|,x))
= integral+(M2,ProjPMap1(|.f.|,x)) by MESFUN11:31
.= Integral(M2,ProjPMap1(|.f.|,x))
by A6,A7,A17,A19,MESFUN12:47,MESFUNC5:88
.= Integral2(M2,|.f.|).x by MESFUN12:def 8
.= (Integral2(M2,|.f.|)|U`).x by A15,FUNCT_1:49; then
A20: integral+(M2,max+ ProjPMap1(|.f.|,x)) < +infty
by A10,A16,PARTFUN1:4,XXREAL_0:9;
integral+(M2,max- ProjPMap1(|.f.|,x)) < +infty
by A17,A18,A19,MESFUN11:53; then
|.ProjPMap1(f,x).| is_integrable_on M2
by A6,A7,A17,A19,A20,MESFUN12:47,MESFUNC5:def 17;
hence ProjPMap1(f,x) is_integrable_on M2 by A17,A18,MESFUNC5:100;
end;
thus Integral2(M2,|.f.|)|U` is PartFunc of X1,REAL by A10;
set G1 = Integral2(M2,max+f)|U`;
set G2 = Integral2(M2,max-f)|U`;
reconsider G = G1 - G2 as PartFunc of X1,ExtREAL;
A21:dom G1 = U` & dom G2 = U` by A13,RELAT_1:62;
A22:now let x be object;
per cases;
suppose A23: x in dom G1; then
reconsider x1 = x as Element of X1;
A24: G1.x = Integral2(M2,max+f).x by A21,A23,FUNCT_1:49
.= Integral(M2,ProjPMap1(max+f,x1)) by MESFUN12:def 8
.= Integral(M2,max+ ProjPMap1(f,x1)) by MESFUN12:45;
A25: ProjPMap1(f,x1) is_integrable_on M2 by A14,A21,A23; then
consider B be Element of S2 such that
A26: B = dom ProjPMap1(f,x1) & ProjPMap1(f,x1) is B-measurable
by MESFUNC5:def 17;
A27: B = dom max+ ProjPMap1(f,x1) & max+ ProjPMap1(f,x1) is B-measurable
by A26,MESFUNC2:def 2,MESFUN11:10;
integral+(M2,max+ ProjPMap1(f,x1)) < +infty by A25,MESFUNC5:def 17;
hence G1.x < +infty by A24,A27,MESFUNC5:88,MESFUN11:5;
end;
suppose not x in dom G1;
hence G1.x < +infty by FUNCT_1:def 2;
end;
end;
now let x be object;
per cases;
suppose A28: x in dom G1; then
reconsider x1 = x as Element of X1;
A29: G1.x = Integral2(M2,max+f).x by A21,A28,FUNCT_1:49
.= Integral(M2,ProjPMap1(max+f,x1)) by MESFUN12:def 8
.= Integral(M2,max+ ProjPMap1(f,x1)) by MESFUN12:45;
ProjPMap1(f,x1) is_integrable_on M2 by A14,A21,A28; then
consider B be Element of S2 such that
A30: B = dom ProjPMap1(f,x1) & ProjPMap1(f,x1) is B-measurable
by MESFUNC5:def 17;
B = dom max+ ProjPMap1(f,x1) & max+ ProjPMap1(f,x1) is B-measurable
by A30,MESFUNC2:def 2,MESFUN11:10;
hence G1.x > -infty by A29,MESFUNC5:90,MESFUN11:5;
end;
suppose not x in dom G1;
hence G1.x > -infty by FUNCT_1:def 2;
end;
end; then
A31:G1 is without-infty without+infty by A22,MESFUNC5:def 5,def 6; then
A32:dom G = dom G1 /\ dom G2 by MESFUN11:23;
A33:ex A1 be Element of S1 st
A1 = dom G1 & G1 is A1-measurable by A12,MESFUNC5:def 17;
A34:ex A2 be Element of S1 st
A2 = dom G2 & G2 is A2-measurable by A12,MESFUNC5:def 17;
now let x be object;
per cases;
suppose A35: x in dom G2; then
reconsider x1 = x as Element of X1;
A36: G2.x = Integral2(M2,max-f).x by A21,A35,FUNCT_1:49
.= Integral(M2,ProjPMap1(max-f,x1)) by MESFUN12:def 8
.= Integral(M2,max-ProjPMap1(f,x1)) by MESFUN12:45;
ProjPMap1(f,x1) is_integrable_on M2 by A14,A21,A35; then
consider B be Element of S2 such that
A37: B = dom ProjPMap1(f,x1) & ProjPMap1(f,x1) is B-measurable
by MESFUNC5:def 17;
B = dom max- ProjPMap1(f,x1) & max- ProjPMap1(f,x1) is B-measurable
by A37,MESFUNC2:def 3,MESFUN11:10;
hence G2.x > -infty by A36,MESFUNC5:90,MESFUN11:5;
end;
suppose not x in dom G2;
hence G2.x > -infty by FUNCT_1:def 2;
end;
end; then
G2 is without-infty by MESFUNC5:def 5; then
A38:G is (SX1\U)-measurable by A11,A21,A31,A32,A33,A34,MEASUR11:66;
A39:dom(Integral2(M2,f)|U`) = U` & dom(G|U`) = U`
& dom(Integral2(M2,|.f.|)|U`) = U` by A13,A21,A32,RELAT_1:62; then
A40:U` = dom (max+(Integral2(M2,f)|U`))
& U` = dom (max-(Integral2(M2,f)|U`)) by MESFUNC2:def 2,def 3;
A41:now let x be Element of X1;
assume A42: x in dom(Integral2(M2,f)|U`); then
A43: x in U` by A13,RELAT_1:62; then
A44: (Integral2(M2,f)|U`).x
= Integral2(M2,f).x by FUNCT_1:49
.= Integral(M2,ProjPMap1(f,x)) by MESFUN12:def 8;
X-section(A,x) = Measurable-X-section(A,x) by MEASUR11:def 6; then
B17: dom ProjPMap1(|.f.|,x) = Measurable-X-section(A,x)
& dom ProjPMap1(f,x) = Measurable-X-section(A,x) by A5,A6,MESFUN12:def 3;
x in dom G by A21,A32,A42,RELAT_1:57; then
(G|U`).x = G1.x - G2.x by A21,A32,MESFUNC1:def 4
.= Integral2(M2,max+f).x - G2.x by A43,FUNCT_1:49
.= Integral2(M2,max+f).x - Integral2(M2,max-f).x by A43,FUNCT_1:49
.= Integral(M2,ProjPMap1(max+f,x)) - Integral2(M2,max-f).x
by MESFUN12:def 8
.= Integral(M2,ProjPMap1(max+f,x)) - Integral(M2,ProjPMap1(max-f,x))
by MESFUN12:def 8
.= Integral(M2,max+ ProjPMap1(f,x)) - Integral(M2,ProjPMap1(max-f,x))
by MESFUN12:45
.= Integral(M2,max+ ProjPMap1(f,x)) - Integral(M2,max- ProjPMap1(f,x))
by MESFUN12:45
.= Integral(M2,ProjPMap1(f,x)) by A5,B17,MESFUN12:47,MESFUN11:54;
hence (Integral2(M2,f)|U`).x = (G|U`).x by A44;
end;
hence Integral2(M2,f) is (SX1\U)-measurable
by A11,A13,A21,A32,A38,A39,PARTFUN1:5,MESFUN12:36;
Integral2(M2,f)|U` is (SX1\U)-measurable
by A13,A21,A32,A38,A41,RELAT_1:62,PARTFUN1:5; then
A45:max+(Integral2(M2,f)|U`) is (SX1\U)-measurable &
max-(Integral2(M2,f)|U`) is (SX1\U)-measurable
by A11,A39,MESFUNC2:25,26;
now let y be set;
assume y in rng(Integral2(M2,f)|U`); then
consider x be Element of X1 such that
A47: x in dom(Integral2(M2,f)|U`) & y = (Integral2(M2,f)|U`).x
by PARTFUN1:3;
A48: x in dom(Integral2(M2,f)) & x in U` by A47,RELAT_1:57; then
x in dom(Integral2(M2,|.f.|)|U`) by A13,RELAT_1:57; then
A49: (Integral2(M2,|.f.|)|U`).x < +infty by A10,PARTFUN1:4,XXREAL_0:9;
Integral2(M2,f).x = Integral(M2,ProjPMap1(f,x)) by MESFUN12:def 8; then
|. Integral2(M2,f).x .| <= Integral(M2,|.ProjPMap1(f,x).|)
by A14,A48,MESFUNC5:101; then
|. Integral2(M2,f).x .| <= Integral(M2,ProjPMap1(|.f.|,x)) by Th27; then
|. Integral2(M2,f).x .| <= Integral2(M2,|.f.|).x by MESFUN12:def 8; then
|. Integral2(M2,f).x .| <= (Integral2(M2,|.f.|)|U`).x
by A48,FUNCT_1:49; then
|. (Integral2(M2,f)|U`).x .| <= (Integral2(M2,|.f.|)|U`).x
by A47,FUNCT_1:47; then
|. (Integral2(M2,f)|U`).x .| < +infty by A49,XXREAL_0:2;
hence y in REAL by A47,EXTREAL1:41;
end; then
A50:rng(Integral2(M2,f)|U`) c= REAL;
now let x be Element of X1;
assume A51: x in dom (max+(Integral2(M2,f)|U`)); then
A52: x in dom(Integral2(M2,f)) & x in U` by A13,A39,MESFUNC2:def 2; then
A53: x in dom(max+ Integral2(M2,f)) by MESFUNC2:def 2;
A54: x in dom(|.Integral2(M2,f).|) by A52,MESFUNC1:def 10;
(max+(Integral2(M2,f)|U`)).x
= max((Integral2(M2,f)|U`).x,0) by A51,MESFUNC2:def 2
.= max(Integral2(M2,f).x,0) by A39,A40,A51,FUNCT_1:47
.= (max+ Integral2(M2,f)).x by A53,MESFUNC2:def 2; then
(max+(Integral2(M2,f)|U`)).x <= |.Integral2(M2,f).| .x by Th29; then
(max+(Integral2(M2,f)|U`)).x <= |. Integral2(M2,f).x .|
by A54,MESFUNC1:def 10; then
A55: |. (max+(Integral2(M2,f)|U`)).x .| <= |. Integral2(M2,f).x .|
by EXTREAL1:3,MESFUNC2:12;
Integral2(M2,f).x = Integral(M2,ProjPMap1(f,x)) by MESFUN12:def 8; then
|. Integral2(M2,f).x .| <= Integral(M2,|.ProjPMap1(f,x).|)
by A14,A40,A51,MESFUNC5:101; then
|. Integral2(M2,f).x .| <= Integral(M2,ProjPMap1(|.f.|,x)) by Th27; then
|. Integral2(M2,f).x .| <= Integral2(M2,|.f.|).x by MESFUN12:def 8; then
|. Integral2(M2,f).x .| <= (Integral2(M2,|.f.|)|U`).x
by A40,A51,FUNCT_1:49;
hence |. max+(Integral2(M2,f)|U`).x .| <= (Integral2(M2,|.f.|)|U`).x
by A55,XXREAL_0:2;
end; then
A56:max+(Integral2(M2,f)|U`) is_integrable_on M1
by A11,A12,A39,A45,A40,MESFUNC5:102;
now let x be Element of X1;
assume A57: x in dom(max-(Integral2(M2,f)|U`)); then
A58: x in dom(Integral2(M2,f)) & x in U`by A13,A39,MESFUNC2:def 3; then
A59: x in dom(max- Integral2(M2,f)) by MESFUNC2:def 3;
A60: x in dom(|.Integral2(M2,f).|) by A58,MESFUNC1:def 10;
(max-(Integral2(M2,f)|U`)).x
= max(-((Integral2(M2,f)|U`).x),0) by A57,MESFUNC2:def 3
.= max(-Integral2(M2,f).x,0) by A39,A40,A57,FUNCT_1:47
.= (max- Integral2(M2,f)).x by A59,MESFUNC2:def 3; then
(max-(Integral2(M2,f)|U`)).x <= |.Integral2(M2,f).| .x by Th29; then
(max-(Integral2(M2,f)|U`)).x <= |. Integral2(M2,f).x .|
by A60,MESFUNC1:def 10; then
A61: |. (max-(Integral2(M2,f)|U`)).x .| <= |. Integral2(M2,f).x .|
by EXTREAL1:3,MESFUNC2:13;
Integral2(M2,f).x = Integral(M2,ProjPMap1(f,x)) by MESFUN12:def 8; then
|. Integral2(M2,f).x .| <= Integral(M2,|.ProjPMap1(f,x).|)
by A14,A40,A57,MESFUNC5:101; then
|. Integral2(M2,f).x .| <= Integral(M2,ProjPMap1(|.f.|,x)) by Th27; then
|. Integral2(M2,f).x .| <= Integral2(M2,|.f.|).x by MESFUN12:def 8; then
|. Integral2(M2,f).x .| <= (Integral2(M2,|.f.|)|U`).x
by A40,A57,FUNCT_1:49;
hence |. max-(Integral2(M2,f)|U`).x .| <= (Integral2(M2,|.f.|)|U`).x
by A61,XXREAL_0:2;
end; then
max-(Integral2(M2,f)|U`) is_integrable_on M1
by A11,A12,A39,A45,A40,MESFUNC5:102; then
max+(Integral2(M2,f)|U`) - max-(Integral2(M2,f)|U`)
is_integrable_on M1 by A56,MESFUN10:12;
hence
A62: Integral2(M2,f)|U` is_integrable_on M1 by MESFUNC2:23;
reconsider F = Integral2(M2,f)|U` as PartFunc of X1,REAL by A50,RELSET_1:6;
R_EAL F is_integrable_on M1 by A62,MESFUNC5:def 7; then
F is_integrable_on M1 by MESFUNC6:def 4; then
F in { f where f is PartFunc of X1,REAL :
ex ND be Element of S1 st M1.ND=0 & dom f = ND`
& f is_integrable_on M1 } by A10,A39;
hence Integral2(M2,f)|U` in L1_Functions M1 by LPSPACE1:def 8;
consider g1 be PartFunc of X1,ExtREAL such that
A64: dom g1 = dom(Integral2(M2,max+f))
& g1|U` = Integral2(M2,max+f)|U`
& g1 is_integrable_on M1
& Integral(M1,g1) = Integral(M1,Integral2(M2,max+f)|U`)
by A8,A10,A11,A13,Th23,MESFUNC5:97;
consider g2 be PartFunc of X1,ExtREAL such that
A65: dom g2 = dom(Integral2(M2,max-f))
& g2|U` = Integral2(M2,max-f)|U`
& g2 is_integrable_on M1
& Integral(M1,g2) = Integral(M1,Integral2(M2,max-f)|U`)
by A8,A10,A11,A13,Th23,MESFUNC5:97;
consider g be PartFunc of X1,ExtREAL such that
A66: dom g = dom Integral2(M2,f)
& g|U` = Integral2(M2,f)|U`
& g is_integrable_on M1
& Integral(M1,g) = Integral(M1,Integral2(M2,f)|U`)
by A10,A13,A62,Th23;
reconsider g as Function of X1,ExtREAL by A13,A66,FUNCT_2:def 1;
A67:dom(g|U`) = dom g /\ U` & dom(g1|U`) = dom g1 /\ U`
& dom(g2|U`) = dom g2 /\ U` by RELAT_1:61;
now let x be Element of X1;
assume A72: x in dom(g2|U`); then
A68: x in U` by RELAT_1:57;
A69: ProjPMap1(f,x) is_integrable_on M2 by A14,A72,RELAT_1:57; then
consider DP be Element of S2 such that
A70: DP = dom ProjPMap1(f,x) & ProjPMap1(f,x) is DP-measurable
by MESFUNC5:def 17;
A71: DP = dom(max- ProjPMap1(f,x)) & max- ProjPMap1(f,x) is DP-measurable
by A70,MESFUNC2:def 3,26;
A73: max- ProjPMap1(f,x) is nonnegative by MESFUN11:5;
A74: (g2|U`).x = Integral2(M2,max-f).x by A65,A68,FUNCT_1:49
.= Integral(M2,ProjPMap1(max-f,x)) by MESFUN12:def 8
.= Integral(M2,max- ProjPMap1(f,x)) by MESFUN12:45
.= integral+(M2,max- ProjPMap1(f,x)) by A71,MESFUNC5:88,MESFUN11:5; then
(g2|U`).x < +infty by A69,MESFUNC5:def 17;
hence |. (g2|U`).x .| < +infty by A71,A73,A74,MESFUNC5:79,EXTREAL1:def 1;
end; then
(g2|U`) is real-valued by MESFUNC2:def 1; then
A75:dom(g1|U` - g2|U`) = (dom g1 /\ U`) /\ (dom g2 /\ U`)
by A67,MESFUNC2:2; then
A76:dom(g1|U` - g2|U`) = dom(g|U`) by A13,A64,A65,A66,RELAT_1:61;
dom(g1|U`) = U` & dom(g2|U`) = U` by A13,A64,A65,RELAT_1:62; then
A77:U` = dom(g1|U`) /\ dom(g2|U`);
A78:g1|U` is_integrable_on M1 & g2|U` is_integrable_on M1
by A11,A64,A65,MESFUNC5:97;
now let x be Element of X1;
assume A79: x in dom(g|U`); then
A80: x in U` by RELAT_1:57; then
A81: (g|U`).x = Integral2(M2,f).x by A66,FUNCT_1:49;
ProjPMap1(f,x) is_integrable_on M2 by A14,A79,RELAT_1:57; then
A82: ex A be Element of S2 st
A = dom ProjPMap1(f,x) & ProjPMap1(f,x) is A-measurable
by MESFUNC5:def 17;
Integral2(M2,max+f).x = Integral(M2,ProjPMap1(max+f,x))
& Integral2(M2,max-f).x = Integral(M2,ProjPMap1(max-f,x))
by MESFUN12:def 8; then
Integral2(M2,max+f).x = Integral(M2,max+ ProjPMap1(f,x))
& Integral2(M2,max-f).x = Integral(M2,max- ProjPMap1(f,x))
by MESFUN12:45; then
Integral2(M2,max+f).x - Integral2(M2,max-f).x
= Integral(M2,ProjPMap1(f,x)) by A82,MESFUN11:54
.= Integral2(M2,f).x by MESFUN12:def 8; then
(g|U`).x = (Integral2(M2,max+f)|U`).x - Integral2(M2,max-f).x
by A80,A81,FUNCT_1:49
.= (g1|U`).x - (g2|U`).x by A64,A65,A80,FUNCT_1:49;
hence (g|U`).x = ((g1|U`) - (g2|U`)).x by A76,A79,MESFUNC1:def 4;
end; then
A83:g|U` = g1|U` - g2|U` by A13,A64,A65,A66,A75,RELAT_1:61,PARTFUN1:5;
A84:Integral2(M2,max+f) is SX1-measurable
& Integral2(M2,max-f) is SX1-measurable by A2,A6,A7,MESFUN11:5,MESFUN12:60;
A85:Integral(Prod_Measure(M1,M2),max+f)
= Integral(M1,Integral2(M2,max+f)) by A1,A2,A6,A7,A9,MESFUN12:84
.= Integral(M1,Integral2(M2,max+f)|(SX1 \ U)) by A4,A10,A13,A84,MESFUNC5:95
.= Integral(M1,g1|U`) by A4,A64,SUBSET_1:def 4;
A86:Integral(Prod_Measure(M1,M2),max-f)
= Integral(M1,Integral2(M2,max-f)) by A1,A2,A6,A7,A9,MESFUN12:84
.= Integral(M1,Integral2(M2,max-f)|(SX1 \ U)) by A4,A10,A13,A84,MESFUNC5:95
.= Integral(M1,g2|U`) by A4,A65,SUBSET_1:def 4;
Integral(Prod_Measure(M1,M2),f)
= Integral(M1,(g1|U`)|U`) - Integral(M1,(g2|U`)|U`)
by A5,A85,A86,MESFUN11:54; then
Integral(Prod_Measure(M1,M2),f)
= Integral(M1,g|U`) by A77,A78,A83,Th21;
hence ex g be Function of X1,ExtREAL st
g is_integrable_on M1 & g|U` = Integral2(M2,f)|U`
& Integral(Prod_Measure(M1,M2),f) = Integral(M1,g) by A66;
end;
theorem
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, f being PartFunc of [:X1,X2:],ExtREAL,
SX2 being Element of S2
st M1 is sigma_finite & M2 is sigma_finite
& f is_integrable_on Prod_Measure(M1,M2) & X2 = SX2
holds
ex V be Element of S2 st M2.V = 0
& (for y being Element of X2 st y in V` holds
ProjPMap2(f,y) is_integrable_on M1)
& Integral1(M1,|.f.|)|V` is PartFunc of X2,REAL
& Integral1(M1,f) is (SX2\V)-measurable
& Integral1(M1,f)|V` is_integrable_on M2
& Integral1(M1,f)|V` in L1_Functions M2
& (ex g be Function of X2,ExtREAL st
g is_integrable_on M2 & g|V` = Integral1(M1,f)|V`
& Integral(Prod_Measure(M1,M2),f) = Integral(M2,g))
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,
f be PartFunc of [:X1,X2:],ExtREAL, SX2 be Element of S2;
assume that
A1: M1 is sigma_finite and
A2: M2 is sigma_finite and
A3: f is_integrable_on Prod_Measure(M1,M2) and
A4: X2 = SX2;
consider A be Element of sigma measurable_rectangles(S1,S2) such that
A5: A = dom f & f is A-measurable by A3,MESFUNC5:def 17;
A6: A = dom |.f.| & A = dom (max+f) & A = dom (max-f)
by A5,MESFUNC1:def 10,MESFUNC2:def 2,def 3;
A7: |.f.| is A-measurable & max+f is A-measurable & max-f is A-measurable
by A5,MESFUNC2:25,26,27;
A8: Integral1(M1,|.f.|) is_integrable_on M2
& Integral1(M1,max+f) is_integrable_on M2
& Integral1(M1,max-f) is_integrable_on M2 by A1,A2,A3,Th20;
A9: max+f is nonnegative & max-f is nonnegative by MESFUN11:5;
Integral1(M1,|.f.|) is_a.e.finite M2 by A8,Th19; then
consider V be Element of S2 such that
A10: M2.V = 0 & Integral1(M1,|.f.|)|V` is PartFunc of X2,REAL;
A11:V` = SX2 \ V by A4,SUBSET_1:def 4; then
A12:Integral1(M1,|.f.|)|V` is_integrable_on M2
& Integral1(M1,max+f)|V` is_integrable_on M2
& Integral1(M1,max-f)|V` is_integrable_on M2 by A8,MESFUNC5:97;
A13:dom Integral1(M1,f) = X2 & dom Integral1(M1,max+f) = X2
& dom Integral1(M1,max-f) = X2 & dom Integral1(M1,|.f.|) = X2
by FUNCT_2:def 1;
take V;
thus M2.V = 0 by A10;
thus
A14: for y be Element of X2 st y in V` holds ProjPMap2(f,y) is_integrable_on M1
proof
let y be Element of X2;
assume
A15: y in V`; then
A16: y in dom(Integral1(M1,|.f.|)|V`) by A13,RELAT_1:57;
Y-section(A,y) = Measurable-Y-section(A,y) by MEASUR11:def 7; then
A17: dom ProjPMap2(|.f.|,y) = Measurable-Y-section(A,y)
& dom ProjPMap2(f,y) = Measurable-Y-section(A,y) by A5,A6,MESFUN12:def 4;
A18: ProjPMap2(|.f.|,y) is (Measurable-Y-section(A,y))-measurable
& ProjPMap2(f,y) is (Measurable-Y-section(A,y))-measurable
by A5,A6,A7,MESFUN12:47;
A19: ProjPMap2(|.f.|,y) = |.ProjPMap2(f,y).| by Th27; then
integral+(M1,max+ ProjPMap2(|.f.|,y))
= integral+(M1,ProjPMap2(|.f.|,y)) by MESFUN11:31
.= Integral(M1,ProjPMap2(|.f.|,y))
by A6,A7,A17,A19,MESFUN12:47,MESFUNC5:88
.= Integral1(M1,|.f.|).y by MESFUN12:def 7
.= (Integral1(M1,|.f.|)|V`).y by A15,FUNCT_1:49; then
A20: integral+(M1,max+ ProjPMap2(|.f.|,y)) < +infty
by A10,A16,PARTFUN1:4,XXREAL_0:9;
integral+(M1,max- ProjPMap2(|.f.|,y)) < +infty
by A17,A18,A19,MESFUN11:53; then
|.ProjPMap2(f,y).| is_integrable_on M1
by A6,A7,A17,A19,A20,MESFUN12:47,MESFUNC5:def 17;
hence ProjPMap2(f,y) is_integrable_on M1 by A17,A18,MESFUNC5:100;
end;
thus Integral1(M1,|.f.|)|V` is PartFunc of X2,REAL by A10;
set G1 = Integral1(M1,max+f)|V`;
set G2 = Integral1(M1,max-f)|V`;
reconsider G = G1 - G2 as PartFunc of X2,ExtREAL;
A21:dom G1 = V` & dom G2 = V` by A13,RELAT_1:62;
A22:now let x be object;
per cases;
suppose A23: x in dom G1; then
reconsider x1 = x as Element of X2;
A24: G1.x = Integral1(M1,max+f).x by A21,A23,FUNCT_1:49
.= Integral(M1,ProjPMap2(max+f,x1)) by MESFUN12:def 7
.= Integral(M1,max+ ProjPMap2(f,x1)) by MESFUN12:46;
A25: ProjPMap2(f,x1) is_integrable_on M1 by A14,A21,A23; then
consider B be Element of S1 such that
A26: B = dom ProjPMap2(f,x1) & ProjPMap2(f,x1) is B-measurable
by MESFUNC5:def 17;
A27: B = dom max+ ProjPMap2(f,x1) & max+ ProjPMap2(f,x1) is B-measurable
by A26,MESFUNC2:def 2,MESFUN11:10;
integral+(M1,max+ ProjPMap2(f,x1)) < +infty by A25,MESFUNC5:def 17;
hence G1.x < +infty by A24,A27,MESFUNC5:88,MESFUN11:5;
end;
suppose not x in dom G1;
hence G1.x < +infty by FUNCT_1:def 2;
end;
end;
now let x be object;
per cases;
suppose A28: x in dom G1; then
reconsider x1 = x as Element of X2;
A29: G1.x = Integral1(M1,max+f).x by A21,A28,FUNCT_1:49
.= Integral(M1,ProjPMap2(max+f,x1)) by MESFUN12:def 7
.= Integral(M1,max+ ProjPMap2(f,x1)) by MESFUN12:46;
ProjPMap2(f,x1) is_integrable_on M1 by A14,A21,A28; then
consider B be Element of S1 such that
A30: B = dom ProjPMap2(f,x1) & ProjPMap2(f,x1) is B-measurable
by MESFUNC5:def 17;
B = dom max+ ProjPMap2(f,x1) & max+ ProjPMap2(f,x1) is B-measurable
by A30,MESFUNC2:def 2,MESFUN11:10;
hence G1.x > -infty by A29,MESFUNC5:90,MESFUN11:5;
end;
suppose not x in dom G1;
hence G1.x > -infty by FUNCT_1:def 2;
end;
end; then
A31:G1 is without-infty without+infty by A22,MESFUNC5:def 5,def 6; then
A32:dom G = dom G1 /\ dom G2 by MESFUN11:23;
A33:ex A1 be Element of S2 st
A1 = dom G1 & G1 is A1-measurable by A12,MESFUNC5:def 17;
A34:ex A2 be Element of S2 st
A2 = dom G2 & G2 is A2-measurable by A12,MESFUNC5:def 17;
now let x be object;
per cases;
suppose A35: x in dom G2; then
reconsider x1 = x as Element of X2;
A36: G2.x = Integral1(M1,max-f).x by A21,A35,FUNCT_1:49
.= Integral(M1,ProjPMap2(max-f,x1)) by MESFUN12:def 7
.= Integral(M1,max-ProjPMap2(f,x1)) by MESFUN12:46;
ProjPMap2(f,x1) is_integrable_on M1 by A14,A21,A35; then
consider B be Element of S1 such that
A37: B = dom ProjPMap2(f,x1) & ProjPMap2(f,x1) is B-measurable
by MESFUNC5:def 17;
B = dom max- ProjPMap2(f,x1) & max- ProjPMap2(f,x1) is B-measurable
by A37,MESFUNC2:def 3,MESFUN11:10;
hence G2.x > -infty by A36,MESFUNC5:90,MESFUN11:5;
end;
suppose not x in dom G2;
hence G2.x > -infty by FUNCT_1:def 2;
end;
end; then
G2 is without-infty by MESFUNC5:def 5; then
A38:G is (SX2\V)-measurable by A11,A21,A31,A32,A33,A34,MEASUR11:66;
A39:dom(Integral1(M1,f)|V`) = V` & dom(G|V`) = V`
& dom(Integral1(M1,|.f.|)|V`) = V` by A13,A21,A32,RELAT_1:62; then
A40:V` = dom (max+(Integral1(M1,f)|V`))
& V` = dom (max-(Integral1(M1,f)|V`)) by MESFUNC2:def 2,def 3;
A41:now let x be Element of X2;
assume A42: x in dom(Integral1(M1,f)|V`); then
A43: x in V` by A13,RELAT_1:62; then
A44: (Integral1(M1,f)|V`).x
= Integral1(M1,f).x by FUNCT_1:49
.= Integral(M1,ProjPMap2(f,x)) by MESFUN12:def 7;
Y-section(A,x) = Measurable-Y-section(A,x) by MEASUR11:def 7; then
B17: dom ProjPMap2(|.f.|,x) = Measurable-Y-section(A,x)
& dom ProjPMap2(f,x) = Measurable-Y-section(A,x) by A5,A6,MESFUN12:def 4;
x in dom G by A21,A32,A42,RELAT_1:57; then
(G|V`).x = G1.x - G2.x by A21,A32,MESFUNC1:def 4
.= Integral1(M1,max+f).x - G2.x by A43,FUNCT_1:49
.= Integral1(M1,max+f).x - Integral1(M1,max-f).x by A43,FUNCT_1:49
.= Integral(M1,ProjPMap2(max+f,x)) - Integral1(M1,max-f).x
by MESFUN12:def 7
.= Integral(M1,ProjPMap2(max+f,x)) - Integral(M1,ProjPMap2(max-f,x))
by MESFUN12:def 7
.= Integral(M1,max+ ProjPMap2(f,x)) - Integral(M1,ProjPMap2(max-f,x))
by MESFUN12:46
.= Integral(M1,max+ ProjPMap2(f,x)) - Integral(M1,max- ProjPMap2(f,x))
by MESFUN12:46
.= Integral(M1,ProjPMap2(f,x)) by A5,B17,MESFUN12:47,MESFUN11:54;
hence (Integral1(M1,f)|V`).x = (G|V`).x by A44;
end;
hence Integral1(M1,f) is (SX2\V)-measurable
by A11,A13,A21,A32,A38,A39,PARTFUN1:5,MESFUN12:36;
Integral1(M1,f)|V` is (SX2\V)-measurable
by A13,A21,A32,A38,A41,RELAT_1:62,PARTFUN1:5; then
A45:max+(Integral1(M1,f)|V`) is (SX2\V)-measurable &
max-(Integral1(M1,f)|V`) is (SX2\V)-measurable
by A11,A39,MESFUNC2:25,26;
now let y be set;
assume y in rng(Integral1(M1,f)|V`); then
consider x be Element of X2 such that
A47: x in dom(Integral1(M1,f)|V`) & y = (Integral1(M1,f)|V`).x
by PARTFUN1:3;
A48: x in dom(Integral1(M1,f)) & x in V` by A47,RELAT_1:57; then
x in dom(Integral1(M1,|.f.|)|V`) by A13,RELAT_1:57; then
A49: (Integral1(M1,|.f.|)|V`).x < +infty by A10,PARTFUN1:4,XXREAL_0:9;
Integral1(M1,f).x = Integral(M1,ProjPMap2(f,x)) by MESFUN12:def 7; then
|. Integral1(M1,f).x .| <= Integral(M1,|.ProjPMap2(f,x).|)
by A14,A48,MESFUNC5:101; then
|. Integral1(M1,f).x .| <= Integral(M1,ProjPMap2(|.f.|,x)) by Th27; then
|. Integral1(M1,f).x .| <= Integral1(M1,|.f.|).x by MESFUN12:def 7; then
|. Integral1(M1,f).x .| <= (Integral1(M1,|.f.|)|V`).x
by A48,FUNCT_1:49; then
|. (Integral1(M1,f)|V`).x .| <= (Integral1(M1,|.f.|)|V`).x
by A47,FUNCT_1:47; then
|. (Integral1(M1,f)|V`).x .| < +infty by A49,XXREAL_0:2;
hence y in REAL by A47,EXTREAL1:41;
end; then
A50:rng(Integral1(M1,f)|V`) c= REAL;
now let x be Element of X2;
assume A51: x in dom (max+(Integral1(M1,f)|V`)); then
A52: x in dom(Integral1(M1,f)) & x in V` by A13,A39,MESFUNC2:def 2; then
A53: x in dom(max+ Integral1(M1,f)) by MESFUNC2:def 2;
A54: x in dom(|.Integral1(M1,f).|) by A52,MESFUNC1:def 10;
(max+(Integral1(M1,f)|V`)).x
= max((Integral1(M1,f)|V`).x,0) by A51,MESFUNC2:def 2
.= max(Integral1(M1,f).x,0) by A39,A40,A51,FUNCT_1:47
.= (max+ Integral1(M1,f)).x by A53,MESFUNC2:def 2; then
(max+(Integral1(M1,f)|V`)).x <= |.Integral1(M1,f).| .x by Th29; then
(max+(Integral1(M1,f)|V`)).x <= |. Integral1(M1,f).x .|
by A54,MESFUNC1:def 10; then
A55: |. (max+(Integral1(M1,f)|V`)).x .| <= |. Integral1(M1,f).x .|
by EXTREAL1:3,MESFUNC2:12;
Integral1(M1,f).x = Integral(M1,ProjPMap2(f,x)) by MESFUN12:def 7; then
|. Integral1(M1,f).x .| <= Integral(M1,|.ProjPMap2(f,x).|)
by A14,A40,A51,MESFUNC5:101; then
|. Integral1(M1,f).x .| <= Integral(M1,ProjPMap2(|.f.|,x)) by Th27; then
|. Integral1(M1,f).x .| <= Integral1(M1,|.f.|).x by MESFUN12:def 7; then
|. Integral1(M1,f).x .| <= (Integral1(M1,|.f.|)|V`).x
by A40,A51,FUNCT_1:49;
hence
|. max+(Integral1(M1,f)|V`).x .| <= (Integral1(M1,|.f.|)|V`).x
by A55,XXREAL_0:2;
end; then
A56:max+(Integral1(M1,f)|V`) is_integrable_on M2
by A11,A12,A39,A45,A40,MESFUNC5:102;
now let x be Element of X2;
assume A57: x in dom(max-(Integral1(M1,f)|V`)); then
A58: x in dom(Integral1(M1,f)) & x in V`by A13,A39,MESFUNC2:def 3; then
A59: x in dom(max- Integral1(M1,f)) by MESFUNC2:def 3;
A60: x in dom(|.Integral1(M1,f).|) by A58,MESFUNC1:def 10;
(max-(Integral1(M1,f)|V`)).x
= max(-((Integral1(M1,f)|V`).x),0) by A57,MESFUNC2:def 3
.= max(-Integral1(M1,f).x,0) by A39,A40,A57,FUNCT_1:47
.= (max- Integral1(M1,f)).x by A59,MESFUNC2:def 3; then
(max-(Integral1(M1,f)|V`)).x <= |.Integral1(M1,f).| .x by Th29; then
(max-(Integral1(M1,f)|V`)).x <= |. Integral1(M1,f).x .|
by A60,MESFUNC1:def 10; then
A61: |. (max-(Integral1(M1,f)|V`)).x .| <= |. Integral1(M1,f).x .|
by EXTREAL1:3,MESFUNC2:13;
Integral1(M1,f).x = Integral(M1,ProjPMap2(f,x)) by MESFUN12:def 7; then
|. Integral1(M1,f).x .| <= Integral(M1,|.ProjPMap2(f,x).|)
by A14,A40,A57,MESFUNC5:101; then
|. Integral1(M1,f).x .| <= Integral(M1,ProjPMap2(|.f.|,x)) by Th27; then
|. Integral1(M1,f).x .| <= Integral1(M1,|.f.|).x by MESFUN12:def 7; then
|. Integral1(M1,f).x .| <= (Integral1(M1,|.f.|)|V`).x
by A40,A57,FUNCT_1:49;
hence |. max-(Integral1(M1,f)|V`).x .| <= (Integral1(M1,|.f.|)|V`).x
by A61,XXREAL_0:2;
end; then
max-(Integral1(M1,f)|V`) is_integrable_on M2
by A11,A12,A39,A45,A40,MESFUNC5:102; then
max+(Integral1(M1,f)|V`) - max-(Integral1(M1,f)|V`)
is_integrable_on M2 by A56,MESFUN10:12;
hence
A62: Integral1(M1,f)|V` is_integrable_on M2 by MESFUNC2:23;
reconsider F = Integral1(M1,f)|V` as PartFunc of X2,REAL by A50,RELSET_1:6;
R_EAL F is_integrable_on M2 by A62,MESFUNC5:def 7; then
F is_integrable_on M2 by MESFUNC6:def 4; then
F in { f where f is PartFunc of X2,REAL :
ex ND be Element of S2 st M2.ND=0 & dom f = ND`
& f is_integrable_on M2 } by A10,A39;
hence Integral1(M1,f)|V` in L1_Functions M2 by LPSPACE1:def 8;
consider g1 be PartFunc of X2,ExtREAL such that
A64: dom g1 = dom(Integral1(M1,max+f))
& g1|V` = Integral1(M1,max+f)|V`
& g1 is_integrable_on M2
& Integral(M2,g1) = Integral(M2,Integral1(M1,max+f)|V`)
by A8,A10,A11,A13,Th23,MESFUNC5:97;
consider g2 be PartFunc of X2,ExtREAL such that
A65: dom g2 = dom(Integral1(M1,max-f))
& g2|V` = Integral1(M1,max-f)|V`
& g2 is_integrable_on M2
& Integral(M2,g2) = Integral(M2,Integral1(M1,max-f)|V`)
by A8,A10,A11,A13,Th23,MESFUNC5:97;
consider g be PartFunc of X2,ExtREAL such that
A66: dom g = dom Integral1(M1,f)
& g|V` = Integral1(M1,f)|V`
& g is_integrable_on M2
& Integral(M2,g) = Integral(M2,Integral1(M1,f)|V`)
by A10,A13,A62,Th23;
reconsider g as Function of X2,ExtREAL by A13,A66,FUNCT_2:def 1;
A67:dom(g|V`) = dom g /\ V` & dom(g1|V`) = dom g1 /\ V`
& dom(g2|V`) = dom g2 /\ V` by RELAT_1:61;
now let x be Element of X2;
assume A72: x in dom(g2|V`); then
A68: x in V` by RELAT_1:57;
A69: ProjPMap2(f,x) is_integrable_on M1 by A14,A72,RELAT_1:57; then
consider DP be Element of S1 such that
A70: DP = dom ProjPMap2(f,x) & ProjPMap2(f,x) is DP-measurable
by MESFUNC5:def 17;
A71: DP = dom(max- ProjPMap2(f,x)) & max- ProjPMap2(f,x) is DP-measurable
by A70,MESFUNC2:def 3,26;
A73: max- ProjPMap2(f,x) is nonnegative by MESFUN11:5;
A74: (g2|V`).x = Integral1(M1,max-f).x by A65,A68,FUNCT_1:49
.= Integral(M1,ProjPMap2(max-f,x)) by MESFUN12:def 7
.= Integral(M1,max- ProjPMap2(f,x)) by MESFUN12:46
.= integral+(M1,max- ProjPMap2(f,x)) by A71,MESFUNC5:88,MESFUN11:5; then
(g2|V`).x < +infty by A69,MESFUNC5:def 17;
hence |. (g2|V`).x .| < +infty by A71,A73,A74,MESFUNC5:79,EXTREAL1:def 1;
end; then
(g2|V`) is real-valued by MESFUNC2:def 1; then
A75:dom(g1|V` - g2|V`) = (dom g1 /\ V`) /\ (dom g2 /\ V`)
by A67,MESFUNC2:2; then
A76:dom(g1|V` - g2|V`) = dom(g|V`) by A13,A64,A65,A66,RELAT_1:61;
dom(g1|V`) = V` & dom(g2|V`) = V` by A13,A64,A65,RELAT_1:62; then
A77:V` = dom(g1|V`) /\ dom(g2|V`);
A78:g1|V` is_integrable_on M2 & g2|V` is_integrable_on M2
by A11,A64,A65,MESFUNC5:97;
now let x be Element of X2;
assume A79: x in dom(g|V`); then
A80: x in V` by RELAT_1:57; then
A81: (g|V`).x = Integral1(M1,f).x by A66,FUNCT_1:49;
ProjPMap2(f,x) is_integrable_on M1 by A14,A79,RELAT_1:57; then
A82: ex A be Element of S1 st
A = dom ProjPMap2(f,x) & ProjPMap2(f,x) is A-measurable
by MESFUNC5:def 17;
Integral1(M1,max+f).x = Integral(M1,ProjPMap2(max+f,x))
& Integral1(M1,max-f).x = Integral(M1,ProjPMap2(max-f,x))
by MESFUN12:def 7; then
Integral1(M1,max+f).x = Integral(M1,max+ ProjPMap2(f,x))
& Integral1(M1,max-f).x = Integral(M1,max- ProjPMap2(f,x))
by MESFUN12:46; then
Integral1(M1,max+f).x - Integral1(M1,max-f).x
= Integral(M1,ProjPMap2(f,x)) by A82,MESFUN11:54
.= Integral1(M1,f).x by MESFUN12:def 7; then
(g|V`).x = (Integral1(M1,max+f)|V`).x - Integral1(M1,max-f).x
by A80,A81,FUNCT_1:49
.= (g1|V`).x - (g2|V`).x by A64,A65,A80,FUNCT_1:49;
hence (g|V`).x = ((g1|V`) - (g2|V`)).x by A76,A79,MESFUNC1:def 4;
end; then
A83:g|V` = g1|V` - g2|V` by A13,A64,A65,A66,A75,RELAT_1:61,PARTFUN1:5;
A84:Integral1(M1,max+f) is SX2-measurable
& Integral1(M1,max-f) is SX2-measurable by A1,A6,A7,MESFUN11:5,MESFUN12:59;
A85:Integral(Prod_Measure(M1,M2),max+f)
= Integral(M2,Integral1(M1,max+f)) by A1,A2,A6,A7,A9,MESFUN12:84
.= Integral(M2,Integral1(M1,max+f)|(SX2 \ V)) by A4,A10,A13,A84,MESFUNC5:95
.= Integral(M2,g1|V`) by A4,A64,SUBSET_1:def 4;
A86:Integral(Prod_Measure(M1,M2),max-f)
= Integral(M2,Integral1(M1,max-f)) by A1,A2,A6,A7,A9,MESFUN12:84
.= Integral(M2,Integral1(M1,max-f)|(SX2 \ V)) by A4,A10,A13,A84,MESFUNC5:95
.= Integral(M2,g2|V`) by A4,A65,SUBSET_1:def 4;
Integral(Prod_Measure(M1,M2),f)
= Integral(M2,(g1|V`)|V`) - Integral(M2,(g2|V`)|V`)
by A5,A85,A86,MESFUN11:54; then
Integral(Prod_Measure(M1,M2),f)
= Integral(M2,g|V`) by A77,A78,A83,Th21;
hence thesis by A66;
end;
theorem
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, f being PartFunc of [:X1,X2:],ExtREAL
st M1 is sigma_finite & M2 is sigma_finite
& f is_integrable_on Prod_Measure(M1,M2)
& (for x being Element of X1 holds Integral2(M2,|.f.|).x < +infty)
holds
(for x being Element of X1 holds ProjPMap1(f,x) is_integrable_on M2)
& (for U being Element of S1 holds Integral2(M2,f) is U-measurable)
& Integral2(M2,f) is_integrable_on M1
& Integral(Prod_Measure(M1,M2),f) = Integral(M1,Integral2(M2,f))
& Integral2(M2,f) in L1_Functions M1
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,
f be PartFunc of [:X1,X2:],ExtREAL;
assume that
A1: M1 is sigma_finite and
A2: M2 is sigma_finite and
A3: f is_integrable_on Prod_Measure(M1,M2) and
A4: for x be Element of X1 holds Integral2(M2,|.f.|).x < +infty;
reconsider XX1 = X1 as Element of S1 by MEASURE1:7;
consider A be Element of sigma measurable_rectangles(S1,S2) such that
A5: A = dom f & f is A-measurable by A3,MESFUNC5:def 17;
A6: A = dom |.f.| by A5,MESFUNC1:def 10;
A7: now let x be Element of X1;
X-section(A,x) = Measurable-X-section(A,x) by MEASUR11:def 6; then
A8: dom ProjPMap1(|.f.|,x) = Measurable-X-section(A,x) by A6,MESFUN12:def 3;
A9: |.f.| is A-measurable by A5,MESFUNC2:27; then
A10: ProjPMap1(|.f.|,x) is (Measurable-X-section(A,x))-measurable
by A6,MESFUN12:47;
A11: ProjPMap1(|.f.|,x) = |.ProjPMap1(f,x).| by Th27; then
integral+(M2,max+ ProjPMap1(|.f.|,x))
= integral+(M2,ProjPMap1(|.f.|,x)) by MESFUN11:31
.= Integral(M2,ProjPMap1(|.f.|,x)) by A6,A8,A9,A11,MESFUNC5:88,MESFUN12:47
.= Integral2(M2,|.f.|).x by MESFUN12:def 8; then
A12: integral+(M2,max+ ProjPMap1(|.f.|,x)) < +infty by A4;
integral+(M2,max- ProjPMap1(|.f.|,x)) = 0 by A8,A10,A11,MESFUN11:53; then
A13: ProjPMap1(|.f.|,x) is_integrable_on M2
by A6,A8,A9,A12,MESFUNC5:def 17,MESFUN12:47;
A14: dom(ProjPMap1(f,x)) = (Measurable-X-section(A,x))
by A8,A11,MESFUNC1:def 10;
ProjPMap1(f,x) is (Measurable-X-section(A,x))-measurable
by A5,MESFUN12:47;
hence ProjPMap1(f,x) is_integrable_on M2 by A11,A13,A14,MESFUNC5:100;
end;
hence for x be Element of X1 holds ProjPMap1(f,x) is_integrable_on M2;
set G1 = Integral2(M2,max+f);
set G2 = Integral2(M2,max-f);
set G = G1 - G2;
A15:dom G1 = X1 & dom G2 = X1 & dom Integral2(M2,f) = X1
& dom(Integral2(M2,|.f.|)) = X1 by FUNCT_2:def 1;
A16:now let x be object;
per cases;
suppose x in dom G1; then
reconsider x1 = x as Element of X1;
G1.x = Integral(M2,ProjPMap1(max+f,x1)) by MESFUN12:def 8; then
A17: G1.x = Integral(M2,max+ ProjPMap1(f,x1)) by MESFUN12:45;
A18: ProjPMap1(f,x1) is_integrable_on M2 by A7; then
consider B be Element of S2 such that
A19: B = dom ProjPMap1(f,x1) & ProjPMap1(f,x1) is B-measurable
by MESFUNC5:def 17;
A20: B = dom max+ ProjPMap1(f,x1) & max+ ProjPMap1(f,x1) is B-measurable
by A19,MESFUNC2:def 2,MESFUN11:10;
integral+(M2,max+ ProjPMap1(f,x1)) < +infty by A18,MESFUNC5:def 17;
hence G1.x < +infty by A17,A20,MESFUNC5:88,MESFUN11:5;
end;
suppose not x in dom G1;
hence G1.x < +infty by FUNCT_1:def 2;
end;
end;
now let x be object;
per cases;
suppose x in dom G1; then
reconsider x1 = x as Element of X1;
G1.x = Integral(M2,ProjPMap1(max+f,x1)) by MESFUN12:def 8; then
A21: G1.x = Integral(M2,max+ ProjPMap1(f,x1)) by MESFUN12:45;
ProjPMap1(f,x1) is_integrable_on M2 by A7; then
consider B be Element of S2 such that
A22: B = dom ProjPMap1(f,x1) & ProjPMap1(f,x1) is B-measurable
by MESFUNC5:def 17;
B = dom max+ ProjPMap1(f,x1) & max+ ProjPMap1(f,x1) is B-measurable
by A22,MESFUNC2:def 2,MESFUN11:10;
hence G1.x > -infty by A21,MESFUNC5:90,MESFUN11:5;
end;
suppose not x in dom G1;
hence G1.x > -infty by FUNCT_1:def 2;
end;
end; then
A23:G1 is without-infty without+infty by A16,MESFUNC5:def 5,def 6; then
A24:dom G = dom G1 /\ dom G2 by MESFUN11:23;
TT: Integral2(M2,max+f) is_integrable_on M1 &
Integral2(M2,max-f) is_integrable_on M1 by A1,A2,A3,Th20; then
A25:ex A1 be Element of S1 st
A1 = dom Integral2(M2,max+f) & Integral2(M2,max+f) is A1-measurable
by MESFUNC5:def 17;
A26:ex A2 be Element of S1 st
A2 = dom Integral2(M2,max-f) & Integral2(M2,max-f) is A2-measurable
by TT,MESFUNC5:def 17;
now let x be object;
per cases;
suppose x in dom G2; then
reconsider x1 = x as Element of X1;
G2.x = Integral(M2,ProjPMap1(max-f,x1)) by MESFUN12:def 8; then
A27: G2.x = Integral(M2,max-ProjPMap1(f,x1)) by MESFUN12:45;
ProjPMap1(f,x1) is_integrable_on M2 by A7; then
consider B be Element of S2 such that
A28: B = dom ProjPMap1(f,x1) & ProjPMap1(f,x1) is B-measurable
by MESFUNC5:def 17;
B = dom max- ProjPMap1(f,x1) & max- ProjPMap1(f,x1) is B-measurable
by A28,MESFUNC2:def 3,MESFUN11:10;
hence G2.x > -infty by A27,MESFUNC5:90,MESFUN11:5;
end;
suppose not x in dom G2;
hence G2.x > -infty by FUNCT_1:def 2;
end;
end; then
G2 is without-infty by MESFUNC5:def 5; then
A29:G is XX1-measurable by A15,A23,A24,A25,A26,MEASUR11:66;
now let x be Element of X1;
assume x in dom Integral2(M2,f);
A30: Integral2(M2,f).x = Integral(M2,ProjPMap1(f,x)) by MESFUN12:def 8;
ProjPMap1(f,x) is_integrable_on M2 by A7; then
B30: ex A be Element of S2 st
A = dom ProjPMap1(f,x) & ProjPMap1(f,x) is A-measurable
by MESFUNC5:def 17;
G.x = G1.x - G2.x by A15,A24,MESFUNC1:def 4
.= Integral(M2,ProjPMap1(max+f,x)) - Integral2(M2,max-f).x
by MESFUN12:def 8
.= Integral(M2,ProjPMap1(max+f,x)) - Integral(M2,ProjPMap1(max-f,x))
by MESFUN12:def 8
.= Integral(M2,max+ ProjPMap1(f,x)) - Integral(M2,ProjPMap1(max-f,x))
by MESFUN12:45
.= Integral(M2,max+ ProjPMap1(f,x)) - Integral(M2,max- ProjPMap1(f,x))
by MESFUN12:45;
hence G.x = Integral2(M2,f).x by A30,B30,MESFUN11:54;
end; then
A31:Integral2(M2,f) = G by A15,A24,PARTFUN1:5;
hence for U be Element of S1 holds Integral2(M2,f) is U-measurable
by A29,MESFUNC1:30;
A32:X1 = dom max+(Integral2(M2,f)) & X1 = dom max-(Integral2(M2,f))
by A15,MESFUNC2:def 2,def 3;
A33:max+(Integral2(M2,f)) is XX1-measurable
& max-(Integral2(M2,f)) is XX1-measurable by A15,A29,A31,MESFUNC2:25,26;
A34:Integral2(M2,|.f.|) is_integrable_on M1 by A1,A2,A3,Th20;
now let x be Element of X1;
assume x in dom (max+(Integral2(M2,f))); then
A35: x in dom(|.Integral2(M2,f).|) by A15,A32,MESFUNC1:def 10;
(max+(Integral2(M2,f))).x <= |.Integral2(M2,f).| .x by Th29; then
(max+(Integral2(M2,f))).x <= |. Integral2(M2,f).x .|
by A35,MESFUNC1:def 10; then
A36: |. (max+(Integral2(M2,f))).x .| <= |. Integral2(M2,f).x .|
by EXTREAL1:3,MESFUNC2:12;
Integral2(M2,f).x = Integral(M2,ProjPMap1(f,x)) by MESFUN12:def 8; then
|. Integral2(M2,f).x .| <= Integral(M2,|.ProjPMap1(f,x).|)
by A7,MESFUNC5:101; then
|. Integral2(M2,f).x .| <= Integral(M2,ProjPMap1(|.f.|,x)) by Th27; then
|. Integral2(M2,f).x .| <= Integral2(M2,|.f.|).x by MESFUN12:def 8;
hence |. max+(Integral2(M2,f)).x .| <= (Integral2(M2,|.f.|)).x
by A36,XXREAL_0:2;
end; then
A37:max+(Integral2(M2,f)) is_integrable_on M1 by A15,A32,A33,A34,MESFUNC5:102;
now let x be Element of X1;
assume x in dom(max-(Integral2(M2,f))); then
A38: x in dom(|.Integral2(M2,f).|) by A15,A32,MESFUNC1:def 10;
(max-(Integral2(M2,f))).x <= |.Integral2(M2,f).| .x by Th29; then
(max-(Integral2(M2,f))).x <= |. Integral2(M2,f).x .|
by A38,MESFUNC1:def 10; then
A39: |. (max-(Integral2(M2,f))).x .| <= |. Integral2(M2,f).x .|
by EXTREAL1:3,MESFUNC2:13;
Integral2(M2,f).x = Integral(M2,ProjPMap1(f,x)) by MESFUN12:def 8; then
|. Integral2(M2,f).x .| <= Integral(M2,|.ProjPMap1(f,x).|)
by A7,MESFUNC5:101; then
|. Integral2(M2,f).x .| <= Integral(M2,ProjPMap1(|.f.|,x)) by Th27; then
|. Integral2(M2,f).x .| <= Integral2(M2,|.f.|).x by MESFUN12:def 8;
hence |. max-(Integral2(M2,f)).x .| <= (Integral2(M2,|.f.|)).x
by A39,XXREAL_0:2;
end; then
max-(Integral2(M2,f)) is_integrable_on M1 by A15,A32,A33,A34,MESFUNC5:102;
then max+(Integral2(M2,f)) - max-(Integral2(M2,f)) is_integrable_on M1
by A37,MESFUN10:12;
hence
A40: Integral2(M2,f) is_integrable_on M1 by MESFUNC2:23;
A41:max+f is nonnegative & max-f is nonnegative by MESFUN11:5;
A42:dom(max+f) = A & dom(max-f) = A by A5,MESFUNC2:def 2,def 3;
A43:max+f is A-measurable & max-f is A-measurable by A5,MESFUNC2:25,26; then
A44:Integral(Prod_Measure(M1,M2),max-f) = Integral(M1,G2)
by A1,A2,A41,A42,MESFUN12:84;
Integral(Prod_Measure(M1,M2),f)
= Integral(Prod_Measure(M1,M2),max+f)
- Integral(Prod_Measure(M1,M2),max-f) by A5,MESFUN11:54
.= Integral(M1,G1|XX1) - Integral(M1,G2|XX1)
by A1,A2,A41,A42,A43,A44,MESFUN12:84;
hence Integral(Prod_Measure(M1,M2),f) = Integral(M1,Integral2(M2,f))
by A15,A24,A31,TT,Th21;
now let y be set;
assume y in rng Integral2(M2,f); then
consider x be Element of X1 such that
A45: x in dom Integral2(M2,f) & y = Integral2(M2,f).x by PARTFUN1:3;
Integral2(M2,f).x = Integral(M2,ProjPMap1(f,x)) by MESFUN12:def 8; then
|. Integral2(M2,f).x .| <= Integral(M2,|.ProjPMap1(f,x).|)
by A7,MESFUNC5:101; then
|. Integral2(M2,f).x .| <= Integral(M2,ProjPMap1(|.f.|,x)) by Th27; then
|. Integral2(M2,f).x .| <= Integral2(M2,|.f.|).x by MESFUN12:def 8; then
|. Integral2(M2,f).x .| < +infty by A4,XXREAL_0:2;
hence y in REAL by A45,EXTREAL1:41;
end; then
rng Integral2(M2,f) c= REAL; then
reconsider F = Integral2(M2,f) as PartFunc of X1,REAL by RELSET_1:6;
reconsider ND = {} as Element of S1 by MEASURE1:7;
A46:M1.ND = 0 by VALUED_0:def 19;
ND` = X1 \ {} by SUBSET_1:def 4 .= X1; then
A47:dom F = ND` by FUNCT_2:def 1;
R_EAL F is_integrable_on M1 by A40,MESFUNC5:def 7; then
F is_integrable_on M1 by MESFUNC6:def 4; then
F in { f where f is PartFunc of X1,REAL :
ex ND be Element of S1 st M1.ND=0 & dom f = ND`
& f is_integrable_on M1 } by A46,A47;
hence Integral2(M2,f) in L1_Functions M1 by LPSPACE1:def 8;
end;
theorem
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, f being PartFunc of [:X1,X2:],ExtREAL
st M1 is sigma_finite & M2 is sigma_finite
& f is_integrable_on Prod_Measure(M1,M2)
& (for y being Element of X2 holds Integral1(M1,|.f.|).y < +infty)
holds
(for y being Element of X2 holds ProjPMap2(f,y) is_integrable_on M1)
& (for V being Element of S2 holds Integral1(M1,f) is V-measurable)
& Integral1(M1,f) is_integrable_on M2
& Integral(Prod_Measure(M1,M2),f) = Integral(M2,Integral1(M1,f))
& Integral1(M1,f) in L1_Functions M2
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,
f be PartFunc of [:X1,X2:],ExtREAL;
assume that
A1: M1 is sigma_finite and
A2: M2 is sigma_finite and
A3: f is_integrable_on Prod_Measure(M1,M2) and
A4: for y be Element of X2 holds Integral1(M1,|.f.|).y < +infty;
reconsider XX2 = X2 as Element of S2 by MEASURE1:7;
consider A be Element of sigma measurable_rectangles(S1,S2) such that
A5: A = dom f & f is A-measurable
by A3,MESFUNC5:def 17;
A6: A = dom |.f.| by A5,MESFUNC1:def 10;
A7: now let x be Element of X2;
Y-section(A,x) = Measurable-Y-section(A,x) by MEASUR11:def 7; then
A8: dom ProjPMap2(|.f.|,x) = Measurable-Y-section(A,x) by A6,MESFUN12:def 4;
A9: |.f.| is A-measurable by A5,MESFUNC2:27; then
A10: ProjPMap2(|.f.|,x) is (Measurable-Y-section(A,x))-measurable
by A6,MESFUN12:47;
A11: ProjPMap2(|.f.|,x) = |.ProjPMap2(f,x).| by Th27; then
integral+(M1,max+ ProjPMap2(|.f.|,x))
= integral+(M1,ProjPMap2(|.f.|,x)) by MESFUN11:31
.= Integral(M1,ProjPMap2(|.f.|,x)) by A6,A8,A9,A11,MESFUNC5:88,MESFUN12:47
.= Integral1(M1,|.f.|).x by MESFUN12:def 7; then
A12: integral+(M1,max+ ProjPMap2(|.f.|,x)) < +infty by A4;
integral+(M1,max- ProjPMap2(|.f.|,x)) = 0 by A8,A10,A11,MESFUN11:53; then
A13: ProjPMap2(|.f.|,x) is_integrable_on M1
by A6,A8,A9,A12,MESFUNC5:def 17,MESFUN12:47;
A14: dom(ProjPMap2(f,x)) = (Measurable-Y-section(A,x))
by A8,A11,MESFUNC1:def 10;
ProjPMap2(f,x) is (Measurable-Y-section(A,x))-measurable
by A5,MESFUN12:47;
hence ProjPMap2(f,x) is_integrable_on M1 by A11,A13,A14,MESFUNC5:100;
end;
hence for x be Element of X2 holds ProjPMap2(f,x) is_integrable_on M1;
set G1 = Integral1(M1,max+f);
set G2 = Integral1(M1,max-f);
set G = G1 - G2;
A15:dom G1 = X2 & dom G2 = X2 & dom Integral1(M1,f) = X2
& dom(Integral1(M1,|.f.|)) = X2 by FUNCT_2:def 1;
A16:now let x be object;
per cases;
suppose x in dom G1; then
reconsider x1 = x as Element of X2;
G1.x = Integral(M1,ProjPMap2(max+f,x1)) by MESFUN12:def 7; then
A17: G1.x = Integral(M1,max+ ProjPMap2(f,x1)) by MESFUN12:46;
A18: ProjPMap2(f,x1) is_integrable_on M1 by A7; then
consider B be Element of S1 such that
A19: B = dom ProjPMap2(f,x1) & ProjPMap2(f,x1) is B-measurable
by MESFUNC5:def 17;
A20: B = dom max+ ProjPMap2(f,x1) & max+ ProjPMap2(f,x1) is B-measurable
by A19,MESFUNC2:def 2,MESFUN11:10;
integral+(M1,max+ ProjPMap2(f,x1)) < +infty by A18,MESFUNC5:def 17;
hence G1.x < +infty by A17,A20,MESFUNC5:88,MESFUN11:5;
end;
suppose not x in dom G1;
hence G1.x < +infty by FUNCT_1:def 2;
end;
end;
now let x be object;
per cases;
suppose x in dom G1; then
reconsider x1 = x as Element of X2;
G1.x = Integral(M1,ProjPMap2(max+f,x1)) by MESFUN12:def 7; then
A21: G1.x = Integral(M1,max+ ProjPMap2(f,x1)) by MESFUN12:46;
ProjPMap2(f,x1) is_integrable_on M1 by A7; then
consider B be Element of S1 such that
A22: B = dom ProjPMap2(f,x1) & ProjPMap2(f,x1) is B-measurable
by MESFUNC5:def 17;
B = dom max+ ProjPMap2(f,x1) & max+ ProjPMap2(f,x1) is B-measurable
by A22,MESFUNC2:def 2,MESFUN11:10;
hence G1.x > -infty by A21,MESFUNC5:90,MESFUN11:5;
end;
suppose not x in dom G1;
hence G1.x > -infty by FUNCT_1:def 2;
end;
end; then
A23:G1 is without-infty without+infty by A16,MESFUNC5:def 5,def 6; then
A24:dom G = dom G1 /\ dom G2 by MESFUN11:23;
TT: Integral1(M1,max+f) is_integrable_on M2 &
Integral1(M1,max-f) is_integrable_on M2 by A1,A2,A3,Th20; then
A25:ex A1 be Element of S2 st
A1 = dom Integral1(M1,max+f) & Integral1(M1,max+f) is A1-measurable
by MESFUNC5:def 17;
A26:ex A2 be Element of S2 st
A2 = dom Integral1(M1,max-f) & Integral1(M1,max-f) is A2-measurable
by TT,MESFUNC5:def 17;
now let x be object;
per cases;
suppose x in dom G2; then
reconsider x1 = x as Element of X2;
G2.x = Integral(M1,ProjPMap2(max-f,x1)) by MESFUN12:def 7; then
A27: G2.x = Integral(M1,max-ProjPMap2(f,x1)) by MESFUN12:46;
ProjPMap2(f,x1) is_integrable_on M1 by A7; then
consider B be Element of S1 such that
A28: B = dom ProjPMap2(f,x1) & ProjPMap2(f,x1) is B-measurable
by MESFUNC5:def 17;
B = dom max- ProjPMap2(f,x1) & max- ProjPMap2(f,x1) is B-measurable
by A28,MESFUNC2:def 3,MESFUN11:10;
hence G2.x > -infty by A27,MESFUNC5:90,MESFUN11:5;
end;
suppose not x in dom G2;
hence G2.x > -infty by FUNCT_1:def 2;
end;
end; then
G2 is without-infty by MESFUNC5:def 5; then
A29:G is XX2-measurable by A15,A23,A24,A25,A26,MEASUR11:66;
now let x be Element of X2;
assume x in dom Integral1(M1,f);
A30: Integral1(M1,f).x = Integral(M1,ProjPMap2(f,x)) by MESFUN12:def 7;
ProjPMap2(f,x) is_integrable_on M1 by A7; then
B30: ex A be Element of S1 st
A = dom ProjPMap2(f,x) & ProjPMap2(f,x) is A-measurable
by MESFUNC5:def 17;
G.x = G1.x - G2.x by A15,A24,MESFUNC1:def 4
.= Integral(M1,ProjPMap2(max+f,x)) - Integral1(M1,max-f).x
by MESFUN12:def 7
.= Integral(M1,ProjPMap2(max+f,x)) - Integral(M1,ProjPMap2(max-f,x))
by MESFUN12:def 7
.= Integral(M1,max+ ProjPMap2(f,x)) - Integral(M1,ProjPMap2(max-f,x))
by MESFUN12:46
.= Integral(M1,max+ ProjPMap2(f,x)) - Integral(M1,max- ProjPMap2(f,x))
by MESFUN12:46;
hence G.x = Integral1(M1,f).x by A30,B30,MESFUN11:54;
end; then
A31:Integral1(M1,f) = G by A15,A24,PARTFUN1:5;
hence for V be Element of S2 holds Integral1(M1,f) is V-measurable
by A29,MESFUNC1:30;
A32:X2 = dom max+(Integral1(M1,f)) & X2 = dom max-(Integral1(M1,f))
by A15,MESFUNC2:def 2,def 3;
A33:max+(Integral1(M1,f)) is XX2-measurable
& max-(Integral1(M1,f)) is XX2-measurable by A15,A29,A31,MESFUNC2:25,26;
A34:Integral1(M1,|.f.|) is_integrable_on M2 by A1,A2,A3,Th20;
now let x be Element of X2;
assume x in dom (max+(Integral1(M1,f))); then
A35: x in dom(|.Integral1(M1,f).|) by A15,A32,MESFUNC1:def 10;
(max+(Integral1(M1,f))).x <= |.Integral1(M1,f).| .x by Th29; then
(max+(Integral1(M1,f))).x <= |. Integral1(M1,f).x .|
by A35,MESFUNC1:def 10; then
A36: |. (max+(Integral1(M1,f))).x .| <= |. Integral1(M1,f).x .|
by EXTREAL1:3,MESFUNC2:12;
Integral1(M1,f).x = Integral(M1,ProjPMap2(f,x)) by MESFUN12:def 7; then
|. Integral1(M1,f).x .| <= Integral(M1,|.ProjPMap2(f,x).|)
by A7,MESFUNC5:101; then
|. Integral1(M1,f).x .| <= Integral(M1,ProjPMap2(|.f.|,x)) by Th27; then
|. Integral1(M1,f).x .| <= Integral1(M1,|.f.|).x by MESFUN12:def 7;
hence |. max+(Integral1(M1,f)).x .| <= (Integral1(M1,|.f.|)).x
by A36,XXREAL_0:2;
end; then
A37:max+(Integral1(M1,f)) is_integrable_on M2 by A15,A32,A33,A34,MESFUNC5:102;
now let x be Element of X2;
assume x in dom(max-(Integral1(M1,f))); then
A38: x in dom(|.Integral1(M1,f).|) by A15,A32,MESFUNC1:def 10;
(max-(Integral1(M1,f))).x <= |.Integral1(M1,f).| .x by Th29; then
(max-(Integral1(M1,f))).x <= |. Integral1(M1,f).x .|
by A38,MESFUNC1:def 10; then
A39: |. (max-(Integral1(M1,f))).x .| <= |. Integral1(M1,f).x .|
by EXTREAL1:3,MESFUNC2:13;
Integral1(M1,f).x = Integral(M1,ProjPMap2(f,x)) by MESFUN12:def 7; then
|. Integral1(M1,f).x .| <= Integral(M1,|.ProjPMap2(f,x).|)
by A7,MESFUNC5:101; then
|. Integral1(M1,f).x .| <= Integral(M1,ProjPMap2(|.f.|,x)) by Th27; then
|. Integral1(M1,f).x .| <= Integral1(M1,|.f.|).x by MESFUN12:def 7;
hence |. max-(Integral1(M1,f)).x .| <= (Integral1(M1,|.f.|)).x
by A39,XXREAL_0:2;
end; then
max-(Integral1(M1,f)) is_integrable_on M2
by A15,A32,A33,A34,MESFUNC5:102; then
max+(Integral1(M1,f)) - max-(Integral1(M1,f)) is_integrable_on M2
by A37,MESFUN10:12;
hence
A40: Integral1(M1,f) is_integrable_on M2 by MESFUNC2:23;
A41:max+f is nonnegative & max-f is nonnegative by MESFUN11:5;
A42:dom(max+f) = A & dom(max-f) = A by A5,MESFUNC2:def 2,def 3;
A43:max+f is A-measurable & max-f is A-measurable by A5,MESFUNC2:25,26; then
A44:Integral(Prod_Measure(M1,M2),max-f) = Integral(M2,G2)
by A1,A2,A41,A42,MESFUN12:84;
Integral(Prod_Measure(M1,M2),f)
= Integral(Prod_Measure(M1,M2),max+f)
- Integral(Prod_Measure(M1,M2),max-f) by A5,MESFUN11:54
.= Integral(M2,G1|XX2) - Integral(M2,G2|XX2)
by A1,A2,A41,A42,A43,A44,MESFUN12:84;
hence Integral(Prod_Measure(M1,M2),f) = Integral(M2,Integral1(M1,f))
by A15,A24,A31,TT,Th21;
now let y be set;
assume y in rng Integral1(M1,f); then
consider x be Element of X2 such that
A45: x in dom Integral1(M1,f) & y = Integral1(M1,f).x by PARTFUN1:3;
Integral1(M1,f).x = Integral(M1,ProjPMap2(f,x)) by MESFUN12:def 7; then
|. Integral1(M1,f).x .| <= Integral(M1,|.ProjPMap2(f,x).|)
by A7,MESFUNC5:101; then
|. Integral1(M1,f).x .| <= Integral(M1,ProjPMap2(|.f.|,x)) by Th27; then
|. Integral1(M1,f).x .| <= Integral1(M1,|.f.|).x by MESFUN12:def 7; then
|. Integral1(M1,f).x .| < +infty by A4,XXREAL_0:2;
hence y in REAL by A45,EXTREAL1:41;
end; then
rng Integral1(M1,f) c= REAL; then
reconsider F = Integral1(M1,f) as PartFunc of X2,REAL by RELSET_1:6;
reconsider ND = {} as Element of S2 by MEASURE1:7;
A46:M2.ND = 0 by VALUED_0:def 19;
ND` = X2 \ {} by SUBSET_1:def 4 .= X2; then
A47:dom F = ND` by FUNCT_2:def 1;
R_EAL F is_integrable_on M2 by A40,MESFUNC5:def 7; then
F is_integrable_on M2 by MESFUNC6:def 4; then
F in { f where f is PartFunc of X2,REAL :
ex ND be Element of S2 st M2.ND=0 & dom f = ND`
& f is_integrable_on M2 } by A46,A47;
hence Integral1(M1,f) in L1_Functions M2 by LPSPACE1:def 8;
end;