:: by Noboru Endou

::

:: Received September 30, 2021

:: Copyright (c) 2021 Association of Mizar Users

Lm1: for a1, b1 being Real

for a2, b2 being R_eal st a1 = a2 & b1 = b2 holds

a1 - b1 = a2 - b2

proof end;

theorem Th1: :: MESFUN14:1

for X being non empty set

for f being PartFunc of X,ExtREAL holds

( rng (max+ f) c= (rng f) \/ {0} & rng (max- f) c= (rng (- f)) \/ {0} )

for f being PartFunc of X,ExtREAL holds

( rng (max+ f) c= (rng f) \/ {0} & rng (max- f) c= (rng (- f)) \/ {0} )

proof end;

theorem Th2: :: MESFUN14:2

for X being non empty set

for f being PartFunc of X,ExtREAL st f is V55() holds

( - f is V55() & max+ f is V55() & max- f is V55() )

for f being PartFunc of X,ExtREAL st f is V55() holds

( - f is V55() & max+ f is V55() & max- f is V55() )

proof end;

theorem Th3: :: MESFUN14:3

for X being non empty set

for f being PartFunc of X,ExtREAL st f is V171() & f is V172() holds

f is PartFunc of X,REAL

for f being PartFunc of X,ExtREAL st f is V171() & f is V172() holds

f is PartFunc of X,REAL

proof end;

theorem Th4: :: MESFUN14:4

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 st f is_simple_func_in S holds

( max+ f is_simple_func_in S & max- f is_simple_func_in S )

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds

( max+ f is_simple_func_in S & max- f is_simple_func_in S )

proof end;

theorem Th5: :: MESFUN14:5

for a, b being Real st a <= b holds

( B-Meas . [.a,b.] = b - a & B-Meas . [.a,b.[ = b - a & B-Meas . ].a,b.] = b - a & B-Meas . ].a,b.[ = b - a & L-Meas . [.a,b.] = b - a & L-Meas . [.a,b.[ = b - a & L-Meas . ].a,b.] = b - a & L-Meas . ].a,b.[ = b - a )

( B-Meas . [.a,b.] = b - a & B-Meas . [.a,b.[ = b - a & B-Meas . ].a,b.] = b - a & B-Meas . ].a,b.[ = b - a & L-Meas . [.a,b.] = b - a & L-Meas . [.a,b.[ = b - a & L-Meas . ].a,b.] = b - a & L-Meas . ].a,b.[ = b - a )

proof end;

theorem :: MESFUN14:6

for a, b being Real st a > b holds

( B-Meas . [.a,b.] = 0 & B-Meas . [.a,b.[ = 0 & B-Meas . ].a,b.] = 0 & B-Meas . ].a,b.[ = 0 & L-Meas . [.a,b.] = 0 & L-Meas . [.a,b.[ = 0 & L-Meas . ].a,b.] = 0 & L-Meas . ].a,b.[ = 0 )

( B-Meas . [.a,b.] = 0 & B-Meas . [.a,b.[ = 0 & B-Meas . ].a,b.] = 0 & B-Meas . ].a,b.[ = 0 & L-Meas . [.a,b.] = 0 & L-Meas . [.a,b.[ = 0 & L-Meas . ].a,b.] = 0 & L-Meas . ].a,b.[ = 0 )

proof end;

theorem :: MESFUN14:7

for A1 being Element of Borel_Sets

for A2 being Element of L-Field

for f being PartFunc of REAL,ExtREAL st A1 = A2 & f is A1 -measurable holds

f is A2 -measurable

for A2 being Element of L-Field

for f being PartFunc of REAL,ExtREAL st A1 = A2 & f is A1 -measurable holds

f is A2 -measurable

proof end;

theorem Th8: :: MESFUN14:8

for a, b being Real

for A being non empty closed_interval Subset of REAL st a < b & A = [.a,b.] holds

for n being Nat st n > 0 holds

ex D being Division of A st D divide_into_equal n

for A being non empty closed_interval Subset of REAL st a < b & A = [.a,b.] holds

for n being Nat st n > 0 holds

ex D being Division of A st D divide_into_equal n

proof end;

Lm2: for r being Real

for F being FinSequence of REAL st ( for n being Nat st n in dom F holds

F . n = r ) holds

Sum F = r * (len F)

proof end;

definition

let F be FinSequence of Borel_Sets ;

let n be Nat;

:: original: .

redefine func F . n -> ext-real-membered set ;

correctness

coherence

F . n is ext-real-membered set ;

end;
let n be Nat;

:: original: .

redefine func F . n -> ext-real-membered set ;

correctness

coherence

F . n is ext-real-membered set ;

proof end;

theorem Th9: :: MESFUN14:9

for a, b being Real

for A being non empty closed_interval Subset of REAL

for D being Division of A st A = [.a,b.] holds

ex F being Finite_Sep_Sequence of Borel_Sets st

( dom D = dom F & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) )

for A being non empty closed_interval Subset of REAL

for D being Division of A st A = [.a,b.] holds

ex F being Finite_Sep_Sequence of Borel_Sets st

( dom D = dom F & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) )

proof end;

theorem Th10: :: MESFUN14:10

for a, b being Real

for A being non empty closed_interval Subset of REAL

for D being Division of A

for f being PartFunc of A,REAL st A = [.a,b.] holds

ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st

( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = lower_bound (rng (f | (divset (D,k)))) ) ) )

for A being non empty closed_interval Subset of REAL

for D being Division of A

for f being PartFunc of A,REAL st A = [.a,b.] holds

ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st

( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = lower_bound (rng (f | (divset (D,k)))) ) ) )

proof end;

theorem Th11: :: MESFUN14:11

for a, b being Real

for A being non empty closed_interval Subset of REAL

for D being Division of A

for f being PartFunc of A,REAL st A = [.a,b.] holds

ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st

( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) )

for A being non empty closed_interval Subset of REAL

for D being Division of A

for f being PartFunc of A,REAL st A = [.a,b.] holds

ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st

( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) )

proof end;

theorem Th12: :: MESFUN14:12

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 F being Finite_Sep_Sequence of S

for a being FinSequence of ExtREAL

for n being Nat st f is_simple_func_in S & F,a are_Re-presentation_of f & n in dom F & not F . n = {} holds

a . n is Real

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for F being Finite_Sep_Sequence of S

for a being FinSequence of ExtREAL

for n being Nat st f is_simple_func_in S & F,a are_Re-presentation_of f & n in dom F & not F . n = {} holds

a . n is Real

proof end;

Lm3: for A being non empty closed_interval Subset of REAL

for n being Nat st n > 0 & vol A > 0 holds

ex D being Division of A st D divide_into_equal n

proof end;

definition

let A be non empty closed_interval Subset of REAL;

let n be Nat;

assume A1: ( n > 0 & vol A > 0 ) ;

existence

ex b_{1} being Division of A st b_{1} divide_into_equal n
by A1, Lm3;

uniqueness

for b_{1}, b_{2} being Division of A st b_{1} divide_into_equal n & b_{2} divide_into_equal n holds

b_{1} = b_{2}

end;
let n be Nat;

assume A1: ( n > 0 & vol A > 0 ) ;

existence

ex b

uniqueness

for b

b

proof end;

:: deftheorem Def1 defines EqDiv MESFUN14:def 1 :

for A being non empty closed_interval Subset of REAL

for n being Nat st n > 0 & vol A > 0 holds

for b_{3} being Division of A holds

( b_{3} = EqDiv (A,n) iff b_{3} divide_into_equal n );

for A being non empty closed_interval Subset of REAL

for n being Nat st n > 0 & vol A > 0 holds

for b

( b

theorem :: MESFUN14:13

for A being non empty closed_interval Subset of REAL

for n being Nat st vol A > 0 & len (EqDiv (A,(2 |^ n))) = 1 holds

n = 0

for n being Nat st vol A > 0 & len (EqDiv (A,(2 |^ n))) = 1 holds

n = 0

proof end;

theorem :: MESFUN14:14

for a, b being Real

for A being non empty closed_interval Subset of REAL st a < b & A = [.a,b.] holds

ex D being DivSequence of A st

for n being Nat holds D . n divide_into_equal 2 |^ n

for A being non empty closed_interval Subset of REAL st a < b & A = [.a,b.] holds

ex D being DivSequence of A st

for n being Nat holds D . n divide_into_equal 2 |^ n

proof end;

theorem Th15: :: MESFUN14:15

for A being non empty closed_interval Subset of REAL

for D being Division of A

for n, k being Nat st D divide_into_equal n & k in dom D holds

vol (divset (D,k)) = (vol A) / n

for D being Division of A

for n, k being Nat st D divide_into_equal n & k in dom D holds

vol (divset (D,k)) = (vol A) / n

proof end;

theorem Th17: :: MESFUN14:17

for A being non empty closed_interval Subset of REAL

for T being sequence of (divs A) st vol A > 0 & ( for n being Nat holds T . n = EqDiv (A,(2 |^ n)) ) holds

( delta T is 0 -convergent & delta T is non-zero )

for T being sequence of (divs A) st vol A > 0 & ( for n being Nat holds T . n = EqDiv (A,(2 |^ n)) ) holds

( delta T is 0 -convergent & delta T is non-zero )

proof end;

Lm4: for A being non empty closed_interval Subset of REAL

for n being Nat st vol A > 0 & len (EqDiv (A,(2 |^ n))) = 1 holds

divset ((EqDiv (A,(2 |^ n))),1) = A

proof end;

Lm5: for l being Real

for m, n being Nat st l > 1 & n <= m holds

( (l |^ n) * (l |^ (m -' n)) = l |^ m & (l |^ n) * ((l |^ (m -' n)) -' 1) < l |^ m )

proof end;

theorem Th18: :: MESFUN14:18

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f being PartFunc of X,ExtREAL

for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds

x . i = (a . i) * ((M * F) . i) ) holds

Integral (M,f) = Sum x

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f being PartFunc of X,ExtREAL

for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds

x . i = (a . i) * ((M * F) . i) ) holds

Integral (M,f) = Sum x

proof end;

theorem Th19: :: MESFUN14:19

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL

for D being Division of A st f is bounded & A c= dom f holds

ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st

( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.(inf A),(sup A).] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.(inf A),(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = lower_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = lower_sum (f,D) & ( for x being Real st x in A holds

( lower_bound (rng f) <= g . x & g . x <= f . x ) ) )

for f being PartFunc of A,REAL

for D being Division of A st f is bounded & A c= dom f holds

ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st

( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.(inf A),(sup A).] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.(inf A),(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = lower_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = lower_sum (f,D) & ( for x being Real st x in A holds

( lower_bound (rng f) <= g . x & g . x <= f . x ) ) )

proof end;

theorem Th20: :: MESFUN14:20

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL

for D being Division of A st f is bounded & A c= dom f holds

ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st

( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.(inf A),(sup A).] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.(inf A),(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = upper_sum (f,D) & ( for x being Real st x in A holds

( upper_bound (rng f) >= g . x & g . x >= f . x ) ) )

for f being PartFunc of A,REAL

for D being Division of A st f is bounded & A c= dom f holds

ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st

( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.(inf A),(sup A).] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.(inf A),(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) & dom g = A & Integral (B-Meas,g) = upper_sum (f,D) & ( for x being Real st x in A holds

( upper_bound (rng f) >= g . x & g . x >= f . x ) ) )

proof end;

theorem Th21: :: MESFUN14:21

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL st f is bounded & A c= dom f & vol A > 0 holds

ex F being with_the_same_dom Functional_Sequence of REAL,ExtREAL ex I being ExtREAL_sequence st

( A = dom (F . 0) & ( for n being Nat holds

( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds

( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds

for x being Element of REAL st x in A holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of REAL st x in A holds

( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) )

for f being PartFunc of A,REAL st f is bounded & A c= dom f & vol A > 0 holds

ex F being with_the_same_dom Functional_Sequence of REAL,ExtREAL ex I being ExtREAL_sequence st

( A = dom (F . 0) & ( for n being Nat holds

( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds

( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds

for x being Element of REAL st x in A holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of REAL st x in A holds

( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) )

proof end;

theorem Th22: :: MESFUN14:22

for A being non empty closed_interval Subset of REAL

for f being PartFunc of A,REAL st f is bounded & A c= dom f & vol A > 0 holds

ex F being with_the_same_dom Functional_Sequence of REAL,ExtREAL ex I being ExtREAL_sequence st

( A = dom (F . 0) & ( for n being Nat holds

( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = upper_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds

( upper_bound (rng f) >= (F . n) . x & (F . n) . x >= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds

for x being Element of REAL st x in A holds

(F . n) . x >= (F . m) . x ) & ( for x being Element of REAL st x in A holds

( F # x is convergent & lim (F # x) = inf (F # x) & inf (F # x) >= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) )

for f being PartFunc of A,REAL st f is bounded & A c= dom f & vol A > 0 holds

ex F being with_the_same_dom Functional_Sequence of REAL,ExtREAL ex I being ExtREAL_sequence st

( A = dom (F . 0) & ( for n being Nat holds

( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = upper_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds

( upper_bound (rng f) >= (F . n) . x & (F . n) . x >= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds

for x being Element of REAL st x in A holds

(F . n) . x >= (F . m) . x ) & ( for x being Element of REAL st x in A holds

( F # x is convergent & lim (F # x) = inf (F # x) & inf (F # x) >= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) )

proof end;

theorem Th23: :: MESFUN14:23

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 E being Element of S

for n being Nat st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds

M . (E /\ (great_eq_dom (f,(1 / (n + 1))))) = 0

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for E being Element of S

for n being Nat st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds

M . (E /\ (great_eq_dom (f,(1 / (n + 1))))) = 0

proof end;

theorem Th24: :: MESFUN14:24

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 E being Element of S st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds

M . (E /\ (great_dom (f,0))) = 0

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for E being Element of S st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds

M . (E /\ (great_dom (f,0))) = 0

proof end;

theorem Th25: :: MESFUN14:25

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,REAL

for E being Element of S st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds

f a.e.= (X --> 0) | E,M

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,REAL

for E being Element of S st E = dom f & f is nonnegative & f is E -measurable & Integral (M,f) = 0 holds

f a.e.= (X --> 0) | E,M

proof end;

theorem Th26: :: MESFUN14:26

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL

for E1 being Element of S st M is complete & f is E1 -measurable & f a.e.= g,M & E1 = dom f holds

g is E1 -measurable

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL

for E1 being Element of S st M is complete & f is E1 -measurable & f a.e.= g,M & E1 = dom f holds

g is E1 -measurable

proof end;

theorem Th27: :: MESFUN14:27

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S holds E is Element of COM (S,M)

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S holds E is Element of COM (S,M)

proof end;

theorem :: MESFUN14:28

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL st f a.e.= g,M holds

f a.e.= g, COM M

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL st f a.e.= g,M holds

f a.e.= g, COM M

proof end;

theorem Th30: :: MESFUN14:30

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E1 being Element of S

for E2 being Element of COM (S,M)

for f being PartFunc of X,ExtREAL st E1 = E2 & f is E1 -measurable holds

f is E2 -measurable

for S being SigmaField of X

for M being sigma_Measure of S

for E1 being Element of S

for E2 being Element of COM (S,M)

for f being PartFunc of X,ExtREAL st E1 = E2 & f is E1 -measurable holds

f is E2 -measurable

proof end;

theorem :: MESFUN14:31

for E1 being Element of Borel_Sets

for E2 being Element of L-Field

for f being PartFunc of REAL,ExtREAL st E1 = E2 & f is E1 -measurable holds

f is E2 -measurable by Th30, MEASUR12:def 11;

for E2 being Element of L-Field

for f being PartFunc of REAL,ExtREAL st E1 = E2 & f is E1 -measurable holds

f is E2 -measurable by Th30, MEASUR12:def 11;

theorem Th32: :: MESFUN14:32

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for F being Finite_Sep_Sequence of S holds F is Finite_Sep_Sequence of COM (S,M)

for S being SigmaField of X

for M being sigma_Measure of S

for F being Finite_Sep_Sequence of S holds F is Finite_Sep_Sequence of COM (S,M)

proof end;

theorem Th33: :: MESFUN14:33

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 st f is_simple_func_in S holds

f is_simple_func_in COM (S,M)

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds

f is_simple_func_in COM (S,M)

proof end;

theorem Th35: :: MESFUN14:35

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S holds M . E = (COM M) . E

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S holds M . E = (COM M) . E

proof end;

theorem Th36: :: MESFUN14:36

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 st f is_simple_func_in S & f is nonnegative holds

integral (M,f) = integral ((COM M),f)

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative holds

integral (M,f) = integral ((COM M),f)

proof end;

theorem Th37: :: MESFUN14:37

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 E being Element of S st E = dom f & f is E -measurable & f is nonnegative holds

integral+ (M,f) = integral+ ((COM M),f)

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for E being Element of S st E = dom f & f is E -measurable & f is nonnegative holds

integral+ (M,f) = integral+ ((COM M),f)

proof end;

theorem Th38: :: MESFUN14:38

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 st f is_integrable_on M holds

( f is_integrable_on COM M & Integral (M,f) = Integral ((COM M),f) )

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_integrable_on M holds

( f is_integrable_on COM M & Integral (M,f) = Integral ((COM M),f) )

proof end;

theorem :: MESFUN14:39

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f, g being PartFunc of X,REAL st ( E = dom f or E = dom g ) & f a.e.= g,M holds

f - g a.e.= (X --> 0) | E,M

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f, g being PartFunc of X,REAL st ( E = dom f or E = dom g ) & f a.e.= g,M holds

f - g a.e.= (X --> 0) | E,M

proof end;

theorem Th40: :: MESFUN14:40

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f, g being PartFunc of X,REAL st E = dom (f - g) & f - g a.e.= (X --> 0) | E,M holds

f | E a.e.= g | E,M

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f, g being PartFunc of X,REAL st E = dom (f - g) & f - g a.e.= (X --> 0) | E,M holds

f | E a.e.= g | E,M

proof end;

theorem Th41: :: MESFUN14:41

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f being PartFunc of X,REAL st E = dom f & M . E < +infty & f is bounded & f is E -measurable holds

f is_integrable_on M

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f being PartFunc of X,REAL st E = dom f & M . E < +infty & f is bounded & f is E -measurable holds

f is_integrable_on M

proof end;

theorem Th42: :: MESFUN14:42

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL holds

( f a.e.= g,M iff ( max+ f a.e.= max+ g,M & max- f a.e.= max- g,M ) )

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL holds

( f a.e.= g,M iff ( max+ f a.e.= max+ g,M & max- f a.e.= max- g,M ) )

proof end;

theorem Th43: :: MESFUN14:43

for X being non empty set

for f being PartFunc of X,REAL holds

( max+ (R_EAL f) = R_EAL (max+ f) & max- (R_EAL f) = R_EAL (max- f) )

for f being PartFunc of X,REAL holds

( max+ (R_EAL f) = R_EAL (max+ f) & max- (R_EAL f) = R_EAL (max- f) )

proof end;

theorem Th44: :: MESFUN14:44

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL

for E being Element of S st M is complete & f is_integrable_on M & f a.e.= g,M & E = dom f & E = dom g holds

( g is_integrable_on M & Integral (M,f) = Integral (M,g) )

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL

for E being Element of S st M is complete & f is_integrable_on M & f a.e.= g,M & E = dom f & E = dom g holds

( g is_integrable_on M & Integral (M,f) = Integral (M,g) )

proof end;

Lm6: for a being Real holds {a} is Element of Borel_Sets

proof end;

theorem Th45: :: MESFUN14:45

for f being PartFunc of REAL,ExtREAL

for a being Real st a in dom f holds

ex A being Element of Borel_Sets st

( A = {a} & f is A -measurable & f | A is_integrable_on B-Meas & Integral (B-Meas,(f | A)) = 0 )

for a being Real st a in dom f holds

ex A being Element of Borel_Sets st

( A = {a} & f is A -measurable & f | A is_integrable_on B-Meas & Integral (B-Meas,(f | A)) = 0 )

proof end;

theorem Th46: :: MESFUN14:46

for f being PartFunc of REAL,REAL

for a being Real st a in dom f holds

ex A being Element of Borel_Sets st

( A = {a} & f is A -measurable & f | A is_integrable_on B-Meas & Integral (B-Meas,(f | A)) = 0 )

for a being Real st a in dom f holds

ex A being Element of Borel_Sets st

( A = {a} & f is A -measurable & f | A is_integrable_on B-Meas & Integral (B-Meas,(f | A)) = 0 )

proof end;

theorem :: MESFUN14:47

for f being PartFunc of REAL,ExtREAL st f is_integrable_on B-Meas holds

( f is_integrable_on L-Meas & Integral (B-Meas,f) = Integral (L-Meas,f) ) by Th38, MEASUR12:def 11, MEASUR12:def 12;

( f is_integrable_on L-Meas & Integral (B-Meas,f) = Integral (L-Meas,f) ) by Th38, MEASUR12:def 11, MEASUR12:def 12;

theorem Th48: :: MESFUN14:48

for f being PartFunc of REAL,REAL st f is_integrable_on B-Meas holds

( f is_integrable_on L-Meas & Integral (B-Meas,f) = Integral (L-Meas,f) )

( f is_integrable_on L-Meas & Integral (B-Meas,f) = Integral (L-Meas,f) )

proof end;

theorem Th49: :: MESFUN14:49

for A being non empty closed_interval Subset of REAL

for A1 being Element of L-Field

for f being PartFunc of REAL,REAL st A = A1 & A c= dom f & f || A is bounded & f is_integrable_on A holds

( f is A1 -measurable & f | A1 is_integrable_on L-Meas & integral (f || A) = Integral (L-Meas,(f | A)) )

for A1 being Element of L-Field

for f being PartFunc of REAL,REAL st A = A1 & A c= dom f & f || A is bounded & f is_integrable_on A holds

( f is A1 -measurable & f | A1 is_integrable_on L-Meas & integral (f || A) = Integral (L-Meas,(f | A)) )

proof end;

theorem :: MESFUN14:50

for a, b being Real

for f being PartFunc of REAL,REAL st a <= b & [.a,b.] c= dom f & f || ['a,b'] is bounded & f is_integrable_on ['a,b'] holds

integral (f,a,b) = Integral (L-Meas,(f | [.a,b.]))

for f being PartFunc of REAL,REAL st a <= b & [.a,b.] c= dom f & f || ['a,b'] is bounded & f is_integrable_on ['a,b'] holds

integral (f,a,b) = Integral (L-Meas,(f | [.a,b.]))

proof end;