let X, Y be non empty set ; for S1 being SigmaField of X
for S2 being SigmaField of Y
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2 st M1 is sigma_finite & M2 is sigma_finite holds
Prod_Measure (M1,M2) is sigma_finite
let S1 be SigmaField of X; for S2 being SigmaField of Y
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2 st M1 is sigma_finite & M2 is sigma_finite holds
Prod_Measure (M1,M2) is sigma_finite
let S2 be SigmaField of Y; for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2 st M1 is sigma_finite & M2 is sigma_finite holds
Prod_Measure (M1,M2) is sigma_finite
let M1 be sigma_Measure of S1; for M2 being sigma_Measure of S2 st M1 is sigma_finite & M2 is sigma_finite holds
Prod_Measure (M1,M2) is sigma_finite
let M2 be sigma_Measure of S2; ( M1 is sigma_finite & M2 is sigma_finite implies Prod_Measure (M1,M2) is sigma_finite )
assume A1:
( M1 is sigma_finite & M2 is sigma_finite )
; Prod_Measure (M1,M2) is sigma_finite
set M = Prod_Measure (M1,M2);
consider E1 being Set_Sequence of S1 such that
A2:
( ( for n being Nat holds M1 . (E1 . n) < +infty ) & Union E1 = X )
by A1, MEASUR11:def 12;
consider E2 being Set_Sequence of S2 such that
A3:
( ( for n being Nat holds M2 . (E2 . n) < +infty ) & Union E2 = Y )
by A1, MEASUR11:def 12;
set F1 = Partial_Union E1;
set F2 = Partial_Union E2;
A4:
( Partial_Union E1 is non-descending & Partial_Union E2 is non-descending )
by PROB_3:11;
deffunc H1( Nat) -> Element of sigma (measurable_rectangles (S1,S2)) = In ([:((Partial_Union E1) . $1),((Partial_Union E2) . $1):],(sigma (measurable_rectangles (S1,S2))));
consider E being Function of NAT,(sigma (measurable_rectangles (S1,S2))) such that
A5:
for i being Element of NAT holds E . i = H1(i)
from FUNCT_2:sch 4();
A6:
for i being Nat holds E . i = [:((Partial_Union E1) . i),((Partial_Union E2) . i):]
proof
let i be
Nat;
E . i = [:((Partial_Union E1) . i),((Partial_Union E2) . i):]
(
(Partial_Union E1) . i in S1 &
(Partial_Union E2) . i in S2 )
by Th26;
then A7:
[:((Partial_Union E1) . i),((Partial_Union E2) . i):] in measurable_rectangles (
S1,
S2)
;
measurable_rectangles (
S1,
S2)
c= sigma (measurable_rectangles (S1,S2))
by PROB_1:def 9;
then A8:
In (
[:((Partial_Union E1) . i),((Partial_Union E2) . i):],
(sigma (measurable_rectangles (S1,S2))))
= [:((Partial_Union E1) . i),((Partial_Union E2) . i):]
by A7, SUBSET_1:def 8;
i in NAT
by ORDINAL1:def 12;
hence
E . i = [:((Partial_Union E1) . i),((Partial_Union E2) . i):]
by A5, A8;
verum
end;
reconsider E = E as SetSequence of [:X,Y:] by FUNCT_2:7;
A9:
measurable_rectangles (S1,S2) c= sigma (measurable_rectangles (S1,S2))
by PROB_1:def 9;
A10:
for i being Nat holds E . i in sigma (measurable_rectangles (S1,S2))
reconsider E = E as Set_Sequence of sigma (measurable_rectangles (S1,S2)) by A10, MEASURE8:def 2;
A12:
( Union (Partial_Union E1) = Union E1 & Union (Partial_Union E2) = Union E2 )
by PROB_3:15;
for z being object holds
( z in Union E iff z in [:X,Y:] )
proof
let z be
object ;
( z in Union E iff z in [:X,Y:] )
thus
(
z in Union E implies
z in [:X,Y:] )
;
( z in [:X,Y:] implies z in Union E )
assume
z in [:X,Y:]
;
z in Union E
then consider x,
y being
object such that A13:
(
x in X &
y in Y &
z = [x,y] )
by ZFMISC_1:def 2;
A14:
(
x in union (rng (Partial_Union E1)) &
y in union (rng (Partial_Union E2)) )
by A2, A3, A12, A13, CARD_3:def 4;
consider W1 being
set such that A15:
(
x in W1 &
W1 in rng (Partial_Union E1) )
by A14, TARSKI:def 4;
consider W2 being
set such that A16:
(
y in W2 &
W2 in rng (Partial_Union E2) )
by A14, TARSKI:def 4;
consider i being
object such that A17:
(
i in dom (Partial_Union E1) &
W1 = (Partial_Union E1) . i )
by A15, FUNCT_1:def 3;
reconsider i =
i as
Nat by A17;
consider j being
object such that A18:
(
j in dom (Partial_Union E2) &
W2 = (Partial_Union E2) . j )
by A16, FUNCT_1:def 3;
reconsider j =
j as
Nat by A18;
reconsider k =
max (
i,
j) as
Nat by XXREAL_0:16;
(
(Partial_Union E1) . i c= (Partial_Union E1) . k &
(Partial_Union E2) . j c= (Partial_Union E2) . k )
by A4, XXREAL_0:25;
then
z in [:((Partial_Union E1) . k),((Partial_Union E2) . k):]
by A13, A17, A15, A18, A16, ZFMISC_1:87;
then A19:
z in E . k
by A6;
k in NAT
by ORDINAL1:def 12;
then
k in dom E
by FUNCT_2:def 1;
then
E . k in rng E
by FUNCT_1:3;
then
z in union (rng E)
by A19, TARSKI:def 4;
hence
z in Union E
by CARD_3:def 4;
verum
end;
then A20:
Union E = [:X,Y:]
;
A21:
( M1 is nonnegative & M2 is nonnegative )
;
defpred S1[ Nat] means ( M1 . ((Partial_Union E1) . $1) in REAL & M2 . ((Partial_Union E2) . $1) in REAL );
A22:
( M1 . (E1 . 0) < +infty & M2 . (E2 . 0) < +infty )
by A2, A3;
( 0 <= M1 . (E1 . 0) & 0 <= M2 . (E2 . 0) )
by A21;
then
( M1 . (E1 . 0) in REAL & M2 . (E2 . 0) in REAL )
by A22, XXREAL_0:14;
then A23:
S1[ 0 ]
by PROB_3:def 2;
A24:
for i being Nat st S1[i] holds
S1[i + 1]
A31:
for i being Nat holds S1[i]
from NAT_1:sch 2(A23, A24);
for i being Nat holds (Prod_Measure (M1,M2)) . (E . i) < +infty
proof
let i be
Nat;
(Prod_Measure (M1,M2)) . (E . i) < +infty
A32:
E . i = [:((Partial_Union E1) . i),((Partial_Union E2) . i):]
by A6;
A33:
(
(Partial_Union E1) . i in S1 &
(Partial_Union E2) . i in S2 )
by Th26;
(Prod_Measure (M1,M2)) . (E . i) = (product_sigma_Measure (M1,M2)) . [:((Partial_Union E1) . i),((Partial_Union E2) . i):]
by A32, MESFUN12:def 9;
then A34:
(Prod_Measure (M1,M2)) . (E . i) = (M1 . ((Partial_Union E1) . i)) * (M2 . ((Partial_Union E2) . i))
by A32, A33, MEASUR11:16;
(
M1 . ((Partial_Union E1) . i) in REAL &
M2 . ((Partial_Union E2) . i) in REAL )
by A31;
then reconsider m1 =
M1 . ((Partial_Union E1) . i),
m2 =
M2 . ((Partial_Union E2) . i) as
Real ;
(M1 . ((Partial_Union E1) . i)) * (M2 . ((Partial_Union E2) . i)) = m1 * m2
;
hence
(Prod_Measure (M1,M2)) . (E . i) < +infty
by A34, XREAL_0:def 1, XXREAL_0:9;
verum
end;
hence
Prod_Measure (M1,M2) is sigma_finite
by A20, MEASUR11:def 12; verum