:: Fubini's Theorem
:: by Noboru Endou
::
:: Received March 11, 2019
:: Copyright (c) 2019 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;
begin :: Preliminaries
reserve X for set;
theorem :: MESFUN13:1
for A being Subset of X, f being X-defined Relation holds
f|A` = f|(dom f \ A);
theorem :: MESFUN13:2
for f being PartFunc of X,ExtREAL holds
great_eq_dom(f,+infty) = eq_dom(f,+infty);
theorem :: MESFUN13:3
for f being PartFunc of X,ExtREAL holds
less_eq_dom(f,-infty) = eq_dom(f,-infty);
theorem :: MESFUN13:4
for f being PartFunc of X,ExtREAL, er being ExtReal
holds great_eq_dom(f,er) misses less_dom(f,er);
theorem :: MESFUN13:5
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);
reserve X,X1,X2 for non empty set;
theorem :: MESFUN13:6
for f being PartFunc of X,ExtREAL, x being Element of X
holds (max+f).x <= (|.f.|).x & (max-f).x <= (|.f.|).x;
theorem :: MESFUN13:7
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).|;
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;
end;
theorem :: MESFUN13:8
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;
theorem :: MESFUN13:9
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.|);
theorem :: MESFUN13:10
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;
theorem :: MESFUN13:11
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;
theorem :: MESFUN13:12
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;
theorem :: MESFUN13:13
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;
theorem :: MESFUN13:14
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;
theorem :: MESFUN13:15
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;
::$N Markov's inequality
theorem :: MESFUN13:16 :: 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);
begin :: Fubini's Theorem
theorem :: MESFUN13:17
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));
theorem :: MESFUN13:18
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;
theorem :: MESFUN13:19
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;
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
:: MESFUN13:def 1
ex A be Element of S st M.A = 0 & A c= dom f & f|A` is_integrable_on M;
end;
theorem :: MESFUN13:20
for f being PartFunc of X,ExtREAL
st f is_a.e.integrable_on M holds dom f in S;
theorem :: MESFUN13:21
for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
f is_a.e.integrable_on M;
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
:: MESFUN13:def 2
ex A be Element of S st M.A = 0 & A c= dom f & f|A` is PartFunc of X,REAL;
end;
theorem :: MESFUN13:22
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;
theorem :: MESFUN13:23
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;
theorem :: MESFUN13:24
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;
theorem :: MESFUN13:25
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;
theorem :: MESFUN13:26
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);
theorem :: MESFUN13:27
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));
theorem :: MESFUN13:28
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 );
theorem :: MESFUN13:29
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 );
::$N Fubini`s theorem
theorem :: MESFUN13:30
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));
theorem :: MESFUN13:31
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));
theorem :: MESFUN13:32
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;
theorem :: MESFUN13:33
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;