:: 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 b_{1} -defined Relation holds f | (A `) = f | ((dom f) \ A)

for A being Subset of X

for f being b

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)

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))

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 )

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)).| )

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;

ex b_{1} being PartFunc of X,ExtREAL st b_{1} is E -measurable

end;
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 b

proof 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 b_{3} -measurable PartFunc of X,ExtREAL st dom f = E holds

( eq_dom (f,+infty) in S & eq_dom (f,-infty) in S )

for S being SigmaField of X

for E being Element of S

for f being b

( 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 b_{7} -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.|) )

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 b

( 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 b

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 b_{7} -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;

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 b

( 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 b_{7} -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;

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 b

( 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 b_{6} -measurable PartFunc of [:X1,X2:],ExtREAL st M2 is sigma_finite & E = dom f holds

Integral2 (M2,|.f.|) is U -measurable

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 b

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 b_{6} -measurable PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & E = dom f holds

Integral1 (M1,|.f.|) is V -measurable

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 b

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 )

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 )

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;

:: 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 b_{4} -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)

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f being b

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))))) )

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 ) )

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

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;

end;
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 );

ex A being Element of S st

( M . A = 0 & A c= dom f & f | (A `) is_integrable_on M );

:: 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 ) );

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

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

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;

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

let f be PartFunc of X,ExtREAL;

:: 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 ) );

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 b_{4} -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 )

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f being b

( 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 ) )

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 )

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 b_{4} -measurable PartFunc of X,ExtREAL st dom f c= E & f is_a.e.integrable_on M holds

f is_integrable_on M

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f being b

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) )

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))))) )

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 ) )

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 ) )

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;

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) ) )

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) ) )

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 )

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 )

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;