:: Integral of Real-valued Measurable Function
:: by Yasunari Shidama and Noboru Endou
::
:: Received October 27, 2006
:: Copyright (c) 2006-2021 Association of Mizar Users

theorem Th1: :: MESFUNC6:1

for X being non empty set
for f being PartFunc of X,REAL holds |.(R_EAL f).| = R_EAL (abs f)

proof end;

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

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

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

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

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

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

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)

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)

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)

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)

proof end;

definition

let X be non empty set ;
let S be SigmaField of X;
let A be Element of S;
let f be PartFunc of X,REAL;

attr f is A -measurable means :: MESFUNC6:def 1
R_EAL f is A -measurable ;

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

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;

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;

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;

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;

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;

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;

theorem :: MESFUNC6:18

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_dom (f,r))) /\ (less_dom (f,s)) in S by MESFUNC1:32;

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;

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)

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

proof end;

theorem :: MESFUNC6:22

for X being non empty set
for f being PartFunc of X,REAL holds R_EAL f is V75() ;

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

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)

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;

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

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

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

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

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 )

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

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

proof end;

theorem :: MESFUNC6:33

for X being non empty set
for f being PartFunc of X,REAL holds max- f = max+ (- f)

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

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

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

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

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

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)

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

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

proof end;

theorem :: MESFUNC6:42

for X being non empty set
for f being PartFunc of X,REAL holds f = (max+ f) - (max- f)

proof end;

theorem Th43: :: MESFUNC6:43

for r being Real holds |.r.| = |.r.|

proof end;

theorem Th44: :: MESFUNC6:44

for X being non empty set
for f being PartFunc of X,REAL holds R_EAL (abs f) = |.(R_EAL f).|

proof end;

theorem :: MESFUNC6:45

for X being non empty set
for f being PartFunc of X,REAL holds abs f = (max+ f) + (max- f)

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

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

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

proof end;

definition

let X be non empty set ;
let S be SigmaField of X;
let f be PartFunc of X,REAL;

pred f is_simple_func_in S means :: MESFUNC6:def 2
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 ) );

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

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;

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;

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 )

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

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 )

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

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

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

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

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

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

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)

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 )

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 )

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)

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

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

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 )

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

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}

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

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

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;

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

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

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

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

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

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

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

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

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 )

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

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;

func Integral (M,f) -> Element of ExtREAL equals :: MESFUNC6:def 3
Integral (M,(R_EAL f));

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

end;

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

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;

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

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;

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;

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;

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;

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;

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;

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;

pred f is_integrable_on M means :: MESFUNC6:def 4
R_EAL f is_integrable_on M;

end;

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

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;

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;

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;

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;

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 )

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

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

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

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

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

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

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

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

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;

func Integral_on (M,B,f) -> Element of ExtREAL equals :: MESFUNC6:def 5
Integral (M,(f | B));

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

end;

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

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

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

proof end;