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

( ( [: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;

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

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)

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

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

coherence

{ I where I is Interval : verum } is semialgebra_of_sets of REAL ;

by SRINGS_3:28;

end;

func Family_of_Intervals -> semialgebra_of_sets of REAL equals :: MEASUR10:def 1

{ I where I is Interval : verum } ;

correctness { I where I is Interval : verum } ;

coherence

{ I where I is Interval : verum } is semialgebra_of_sets of REAL ;

by SRINGS_3:28;

:: deftheorem defines Family_of_Intervals MEASUR10:def 1 :

Family_of_Intervals = { I where I is Interval : verum } ;

Family_of_Intervals = { I where I is Interval : verum } ;

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 :: 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:]

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:]

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

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:]

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:]

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:]

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;

ex b_{1} being n -element FinSequence st

for i being Nat st i in Seg n holds

b_{1} . i is semialgebra_of_sets of X . i

end;
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 for i being Nat st i in Seg n holds

it . i is semialgebra_of_sets of X . i;

ex b

for i being Nat st i in Seg n holds

b

proof end;

:: deftheorem Def2 defines SemialgebraFamily MEASUR10:def 2 :

for n being non zero Nat

for X being non-empty b_{1} -element FinSequence

for b_{3} being b_{1} -element FinSequence holds

( b_{3} is SemialgebraFamily of X iff for i being Nat st i in Seg n holds

b_{3} . i is semialgebra_of_sets of X . i );

for n being non zero Nat

for X being non-empty b

for b

( b

b

Lm05: for n being non zero Nat

for X being non-empty b

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_{1} being SemialgebraFamily of X holds b_{1} is cap-closed-yielding SemiringFamily of X;

by Lm05;

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

by Lm05;

theorem Th11: :: MEASUR10:13

for n being non zero Nat

for X being non-empty b_{1} -element FinSequence

for S being SemialgebraFamily of X

for i being Nat st i in Seg n holds

X . i in S . i

for X being non-empty b

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 }

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

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:]

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_{1} -element FinSequence

for S being SemialgebraFamily of X holds SemiringProduct S is semialgebra_of_sets of product X

for X being non-empty b

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_{1} -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)

for Xn being non-empty b

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;

ex b_{1} being n -element FinSequence st

for i being Nat st i in Seg n holds

b_{1} . i is Field_Subset of (X . i)

end;
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 for i being Nat st i in Seg n holds

it . i is Field_Subset of (X . i);

ex b

for i being Nat st i in Seg n holds

b

proof end;

:: deftheorem Def3 defines FieldFamily MEASUR10:def 3 :

for n being non zero Nat

for X being non-empty b_{1} -element FinSequence

for b_{3} being b_{1} -element FinSequence holds

( b_{3} is FieldFamily of X iff for i being Nat st i in Seg n holds

b_{3} . i is Field_Subset of (X . i) );

for n being non zero Nat

for X being non-empty b

for b

( b

b

Lm06: for n being non zero Nat

for X being non-empty b

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_{1} being FieldFamily of X holds b_{1} is SemialgebraFamily of X;

by Lm06;

end;
let X be non-empty n -element FinSequence;

:: original: FieldFamily

redefine mode FieldFamily of X -> SemialgebraFamily of X;

correctness

coherence

for b

by Lm06;

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 }

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)

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;

ex b_{1} 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_{1} . i is Measure of F )

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

ex b

for i being Nat st i in Seg n holds

ex F being Field_Subset of (X . i) st

( F = S . i & b

proof end;

:: deftheorem defines MeasureFamily MEASUR10:def 4 :

for n being non zero Nat

for X being non-empty b_{1} -element FinSequence

for S being FieldFamily of X

for b_{4} being b_{1} -element FinSequence holds

( b_{4} 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_{4} . i is Measure of F ) );

for n being non zero Nat

for X being non-empty b

for S being FieldFamily of X

for b

( b

ex F being Field_Subset of (X . i) st

( F = S . i & b

definition

let X1, X2 be set ;

let S1 be Field_Subset of X1;

let S2 be Field_Subset of X2;

coherence

{ [:A,B:] where A is Element of S1, B is Element of S2 : verum } is semialgebra_of_sets of [:X1,X2:];

end;
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 { [:A,B:] where A is Element of S1, B is Element of S2 : verum } ;

coherence

{ [:A,B:] where A is Element of S1, B is Element of S2 : verum } is semialgebra_of_sets of [:X1,X2:];

proof 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 } ;

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 )

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;

ex b_{1} 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_{1} . C = (m1 . A) * (m2 . B) )

for b_{1}, b_{2} 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_{1} . 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_{2} . C = (m1 . A) * (m2 . B) ) ) holds

b_{1} = b_{2}

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

ex 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

proof end;

uniqueness for b

( C = [:A,B:] & b

( C = [:A,B:] & b

b

proof 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_{7} being zeroed V161() Function of (measurable_rectangles (S1,S2)),ExtREAL holds

( b_{7} = 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_{7} . C = (m1 . A) * (m2 . B) ) );

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

( b

( C = [:A,B:] & 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)

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

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 )

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)

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

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

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

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

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 )

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

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 ;

ex b_{1} being Function of X,ExtREAL st

for x being object st x in X holds

( ( x in A implies b_{1} . x = +infty ) & ( not x in A implies b_{1} . x = 0 ) )

for b_{1}, b_{2} being Function of X,ExtREAL st ( for x being object st x in X holds

( ( x in A implies b_{1} . x = +infty ) & ( not x in A implies b_{1} . x = 0 ) ) ) & ( for x being object st x in X holds

( ( x in A implies b_{2} . x = +infty ) & ( not x in A implies b_{2} . x = 0 ) ) ) holds

b_{1} = b_{2}

end;
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 for x being object st x in X holds

( ( x in A implies it . x = +infty ) & ( not x in A implies it . x = 0 ) );

ex b

for x being object st x in X holds

( ( x in A implies b

proof end;

uniqueness for b

( ( x in A implies b

( ( x in A implies b

b

proof end;

:: deftheorem DefXchi defines Xchi MEASUR10:def 7 :

for A, X being set

for b_{3} being Function of X,ExtREAL holds

( b_{3} = Xchi (A,X) iff for x being object st x in X holds

( ( x in A implies b_{3} . x = +infty ) & ( not x in A implies b_{3} . x = 0 ) ) );

for A, X being set

for b

( b

( ( x in A implies b

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

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;

coherence

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

end;
let S be SigmaField of X;

let A be Element of S;

coherence

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

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

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)

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)

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 )

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)

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)

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