:: Fubini's Theorem
:: by Noboru Endou
::
:: Received March 11, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users


theorem Th15: :: MESFUN13:1
for X being set
for A being Subset of X
for f being b1 -defined Relation holds f | (A `) = f | ((dom f) \ A)
proof end;

theorem Th10: :: MESFUN13:2
for X being set
for f being PartFunc of X,ExtREAL holds great_eq_dom (f,+infty) = eq_dom (f,+infty)
proof end;

theorem :: MESFUN13:3
for X being set
for f being PartFunc of X,ExtREAL holds less_eq_dom (f,-infty) = eq_dom (f,-infty)
proof end;

theorem :: MESFUN13:4
for X being set
for f being PartFunc of X,ExtREAL
for er being ExtReal holds great_eq_dom (f,er) misses less_dom (f,er)
proof end;

theorem :: MESFUN13:5
for X being set
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 end;

theorem Th29: :: MESFUN13:6
for X being non empty set
for f being PartFunc of X,ExtREAL
for x being Element of X holds
( (max+ f) . x <= |.f.| . x & (max- f) . x <= |.f.| . x )
proof end;

theorem Th27: :: MESFUN13:7
for X1, X2 being non empty set
for f being PartFunc of [:X1,X2:],ExtREAL
for x being Element of X1
for y being Element of X2 holds
( ProjPMap1 (|.f.|,x) = |.(ProjPMap1 (f,x)).| & ProjPMap2 (|.f.|,y) = |.(ProjPMap2 (f,y)).| )
proof end;

registration
let X be non empty set ;
let S be SigmaField of X;
let E be Element of S;
cluster Relation-like X -defined ExtREAL -valued Function-like V69() E -measurable for Element of bool [:X,ExtREAL:];
existence
ex b1 being PartFunc of X,ExtREAL st b1 is E -measurable
proof end;
end;

theorem Th9: :: MESFUN13:8
for X being non empty set
for S being SigmaField of X
for E being Element of S
for f being b3 -measurable PartFunc of X,ExtREAL st dom f = E holds
( eq_dom (f,+infty) in S & eq_dom (f,-infty) in S )
proof end;

theorem Th1: :: MESFUN13:9
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for f being b7 -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 end;

Lm1: for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
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 end;

Lm2: for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for f being b7 -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 end;

theorem :: MESFUN13:10
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for f being b7 -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 :: MESFUN13:11
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for f being b7 -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: :: MESFUN13:12
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for U being Element of S1
for f being b6 -measurable PartFunc of [:X1,X2:],ExtREAL st M2 is sigma_finite & E = dom f holds
Integral2 (M2,|.f.|) is U -measurable
proof end;

theorem Th5: :: MESFUN13:13
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for E being Element of sigma (measurable_rectangles (S1,S2))
for V being Element of S2
for f being b6 -measurable PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & E = dom f holds
Integral1 (M1,|.f.|) is V -measurable
proof end;

theorem :: MESFUN13:14
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
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 end;

theorem :: MESFUN13:15
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
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 end;

:: WP: Markov's inequality
theorem Th14: :: MESFUN13:16
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being b4 -measurable PartFunc of X,ExtREAL
for er being ExtReal st dom f = E & f is nonnegative & er >= 0 holds
er * (M . (great_eq_dom (f,er))) <= Integral (M,f)
proof end;

theorem Th21: :: MESFUN13:17
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
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 end;

theorem :: MESFUN13:18
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
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 end;

theorem :: MESFUN13:19
for X being non empty set
for S being SigmaField of X
for A, B being Element of S
for f being PartFunc of X,ExtREAL st B c= A & f | A is B -measurable holds
f is B -measurable
proof end;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,ExtREAL;
pred f is_a.e.integrable_on M means :: MESFUN13:def 1
 ex A being Element of S st
( M . A = 0 & A c= dom f & f | (A `) is_integrable_on M );
end;

:: deftheorem defines is_a.e.integrable_on MESFUN13:def 1 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL holds
( f is_a.e.integrable_on M iff ex A being Element of S st
( M . A = 0 & A c= dom f & f | (A `) is_integrable_on M ) );

theorem Th16: :: MESFUN13:20
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_a.e.integrable_on M holds
dom f in S
proof end;

theorem :: MESFUN13:21
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
f is_a.e.integrable_on M
proof end;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,ExtREAL;
pred f is_a.e.finite M means :: MESFUN13:def 2
 ex A being Element of S st
( M . A = 0 & A c= dom f & f | (A `) is PartFunc of X,REAL );
end;

:: deftheorem defines is_a.e.finite MESFUN13:def 2 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL holds
( f is_a.e.finite M iff ex A being Element of S st
( M . A = 0 & A c= dom f & f | (A `) is PartFunc of X,REAL ) );

theorem :: MESFUN13:22
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being b4 -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 end;

theorem Th19: :: MESFUN13:23
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
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 end;

theorem Th20: :: MESFUN13:24
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
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 end;

theorem :: MESFUN13:25
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being b4 -measurable PartFunc of X,ExtREAL st dom f c= E & f is_a.e.integrable_on M holds
f is_integrable_on M
proof end;

theorem Th23: :: MESFUN13:26
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for A being Element of S
for f being PartFunc of X,ExtREAL st M . A = 0 & A c= dom f & f | (A `) is_integrable_on M holds
ex g being 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 end;

theorem :: MESFUN13:27
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
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 end;

theorem :: MESFUN13:28
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for E being Element of sigma (measurable_rectangles (S1,S2))
for y being 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 end;

theorem :: MESFUN13:29
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for x being 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 end;

:: WP: Fubini`s theorem
theorem :: MESFUN13:30
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for 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 being 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 being 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 end;

theorem :: MESFUN13:31
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for 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 being 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 being 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 end;

theorem :: MESFUN13:32
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
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) & ( 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 end;

theorem :: MESFUN13:33
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
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) & ( 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 end;