MEASUR14: Universality of Measure Space

:: Universality of Measure Space
:: by Noboru Endou and Yasunari Shidama
::
:: Received December 9, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users

theorem Th1: :: MEASUR14:1

for X, Y being non empty set
for f being Function of X,Y st f is bijective holds
( .: f is bijective & ( for s being Subset of X holds (.: f) . s = f .: s ) )

proof end;

theorem Th2: :: MEASUR14:2

for X, Y being non empty set
for f being Function of X,Y
for S being Field_Subset of X st f is bijective holds
(.: f) .: S is Field_Subset of Y

proof end;

definition

let X, Y be non empty set ;
let f be Function of X,Y;
let S be Field_Subset of X;
assume A1: f is bijective ;

func CopyField (f,S) -> Field_Subset of Y equals :Def1: :: MEASUR14:def 1
(.: f) .: S;

correctness by Th2, A1;

end;

:: deftheorem Def1 defines CopyField MEASUR14:def 1 :

theorem Th3: :: MEASUR14:3

for X, Y being non empty set
for f being Function of X,Y
for S being SigmaField of X st f is bijective holds
(.: f) .: S is SigmaField of Y

proof end;

definition

let X, Y be non empty set ;
let f be Function of X,Y;
let S be SigmaField of X;
assume A1: f is bijective ;

func CopyField (f,S) -> SigmaField of Y equals :Def2: :: MEASUR14:def 2
(.: f) .: S;

correctness by Th3, A1;

end;

:: deftheorem Def2 defines CopyField MEASUR14:def 2 :

theorem Th4: :: MEASUR14:4

for X, Y being non empty set
for f being Function of X,Y
for S being Field_Subset of X
for M being Measure of S st f is bijective holds
( ex G being Function of S,(CopyField (f,S)) st
( G = (.: f) | S & dom G = S & rng G = CopyField (f,S) & G is bijective ) & ex F being Function of (CopyField (f,S)),S st
( F = ((.: f) | S) " & rng F = S & dom F = CopyField (f,S) & F is bijective ) )

proof end;

theorem Th5: :: MEASUR14:5

for X, Y being non empty set
for f being Function of X,Y
for S being Field_Subset of X
for M being Measure of S st f is bijective holds
ex M1 being Measure of (CopyField (f,S)) st
( M1 = M * (((.: f) | S) ") & ( for s being Element of CopyField (f,S) ex t being Element of S st
( s = f .: t & M1 . s = M . t ) ) )

proof end;

definition

let X, Y be non empty set ;
let f be Function of X,Y;
let S be Field_Subset of X;
let M be Measure of S;
assume A1: f is bijective ;

func CopyMeasure (f,M) -> Measure of (CopyField (f,S)) means :: MEASUR14:def 3
( it = M * (((.: f) | S) ") & ( for s being Element of CopyField (f,S) ex t being Element of S st
( s = f .: t & it . s = M . t ) ) );

existence by A1, Th5;
uniqueness ;

end;

:: deftheorem defines CopyMeasure MEASUR14:def 3 :

theorem Th6: :: MEASUR14:6

for X, Y being non empty set
for f being Function of X,Y
for S being SigmaField of X
for M being sigma_Measure of S st f is bijective holds
ex M1 being sigma_Measure of (CopyField (f,S)) st
( M1 = M * (((.: f) | S) ") & ( for s being Element of CopyField (f,S) ex t being Element of S st
( s = f .: t & M1 . s = M . t ) ) )

proof end;

definition

let X, Y be non empty set ;
let f be Function of X,Y;
let S be SigmaField of X;
let M be sigma_Measure of S;
assume A1: f is bijective ;

func CopyMeasure (f,M) -> sigma_Measure of (CopyField (f,S)) means :Def4: :: MEASUR14:def 4
( it = M * (((.: f) | S) ") & ( for s being Element of CopyField (f,S) ex t being Element of S st
( s = f .: t & it . s = M . t ) ) );

existence by A1, Th6;
uniqueness ;

end;

:: deftheorem Def4 defines CopyMeasure MEASUR14:def 4 :

definition

let m be non zero Nat;
let X be non-empty m -element FinSequence;

func Pt2FinSeq X -> m -element FinSequence means :Def5: :: MEASUR14:def 5
( ex id1 being Function of (CarProduct (SubFin (X,1))),(product (SubFin (X,1))) st
( it . 1 = id1 & id1 is bijective & ( for x being object st x in CarProduct (SubFin (X,1)) holds
id1 . x = <*x*> ) ) & ( for i being non zero Nat st i < m holds
ex Fi being Function of (CarProduct (SubFin (X,i))),(product (SubFin (X,i))) ex IK being Function of [:(CarProduct (SubFin (X,i))),(ElmFin (X,(i + 1))):],(product (SubFin (X,(i + 1)))) st
( Fi = it . i & IK = it . (i + 1) & Fi is bijective & IK is bijective & ( for x, y being object st x in CarProduct (SubFin (X,i)) & y in ElmFin (X,(i + 1)) holds
ex s being FinSequence st
( Fi . x = s & IK . (x,y) = s ^ <*y*> ) ) ) ) );

proof end;

proof end;

end;

:: deftheorem Def5 defines Pt2FinSeq MEASUR14:def 5 :

theorem Th7: :: MEASUR14:7

for m, n being non zero Nat
for X being non-empty b₁ -element FinSequence st n <= m holds
(Pt2FinSeq X) . n is Function of (CarProduct (SubFin (X,n))),(product (SubFin (X,n)))

proof end;

theorem Th8: :: MEASUR14:8

for m, n1, n2, k being non zero Nat
for X being non-empty b₁ -element FinSequence st k <= n1 & n1 <= n2 & n2 <= m holds
( SubFin ((SubFin (X,n1)),k) = SubFin ((SubFin (X,n2)),k) & ElmFin ((SubFin (X,n1)),k) = ElmFin ((SubFin (X,n2)),k) )

proof end;

theorem Th9: :: MEASUR14:9

for m, n1, n2, k being non zero Nat
for X being non-empty b₁ -element FinSequence st k <= n1 & n1 <= n2 & n2 <= m holds
(Pt2FinSeq (SubFin (X,n1))) . k = (Pt2FinSeq (SubFin (X,n2))) . k

proof end;

theorem Th10: :: MEASUR14:10

for m, n, k being non zero Nat
for X being non-empty b₁ -element FinSequence st k <= n & n <= m holds
(Pt2FinSeq X) . k = (Pt2FinSeq (SubFin (X,n))) . k

proof end;

theorem Th11: :: MEASUR14:11

for m, n being non zero Nat
for X being non-empty b₁ -element FinSequence
for P being Function of (CarProduct (SubFin (X,n))),(product (SubFin (X,n))) st n <= m & P = (Pt2FinSeq X) . n holds
P is bijective

proof end;

definition

let m be non zero Nat;
let X be non-empty m -element FinSequence;

func CarProd X -> Function of (CarProduct X),(product X) equals :: MEASUR14:def 6
(Pt2FinSeq X) . m;

proof end;

end;

:: deftheorem defines CarProd MEASUR14:def 6 :

theorem Th12: :: MEASUR14:12

for m being non zero Nat
for X being non-empty b₁ -element FinSequence holds CarProd X is bijective

proof end;

theorem Th13: :: MEASUR14:13

for n being non zero Nat
for X being non-empty b₁ + 1 -element FinSequence
for x, y being object st x in CarProduct (SubFin (X,n)) & y in ElmFin (X,(n + 1)) holds
ex s, t being FinSequence st
( (CarProd (SubFin (X,n))) . x = s & <*y*> = t & (CarProd X) . (x,y) = s ^ t )

proof end;

definition

let n be non zero Nat;
let X be non-empty n -element FinSequence;
let S be sigmaFieldFamily of X;

func XProd_Field S -> SigmaField of (product X) equals :: MEASUR14:def 7
CopyField ((CarProd X),(Prod_Field S));

end;

:: deftheorem defines XProd_Field MEASUR14:def 7 :

definition

let n be non zero Nat;
let X be non-empty n -element FinSequence;
let S be sigmaFieldFamily of X;
let m be sigmaMeasureFamily of S;

func XProd_Measure m -> sigma_Measure of (XProd_Field S) equals :: MEASUR14:def 8
CopyMeasure ((CarProd X),(Prod_Measure m));

end;

:: deftheorem defines XProd_Measure MEASUR14:def 8 :

theorem Th14: :: MEASUR14:14

for X, Y being non empty set
for f being Function of X,Y st f is bijective holds
ex g being Function of Y,X st
( g is bijective & g = f " & .: g = (.: f) " )

proof end;

theorem Th15: :: MEASUR14:15

for X, Y being non empty set
for T being Function of X,Y
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") holds
( dom g = T .: (dom f) & dom g = (.: T) . (dom f) )

proof end;

theorem Th16: :: MEASUR14:16

for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL
for A being Element of S
for B being Element of CopyField (T,S) st T is bijective & g = f * (T ") holds
for r being Real holds T .: (less_dom (f,r)) = less_dom (g,r)

proof end;

theorem Th17: :: MEASUR14:17

for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y st T is bijective holds
ex H being Function of Y,X st
( H is bijective & H = T " & H " = T & .: H = (.: T) " & (.: H) .: (CopyField (T,S)) = S & CopyField (H,(CopyField (T,S))) = S )

proof end;

theorem Th18: :: MEASUR14:18

for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y
for A being Subset of X st T is bijective holds
( A in S iff T .: A in CopyField (T,S) )

proof end;

theorem Th19: :: MEASUR14:19

for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y
for B being Subset of Y st T is bijective holds
( T " B in S iff B in CopyField (T,S) )

proof end;

theorem Th20: :: MEASUR14:20

for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL
for A being Element of S
for B being Element of CopyField (T,S) st T is bijective & B = T .: A & g = f * (T ") holds
( f is A -measurable iff g is B -measurable )

proof end;

theorem Th21: :: MEASUR14:21

for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y
for F being Finite_Sep_Sequence of S st T is bijective holds
((.: T) | S) * F is Finite_Sep_Sequence of CopyField (T,S)

proof end;

Lm1: for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") & f is_simple_func_in S holds
g is_simple_func_in CopyField (T,S)

proof end;

theorem Th22: :: MEASUR14:22

for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") holds
( f is_simple_func_in S iff g is_simple_func_in CopyField (T,S) )

proof end;

theorem Th23: :: MEASUR14:23

for X, Y being non empty set
for T being Function of X,Y
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") holds
( f is nonnegative iff g is nonnegative )

proof end;

theorem Th24: :: MEASUR14:24

for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y
for F being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") & F,a are_Re-presentation_of f holds
ex G being Finite_Sep_Sequence of CopyField (T,S) st
( G = ((.: T) | S) * F & G,a are_Re-presentation_of g )

proof end;

theorem Th25: :: MEASUR14:25

for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") & f is_simple_func_in S & f is nonnegative holds
integral ((CopyMeasure (T,M)),g) = integral (M,f)

proof end;

theorem Th26: :: MEASUR14:26

for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") & f is_simple_func_in S & f is nonnegative holds
integral' ((CopyMeasure (T,M)),g) = integral' (M,f)

proof end;

theorem Th27: :: MEASUR14:27

for X, Y being non empty set
for T being Function of X,Y
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") holds
( max+ g = (max+ f) * (T ") & max- g = (max- f) * (T ") )

proof end;

theorem Th28: :: MEASUR14:28

for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL
for A being Element of S st T is bijective & g = f * (T ") & A = dom f & f is A -measurable holds
ex B being Element of CopyField (T,S) st
( B = T .: A & B = dom g & g is B -measurable )

proof end;

theorem Th29: :: MEASUR14:29

for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A being Element of S
for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") & f is nonnegative & A = dom f & f is A -measurable holds
integral+ ((CopyMeasure (T,M)),g) = integral+ (M,f)

proof end;

theorem :: MEASUR14:30

for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL
for B being Element of CopyField (T,S) st T is bijective & g = f * (T ") & B = dom g & g is B -measurable holds
ex A being Element of S st
( B = T .: A & A = dom f & f is A -measurable )

proof end;

theorem Th31: :: MEASUR14:31

for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL
for A being Element of S st T is bijective & g = f * (T ") & A = dom f & f is A -measurable holds
( integral+ (M,(max+ f)) = integral+ ((CopyMeasure (T,M)),(max+ g)) & integral+ (M,(max- f)) = integral+ ((CopyMeasure (T,M)),(max- g)) )

proof end;

theorem Th32: :: MEASUR14:32

for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL
for A being Element of S st T is bijective & g = f * (T ") & A = dom f & f is A -measurable holds
Integral ((CopyMeasure (T,M)),g) = Integral (M,f)

proof end;

theorem Th33: :: MEASUR14:33

for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") holds
( f is_integrable_on M iff g is_integrable_on CopyMeasure (T,M) )

proof end;

theorem Th34: :: MEASUR14:34

for n being non zero Nat
for X being non-empty b₁ -element FinSequence
for S being sigmaFieldFamily of X
for m being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL
for g being PartFunc of (product X),ExtREAL
for A being Element of Prod_Field S
for B being Element of XProd_Field S st B = (CarProd X) .: A & g = f * ((CarProd X) ") holds
( f is A -measurable iff g is B -measurable )

proof end;

theorem :: MEASUR14:35

for n being non zero Nat
for X being non-empty b₁ -element FinSequence
for S being sigmaFieldFamily of X
for m being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL
for g being PartFunc of (product X),ExtREAL
for A being Element of Prod_Field S st g = f * ((CarProd X) ") & A = dom f & f is A -measurable holds
Integral ((XProd_Measure m),g) = Integral ((Prod_Measure m),f) by Th12, Th32;

theorem Th36: :: MEASUR14:36

for n being non zero Nat
for X being non-empty b₁ -element FinSequence
for S being sigmaFieldFamily of X
for m being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL
for g being PartFunc of (product X),ExtREAL st g = f * ((CarProd X) ") holds
( f is_integrable_on Prod_Measure m iff g is_integrable_on XProd_Measure m )

proof end;

Lm2: for n being non zero Nat holds (Seg n) --> REAL is non-empty b₁ -element FinSequence

proof end;

registration

let n be non zero Nat;

cluster (Seg n) --> REAL -> non-empty n -element for FinSequence;

correctness by Lm2;

end;

Lm3: for n being non zero Nat holds (Seg n) --> L-Field is sigmaFieldFamily of (Seg n) --> REAL

proof end;

definition

let n be non zero Nat;

func L-Field n -> sigmaFieldFamily of (Seg n) --> REAL equals :: MEASUR14:def 9
(Seg n) --> L-Field;

correctness by Lm3;

end;

:: deftheorem defines L-Field MEASUR14:def 9 :

Lm4: for n being non zero Nat holds (Seg n) --> L-Meas is sigmaMeasureFamily of L-Field n

proof end;

definition

let n be non zero Nat;

func L-Meas n -> sigmaMeasureFamily of L-Field n equals :: MEASUR14:def 10
(Seg n) --> L-Meas;

correctness by Lm4;

end;

:: deftheorem defines L-Meas MEASUR14:def 10 :

Lm5: for n being non zero Nat holds
( Prod_Field (L-Field n) is SigmaField of (CarProduct ((Seg n) --> REAL)) & Prod_Measure (L-Meas n) is sigma_Measure of (Prod_Field (L-Field n)) & XProd_Field (L-Field n) is SigmaField of (product ((Seg n) --> REAL)) & XProd_Field (L-Field n) is SigmaField of (REAL n) & XProd_Measure (L-Meas n) is sigma_Measure of (XProd_Field (L-Field n)) )

proof end;

definition

let n be non zero Nat;

func XL-Field n -> SigmaField of (REAL n) equals :: MEASUR14:def 11
XProd_Field (L-Field n);

correctness by Lm5;

end;

:: deftheorem defines XL-Field MEASUR14:def 11 :

definition

let n be non zero Nat;

func XL-Meas n -> sigma_Measure of (XL-Field n) equals :: MEASUR14:def 12
XProd_Measure (L-Meas n);

proof end;

end;

:: deftheorem defines XL-Meas MEASUR14:def 12 :

theorem Th37: :: MEASUR14:37

( CarProduct ((Seg 1) --> REAL) = REAL & ElmFin (((Seg 1) --> REAL),1) = REAL & CarProduct ((Seg 2) --> REAL) = [:REAL,REAL:] & ElmFin (((Seg 2) --> REAL),2) = REAL & CarProduct ((Seg 3) --> REAL) = [:REAL,REAL,REAL:] )

proof end;

theorem Th38: :: MEASUR14:38

( CarProd ((Seg 1) --> REAL) is Function of REAL,(REAL 1) & ( for s being object st s in REAL holds
(CarProd ((Seg 1) --> REAL)) . s = <*s*> ) )

proof end;

theorem Th39: :: MEASUR14:39

( CarProd ((Seg 2) --> REAL) is Function of [:REAL,REAL:],(REAL 2) & ( for s, t being object st s in REAL & t in REAL holds
(CarProd ((Seg 2) --> REAL)) . [s,t] = <*s,t*> ) )

proof end;

theorem :: MEASUR14:40

( CarProd ((Seg 3) --> REAL) is Function of [:REAL,REAL,REAL:],(REAL 3) & ( for s, t, u being object st s in REAL & t in REAL & u in REAL holds
(CarProd ((Seg 3) --> REAL)) . [[s,t],u] = <*s,t,u*> ) )

proof end;

theorem Th41: :: MEASUR14:41

( Prod_Field (L-Field 1) = L-Field & Borel_Sets c= Prod_Field (L-Field 1) & ( for I being Subset of REAL st I is Interval holds
I in Prod_Field (L-Field 1) ) )

proof end;

theorem Th42: :: MEASUR14:42

( Prod_Field (L-Field 2) = sigma (measurable_rectangles (L-Field,L-Field)) & measurable_rectangles (L-Field,L-Field) c= sigma (measurable_rectangles (L-Field,L-Field)) & { [:A,B:] where A, B is Element of Borel_Sets : verum } c= measurable_rectangles (L-Field,L-Field) & { [:I,J:] where I, J is Subset of REAL : ( I is Interval & J is Interval ) } c= { [:A,B:] where A, B is Element of Borel_Sets : verum } )

proof end;

theorem :: MEASUR14:43

( Prod_Field (L-Field 3) = sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) & measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field) c= sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) & { [:A,B,C:] where A, B, C is Element of Borel_Sets : verum } c= measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field) & { [:I,J,K:] where I, J, K is Subset of REAL : ( I is Interval & J is Interval & K is Interval ) } c= { [:A,B,C:] where A, B, C is Element of Borel_Sets : verum } )

proof end;

theorem Th44: :: MEASUR14:44

for n being non zero Nat holds Prod_Field (L-Field (n + 1)) = sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field))

proof end;

theorem Th45: :: MEASUR14:45

( Prod_Measure (L-Meas 1) = L-Meas & ( for E being Element of L-Field holds E in Prod_Field (L-Field 1) ) )

proof end;

theorem Th46: :: MEASUR14:46

( Prod_Measure (L-Meas 2) = Prod_Measure (L-Meas,L-Meas) & ( for E1, E2 being Element of L-Field holds
( [:E1,E2:] in measurable_rectangles (L-Field,L-Field) & (Prod_Measure (L-Meas 2)) . [:E1,E2:] = (L-Meas . E1) * (L-Meas . E2) ) ) )

proof end;

theorem :: MEASUR14:47

( Prod_Measure (L-Meas 3) = Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas) & ( for E1, E2, E3 being Element of L-Field holds
( [:E1,E2,E3:] in measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field) & (Prod_Measure (L-Meas 3)) . [:E1,E2,E3:] = ((L-Meas . E1) * (L-Meas . E2)) * (L-Meas . E3) ) ) )

proof end;

theorem :: MEASUR14:48

for n being non zero Nat holds Prod_Measure (L-Meas (n + 1)) = Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)

proof end;

theorem Th49: :: MEASUR14:49

for n being non zero Nat
for f being PartFunc of (CarProduct ((Seg n) --> REAL)),ExtREAL
for g being PartFunc of (REAL n),ExtREAL
for A being Element of Prod_Field (L-Field n)
for B being Element of XL-Field n st g = f * ((CarProd ((Seg n) --> REAL)) ") & B = (CarProd ((Seg n) --> REAL)) .: A holds
( f is A -measurable iff g is B -measurable )

proof end;

theorem Th50: :: MEASUR14:50

for f1 being PartFunc of [:REAL,REAL:],ExtREAL
for f2 being PartFunc of (CarProduct ((Seg 2) --> REAL)),ExtREAL
for A1 being Element of sigma (measurable_rectangles (L-Field,L-Field))
for A2 being Element of Prod_Field (L-Field 2) st f1 = f2 & A1 = A2 holds
( f1 is A1 -measurable iff f2 is A2 -measurable )

proof end;

theorem :: MEASUR14:51

for f being PartFunc of [:REAL,REAL:],ExtREAL
for g being PartFunc of (REAL 2),ExtREAL
for A being Element of sigma (measurable_rectangles (L-Field,L-Field))
for B being Element of XL-Field 2 st g = f * ((CarProd ((Seg 2) --> REAL)) ") & B = (CarProd ((Seg 2) --> REAL)) .: A holds
( f is A -measurable iff g is B -measurable )

proof end;

theorem Th52: :: MEASUR14:52

for f1 being PartFunc of [:[:REAL,REAL:],REAL:],ExtREAL
for f2 being PartFunc of (CarProduct ((Seg 3) --> REAL)),ExtREAL
for A1 being Element of sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field))
for A2 being Element of Prod_Field (L-Field 3) st f1 = f2 & A1 = A2 holds
( f1 is A1 -measurable iff f2 is A2 -measurable )

proof end;

theorem :: MEASUR14:53

for f being PartFunc of [:[:REAL,REAL:],REAL:],ExtREAL
for g being PartFunc of (REAL 3),ExtREAL
for A being Element of sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field))
for B being Element of XL-Field 3 st g = f * ((CarProd ((Seg 3) --> REAL)) ") & B = (CarProd ((Seg 3) --> REAL)) .: A holds
( f is A -measurable iff g is B -measurable )

proof end;

theorem :: MEASUR14:54

for n being non zero Nat
for f being PartFunc of (CarProduct ((Seg n) --> REAL)),ExtREAL
for g being PartFunc of (REAL n),ExtREAL
for A being Element of Prod_Field (L-Field n) st g = f * ((CarProd ((Seg n) --> REAL)) ") & A = dom f & f is A -measurable holds
Integral ((XL-Meas n),g) = Integral ((Prod_Measure (L-Meas n)),f)

proof end;

theorem :: MEASUR14:55

for n being non zero Nat
for f being PartFunc of (CarProduct ((Seg n) --> REAL)),ExtREAL
for g being PartFunc of (REAL n),ExtREAL st g = f * ((CarProd ((Seg n) --> REAL)) ") holds
( f is_integrable_on Prod_Measure (L-Meas n) iff g is_integrable_on XL-Meas n )

proof end;