:: Product Pre-Measure
:: by Noboru Endou
::
:: Received December 31, 2015
:: Copyright (c) 2015-2021 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 chi (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 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

Family_of_halflines c= Family_of_Intervals

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

( sigma Family_of_Intervals = Borel_Sets & sigma (Field_generated_by Family_of_Intervals) = Borel_Sets )

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 b₁ being n -element FinSequence st
for i being Nat st i in Seg n holds
b₁ . 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 b₁ -element FinSequence
for b₃ being b₁ -element FinSequence holds
( b₃ is SemialgebraFamily of X iff for i being Nat st i in Seg n holds
b₃ . i is semialgebra_of_sets of X . i );

Lm05: for n being non zero Nat
for X being non-empty b₁ -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 b₁ being SemialgebraFamily of X holds b₁ 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 b₁ -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 { (product <*s*>) 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 b₁ -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 b₁ -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 b₁ being n -element FinSequence st
for i being Nat st i in Seg n holds
b₁ . 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 b₁ -element FinSequence
for b₃ being b₁ -element FinSequence holds
( b₃ is FieldFamily of X iff for i being Nat st i in Seg n holds
b₃ . i is Field_Subset of (X . i) );

Lm06: for n being non zero Nat
for X being non-empty b₁ -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 b₁ being FieldFamily of X holds b₁ 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 { (product <*s*>) 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 (product X)

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 b₁ 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 & b₁ . 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 b₁ -element FinSequence
for S being FieldFamily of X
for b₄ being b₁ -element FinSequence holds
( b₄ 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 & b₄ . 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 b₁ 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:] & b₁ . C = (m1 . A) * (m2 . B) )

proof end;

uniqueness
for b₁, b₂ 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:] & b₁ . 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:] & b₂ . C = (m1 . A) * (m2 . B) ) ) holds
b₁ = b₂

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 b₇ being zeroed V161() Function of (measurable_rectangles (S1,S2)),ExtREAL holds
( b₇ = 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:] & b₇ . 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 ((Union f),X)) . x = (lim (Partial_Sums F)) . 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 E -measurable ) & ( 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 (Partial_Sums F))) = 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 A -measurable

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 b₁ being Function of X,ExtREAL st
for x being object st x in X holds
( ( x in A implies b₁ . x = +infty ) & ( not x in A implies b₁ . x = 0 ) )

proof end;

uniqueness
for b₁, b₂ being Function of X,ExtREAL st ( for x being object st x in X holds
( ( x in A implies b₁ . x = +infty ) & ( not x in A implies b₁ . x = 0 ) ) ) & ( for x being object st x in X holds
( ( x in A implies b₂ . x = +infty ) & ( not x in A implies b₂ . x = 0 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefXchi defines Xchi MEASUR10:def 7 :
for A, X being set
for b₃ being Function of X,ExtREAL holds
( b₃ = Xchi (A,X) iff for x being object st x in X holds
( ( x in A implies b₃ . x = +infty ) & ( not x in A implies b₃ . 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 B -measurable

proof end;

registration

let X be non empty set ;
let S be SigmaField of X;
let A be Element of S;

cluster Xchi (A,X) -> A -measurable ;

coherence
Xchi (A,X) is A -measurable by Th32;

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)) . (Union K) = 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) = (Partial_Sums s) . (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)) . (Union F) = 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;