:: by Yasunari Shidama and Noboru Endou

::

:: Received October 27, 2006

:: Copyright (c) 2006-2021 Association of Mizar Users

theorem Th2: :: MESFUNC6:2

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 & ( for x being object st x in dom f holds

f . x = r ) holds

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

for r being Real st dom f in S & ( for x being object st x in dom f holds

f . x = r ) holds

f is_simple_func_in S

proof end;

theorem :: MESFUNC6:3

for X being non empty set

for f being PartFunc of X,REAL

for a being Real

for x being set holds

( x in less_dom (f,a) iff ( x in dom f & ex y being Real st

( y = f . x & y < a ) ) )

for f being PartFunc of X,REAL

for a being Real

for x being set holds

( x in less_dom (f,a) iff ( x in dom f & ex y being Real st

( y = f . x & y < a ) ) )

proof end;

theorem :: MESFUNC6:4

for X being non empty set

for f being PartFunc of X,REAL

for a being Real

for x being set holds

( x in less_eq_dom (f,a) iff ( x in dom f & ex y being Real st

( y = f . x & y <= a ) ) )

for f being PartFunc of X,REAL

for a being Real

for x being set holds

( x in less_eq_dom (f,a) iff ( x in dom f & ex y being Real st

( y = f . x & y <= a ) ) )

proof end;

theorem :: MESFUNC6:5

for X being non empty set

for f being PartFunc of X,REAL

for r being Real

for x being set holds

( x in great_dom (f,r) iff ( x in dom f & ex y being Real st

( y = f . x & r < y ) ) )

for f being PartFunc of X,REAL

for r being Real

for x being set holds

( x in great_dom (f,r) iff ( x in dom f & ex y being Real st

( y = f . x & r < y ) ) )

proof end;

theorem :: MESFUNC6:6

for X being non empty set

for f being PartFunc of X,REAL

for r being Real

for x being set holds

( x in great_eq_dom (f,r) iff ( x in dom f & ex y being Real st

( y = f . x & r <= y ) ) )

for f being PartFunc of X,REAL

for r being Real

for x being set holds

( x in great_eq_dom (f,r) iff ( x in dom f & ex y being Real st

( y = f . x & r <= y ) ) )

proof end;

theorem :: MESFUNC6:7

for X being non empty set

for f being PartFunc of X,REAL

for r being Real

for x being set holds

( x in eq_dom (f,r) iff ( x in dom f & ex y being Real st

( y = f . x & r = y ) ) )

for f being PartFunc of X,REAL

for r being Real

for x being set holds

( x in eq_dom (f,r) iff ( x in dom f & ex y being Real st

( y = f . x & r = y ) ) )

proof end;

theorem :: MESFUNC6:8

for X being non empty set

for Y being set

for S being SigmaField of X

for F being sequence of S

for f being PartFunc of X,REAL

for r being Real st ( for n being Nat holds F . n = Y /\ (great_dom (f,(r - (1 / (n + 1))))) ) holds

Y /\ (great_eq_dom (f,r)) = meet (rng F)

for Y being set

for S being SigmaField of X

for F being sequence of S

for f being PartFunc of X,REAL

for r being Real st ( for n being Nat holds F . n = Y /\ (great_dom (f,(r - (1 / (n + 1))))) ) holds

Y /\ (great_eq_dom (f,r)) = meet (rng F)

proof end;

theorem :: MESFUNC6:9

for X being non empty set

for Y being set

for S being SigmaField of X

for F being sequence of S

for f being PartFunc of X,REAL

for r being Real st ( for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds

Y /\ (less_eq_dom (f,r)) = meet (rng F)

for Y being set

for S being SigmaField of X

for F being sequence of S

for f being PartFunc of X,REAL

for r being Real st ( for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds

Y /\ (less_eq_dom (f,r)) = meet (rng F)

proof end;

theorem :: MESFUNC6:10

for X being non empty set

for Y being set

for S being SigmaField of X

for F being sequence of S

for f being PartFunc of X,REAL

for r being Real st ( for n being Nat holds F . n = Y /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) holds

Y /\ (less_dom (f,r)) = union (rng F)

for Y being set

for S being SigmaField of X

for F being sequence of S

for f being PartFunc of X,REAL

for r being Real st ( for n being Nat holds F . n = Y /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) holds

Y /\ (less_dom (f,r)) = union (rng F)

proof end;

theorem :: MESFUNC6:11

for X being non empty set

for Y being set

for S being SigmaField of X

for F being sequence of S

for f being PartFunc of X,REAL

for r being Real st ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) holds

Y /\ (great_dom (f,r)) = union (rng F)

for Y being set

for S being SigmaField of X

for F being sequence of S

for f being PartFunc of X,REAL

for r being Real st ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) holds

Y /\ (great_dom (f,r)) = union (rng F)

proof end;

definition
end;

:: deftheorem defines -measurable MESFUNC6:def 1 :

for X being non empty set

for S being SigmaField of X

for A being Element of S

for f being PartFunc of X,REAL holds

( f is A -measurable iff R_EAL f is A -measurable );

for X being non empty set

for S being SigmaField of X

for A being Element of S

for f being PartFunc of X,REAL holds

( f is A -measurable iff R_EAL f is A -measurable );

theorem Th12: :: MESFUNC6:12

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S holds

( f is A -measurable iff for r being Real holds A /\ (less_dom (f,r)) in S ) by MESFUNC1:def 16;

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S holds

( f is A -measurable iff for r being Real holds A /\ (less_dom (f,r)) in S ) by MESFUNC1:def 16;

theorem Th13: :: MESFUNC6:13

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S st A c= dom f holds

( f is A -measurable iff for r being Real holds A /\ (great_eq_dom (f,r)) in S ) by MESFUNC1:27;

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S st A c= dom f holds

( f is A -measurable iff for r being Real holds A /\ (great_eq_dom (f,r)) in S ) by MESFUNC1:27;

theorem :: MESFUNC6:14

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S holds

( f is A -measurable iff for r being Real holds A /\ (less_eq_dom (f,r)) in S ) by MESFUNC1:28;

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S holds

( f is A -measurable iff for r being Real holds A /\ (less_eq_dom (f,r)) in S ) by MESFUNC1:28;

theorem :: MESFUNC6:15

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S st A c= dom f holds

( f is A -measurable iff for r being Real holds A /\ (great_dom (f,r)) in S ) by MESFUNC1:29;

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S st A c= dom f holds

( f is A -measurable iff for r being Real holds A /\ (great_dom (f,r)) in S ) by MESFUNC1:29;

theorem :: MESFUNC6:16

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL

for A, B being Element of S st B c= A & f is A -measurable holds

f is B -measurable by MESFUNC1:30;

for S being SigmaField of X

for f being PartFunc of X,REAL

for A, B being Element of S st B c= A & f is A -measurable holds

f is B -measurable by MESFUNC1:30;

theorem :: MESFUNC6:17

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL

for A, B being Element of S st f is A -measurable & f is B -measurable holds

f is A \/ B -measurable by MESFUNC1:31;

for S being SigmaField of X

for f being PartFunc of X,REAL

for A, B being Element of S st f is A -measurable & f is B -measurable holds

f is A \/ B -measurable by MESFUNC1:31;

theorem :: MESFUNC6:18

theorem :: MESFUNC6:19

for X being non empty set

for S being SigmaField of X

for f, g being PartFunc of X,REAL

for A being Element of S

for r being Real st f is A -measurable & g is A -measurable & A c= dom g holds

(A /\ (less_dom (f,r))) /\ (great_dom (g,r)) in S by MESFUNC1:36;

for S being SigmaField of X

for f, g being PartFunc of X,REAL

for A being Element of S

for r being Real st f is A -measurable & g is A -measurable & A c= dom g holds

(A /\ (less_dom (f,r))) /\ (great_dom (g,r)) in S by MESFUNC1:36;

theorem Th20: :: MESFUNC6:20

for X being non empty set

for f being PartFunc of X,REAL

for r being Real holds R_EAL (r (#) f) = r (#) (R_EAL f)

for f being PartFunc of X,REAL

for r being Real holds R_EAL (r (#) f) = r (#) (R_EAL f)

proof end;

theorem Th21: :: MESFUNC6:21

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S

for r being Real st f is A -measurable & A c= dom f holds

r (#) f is A -measurable

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S

for r being Real st f is A -measurable & A c= dom f holds

r (#) f is A -measurable

proof end;

theorem :: MESFUNC6:22

theorem Th23: :: MESFUNC6:23

for X being non empty set

for f, g being PartFunc of X,REAL holds

( R_EAL (f + g) = (R_EAL f) + (R_EAL g) & R_EAL (f - g) = (R_EAL f) - (R_EAL g) & dom (R_EAL (f + g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f - g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f + g)) = (dom f) /\ (dom g) & dom (R_EAL (f - g)) = (dom f) /\ (dom g) )

for f, g being PartFunc of X,REAL holds

( R_EAL (f + g) = (R_EAL f) + (R_EAL g) & R_EAL (f - g) = (R_EAL f) - (R_EAL g) & dom (R_EAL (f + g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f - g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f + g)) = (dom f) /\ (dom g) & dom (R_EAL (f - g)) = (dom f) /\ (dom g) )

proof end;

theorem :: MESFUNC6:24

for X being non empty set

for S being SigmaField of X

for f, g being PartFunc of X,REAL

for A being Element of S

for r being Real

for F being Function of RAT,S st ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds

A /\ (less_dom ((f + g),r)) = union (rng F)

for S being SigmaField of X

for f, g being PartFunc of X,REAL

for A being Element of S

for r being Real

for F being Function of RAT,S st ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds

A /\ (less_dom ((f + g),r)) = union (rng F)

proof end;

theorem :: MESFUNC6:25

for X being non empty set

for S being SigmaField of X

for f, g being PartFunc of X,REAL

for A being Element of S

for r being Real st f is A -measurable & g is A -measurable holds

ex F being Function of RAT,S st

for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) by MESFUNC2:6;

for S being SigmaField of X

for f, g being PartFunc of X,REAL

for A being Element of S

for r being Real st f is A -measurable & g is A -measurable holds

ex F being Function of RAT,S st

for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) by MESFUNC2:6;

theorem Th26: :: MESFUNC6:26

for X being non empty set

for S being SigmaField of X

for f, g being PartFunc of X,REAL

for A being Element of S st f is A -measurable & g is A -measurable holds

f + g is A -measurable

for S being SigmaField of X

for f, g being PartFunc of X,REAL

for A being Element of S st f is A -measurable & g is A -measurable holds

f + g is A -measurable

proof end;

theorem :: MESFUNC6:27

for X being non empty set

for f, g being PartFunc of X,REAL holds (R_EAL f) - (R_EAL g) = (R_EAL f) + (R_EAL (- g))

for f, g being PartFunc of X,REAL holds (R_EAL f) - (R_EAL g) = (R_EAL f) + (R_EAL (- g))

proof end;

theorem Th28: :: MESFUNC6:28

for X being non empty set

for f being PartFunc of X,REAL holds

( - (R_EAL f) = R_EAL ((- 1) (#) f) & - (R_EAL f) = R_EAL (- f) )

for f being PartFunc of X,REAL holds

( - (R_EAL f) = R_EAL ((- 1) (#) f) & - (R_EAL f) = R_EAL (- f) )

proof end;

theorem :: MESFUNC6:29

for X being non empty set

for S being SigmaField of X

for f, g being PartFunc of X,REAL

for A being Element of S st f is A -measurable & g is A -measurable & A c= dom g holds

f - g is A -measurable

for S being SigmaField of X

for f, g being PartFunc of X,REAL

for A being Element of S st f is A -measurable & g is A -measurable & A c= dom g holds

f - g is A -measurable

proof end;

theorem Th30: :: MESFUNC6:30

for X being non empty set

for f being PartFunc of X,REAL holds

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

for f being PartFunc of X,REAL holds

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

proof end;

theorem :: MESFUNC6:31

for X being non empty set

for f being PartFunc of X,REAL

for x being Element of X holds 0 <= (max+ f) . x

for f being PartFunc of X,REAL

for x being Element of X holds 0 <= (max+ f) . x

proof end;

theorem :: MESFUNC6:32

for X being non empty set

for f being PartFunc of X,REAL

for x being Element of X holds 0 <= (max- f) . x

for f being PartFunc of X,REAL

for x being Element of X holds 0 <= (max- f) . x

proof end;

theorem :: MESFUNC6:34

for X being non empty set

for f being PartFunc of X,REAL

for x being set st x in dom f & 0 < (max+ f) . x holds

(max- f) . x = 0

for f being PartFunc of X,REAL

for x being set st x in dom f & 0 < (max+ f) . x holds

(max- f) . x = 0

proof end;

theorem :: MESFUNC6:35

for X being non empty set

for f being PartFunc of X,REAL

for x being set st x in dom f & 0 < (max- f) . x holds

(max+ f) . x = 0

for f being PartFunc of X,REAL

for x being set st x in dom f & 0 < (max- f) . x holds

(max+ f) . x = 0

proof end;

theorem :: MESFUNC6:36

for X being non empty set

for f being PartFunc of X,REAL holds

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

for f being PartFunc of X,REAL holds

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

proof end;

theorem :: MESFUNC6:37

for X being non empty set

for f being PartFunc of X,REAL

for x being set st x in dom f holds

( ( (max+ f) . x = f . x or (max+ f) . x = 0 ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) )

for f being PartFunc of X,REAL

for x being set st x in dom f holds

( ( (max+ f) . x = f . x or (max+ f) . x = 0 ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) )

proof end;

theorem :: MESFUNC6:38

for X being non empty set

for f being PartFunc of X,REAL

for x being set st x in dom f & (max+ f) . x = f . x holds

(max- f) . x = 0

for f being PartFunc of X,REAL

for x being set st x in dom f & (max+ f) . x = f . x holds

(max- f) . x = 0

proof end;

theorem :: MESFUNC6:39

for X being non empty set

for f being PartFunc of X,REAL

for x being set st x in dom f & (max+ f) . x = 0 holds

(max- f) . x = - (f . x)

for f being PartFunc of X,REAL

for x being set st x in dom f & (max+ f) . x = 0 holds

(max- f) . x = - (f . x)

proof end;

theorem :: MESFUNC6:40

for X being non empty set

for f being PartFunc of X,REAL

for x being set st x in dom f & (max- f) . x = - (f . x) holds

(max+ f) . x = 0

for f being PartFunc of X,REAL

for x being set st x in dom f & (max- f) . x = - (f . x) holds

(max+ f) . x = 0

proof end;

theorem :: MESFUNC6:41

for X being non empty set

for f being PartFunc of X,REAL

for x being set st x in dom f & (max- f) . x = 0 holds

(max+ f) . x = f . x

for f being PartFunc of X,REAL

for x being set st x in dom f & (max- f) . x = 0 holds

(max+ f) . x = f . x

proof end;

theorem Th46: :: MESFUNC6:46

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S st f is A -measurable holds

max+ f is A -measurable

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S st f is A -measurable holds

max+ f is A -measurable

proof end;

theorem Th47: :: MESFUNC6:47

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S st f is A -measurable & A c= dom f holds

max- f is A -measurable

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S st f is A -measurable & A c= dom f holds

max- f is A -measurable

proof end;

theorem :: MESFUNC6:48

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S st f is A -measurable & A c= dom f holds

abs f is A -measurable

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S st f is A -measurable & A c= dom f holds

abs f is A -measurable

proof end;

:: deftheorem defines is_simple_func_in MESFUNC6:def 2 :

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL holds

( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S st

( dom f = union (rng F) & ( for n being Nat

for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

f . x = f . y ) ) );

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL holds

( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S st

( dom f = union (rng F) & ( for n being Nat

for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

f . x = f . y ) ) );

theorem Th49: :: MESFUNC6:49

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL holds

( f is_simple_func_in S iff R_EAL f is_simple_func_in S ) by MESFUNC2:def 4;

for S being SigmaField of X

for f being PartFunc of X,REAL holds

( f is_simple_func_in S iff R_EAL f is_simple_func_in S ) by MESFUNC2:def 4;

theorem :: MESFUNC6:50

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S st f is_simple_func_in S holds

f is A -measurable by Th49, MESFUNC2:34;

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S st f is_simple_func_in S holds

f is A -measurable by Th49, MESFUNC2:34;

theorem Th51: :: MESFUNC6:51

for X being set

for f being PartFunc of X,REAL holds

( f is nonnegative iff for x being object holds 0 <= f . x )

for f being PartFunc of X,REAL holds

( f is nonnegative iff for x being object holds 0 <= f . x )

proof end;

theorem Th52: :: MESFUNC6:52

for X being set

for f being PartFunc of X,REAL st ( for x being object st x in dom f holds

0 <= f . x ) holds

f is nonnegative

for f being PartFunc of X,REAL st ( for x being object st x in dom f holds

0 <= f . x ) holds

f is nonnegative

proof end;

theorem :: MESFUNC6:53

for X being set

for f being PartFunc of X,REAL holds

( f is nonpositive iff for x being set holds f . x <= 0 )

for f being PartFunc of X,REAL holds

( f is nonpositive iff for x being set holds f . x <= 0 )

proof end;

theorem Th54: :: MESFUNC6:54

for X being non empty set

for f being PartFunc of X,REAL st ( for x being object st x in dom f holds

f . x <= 0 ) holds

f is nonpositive

for f being PartFunc of X,REAL st ( for x being object st x in dom f holds

f . x <= 0 ) holds

f is nonpositive

proof end;

theorem :: MESFUNC6:55

for X being non empty set

for Y being set

for f being PartFunc of X,REAL st f is nonnegative holds

f | Y is nonnegative

for Y being set

for f being PartFunc of X,REAL st f is nonnegative holds

f | Y is nonnegative

proof end;

theorem Th56: :: MESFUNC6:56

for X being non empty set

for f, g being PartFunc of X,REAL st f is nonnegative & g is nonnegative holds

f + g is nonnegative

for f, g being PartFunc of X,REAL st f is nonnegative & g is nonnegative holds

f + g is nonnegative

proof end;

theorem :: MESFUNC6:57

for X being non empty set

for f being PartFunc of X,REAL

for r being Real st f is nonnegative holds

( ( 0 <= r implies r (#) f is nonnegative ) & ( r <= 0 implies r (#) f is nonpositive ) )

for f being PartFunc of X,REAL

for r being Real st f is nonnegative holds

( ( 0 <= r implies r (#) f is nonnegative ) & ( r <= 0 implies r (#) f is nonpositive ) )

proof end;

theorem Th58: :: MESFUNC6:58

for X being non empty set

for f, g being PartFunc of X,REAL st ( for x being set st x in (dom f) /\ (dom g) holds

g . x <= f . x ) holds

f - g is nonnegative

for f, g being PartFunc of X,REAL st ( for x being set st x in (dom f) /\ (dom g) holds

g . x <= f . x ) holds

f - g is nonnegative

proof end;

theorem :: MESFUNC6:59

for X being non empty set

for f, g, h being PartFunc of X,REAL st f is nonnegative & g is nonnegative & h is nonnegative holds

(f + g) + h is nonnegative

for f, g, h being PartFunc of X,REAL st f is nonnegative & g is nonnegative & h is nonnegative holds

(f + g) + h is nonnegative

proof end;

theorem Th60: :: MESFUNC6:60

for X being non empty set

for f, g, h being PartFunc of X,REAL

for x being object st x in dom ((f + g) + h) holds

((f + g) + h) . x = ((f . x) + (g . x)) + (h . x)

for f, g, h being PartFunc of X,REAL

for x being object st x in dom ((f + g) + h) holds

((f + g) + h) . x = ((f . x) + (g . x)) + (h . x)

proof end;

theorem :: MESFUNC6:61

for X being non empty set

for f being PartFunc of X,REAL holds

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

for f being PartFunc of X,REAL holds

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

proof end;

theorem Th62: :: MESFUNC6:62

for X being non empty set

for f, g being PartFunc of X,REAL holds

( dom ((max+ (f + g)) + (max- f)) = (dom f) /\ (dom g) & dom ((max- (f + g)) + (max+ f)) = (dom f) /\ (dom g) & dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) & dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) & (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative )

for f, g being PartFunc of X,REAL holds

( dom ((max+ (f + g)) + (max- f)) = (dom f) /\ (dom g) & dom ((max- (f + g)) + (max+ f)) = (dom f) /\ (dom g) & dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) & dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) & (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative )

proof end;

theorem :: MESFUNC6:63

for X being non empty set

for f, g being PartFunc of X,REAL holds ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g)

for f, g being PartFunc of X,REAL holds ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g)

proof end;

theorem :: MESFUNC6:64

for X being non empty set

for f being PartFunc of X,REAL

for r being Real st 0 <= r holds

( max+ (r (#) f) = r (#) (max+ f) & max- (r (#) f) = r (#) (max- f) )

for f being PartFunc of X,REAL

for r being Real st 0 <= r holds

( max+ (r (#) f) = r (#) (max+ f) & max- (r (#) f) = r (#) (max- f) )

proof end;

theorem :: MESFUNC6:65

for X being non empty set

for f being PartFunc of X,REAL

for r being Real st 0 <= r holds

( max+ ((- r) (#) f) = r (#) (max- f) & max- ((- r) (#) f) = r (#) (max+ f) )

for f being PartFunc of X,REAL

for r being Real st 0 <= r holds

( max+ ((- r) (#) f) = r (#) (max- f) & max- ((- r) (#) f) = r (#) (max+ f) )

proof end;

theorem :: MESFUNC6:66

for X being non empty set

for Y being set

for f being PartFunc of X,REAL holds

( max+ (f | Y) = (max+ f) | Y & max- (f | Y) = (max- f) | Y )

for Y being set

for f being PartFunc of X,REAL holds

( max+ (f | Y) = (max+ f) | Y & max- (f | Y) = (max- f) | Y )

proof end;

theorem :: MESFUNC6:67

for X being non empty set

for Y being set

for f, g being PartFunc of X,REAL st Y c= dom (f + g) holds

( dom ((f + g) | Y) = Y & dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) )

for Y being set

for f, g being PartFunc of X,REAL st Y c= dom (f + g) holds

( dom ((f + g) | Y) = Y & dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) )

proof end;

theorem :: MESFUNC6:68

for X being non empty set

for f being PartFunc of X,REAL

for r being Real holds eq_dom (f,r) = f " {r}

for f being PartFunc of X,REAL

for r being Real holds eq_dom (f,r) = f " {r}

proof end;

theorem :: MESFUNC6:69

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S

for r, s being Real st f is A -measurable & A c= dom f holds

(A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S

for r, s being Real st f is A -measurable & A c= dom f holds

(A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S

proof end;

theorem Th70: :: MESFUNC6:70

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S st f is_simple_func_in S holds

f | A is_simple_func_in S

for S being SigmaField of X

for f being PartFunc of X,REAL

for A being Element of S st f is_simple_func_in S holds

f | A is_simple_func_in S

proof end;

theorem Th71: :: MESFUNC6:71

for X being non empty set

for S being SigmaField of X

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

dom f is Element of S by MESFUNC2:31;

for S being SigmaField of X

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

dom f is Element of S by MESFUNC2:31;

Lm1: 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 is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f holds

( f + g is_simple_func_in S & dom (f + g) <> {} )

proof end;

theorem :: MESFUNC6:72

for X being non empty set

for S being SigmaField of X

for f, g being PartFunc of X,REAL st f is_simple_func_in S & g is_simple_func_in S holds

f + g is_simple_func_in S

for S being SigmaField of X

for f, g being PartFunc of X,REAL st f is_simple_func_in S & g is_simple_func_in S holds

f + g is_simple_func_in S

proof end;

theorem :: MESFUNC6:73

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL

for r being Real st f is_simple_func_in S holds

r (#) f is_simple_func_in S

for S being SigmaField of X

for f being PartFunc of X,REAL

for r being Real st f is_simple_func_in S holds

r (#) f is_simple_func_in S

proof end;

theorem :: MESFUNC6:74

for X being non empty set

for f, g being PartFunc of X,REAL st ( for x being set st x in dom (f - g) holds

g . x <= f . x ) holds

f - g is nonnegative

for f, g being PartFunc of X,REAL st ( for x being set st x in dom (f - g) holds

g . x <= f . x ) holds

f - g is nonnegative

proof end;

theorem :: MESFUNC6:75

for X being non empty set

for S being SigmaField of X

for A being Element of S

for r being Real ex f being PartFunc of X,REAL st

( f is_simple_func_in S & dom f = A & ( for x being object st x in A holds

f . x = r ) )

for S being SigmaField of X

for A being Element of S

for r being Real ex f being PartFunc of X,REAL st

( f is_simple_func_in S & dom f = A & ( for x being object st x in A holds

f . x = r ) )

proof end;

theorem :: MESFUNC6:76

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL

for A, B being Element of S st f is B -measurable & A = (dom f) /\ B holds

f | B is A -measurable

for S being SigmaField of X

for f being PartFunc of X,REAL

for A, B being Element of S st f is B -measurable & A = (dom f) /\ B holds

f | B is A -measurable

proof end;

theorem :: MESFUNC6:77

for X being non empty set

for S being SigmaField of X

for f, g being PartFunc of X,REAL

for A being Element of S st A c= dom f & f is A -measurable & g is A -measurable holds

(max+ (f + g)) + (max- f) is A -measurable

for S being SigmaField of X

for f, g being PartFunc of X,REAL

for A being Element of S st A c= dom f & f is A -measurable & g is A -measurable holds

(max+ (f + g)) + (max- f) is A -measurable

proof end;

theorem :: MESFUNC6:78

for X being non empty set

for S being SigmaField of X

for f, g being PartFunc of X,REAL

for A being Element of S st A c= (dom f) /\ (dom g) & f is A -measurable & g is A -measurable holds

(max- (f + g)) + (max+ f) is A -measurable

for S being SigmaField of X

for f, g being PartFunc of X,REAL

for A being Element of S st A c= (dom f) /\ (dom g) & f is A -measurable & g is A -measurable holds

(max- (f + g)) + (max+ f) is A -measurable

proof end;

theorem :: MESFUNC6:79

for X being non empty set

for S being SigmaField of X

for f, g being PartFunc of X,REAL st dom f in S & dom g in S holds

dom (f + g) in S

for S being SigmaField of X

for f, g being PartFunc of X,REAL st dom f in S & dom g in S holds

dom (f + g) in S

proof end;

theorem Th80: :: MESFUNC6:80

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL

for A, B being Element of S st dom f = A holds

( f is B -measurable iff f is A /\ B -measurable )

for S being SigmaField of X

for f being PartFunc of X,REAL

for A, B being Element of S st dom f = A holds

( f is B -measurable iff f is A /\ B -measurable )

proof end;

theorem :: MESFUNC6:81

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL st ex A being Element of S st dom f = A holds

for c being Real

for B being Element of S st f is B -measurable holds

c (#) f is B -measurable

for S being SigmaField of X

for f being PartFunc of X,REAL st ex A being Element of S st dom f = A holds

for c being Real

for B being Element of S st f is B -measurable holds

c (#) f is B -measurable

proof end;

definition

let X be non empty set ;

let S be SigmaField of X;

let M be sigma_Measure of S;

let f be PartFunc of X,REAL;

coherence

Integral (M,(R_EAL f)) is Element of ExtREAL ;

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

let f be PartFunc of X,REAL;

coherence

Integral (M,(R_EAL f)) is Element of ExtREAL ;

:: deftheorem defines Integral MESFUNC6:def 3 :

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 holds Integral (M,f) = Integral (M,(R_EAL f));

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 holds Integral (M,f) = Integral (M,(R_EAL f));

theorem Th82: :: MESFUNC6:82

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 st ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

Integral (M,f) = integral+ (M,(R_EAL f)) by MESFUNC5:88;

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,REAL st ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

Integral (M,f) = integral+ (M,(R_EAL f)) by MESFUNC5:88;

theorem :: MESFUNC6:83

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

( Integral (M,f) = integral+ (M,(R_EAL f)) & Integral (M,f) = integral' (M,(R_EAL f)) )

for S being SigmaField of X

for M being sigma_Measure of S

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

( Integral (M,f) = integral+ (M,(R_EAL f)) & Integral (M,f) = integral' (M,(R_EAL f)) )

proof end;

theorem :: MESFUNC6:84

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 st ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

0 <= Integral (M,f) by MESFUNC5:90;

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,REAL st ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

0 <= Integral (M,f) by MESFUNC5:90;

theorem :: MESFUNC6:85

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 A, B being Element of S st ex E being Element of S st

( E = dom f & f is E -measurable ) & f is nonnegative & A misses B holds

Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by MESFUNC5:91;

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,REAL

for A, B being Element of S st ex E being Element of S st

( E = dom f & f is E -measurable ) & f is nonnegative & A misses B holds

Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by MESFUNC5:91;

theorem :: MESFUNC6:86

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

( E = dom f & f is E -measurable ) & f is nonnegative holds

0 <= Integral (M,(f | A)) by MESFUNC5:92;

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,REAL

for A being Element of S st ex E being Element of S st

( E = dom f & f is E -measurable ) & f is nonnegative holds

0 <= Integral (M,(f | A)) by MESFUNC5:92;

theorem :: MESFUNC6:87

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 A, B being Element of S st ex E being Element of S st

( E = dom f & f is E -measurable ) & f is nonnegative & A c= B holds

Integral (M,(f | A)) <= Integral (M,(f | B)) by MESFUNC5:93;

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,REAL

for A, B being Element of S st ex E being Element of S st

( E = dom f & f is E -measurable ) & f is nonnegative & A c= B holds

Integral (M,(f | A)) <= Integral (M,(f | B)) by MESFUNC5:93;

theorem :: MESFUNC6:88

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

( E = dom f & f is E -measurable ) & M . A = 0 holds

Integral (M,(f | A)) = 0 by MESFUNC5:94;

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,REAL

for A being Element of S st ex E being Element of S st

( E = dom f & f is E -measurable ) & M . A = 0 holds

Integral (M,(f | A)) = 0 by MESFUNC5:94;

theorem :: MESFUNC6:89

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

Integral (M,(f | (E \ A))) = Integral (M,f) by MESFUNC5:95;

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,REAL

for E, A being Element of S st E = dom f & f is E -measurable & M . A = 0 holds

Integral (M,(f | (E \ A))) = Integral (M,f) by MESFUNC5:95;

definition

let X be non empty set ;

let S be SigmaField of X;

let M be sigma_Measure of S;

let f be PartFunc of X,REAL;

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

let f be PartFunc of X,REAL;

:: deftheorem defines is_integrable_on MESFUNC6:def 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,REAL holds

( f is_integrable_on M iff R_EAL f is_integrable_on M );

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 holds

( f is_integrable_on M iff R_EAL f is_integrable_on M );

theorem :: MESFUNC6:90

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

( -infty < Integral (M,f) & Integral (M,f) < +infty ) by MESFUNC5:96;

for S being SigmaField of X

for M being sigma_Measure of S

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

( -infty < Integral (M,f) & Integral (M,f) < +infty ) by MESFUNC5:96;

theorem :: MESFUNC6:91

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 A being Element of S st f is_integrable_on M holds

f | A is_integrable_on M by MESFUNC5:97;

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,REAL

for A being Element of S st f is_integrable_on M holds

f | A is_integrable_on M by MESFUNC5:97;

theorem :: MESFUNC6:92

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 A, B being Element of S st f is_integrable_on M & A misses B holds

Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by MESFUNC5:98;

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,REAL

for A, B being Element of S st f is_integrable_on M & A misses B holds

Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by MESFUNC5:98;

theorem :: MESFUNC6:93

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 A, B being Element of S st f is_integrable_on M & B = (dom f) \ A holds

( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) ) by MESFUNC5:99;

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,REAL

for A, B being Element of S st f is_integrable_on M & B = (dom f) \ A holds

( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) ) by MESFUNC5:99;

theorem :: MESFUNC6:94

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 st ex A being Element of S st

( A = dom f & f is A -measurable ) holds

( f is_integrable_on M iff abs f is_integrable_on M )

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,REAL st ex A being Element of S st

( A = dom f & f is A -measurable ) holds

( f is_integrable_on M iff abs f is_integrable_on M )

proof end;

theorem :: MESFUNC6:95

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

|.(Integral (M,f)).| <= Integral (M,(abs f))

for S being SigmaField of X

for M being sigma_Measure of S

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

|.(Integral (M,f)).| <= Integral (M,(abs f))

proof end;

theorem :: MESFUNC6:96

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 ex A being Element of S st

( A = dom f & f is A -measurable ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds

|.(f . x).| <= g . x ) holds

( f is_integrable_on M & Integral (M,(abs 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 st ex A being Element of S st

( A = dom f & f is A -measurable ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds

|.(f . x).| <= g . x ) holds

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

proof end;

theorem :: MESFUNC6:97

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

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 :: MESFUNC6:98

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 is_integrable_on M & g is_integrable_on M & f is nonnegative & g is nonnegative holds

f + g is_integrable_on M

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M & f is nonnegative & g is nonnegative holds

f + g is_integrable_on M

proof end;

theorem :: MESFUNC6:99

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 is_integrable_on M & g is_integrable_on M holds

dom (f + g) in S

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds

dom (f + g) in S

proof end;

theorem :: MESFUNC6:100

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 is_integrable_on M & g is_integrable_on M holds

f + g is_integrable_on M

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds

f + g is_integrable_on M

proof end;

theorem :: MESFUNC6:101

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 is_integrable_on M & g is_integrable_on M holds

ex E being Element of S st

( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds

ex E being Element of S st

( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )

proof end;

theorem :: MESFUNC6:102

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

( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) )

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,REAL

for r being Real st f is_integrable_on M holds

( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) )

proof end;

definition

let X be non empty set ;

let S be SigmaField of X;

let M be sigma_Measure of S;

let f be PartFunc of X,REAL;

let B be Element of S;

coherence

Integral (M,(f | B)) is Element of ExtREAL ;

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

let f be PartFunc of X,REAL;

let B be Element of S;

coherence

Integral (M,(f | B)) is Element of ExtREAL ;

:: deftheorem defines Integral_on MESFUNC6:def 5 :

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 B being Element of S holds Integral_on (M,B,f) = Integral (M,(f | B));

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 B being Element of S holds Integral_on (M,B,f) = Integral (M,(f | B));

theorem :: MESFUNC6:103

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 B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds

( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL

for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds

( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )

proof end;

theorem :: MESFUNC6:104

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 r being Real

for B being Element of S st f is_integrable_on M holds

( f | B is_integrable_on M & Integral_on (M,B,(r (#) f)) = r * (Integral_on (M,B,f)) )

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,REAL

for r being Real

for B being Element of S st f is_integrable_on M holds

( f | B is_integrable_on M & Integral_on (M,B,(r (#) f)) = r * (Integral_on (M,B,f)) )

proof end;