:: Product Pre-Measure
:: by Noboru Endou
::
:: Received December 31, 2015
:: Copyright (c) 2015-2018 Association of Mizar Users

theorem Th23: :: MEASUR10:1
for A, A1, A2, B, B1, B2 being non empty set holds
( ( [:A1,B1:] misses [:A2,B2:] & [:A,B:] = [:A1,B1:] \/ [:A2,B2:] ) iff ( ( A1 misses A2 & A = A1 \/ A2 & B = B1 & B = B2 ) or ( B1 misses B2 & B = B1 \/ B2 & A = A1 & A = A2 ) ) )
proof end;

definition
let C, D be non empty set ;
let F be sequence of (Funcs (C,D));
let n be Nat;
:: original: .
redefine func F . n -> Function of C,D;
correctness
coherence
F . n is Function of C,D
;
proof end;
end;

theorem Th26: :: MEASUR10:2
for X, Y, A, B being set
for x, y being object st x in X & y in Y holds
((chi (A,X)) . x) * ((chi (B,Y)) . y) = (chi ([:A,B:],[:X,Y:])) . (x,y)
proof end;

registration
let A, B be set ;
cluster K391(A,B) -> nonnegative ;
coherence
chi (A,B) is nonnegative
proof end;
end;

theorem :: MEASUR10:3
for X being non empty set
for S being semialgebra_of_sets of X
for P being pre-Measure of S
for m being induced_Measure of S,P
for M being induced_sigma_Measure of S,m holds COM M is_complete COM ((),M) by MEASURE3:20;

definition
func Family_of_Intervals -> semialgebra_of_sets of REAL equals :: MEASUR10:def 1
{ I where I is Interval : verum } ;
correctness
coherence
{ I where I is Interval : verum } is semialgebra_of_sets of REAL
;
by SRINGS_3:28;
end;

:: deftheorem defines Family_of_Intervals MEASUR10:def 1 :
Family_of_Intervals = { I where I is Interval : verum } ;

theorem Th02: :: MEASUR10:4
proof end;

Lm01: for I being Subset of REAL st I is open_interval holds
I in Borel_Sets

proof end;

Lm02: for I being Subset of REAL st I is closed_interval holds
I in Borel_Sets

proof end;

Lm03: for I being Subset of REAL st I is right_open_interval holds
I in Borel_Sets

proof end;

Lm04: for I being Subset of REAL st I is left_open_interval holds
I in Borel_Sets

proof end;

theorem Th03: :: MEASUR10:5
for I being Subset of REAL st I is Interval holds
I in Borel_Sets
proof end;

theorem :: MEASUR10:6
proof end;

theorem Th05: :: MEASUR10:7
for X1, X2 being set
for S1 being non empty Subset-Family of X1
for S2 being non empty Subset-Family of X2 holds { [:a,b:] where a is Element of S1, b is Element of S2 : verum } is non empty Subset-Family of [:X1,X2:]
proof end;

theorem :: MEASUR10:8
for X, Y being set
for M being with_empty_element Subset-Family of X
for N being with_empty_element Subset-Family of Y holds { [:A,B:] where A is Element of M, B is Element of N : verum } is with_empty_element Subset-Family of [:X,Y:]
proof end;

theorem Th07: :: MEASUR10:9
for X being set
for F1, F2 being disjoint_valued FinSequence of X st union (rng F1) misses union (rng F2) holds
F1 ^ F2 is disjoint_valued FinSequence of X
proof end;

theorem Th08: :: MEASUR10:10
for X1, X2 being set
for S1 being Semiring of X1
for S2 being Semiring of X2 holds { [:A,B:] where A is Element of S1, B is Element of S2 : verum } is Semiring of [:X1,X2:]
proof end;

theorem Th09: :: MEASUR10:11
for X1, X2 being set
for S1 being semialgebra_of_sets of X1
for S2 being semialgebra_of_sets of X2 holds { [:A,B:] where A is Element of S1, B is Element of S2 : verum } is semialgebra_of_sets of [:X1,X2:]
proof end;

theorem :: MEASUR10:12
for X1, X2 being set
for F1 being Field_Subset of X1
for F2 being Field_Subset of X2 holds { [:A,B:] where A is Element of F1, B is Element of F2 : verum } is semialgebra_of_sets of [:X1,X2:]
proof end;

definition
let n be non zero Nat;
let X be non-empty n -element FinSequence;
mode SemialgebraFamily of X -> n -element FinSequence means :Def2: :: MEASUR10:def 2
for i being Nat st i in Seg n holds
it . i is semialgebra_of_sets of X . i;
existence
ex b1 being n -element FinSequence st
for i being Nat st i in Seg n holds
b1 . i is semialgebra_of_sets of X . i
proof end;
end;

:: deftheorem Def2 defines SemialgebraFamily MEASUR10:def 2 :
for n being non zero Nat
for X being non-empty b1 -element FinSequence
for b3 being b1 -element FinSequence holds
( b3 is SemialgebraFamily of X iff for i being Nat st i in Seg n holds
b3 . i is semialgebra_of_sets of X . i );

Lm05: for n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being SemialgebraFamily of X holds S is cap-closed-yielding SemiringFamily of X

proof end;

definition
let n be non zero Nat;
let X be non-empty n -element FinSequence;
:: original: SemialgebraFamily
redefine mode SemialgebraFamily of X -> cap-closed-yielding SemiringFamily of X;
correctness
coherence
for b1 being SemialgebraFamily of X holds b1 is cap-closed-yielding SemiringFamily of X
;
by Lm05;
end;

theorem Th11: :: MEASUR10:13
for n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being SemialgebraFamily of X
for i being Nat st i in Seg n holds
X . i in S . i
proof end;

theorem Th12: :: MEASUR10:14
for X being non-empty 1 -element FinSequence
for S being SemialgebraFamily of X holds { () where s is Element of S . 1 : verum } is semialgebra_of_sets of { <*x*> where x is Element of X . 1 : verum }
proof end;

theorem Th13: :: MEASUR10:15
for X being non-empty 1 -element FinSequence
for S being SemialgebraFamily of X holds SemiringProduct S is semialgebra_of_sets of product X
proof end;

theorem Th14: :: MEASUR10:16
for X1, X2 being set
for S1 being semialgebra_of_sets of X1
for S2 being semialgebra_of_sets of X2 holds { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } is semialgebra_of_sets of [:X1,X2:]
proof end;

theorem Th15: :: MEASUR10:17
for n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being SemialgebraFamily of X holds SemiringProduct S is semialgebra_of_sets of product X
proof end;

theorem :: MEASUR10:18
for n being non zero Nat
for Xn being non-empty b1 -element FinSequence
for X1 being non-empty 1 -element FinSequence
for Sn being SemialgebraFamily of Xn
for S1 being SemialgebraFamily of X1 holds SemiringProduct (Sn ^ S1) is semialgebra_of_sets of product (Xn ^ X1)
proof end;

definition
let n be non zero Nat;
let X be non-empty n -element FinSequence;
mode FieldFamily of X -> n -element FinSequence means :Def3: :: MEASUR10:def 3
for i being Nat st i in Seg n holds
it . i is Field_Subset of (X . i);
existence
ex b1 being n -element FinSequence st
for i being Nat st i in Seg n holds
b1 . i is Field_Subset of (X . i)
proof end;
end;

:: deftheorem Def3 defines FieldFamily MEASUR10:def 3 :
for n being non zero Nat
for X being non-empty b1 -element FinSequence
for b3 being b1 -element FinSequence holds
( b3 is FieldFamily of X iff for i being Nat st i in Seg n holds
b3 . i is Field_Subset of (X . i) );

Lm06: for n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being FieldFamily of X holds S is SemialgebraFamily of X

proof end;

definition
let n be non zero Nat;
let X be non-empty n -element FinSequence;
:: original: FieldFamily
redefine mode FieldFamily of X -> SemialgebraFamily of X;
correctness
coherence
for b1 being FieldFamily of X holds b1 is SemialgebraFamily of X
;
by Lm06;
end;

theorem Th17: :: MEASUR10:19
for X being non-empty 1 -element FinSequence
for S being FieldFamily of X holds { () where s is Element of S . 1 : verum } is Field_Subset of { <*x*> where x is Element of X . 1 : verum }
proof end;

theorem :: MEASUR10:20
for X being non-empty 1 -element FinSequence
for S being FieldFamily of X holds SemiringProduct S is Field_Subset of ()
proof end;

definition
let n be non zero Nat;
let X be non-empty n -element FinSequence;
let S be FieldFamily of X;
mode MeasureFamily of S -> n -element FinSequence means :: MEASUR10:def 4
for i being Nat st i in Seg n holds
ex F being Field_Subset of (X . i) st
( F = S . i & it . i is Measure of F );
existence
ex b1 being n -element FinSequence st
for i being Nat st i in Seg n holds
ex F being Field_Subset of (X . i) st
( F = S . i & b1 . i is Measure of F )
proof end;
end;

:: deftheorem defines MeasureFamily MEASUR10:def 4 :
for n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being FieldFamily of X
for b4 being b1 -element FinSequence holds
( b4 is MeasureFamily of S iff for i being Nat st i in Seg n holds
ex F being Field_Subset of (X . i) st
( F = S . i & b4 . i is Measure of F ) );

definition
let X1, X2 be set ;
let S1 be Field_Subset of X1;
let S2 be Field_Subset of X2;
func measurable_rectangles (S1,S2) -> semialgebra_of_sets of [:X1,X2:] equals :: MEASUR10:def 5
{ [:A,B:] where A is Element of S1, B is Element of S2 : verum } ;
correctness
coherence
{ [:A,B:] where A is Element of S1, B is Element of S2 : verum } is semialgebra_of_sets of [:X1,X2:]
;
proof end;
end;

:: deftheorem defines measurable_rectangles MEASUR10:def 5 :
for X1, X2 being set
for S1 being Field_Subset of X1
for S2 being Field_Subset of X2 holds measurable_rectangles (S1,S2) = { [:A,B:] where A is Element of S1, B is Element of S2 : verum } ;

theorem :: MEASUR10:21
for X being set
for F being Field_Subset of X ex S being semialgebra_of_sets of X st
( F = S & F = Field_generated_by S )
proof end;

definition
let X1, X2 be set ;
let S1 be Field_Subset of X1;
let S2 be Field_Subset of X2;
let m1 be Measure of S1;
let m2 be Measure of S2;
func product-pre-Measure (m1,m2) -> zeroed V161() Function of (measurable_rectangles (S1,S2)),ExtREAL means :Def6: :: MEASUR10:def 6
for C being Element of measurable_rectangles (S1,S2) ex A being Element of S1 ex B being Element of S2 st
( C = [:A,B:] & it . C = (m1 . A) * (m2 . B) );
existence
ex b1 being zeroed V161() Function of (measurable_rectangles (S1,S2)),ExtREAL st
for C being Element of measurable_rectangles (S1,S2) ex A being Element of S1 ex B being Element of S2 st
( C = [:A,B:] & b1 . C = (m1 . A) * (m2 . B) )
proof end;
uniqueness
for b1, b2 being zeroed V161() Function of (measurable_rectangles (S1,S2)),ExtREAL st ( for C being Element of measurable_rectangles (S1,S2) ex A being Element of S1 ex B being Element of S2 st
( C = [:A,B:] & b1 . C = (m1 . A) * (m2 . B) ) ) & ( for C being Element of measurable_rectangles (S1,S2) ex A being Element of S1 ex B being Element of S2 st
( C = [:A,B:] & b2 . C = (m1 . A) * (m2 . B) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines product-pre-Measure MEASUR10:def 6 :
for X1, X2 being set
for S1 being Field_Subset of X1
for S2 being Field_Subset of X2
for m1 being Measure of S1
for m2 being Measure of S2
for b7 being zeroed V161() Function of (measurable_rectangles (S1,S2)),ExtREAL holds
( b7 = product-pre-Measure (m1,m2) iff for C being Element of measurable_rectangles (S1,S2) ex A being Element of S1 ex B being Element of S2 st
( C = [:A,B:] & b7 . C = (m1 . A) * (m2 . B) ) );

theorem Th20: :: MEASUR10:22
for X1, X2 being set
for S1 being Field_Subset of X1
for S2 being Field_Subset of X2
for m1 being Measure of S1
for m2 being Measure of S2
for A, B being set st A in S1 & B in S2 holds
(product-pre-Measure (m1,m2)) . [:A,B:] = (m1 . A) * (m2 . B)
proof end;

theorem :: MEASUR10:23
for X1, X2 being set
for S1 being non empty Subset-Family of X1
for S2 being non empty Subset-Family of X2
for S being non empty Subset-Family of [:X1,X2:]
for H being FinSequence of S st S = { [:A,B:] where A is Element of S1, B is Element of S2 : verum } holds
ex F being FinSequence of S1 ex G being FinSequence of S2 st
( len H = len F & len H = len G & ( for k being Nat st k in dom H & H . k <> {} holds
H . k = [:(F . k),(G . k):] ) )
proof end;

theorem :: MEASUR10:24
for X being set
for S being non empty cap-closed semi-diff-closed Subset-Family of X
for E1, E2 being Element of S ex F1, F2, F3 being disjoint_valued FinSequence of S st
( union (rng F1) = E1 \ E2 & union (rng F2) = E2 \ E1 & union (rng F3) = E1 /\ E2 & (F1 ^ F2) ^ F3 is disjoint_valued FinSequence of S )
proof end;

theorem :: MEASUR10:25
for X1, X2 being set
for S1 being Field_Subset of X1
for S2 being Field_Subset of X2
for m1 being Measure of S1
for m2 being Measure of S2
for E1, E2 being Element of measurable_rectangles (S1,S2) st E1 misses E2 & E1 \/ E2 in measurable_rectangles (S1,S2) holds
(product-pre-Measure (m1,m2)) . (E1 \/ E2) = ((product-pre-Measure (m1,m2)) . E1) + ((product-pre-Measure (m1,m2)) . E2)
proof end;

theorem Th25: :: MEASUR10:26
for X being non empty set
for S being non empty Subset-Family of X
for f being Function of NAT,S
for F being Functional_Sequence of X,ExtREAL st f is disjoint_valued & ( for n being Nat holds F . n = chi ((f . n),X) ) holds
for x being object st x in X holds
(chi ((),X)) . x = (lim ()) . x
proof end;

theorem Th27: :: MEASUR10:27
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
for r being Real st dom f in S & 0 <= r & ( for x being object st x in dom f holds
f . x = r ) holds
Integral (M,f) = r * (M . (dom f))
proof end;

theorem Th28: :: MEASUR10:28
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
for A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & ( for x being object st x in (dom f) \ A holds
f . x = 0 ) & f is nonnegative holds
Integral (M,f) = Integral (M,(f | A))
proof end;

theorem :: MEASUR10:29
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
for A being Element of S st f is_integrable_on M & ( for x being object st x in (dom f) \ A holds
f . x = 0 ) holds
Integral (M,f) = Integral (M,(f | A))
proof end;

theorem Th30: :: MEASUR10:30
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 D being Function of NAT,S1
for E being Function of NAT,S2
for A being Element of S1
for B being Element of S2
for F being Functional_Sequence of X2,ExtREAL
for RD being sequence of (Funcs (X1,REAL))
for x being Element of X1 st ( for n being Nat holds RD . n = chi ((D . n),X1) ) & ( for n being Nat holds F . n = ((RD . n) . x) (#) (chi ((E . n),X2)) ) & ( for n being Nat holds E . n c= B ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = (M2 . (E . n)) * ((chi ((D . n),X1)) . x) ) & I is summable & Integral (M2,(lim ())) = Sum I )
proof end;

theorem :: MEASUR10:31
for X being non empty set
for S being SigmaField of X
for A being Element of S
for p being R_eal holds X --> p is_measurable_on A
proof end;

definition
let A, X be set ;
func Xchi (A,X) -> Function of X,ExtREAL means :DefXchi: :: MEASUR10:def 7
for x being object st x in X holds
( ( x in A implies it . x = +infty ) & ( not x in A implies it . x = 0 ) );
existence
ex b1 being Function of X,ExtREAL st
for x being object st x in X holds
( ( x in A implies b1 . x = +infty ) & ( not x in A implies b1 . x = 0 ) )
proof end;
uniqueness
for b1, b2 being Function of X,ExtREAL st ( for x being object st x in X holds
( ( x in A implies b1 . x = +infty ) & ( not x in A implies b1 . x = 0 ) ) ) & ( for x being object st x in X holds
( ( x in A implies b2 . x = +infty ) & ( not x in A implies b2 . x = 0 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem DefXchi defines Xchi MEASUR10:def 7 :
for A, X being set
for b3 being Function of X,ExtREAL holds
( b3 = Xchi (A,X) iff for x being object st x in X holds
( ( x in A implies b3 . x = +infty ) & ( not x in A implies b3 . x = 0 ) ) );

Lm08: for X being non empty set
for S being SigmaField of X
for A being Element of S
for r being Real st r > 0 holds
great_eq_dom ((Xchi (A,X)),r) = A

proof end;

Lm09: for X being non empty set
for S being SigmaField of X
for A being Element of S
for r being Real st r <= 0 holds
great_eq_dom ((Xchi (A,X)),r) = X

proof end;

theorem Th32: :: MEASUR10:32
for X being non empty set
for S being SigmaField of X
for A, B being Element of S holds Xchi (A,X) is_measurable_on B
proof end;

registration
let X, A be set ;
cluster Xchi (A,X) -> nonnegative ;
coherence
Xchi (A,X) is nonnegative
proof end;
end;

theorem Th34: :: MEASUR10:33
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 holds
( ( M . A <> 0 implies Integral (M,(Xchi (A,X))) = +infty ) & ( M . A = 0 implies Integral (M,(Xchi (A,X))) = 0 ) )
proof end;

theorem Th35: :: MEASUR10:34
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 K being disjoint_valued Function of NAT,(measurable_rectangles (S1,S2)) st Union K in measurable_rectangles (S1,S2) holds
(product-pre-Measure (M1,M2)) . () = SUM ((product-pre-Measure (M1,M2)) * K)
proof end;

theorem Th36: :: MEASUR10:35
for f being V169() FinSequence of ExtREAL
for s being V169() ExtREAL_sequence st ( for n being object st n in dom f holds
f . n = s . n ) holds
(Sum f) + (s . 0) = () . (len f)
proof end;

theorem Th37: :: MEASUR10:36
for f being nonnegative FinSequence of ExtREAL
for s being ExtREAL_sequence st ( for n being object st n in dom f holds
f . n = s . n ) & ( for n being Element of NAT st not n in dom f holds
s . n = 0 ) holds
( Sum f = Sum s & Sum f = SUM s )
proof end;

theorem Th38: :: MEASUR10:37
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 disjoint_valued FinSequence of measurable_rectangles (S1,S2) st Union F in measurable_rectangles (S1,S2) holds
(product-pre-Measure (M1,M2)) . () = Sum ((product-pre-Measure (M1,M2)) * F)
proof end;

theorem Th39: :: MEASUR10:38
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 holds product-pre-Measure (M1,M2) is pre-Measure of measurable_rectangles (S1,S2)
proof end;

definition
let X1, X2 be non empty set ;
let S1 be SigmaField of X1;
let S2 be SigmaField of X2;
let M1 be sigma_Measure of S1;
let M2 be sigma_Measure of S2;
:: original: product-pre-Measure
redefine func product-pre-Measure (M1,M2) -> pre-Measure of measurable_rectangles (S1,S2);
correctness
coherence
product-pre-Measure (M1,M2) is pre-Measure of measurable_rectangles (S1,S2)
;
by Th39;
end;