:: by Noboru Endou and Yasunari Shidama

::

:: Received May 24, 2006

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

begin

theorem Th3: :: MESFUNC5:3

for x, y being R_eal

for e being real number holds

( not |.(x - y).| < e or ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or ( x <> +infty & x <> -infty & y <> +infty & y <> -infty ) )

for e being real number holds

( not |.(x - y).| < e or ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or ( x <> +infty & x <> -infty & y <> +infty & y <> -infty ) )

proof end;

theorem Th4: :: MESFUNC5:4

for n being Nat

for p being R_eal st 0 <= p & p < n holds

ex k being Nat st

( 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= p & p < k / (2 |^ n) )

for p being R_eal st 0 <= p & p < n holds

ex k being Nat st

( 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= p & p < k / (2 |^ n) )

proof end;

theorem Th6: :: MESFUNC5:6

for x, y, k being ext-real number st 0 <= k holds

( k * (max (x,y)) = max ((k * x),(k * y)) & k * (min (x,y)) = min ((k * x),(k * y)) )

( k * (max (x,y)) = max ((k * x),(k * y)) & k * (min (x,y)) = min ((k * x),(k * y)) )

proof end;

theorem :: MESFUNC5:7

for x, y, k being R_eal st k <= 0 holds

( k * (min (x,y)) = max ((k * x),(k * y)) & k * (max (x,y)) = min ((k * x),(k * y)) )

( k * (min (x,y)) = max ((k * x),(k * y)) & k * (max (x,y)) = min ((k * x),(k * y)) )

proof end;

begin

:: deftheorem Def1 defines nonpositive MESFUNC5:def 1 :

for IT being set holds

( IT is nonpositive iff for x being R_eal st x in IT holds

x <= 0 );

for IT being set holds

( IT is nonpositive iff for x being R_eal st x in IT holds

x <= 0 );

definition
end;

:: deftheorem Def2 defines nonpositive MESFUNC5:def 2 :

for R being Relation holds

( R is nonpositive iff rng R is nonpositive );

for R being Relation holds

( R is nonpositive iff rng R is nonpositive );

theorem Th8: :: MESFUNC5:8

for X being set

for F being PartFunc of X,ExtREAL holds

( F is nonpositive iff for n being set holds F . n <= 0. )

for F being PartFunc of X,ExtREAL holds

( F is nonpositive iff for n being set holds F . n <= 0. )

proof end;

theorem Th9: :: MESFUNC5:9

for X being set

for F being PartFunc of X,ExtREAL st ( for n being set st n in dom F holds

F . n <= 0. ) holds

F is nonpositive

for F being PartFunc of X,ExtREAL st ( for n being set st n in dom F holds

F . n <= 0. ) holds

F is nonpositive

proof end;

:: deftheorem Def3 defines without-infty MESFUNC5:def 3 :

for R being Relation holds

( R is without-infty iff not -infty in rng R );

for R being Relation holds

( R is without-infty iff not -infty in rng R );

:: deftheorem Def4 defines without+infty MESFUNC5:def 4 :

for R being Relation holds

( R is without+infty iff not +infty in rng R );

for R being Relation holds

( R is without+infty iff not +infty in rng R );

definition

let X be non empty set ;

let f be PartFunc of X,ExtREAL;

( f is without-infty iff for x being set holds -infty < f . x )

( f is without+infty iff for x being set holds f . x < +infty )

end;
let f be PartFunc of X,ExtREAL;

:: original: without-infty

redefine attr f is without-infty means :Def5: :: MESFUNC5:def 5

for x being set holds -infty < f . x;

compatibility redefine attr f is without-infty means :Def5: :: MESFUNC5:def 5

for x being set holds -infty < f . x;

( f is without-infty iff for x being set holds -infty < f . x )

proof end;

:: original: without+infty

redefine attr f is without+infty means :Def6: :: MESFUNC5:def 6

for x being set holds f . x < +infty ;

compatibility redefine attr f is without+infty means :Def6: :: MESFUNC5:def 6

for x being set holds f . x < +infty ;

( f is without+infty iff for x being set holds f . x < +infty )

proof end;

:: deftheorem Def5 defines without-infty MESFUNC5:def 5 :

for X being non empty set

for f being PartFunc of X,ExtREAL holds

( f is without-infty iff for x being set holds -infty < f . x );

for X being non empty set

for f being PartFunc of X,ExtREAL holds

( f is without-infty iff for x being set holds -infty < f . x );

:: deftheorem Def6 defines without+infty MESFUNC5:def 6 :

for X being non empty set

for f being PartFunc of X,ExtREAL holds

( f is without+infty iff for x being set holds f . x < +infty );

for X being non empty set

for f being PartFunc of X,ExtREAL holds

( f is without+infty iff for x being set holds f . x < +infty );

theorem Th10: :: MESFUNC5:10

for X being non empty set

for f being PartFunc of X,ExtREAL holds

( ( for x being set st x in dom f holds

-infty < f . x ) iff f is () )

for f being PartFunc of X,ExtREAL holds

( ( for x being set st x in dom f holds

-infty < f . x ) iff f is () )

proof end;

theorem Th11: :: MESFUNC5:11

for X being non empty set

for f being PartFunc of X,ExtREAL holds

( ( for x being set st x in dom f holds

f . x < +infty ) iff f is () )

for f being PartFunc of X,ExtREAL holds

( ( for x being set st x in dom f holds

f . x < +infty ) iff f is () )

proof end;

registration

let X be non empty set ;

coherence

for b_{1} being PartFunc of X,ExtREAL st b_{1} is nonnegative holds

b_{1} is ()
by Th12;

coherence

for b_{1} being PartFunc of X,ExtREAL st b_{1} is nonpositive holds

b_{1} is ()
by Th13;

end;
coherence

for b

b

coherence

for b

b

theorem Th14: :: MESFUNC5:14

for X being non empty set

for S being SigmaField of X

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

( f is () & f is () )

for S being SigmaField of X

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

( f is () & f is () )

proof end;

theorem Th15: :: MESFUNC5:15

for X being non empty set

for Y being set

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

f | Y is nonnegative

for Y being set

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

f | Y is nonnegative

proof end;

theorem Th16: :: MESFUNC5:16

for X being non empty set

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

dom (f + g) = (dom f) /\ (dom g)

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

dom (f + g) = (dom f) /\ (dom g)

proof end;

theorem :: MESFUNC5:17

for X being non empty set

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

dom (f - g) = (dom f) /\ (dom g)

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

dom (f - g) = (dom f) /\ (dom g)

proof end;

theorem Th18: :: MESFUNC5:18

for X being non empty set

for S being SigmaField of X

for f, g being PartFunc of X,ExtREAL

for F being Function of RAT,S

for r being Real

for A being Element of S st f is () & g is () & ( for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ) holds

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

for S being SigmaField of X

for f, g being PartFunc of X,ExtREAL

for F being Function of RAT,S

for r being Real

for A being Element of S st f is () & g is () & ( for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ) holds

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

proof end;

definition

let X be non empty set ;

let f be PartFunc of X,REAL;

coherence

f is PartFunc of X,ExtREAL by NUMBERS:31, RELSET_1:7;

end;
let f be PartFunc of X,REAL;

coherence

f is PartFunc of X,ExtREAL by NUMBERS:31, RELSET_1:7;

:: deftheorem defines R_EAL MESFUNC5:def 7 :

for X being non empty set

for f being PartFunc of X,REAL holds R_EAL f = f;

for X being non empty set

for f being PartFunc of X,REAL holds R_EAL f = f;

theorem Th19: :: MESFUNC5:19

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,ExtREAL st f is nonnegative & g is nonnegative holds

f + g is nonnegative

for S being SigmaField of X

for M being sigma_Measure of S

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

f + g is nonnegative

proof end;

theorem Th20: :: MESFUNC5:20

for X being non empty set

for f being PartFunc of X,ExtREAL

for c being Real st f is nonnegative holds

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

for f being PartFunc of X,ExtREAL

for c being Real st f is nonnegative holds

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

proof end;

theorem Th21: :: MESFUNC5:21

for X being non empty set

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

( g . x <= f . x & -infty < g . x & f . x < +infty ) ) holds

f - g is nonnegative

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

( g . x <= f . x & -infty < g . x & f . x < +infty ) ) holds

f - g is nonnegative

proof end;

Lm1: 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 holds

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

proof end;

theorem Th22: :: MESFUNC5:22

for X being non empty set

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

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

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

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

proof end;

theorem Th23: :: MESFUNC5:23

for X being non empty set

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

( dom ((f + g) + h) = ((dom f) /\ (dom g)) /\ (dom h) & (f + g) + h is nonnegative & ( for x being set st x in ((dom f) /\ (dom g)) /\ (dom h) holds

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

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

( dom ((f + g) + h) = ((dom f) /\ (dom g)) /\ (dom h) & (f + g) + h is nonnegative & ( for x being set st x in ((dom f) /\ (dom g)) /\ (dom h) holds

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

proof end;

theorem Th24: :: MESFUNC5:24

for X being non empty set

for f, g being PartFunc of X,ExtREAL st f is () & g is () 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,ExtREAL st f is () & g is () 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 Th25: :: MESFUNC5:25

for X being non empty set

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

((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g)

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

((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g)

proof end;

theorem Th26: :: MESFUNC5:26

for C being non empty set

for f being PartFunc of C,ExtREAL

for c being Real st 0 <= c holds

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

for f being PartFunc of C,ExtREAL

for c being Real st 0 <= c holds

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

proof end;

theorem Th27: :: MESFUNC5:27

for C being non empty set

for f being PartFunc of C,ExtREAL

for c being Real st 0 <= c holds

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

for f being PartFunc of C,ExtREAL

for c being Real st 0 <= c holds

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

proof end;

theorem Th28: :: MESFUNC5:28

for X being non empty set

for f being PartFunc of X,ExtREAL

for A being set holds

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

for f being PartFunc of X,ExtREAL

for A being set holds

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

proof end;

theorem Th29: :: MESFUNC5:29

for X being non empty set

for f, g being PartFunc of X,ExtREAL

for B being set st B c= dom (f + g) holds

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

for f, g being PartFunc of X,ExtREAL

for B being set st B c= dom (f + g) holds

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

proof end;

theorem Th30: :: MESFUNC5:30

for X being non empty set

for f being PartFunc of X,ExtREAL

for a being R_eal holds eq_dom (f,a) = f " {a}

for f being PartFunc of X,ExtREAL

for a being R_eal holds eq_dom (f,a) = f " {a}

proof end;

begin

theorem Th31: :: MESFUNC5:31

for X being non empty set

for S being SigmaField of X

for f, g being PartFunc of X,ExtREAL

for A being Element of S st f is () & g is () & f is_measurable_on A & g is_measurable_on A holds

f + g is_measurable_on A

for S being SigmaField of X

for f, g being PartFunc of X,ExtREAL

for A being Element of S st f is () & g is () & f is_measurable_on A & g is_measurable_on A holds

f + g is_measurable_on A

proof end;

theorem :: MESFUNC5:32

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 & dom f = {} holds

ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & a . 1 = 0 & ( for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & Sum x = 0 )

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 & dom f = {} holds

ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & a . 1 = 0 & ( for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & Sum x = 0 )

proof end;

theorem Th33: :: MESFUNC5:33

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,ExtREAL

for A being Element of S

for r, s being Real st f is_measurable_on A & A c= dom f holds

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

for S being SigmaField of X

for f being PartFunc of X,ExtREAL

for A being Element of S

for r, s being Real st f is_measurable_on A & A c= dom f holds

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

proof end;

theorem Th34: :: MESFUNC5:34

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for A being Element of S st f is_simple_func_in S holds

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

f | A is_simple_func_in S

proof end;

theorem Th35: :: MESFUNC5:35

for X being non empty set

for S being SigmaField of X

for A being Element of S

for F being Finite_Sep_Sequence of S

for G being FinSequence st dom F = dom G & ( for n being Nat st n in dom F holds

G . n = (F . n) /\ A ) holds

G is Finite_Sep_Sequence of S

for S being SigmaField of X

for A being Element of S

for F being Finite_Sep_Sequence of S

for G being FinSequence st dom F = dom G & ( for n being Nat st n in dom F holds

G . n = (F . n) /\ A ) holds

G is Finite_Sep_Sequence of S

proof end;

theorem Th36: :: MESFUNC5:36

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,ExtREAL

for A being Element of S

for F, G being Finite_Sep_Sequence of S

for a being FinSequence of ExtREAL st dom F = dom G & ( for n being Nat st n in dom F holds

G . n = (F . n) /\ A ) & F,a are_Re-presentation_of f holds

G,a are_Re-presentation_of f | A

for S being SigmaField of X

for f being PartFunc of X,ExtREAL

for A being Element of S

for F, G being Finite_Sep_Sequence of S

for a being FinSequence of ExtREAL st dom F = dom G & ( for n being Nat st n in dom F holds

G . n = (F . n) /\ A ) & F,a are_Re-presentation_of f holds

G,a are_Re-presentation_of f | A

proof end;

theorem Th37: :: MESFUNC5: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 st f is_simple_func_in S holds

dom f is Element of 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

dom f is Element of S

proof end;

Lm2: for Y being set

for p being FinSequence st ( for i being Nat st i in dom p holds

p . i in Y ) holds

p is FinSequence of Y

proof end;

Lm3: 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,ExtREAL 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 Th38: :: MESFUNC5:38

for X being non empty set

for S being SigmaField of X

for f, g being PartFunc of X,ExtREAL 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,ExtREAL st f is_simple_func_in S & g is_simple_func_in S holds

f + g is_simple_func_in S

proof end;

theorem Th39: :: MESFUNC5:39

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

c (#) 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 c being Real st f is_simple_func_in S holds

c (#) f is_simple_func_in S

proof end;

theorem Th40: :: MESFUNC5:40

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,ExtREAL st f is_simple_func_in S & g is_simple_func_in S & ( for x being set st x in dom (f - g) holds

g . x <= f . x ) holds

f - g is nonnegative

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S & ( for x being set st x in dom (f - g) holds

g . x <= f . x ) holds

f - g is nonnegative

proof end;

theorem Th41: :: MESFUNC5:41

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for A being Element of S

for c being R_eal st c <> +infty & c <> -infty holds

ex f being PartFunc of X,ExtREAL st

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

f . x = c ) )

for S being SigmaField of X

for M being sigma_Measure of S

for A being Element of S

for c being R_eal st c <> +infty & c <> -infty holds

ex f being PartFunc of X,ExtREAL st

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

f . x = c ) )

proof end;

theorem Th42: :: MESFUNC5:42

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 B, BF being Element of S st f is_measurable_on B & BF = (dom f) /\ B holds

f | B is_measurable_on BF

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for B, BF being Element of S st f is_measurable_on B & BF = (dom f) /\ B holds

f | B is_measurable_on BF

proof end;

theorem Th43: :: MESFUNC5:43

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for A being Element of S

for f, g being PartFunc of X,ExtREAL st A c= dom f & f is_measurable_on A & g is_measurable_on A & f is () & g is () holds

(max+ (f + g)) + (max- f) is_measurable_on A

for S being SigmaField of X

for M being sigma_Measure of S

for A being Element of S

for f, g being PartFunc of X,ExtREAL st A c= dom f & f is_measurable_on A & g is_measurable_on A & f is () & g is () holds

(max+ (f + g)) + (max- f) is_measurable_on A

proof end;

theorem Th44: :: MESFUNC5:44

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for A being Element of S

for f, g being PartFunc of X,ExtREAL st A c= (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A & f is () & g is () holds

(max- (f + g)) + (max+ f) is_measurable_on A

for S being SigmaField of X

for M being sigma_Measure of S

for A being Element of S

for f, g being PartFunc of X,ExtREAL st A c= (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A & f is () & g is () holds

(max- (f + g)) + (max+ f) is_measurable_on A

proof end;

theorem Th45: :: MESFUNC5:45

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for A being set st A in S holds

0 <= M . A

for S being SigmaField of X

for M being sigma_Measure of S

for A being set st A in S holds

0 <= M . A

proof end;

Lm4: 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 set st x in dom f holds

f . x = r ) holds

f is_simple_func_in S

proof end;

theorem Th46: :: MESFUNC5:46

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,ExtREAL st ex E1 being Element of S st

( E1 = dom f & f is_measurable_on E1 ) & ex E2 being Element of S st

( E2 = dom g & g is_measurable_on E2 ) & f " {+infty} in S & f " {-infty} in S & g " {+infty} in S & g " {-infty} in S 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,ExtREAL st ex E1 being Element of S st

( E1 = dom f & f is_measurable_on E1 ) & ex E2 being Element of S st

( E2 = dom g & g is_measurable_on E2 ) & f " {+infty} in S & f " {-infty} in S & g " {+infty} in S & g " {-infty} in S holds

dom (f + g) in S

proof end;

Lm5: for X being non empty set

for S being SigmaField of X

for A being Element of S

for f being PartFunc of X,ExtREAL

for r being real number holds A /\ (less_dom (f,(R_EAL r))) = less_dom ((f | A),(R_EAL r))

proof end;

Lm6: for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for A being Element of S

for f being PartFunc of X,ExtREAL holds

( f | A is_measurable_on A iff f is_measurable_on A )

proof end;

Lm7: 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,ExtREAL st ex E1 being Element of S st

( E1 = dom f & f is_measurable_on E1 ) & ex E2 being Element of S st

( E2 = dom g & g is_measurable_on E2 ) & dom f = dom g holds

ex DFPG being Element of S st

( DFPG = dom (f + g) & f + g is_measurable_on DFPG )

proof end;

theorem Th47: :: MESFUNC5:47

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,ExtREAL st ex E1 being Element of S st

( E1 = dom f & f is_measurable_on E1 ) & ex E2 being Element of S st

( E2 = dom g & g is_measurable_on E2 ) holds

ex E being Element of S st

( E = dom (f + g) & f + g is_measurable_on E )

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st ex E1 being Element of S st

( E1 = dom f & f is_measurable_on E1 ) & ex E2 being Element of S st

( E2 = dom g & g is_measurable_on E2 ) holds

ex E being Element of S st

( E = dom (f + g) & f + g is_measurable_on E )

proof end;

theorem Th48: :: MESFUNC5:48

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

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

( f is_measurable_on B iff f is_measurable_on A /\ B )

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

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

( f is_measurable_on B iff f is_measurable_on A /\ B )

proof end;

theorem Th49: :: MESFUNC5:49

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 ex A being Element of S st dom f = A holds

for c being Real

for B being Element of S st f is_measurable_on B holds

c (#) f is_measurable_on B

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL 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_measurable_on B holds

c (#) f is_measurable_on B

proof end;

begin

:: deftheorem Def8 defines convergent_to_finite_number MESFUNC5:def 8 :

for seq being ExtREAL_sequence holds

( seq is convergent_to_finite_number iff ex g being real number st

for p being real number st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - (R_EAL g)).| < p );

for seq being ExtREAL_sequence holds

( seq is convergent_to_finite_number iff ex g being real number st

for p being real number st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - (R_EAL g)).| < p );

:: deftheorem Def9 defines convergent_to_+infty MESFUNC5:def 9 :

for seq being ExtREAL_sequence holds

( seq is convergent_to_+infty iff for g being real number st 0 < g holds

ex n being Nat st

for m being Nat st n <= m holds

g <= seq . m );

for seq being ExtREAL_sequence holds

( seq is convergent_to_+infty iff for g being real number st 0 < g holds

ex n being Nat st

for m being Nat st n <= m holds

g <= seq . m );

:: deftheorem Def10 defines convergent_to_-infty MESFUNC5:def 10 :

for seq being ExtREAL_sequence holds

( seq is convergent_to_-infty iff for g being real number st g < 0 holds

ex n being Nat st

for m being Nat st n <= m holds

seq . m <= g );

for seq being ExtREAL_sequence holds

( seq is convergent_to_-infty iff for g being real number st g < 0 holds

ex n being Nat st

for m being Nat st n <= m holds

seq . m <= g );

theorem Th50: :: MESFUNC5:50

for seq being ExtREAL_sequence st seq is convergent_to_+infty holds

( not seq is convergent_to_-infty & not seq is convergent_to_finite_number )

( not seq is convergent_to_-infty & not seq is convergent_to_finite_number )

proof end;

theorem Th51: :: MESFUNC5:51

for seq being ExtREAL_sequence st seq is convergent_to_-infty holds

( not seq is convergent_to_+infty & not seq is convergent_to_finite_number )

( not seq is convergent_to_+infty & not seq is convergent_to_finite_number )

proof end;

definition

let seq be ExtREAL_sequence;

end;
attr seq is convergent means :Def11: :: MESFUNC5:def 11

( seq is convergent_to_finite_number or seq is convergent_to_+infty or seq is convergent_to_-infty );

( seq is convergent_to_finite_number or seq is convergent_to_+infty or seq is convergent_to_-infty );

:: deftheorem Def11 defines convergent MESFUNC5:def 11 :

for seq being ExtREAL_sequence holds

( seq is convergent iff ( seq is convergent_to_finite_number or seq is convergent_to_+infty or seq is convergent_to_-infty ) );

for seq being ExtREAL_sequence holds

( seq is convergent iff ( seq is convergent_to_finite_number or seq is convergent_to_+infty or seq is convergent_to_-infty ) );

definition

let seq be ExtREAL_sequence;

assume A1: seq is convergent ;

ex b_{1} being R_eal st

( ex g being real number st

( b_{1} = g & ( for p being real number st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b_{1}).| < p ) & seq is convergent_to_finite_number ) or ( b_{1} = +infty & seq is convergent_to_+infty ) or ( b_{1} = -infty & seq is convergent_to_-infty ) )

for b_{1}, b_{2} being R_eal st ( ex g being real number st

( b_{1} = g & ( for p being real number st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b_{1}).| < p ) & seq is convergent_to_finite_number ) or ( b_{1} = +infty & seq is convergent_to_+infty ) or ( b_{1} = -infty & seq is convergent_to_-infty ) ) & ( ex g being real number st

( b_{2} = g & ( for p being real number st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b_{2}).| < p ) & seq is convergent_to_finite_number ) or ( b_{2} = +infty & seq is convergent_to_+infty ) or ( b_{2} = -infty & seq is convergent_to_-infty ) ) holds

b_{1} = b_{2}

end;
assume A1: seq is convergent ;

func lim seq -> R_eal means :Def12: :: MESFUNC5:def 12

( ex g being real number st

( it = g & ( for p being real number st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - it).| < p ) & seq is convergent_to_finite_number ) or ( it = +infty & seq is convergent_to_+infty ) or ( it = -infty & seq is convergent_to_-infty ) );

existence ( ex g being real number st

( it = g & ( for p being real number st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - it).| < p ) & seq is convergent_to_finite_number ) or ( it = +infty & seq is convergent_to_+infty ) or ( it = -infty & seq is convergent_to_-infty ) );

ex b

( ex g being real number st

( b

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b

proof end;

uniqueness for b

( b

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b

( b

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b

b

proof end;

:: deftheorem Def12 defines lim MESFUNC5:def 12 :

for seq being ExtREAL_sequence st seq is convergent holds

for b_{2} being R_eal holds

( b_{2} = lim seq iff ( ex g being real number st

( b_{2} = g & ( for p being real number st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b_{2}).| < p ) & seq is convergent_to_finite_number ) or ( b_{2} = +infty & seq is convergent_to_+infty ) or ( b_{2} = -infty & seq is convergent_to_-infty ) ) );

for seq being ExtREAL_sequence st seq is convergent holds

for b

( b

( b

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b

theorem Th52: :: MESFUNC5:52

for seq being ExtREAL_sequence

for r being real number st ( for n being Nat holds seq . n = r ) holds

( seq is convergent_to_finite_number & lim seq = r )

for r being real number st ( for n being Nat holds seq . n = r ) holds

( seq is convergent_to_finite_number & lim seq = r )

proof end;

theorem Th53: :: MESFUNC5:53

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

0 <= F . n ) holds

0 <= Sum F

0 <= F . n ) holds

0 <= Sum F

proof end;

theorem Th54: :: MESFUNC5:54

for L being ExtREAL_sequence st ( for n, m being Nat st n <= m holds

L . n <= L . m ) holds

( L is convergent & lim L = sup (rng L) )

L . n <= L . m ) holds

( L is convergent & lim L = sup (rng L) )

proof end;

theorem Th55: :: MESFUNC5:55

for L, G being ExtREAL_sequence st ( for n being Nat holds L . n <= G . n ) holds

sup (rng L) <= sup (rng G)

sup (rng L) <= sup (rng G)

proof end;

theorem Th57: :: MESFUNC5:57

for L being ExtREAL_sequence

for K being R_eal st ( for n being Nat holds L . n <= K ) holds

sup (rng L) <= K

for K being R_eal st ( for n being Nat holds L . n <= K ) holds

sup (rng L) <= K

proof end;

theorem :: MESFUNC5:58

for L being ExtREAL_sequence

for K being R_eal st K <> +infty & ( for n being Nat holds L . n <= K ) holds

sup (rng L) < +infty

for K being R_eal st K <> +infty & ( for n being Nat holds L . n <= K ) holds

sup (rng L) < +infty

proof end;

theorem Th59: :: MESFUNC5:59

for L being ExtREAL_sequence st L is () holds

( sup (rng L) <> +infty iff ex K being real number st

( 0 < K & ( for n being Nat holds L . n <= K ) ) )

( sup (rng L) <> +infty iff ex K being real number st

( 0 < K & ( for n being Nat holds L . n <= K ) ) )

proof end;

theorem Th60: :: MESFUNC5:60

for L being ExtREAL_sequence

for c being ext-real number st ( for n being Nat holds L . n = c ) holds

( L is convergent & lim L = c & lim L = sup (rng L) )

for c being ext-real number st ( for n being Nat holds L . n = c ) holds

( L is convergent & lim L = c & lim L = sup (rng L) )

proof end;

Lm8: for J being ExtREAL_sequence holds

( not J is () or sup (rng J) in REAL or sup (rng J) = +infty )

proof end;

theorem Th61: :: MESFUNC5:61

for J, K, L being ExtREAL_sequence st ( for n, m being Nat st n <= m holds

J . n <= J . m ) & ( for n, m being Nat st n <= m holds

K . n <= K . m ) & J is () & K is () & ( for n being Nat holds (J . n) + (K . n) = L . n ) holds

( L is convergent & lim L = sup (rng L) & lim L = (lim J) + (lim K) & sup (rng L) = (sup (rng K)) + (sup (rng J)) )

J . n <= J . m ) & ( for n, m being Nat st n <= m holds

K . n <= K . m ) & J is () & K is () & ( for n being Nat holds (J . n) + (K . n) = L . n ) holds

( L is convergent & lim L = sup (rng L) & lim L = (lim J) + (lim K) & sup (rng L) = (sup (rng K)) + (sup (rng J)) )

proof end;

theorem Th62: :: MESFUNC5:62

for L, K being ExtREAL_sequence

for c being Real st 0 <= c & L is () & ( for n being Nat holds K . n = (R_EAL c) * (L . n) ) holds

( sup (rng K) = (R_EAL c) * (sup (rng L)) & K is () )

for c being Real st 0 <= c & L is () & ( for n being Nat holds K . n = (R_EAL c) * (L . n) ) holds

( sup (rng K) = (R_EAL c) * (sup (rng L)) & K is () )

proof end;

theorem Th63: :: MESFUNC5:63

for L, K being ExtREAL_sequence

for c being Real st 0 <= c & ( for n, m being Nat st n <= m holds

L . n <= L . m ) & ( for n being Nat holds K . n = (R_EAL c) * (L . n) ) & L is () holds

( ( for n, m being Nat st n <= m holds

K . n <= K . m ) & K is () & K is convergent & lim K = sup (rng K) & lim K = (R_EAL c) * (lim L) )

for c being Real st 0 <= c & ( for n, m being Nat st n <= m holds

L . n <= L . m ) & ( for n being Nat holds K . n = (R_EAL c) * (L . n) ) & L is () holds

( ( for n, m being Nat st n <= m holds

K . n <= K . m ) & K is () & K is convergent & lim K = sup (rng K) & lim K = (R_EAL c) * (lim L) )

proof end;

begin

definition

let X be non empty set ;

let H be Functional_Sequence of X,ExtREAL;

let x be Element of X;

ex b_{1} being ExtREAL_sequence st

for n being Nat holds b_{1} . n = (H . n) . x

for b_{1}, b_{2} being ExtREAL_sequence st ( for n being Nat holds b_{1} . n = (H . n) . x ) & ( for n being Nat holds b_{2} . n = (H . n) . x ) holds

b_{1} = b_{2}

end;
let H be Functional_Sequence of X,ExtREAL;

let x be Element of X;

func H # x -> ExtREAL_sequence means :Def13: :: MESFUNC5:def 13

for n being Nat holds it . n = (H . n) . x;

existence for n being Nat holds it . n = (H . n) . x;

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def13 defines # MESFUNC5:def 13 :

for X being non empty set

for H being Functional_Sequence of X,ExtREAL

for x being Element of X

for b_{4} being ExtREAL_sequence holds

( b_{4} = H # x iff for n being Nat holds b_{4} . n = (H . n) . x );

for X being non empty set

for H being Functional_Sequence of X,ExtREAL

for x being Element of X

for b

( b

definition

let D1, D2 be set ;

let F be Function of NAT,(PFuncs (D1,D2));

let n be Nat;

:: original: .

redefine func F . n -> PartFunc of D1,D2;

coherence

F . n is PartFunc of D1,D2

end;
let F be Function of NAT,(PFuncs (D1,D2));

let n be Nat;

:: original: .

redefine func F . n -> PartFunc of D1,D2;

coherence

F . n is PartFunc of D1,D2

proof end;

theorem Th64: :: MESFUNC5:64

for X being non empty set

for S being SigmaField of X

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

( A = dom f & f is_measurable_on A ) & f is nonnegative holds

ex F being Functional_Sequence of X,ExtREAL st

( ( for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in dom f holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds

( F # x is convergent & lim (F # x) = f . x ) ) )

for S being SigmaField of X

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

( A = dom f & f is_measurable_on A ) & f is nonnegative holds

ex F being Functional_Sequence of X,ExtREAL st

( ( for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in dom f holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds

( F # x is convergent & lim (F # x) = f . x ) ) )

proof end;

begin

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

coherence

( ( dom f <> {} implies integral (X,S,M,f) is Element of ExtREAL ) & ( not dom f <> {} implies 0. is Element of ExtREAL ) );

consistency

for b_{1} being Element of ExtREAL holds verum;

;

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

let f be PartFunc of X,ExtREAL;

func integral' (M,f) -> Element of ExtREAL equals :Def14: :: MESFUNC5:def 14

integral (X,S,M,f) if dom f <> {}

otherwise 0. ;

correctness integral (X,S,M,f) if dom f <> {}

otherwise 0. ;

coherence

( ( dom f <> {} implies integral (X,S,M,f) is Element of ExtREAL ) & ( not dom f <> {} implies 0. is Element of ExtREAL ) );

consistency

for b

;

:: deftheorem Def14 defines integral' MESFUNC5:def 14 :

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 holds

( ( dom f <> {} implies integral' (M,f) = integral (X,S,M,f) ) & ( not dom f <> {} implies integral' (M,f) = 0. ) );

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 holds

( ( dom f <> {} implies integral' (M,f) = integral (X,S,M,f) ) & ( not dom f <> {} implies integral' (M,f) = 0. ) );

theorem Th65: :: MESFUNC5:65

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

( dom (f + g) = (dom f) /\ (dom g) & integral' (M,(f + g)) = (integral' (M,(f | (dom (f + g))))) + (integral' (M,(g | (dom (f + g))))) )

for S being SigmaField of X

for M being sigma_Measure of S

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

( dom (f + g) = (dom f) /\ (dom g) & integral' (M,(f + g)) = (integral' (M,(f | (dom (f + g))))) + (integral' (M,(g | (dom (f + g))))) )

proof end;

theorem Th66: :: MESFUNC5:66

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 c being Real st f is_simple_func_in S & f is nonnegative & 0 <= c holds

integral' (M,(c (#) f)) = (R_EAL c) * (integral' (M,f))

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for c being Real st f is_simple_func_in S & f is nonnegative & 0 <= c holds

integral' (M,(c (#) f)) = (R_EAL c) * (integral' (M,f))

proof end;

theorem Th67: :: MESFUNC5:67

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for A, B being Element of S st f is_simple_func_in S & f is nonnegative & A misses B holds

integral' (M,(f | (A \/ B))) = (integral' (M,(f | A))) + (integral' (M,(f | B)))

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for A, B being Element of S st f is_simple_func_in S & f is nonnegative & A misses B holds

integral' (M,(f | (A \/ B))) = (integral' (M,(f | A))) + (integral' (M,(f | B)))

proof end;

theorem Th68: :: MESFUNC5:68

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

0 <= integral' (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

0 <= integral' (M,f)

proof end;

Lm9: 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,ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & g is_simple_func_in S & dom g = dom f & g is nonnegative & ( for x being set st x in dom f holds

g . x <= f . x ) holds

( f - g is_simple_func_in S & dom (f - g) <> {} & f - g is nonnegative & integral (X,S,M,f) = (integral (X,S,M,(f - g))) + (integral (X,S,M,g)) )

proof end;

theorem Th69: :: MESFUNC5:69

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,ExtREAL st f is_simple_func_in S & f is nonnegative & g is_simple_func_in S & g is nonnegative & ( for x being set st x in dom (f - g) holds

g . x <= f . x ) holds

( dom (f - g) = (dom f) /\ (dom g) & integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g))))) )

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative & g is_simple_func_in S & g is nonnegative & ( for x being set st x in dom (f - g) holds

g . x <= f . x ) holds

( dom (f - g) = (dom f) /\ (dom g) & integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g))))) )

proof end;

theorem Th70: :: MESFUNC5:70

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,ExtREAL st f is_simple_func_in S & g is_simple_func_in S & f is nonnegative & g is nonnegative & ( for x being set st x in dom (f - g) holds

g . x <= f . x ) holds

integral' (M,(g | (dom (f - g)))) <= integral' (M,(f | (dom (f - g))))

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S & f is nonnegative & g is nonnegative & ( for x being set st x in dom (f - g) holds

g . x <= f . x ) holds

integral' (M,(g | (dom (f - g)))) <= integral' (M,(f | (dom (f - g))))

proof end;

theorem Th71: :: MESFUNC5:71

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 c being R_eal st 0 <= c & f is_simple_func_in S & ( for x being set st x in dom f holds

f . x = c ) holds

integral' (M,f) = c * (M . (dom f))

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for c being R_eal st 0 <= c & f is_simple_func_in S & ( for x being set st x in dom f holds

f . x = c ) holds

integral' (M,f) = c * (M . (dom f))

proof end;

theorem Th72: :: MESFUNC5:72

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 | (eq_dom (f,(R_EAL 0))))) = 0

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 | (eq_dom (f,(R_EAL 0))))) = 0

proof end;

theorem Th73: :: MESFUNC5:73

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for B being Element of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S & M . B = 0 & f is nonnegative holds

integral' (M,(f | B)) = 0

for S being SigmaField of X

for M being sigma_Measure of S

for B being Element of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S & M . B = 0 & f is nonnegative holds

integral' (M,(f | B)) = 0

proof end;

theorem Th74: :: MESFUNC5:74

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for g being PartFunc of X,ExtREAL

for F being Functional_Sequence of X,ExtREAL

for L being ExtREAL_sequence st g is_simple_func_in S & ( for x being set st x in dom g holds

0 < g . x ) & ( for n being Nat holds F . n is_simple_func_in S ) & ( for n being Nat holds dom (F . n) = dom g ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in dom g holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom g holds

( F # x is convergent & g . x <= lim (F # x) ) ) & ( for n being Nat holds L . n = integral' (M,(F . n)) ) holds

( L is convergent & integral' (M,g) <= lim L )

for S being SigmaField of X

for M being sigma_Measure of S

for g being PartFunc of X,ExtREAL

for F being Functional_Sequence of X,ExtREAL

for L being ExtREAL_sequence st g is_simple_func_in S & ( for x being set st x in dom g holds

0 < g . x ) & ( for n being Nat holds F . n is_simple_func_in S ) & ( for n being Nat holds dom (F . n) = dom g ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in dom g holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom g holds

( F # x is convergent & g . x <= lim (F # x) ) ) & ( for n being Nat holds L . n = integral' (M,(F . n)) ) holds

( L is convergent & integral' (M,g) <= lim L )

proof end;

theorem Th75: :: MESFUNC5:75

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for g being PartFunc of X,ExtREAL

for F being Functional_Sequence of X,ExtREAL st g is_simple_func_in S & g is nonnegative & ( for n being Nat holds F . n is_simple_func_in S ) & ( for n being Nat holds dom (F . n) = dom g ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in dom g holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom g holds

( F # x is convergent & g . x <= lim (F # x) ) ) holds

ex G being ExtREAL_sequence st

( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G )

for S being SigmaField of X

for M being sigma_Measure of S

for g being PartFunc of X,ExtREAL

for F being Functional_Sequence of X,ExtREAL st g is_simple_func_in S & g is nonnegative & ( for n being Nat holds F . n is_simple_func_in S ) & ( for n being Nat holds dom (F . n) = dom g ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in dom g holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom g holds

( F # x is convergent & g . x <= lim (F # x) ) ) holds

ex G being ExtREAL_sequence st

( ( for n being Nat holds G . n = integral' (M,(F . n)) ) & G is convergent & sup (rng G) = lim G & integral' (M,g) <= lim G )

proof end;

theorem Th76: :: MESFUNC5:76

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for A being Element of S

for F, G being Functional_Sequence of X,ExtREAL

for K, L being ExtREAL_sequence st ( for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = A ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in A holds

(F . n) . x <= (F . m) . x ) & ( for n being Nat holds

( G . n is_simple_func_in S & dom (G . n) = A ) ) & ( for n being Nat holds G . n is nonnegative ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in A holds

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

( F # x is convergent & G # x is convergent & lim (F # x) = lim (G # x) ) ) & ( for n being Nat holds

( K . n = integral' (M,(F . n)) & L . n = integral' (M,(G . n)) ) ) holds

( K is convergent & L is convergent & lim K = lim L )

for S being SigmaField of X

for M being sigma_Measure of S

for A being Element of S

for F, G being Functional_Sequence of X,ExtREAL

for K, L being ExtREAL_sequence st ( for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = A ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in A holds

(F . n) . x <= (F . m) . x ) & ( for n being Nat holds

( G . n is_simple_func_in S & dom (G . n) = A ) ) & ( for n being Nat holds G . n is nonnegative ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in A holds

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

( F # x is convergent & G # x is convergent & lim (F # x) = lim (G # x) ) ) & ( for n being Nat holds

( K . n = integral' (M,(F . n)) & L . n = integral' (M,(G . n)) ) ) holds

( K is convergent & L is convergent & lim K = lim L )

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

assume that

A1: ex A being Element of S st

( A = dom f & f is_measurable_on A ) and

A2: f is nonnegative ;

ex b_{1} being Element of ExtREAL ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st

( ( for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in dom f holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds

( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' (M,(F . n)) ) & K is convergent & b_{1} = lim K )

for b_{1}, b_{2} being Element of ExtREAL st ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st

( ( for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in dom f holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds

( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' (M,(F . n)) ) & K is convergent & b_{1} = lim K ) & ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st

( ( for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in dom f holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds

( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' (M,(F . n)) ) & K is convergent & b_{2} = lim K ) holds

b_{1} = b_{2}

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

let f be PartFunc of X,ExtREAL;

assume that

A1: ex A being Element of S st

( A = dom f & f is_measurable_on A ) and

A2: f is nonnegative ;

func integral+ (M,f) -> Element of ExtREAL means :Def15: :: MESFUNC5:def 15

ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st

( ( for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in dom f holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds

( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' (M,(F . n)) ) & K is convergent & it = lim K );

existence ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st

( ( for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in dom f holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds

( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' (M,(F . n)) ) & K is convergent & it = lim K );

ex b

( ( for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in dom f holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds

( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' (M,(F . n)) ) & K is convergent & b

proof end;

uniqueness for b

( ( for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in dom f holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds

( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' (M,(F . n)) ) & K is convergent & b

( ( for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in dom f holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds

( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' (M,(F . n)) ) & K is convergent & b

b

proof end;

:: deftheorem Def15 defines integral+ MESFUNC5:def 15 :

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

( A = dom f & f is_measurable_on A ) & f is nonnegative holds

for b_{5} being Element of ExtREAL holds

( b_{5} = integral+ (M,f) iff ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st

( ( for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in dom f holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds

( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' (M,(F . n)) ) & K is convergent & b_{5} = lim K ) );

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

( A = dom f & f is_measurable_on A ) & f is nonnegative holds

for b

( b

( ( for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in dom f holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds

( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' (M,(F . n)) ) & K is convergent & b

theorem Th77: :: MESFUNC5:77

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' (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' (M,f)

proof end;

Lm10: 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,ExtREAL st ex A being Element of S st

( A = dom f & A = dom g & f is_measurable_on A & g is_measurable_on A ) & f is nonnegative & g is nonnegative holds

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

proof end;

theorem Th78: :: MESFUNC5:78

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

( A = dom f & f is_measurable_on A ) & ex B being Element of S st

( B = dom g & g is_measurable_on B ) & f is nonnegative & g is nonnegative holds

ex C being Element of S st

( C = dom (f + g) & integral+ (M,(f + g)) = (integral+ (M,(f | C))) + (integral+ (M,(g | C))) )

for S being SigmaField of X

for M being sigma_Measure of S

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

( A = dom f & f is_measurable_on A ) & ex B being Element of S st

( B = dom g & g is_measurable_on B ) & f is nonnegative & g is nonnegative holds

ex C being Element of S st

( C = dom (f + g) & integral+ (M,(f + g)) = (integral+ (M,(f | C))) + (integral+ (M,(g | C))) )

proof end;

theorem Th79: :: MESFUNC5:79

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

( A = dom f & f is_measurable_on A ) & f is nonnegative holds

0 <= integral+ (M,f)

for S being SigmaField of X

for M being sigma_Measure of S

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

( A = dom f & f is_measurable_on A ) & f is nonnegative holds

0 <= integral+ (M,f)

proof end;

theorem Th80: :: MESFUNC5:80

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

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

( E = dom f & f is_measurable_on E ) & f is nonnegative holds

0 <= integral+ (M,(f | A))

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

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

( E = dom f & f is_measurable_on E ) & f is nonnegative holds

0 <= integral+ (M,(f | A))

proof end;

theorem Th81: :: MESFUNC5:81

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

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

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

integral+ (M,(f | (A \/ B))) = (integral+ (M,(f | A))) + (integral+ (M,(f | B)))

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

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

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

integral+ (M,(f | (A \/ B))) = (integral+ (M,(f | A))) + (integral+ (M,(f | B)))

proof end;

theorem Th82: :: MESFUNC5: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,ExtREAL

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

( E = dom f & f is_measurable_on E ) & f is nonnegative & M . A = 0 holds

integral+ (M,(f | A)) = 0

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

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

( E = dom f & f is_measurable_on E ) & f is nonnegative & M . A = 0 holds

integral+ (M,(f | A)) = 0

proof end;

theorem Th83: :: MESFUNC5: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,ExtREAL

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

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

integral+ (M,(f | A)) <= integral+ (M,(f | B))

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

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

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

integral+ (M,(f | A)) <= integral+ (M,(f | B))

proof end;

theorem Th84: :: MESFUNC5: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,ExtREAL

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

integral+ (M,(f | (E \ A))) = integral+ (M,f)

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

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

integral+ (M,(f | (E \ A))) = integral+ (M,f)

proof end;

theorem Th85: :: MESFUNC5:85

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

( E = dom f & E = dom g & f is_measurable_on E & g is_measurable_on E ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds

g . x <= f . x ) holds

integral+ (M,g) <= integral+ (M,f)

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st ex E being Element of S st

( E = dom f & E = dom g & f is_measurable_on E & g is_measurable_on E ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds

g . x <= f . x ) holds

integral+ (M,g) <= integral+ (M,f)

proof end;

theorem Th86: :: MESFUNC5: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,ExtREAL

for c being Real st 0 <= c & ex A being Element of S st

( A = dom f & f is_measurable_on A ) & f is nonnegative holds

integral+ (M,(c (#) f)) = (R_EAL c) * (integral+ (M,f))

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for c being Real st 0 <= c & ex A being Element of S st

( A = dom f & f is_measurable_on A ) & f is nonnegative holds

integral+ (M,(c (#) f)) = (R_EAL c) * (integral+ (M,f))

proof end;

theorem Th87: :: MESFUNC5: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,ExtREAL st ex A being Element of S st

( A = dom f & f is_measurable_on A ) & ( for x being Element of X st x in dom f holds

0 = f . x ) holds

integral+ (M,f) = 0

for S being SigmaField of X

for M being sigma_Measure of S

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

( A = dom f & f is_measurable_on A ) & ( for x being Element of X st x in dom f holds

0 = f . x ) holds

integral+ (M,f) = 0

proof end;

begin

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

(integral+ (M,(max+ f))) - (integral+ (M,(max- 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,ExtREAL;

func Integral (M,f) -> Element of ExtREAL equals :: MESFUNC5:def 16

(integral+ (M,(max+ f))) - (integral+ (M,(max- f)));

coherence (integral+ (M,(max+ f))) - (integral+ (M,(max- f)));

(integral+ (M,(max+ f))) - (integral+ (M,(max- f))) is Element of ExtREAL ;

:: deftheorem defines Integral MESFUNC5:def 16 :

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 holds Integral (M,f) = (integral+ (M,(max+ f))) - (integral+ (M,(max- 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,ExtREAL holds Integral (M,f) = (integral+ (M,(max+ f))) - (integral+ (M,(max- f)));

theorem Th88: :: MESFUNC5: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,ExtREAL st ex A being Element of S st

( A = dom f & f is_measurable_on A ) & f is nonnegative holds

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

for S being SigmaField of X

for M being sigma_Measure of S

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

( A = dom f & f is_measurable_on A ) & f is nonnegative holds

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

proof end;

theorem :: MESFUNC5: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,ExtREAL st f is_simple_func_in S & f is nonnegative holds

( Integral (M,f) = integral+ (M,f) & Integral (M,f) = integral' (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+ (M,f) & Integral (M,f) = integral' (M,f) )

proof end;

theorem :: MESFUNC5: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,ExtREAL st ex A being Element of S st

( A = dom f & f is_measurable_on A ) & f is nonnegative holds

0 <= Integral (M,f)

for S being SigmaField of X

for M being sigma_Measure of S

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

( A = dom f & f is_measurable_on A ) & f is nonnegative holds

0 <= Integral (M,f)

proof end;

theorem :: MESFUNC5: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,ExtREAL

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

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

Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

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

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

Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

proof end;

theorem :: MESFUNC5: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,ExtREAL

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

( E = dom f & f is_measurable_on E ) & f is nonnegative holds

0 <= Integral (M,(f | A))

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

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

( E = dom f & f is_measurable_on E ) & f is nonnegative holds

0 <= Integral (M,(f | A))

proof end;

theorem :: MESFUNC5: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,ExtREAL

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

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

Integral (M,(f | A)) <= Integral (M,(f | B))

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

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

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

Integral (M,(f | A)) <= Integral (M,(f | B))

proof end;

theorem :: MESFUNC5: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,ExtREAL

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

( E = dom f & f is_measurable_on E ) & M . A = 0 holds

Integral (M,(f | A)) = 0

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

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

( E = dom f & f is_measurable_on E ) & M . A = 0 holds

Integral (M,(f | A)) = 0

proof end;

theorem Th95: :: MESFUNC5: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,ExtREAL

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

Integral (M,(f | (E \ A))) = Integral (M,f)

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

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

Integral (M,(f | (E \ A))) = 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,ExtREAL;

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

let f be PartFunc of X,ExtREAL;

pred f is_integrable_on M means :Def17: :: MESFUNC5:def 17

( ex A being Element of S st

( A = dom f & f is_measurable_on A ) & integral+ (M,(max+ f)) < +infty & integral+ (M,(max- f)) < +infty );

( ex A being Element of S st

( A = dom f & f is_measurable_on A ) & integral+ (M,(max+ f)) < +infty & integral+ (M,(max- f)) < +infty );

:: deftheorem Def17 defines is_integrable_on MESFUNC5:def 17 :

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 holds

( f is_integrable_on M iff ( ex A being Element of S st

( A = dom f & f is_measurable_on A ) & integral+ (M,(max+ f)) < +infty & integral+ (M,(max- f)) < +infty ) );

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 holds

( f is_integrable_on M iff ( ex A being Element of S st

( A = dom f & f is_measurable_on A ) & integral+ (M,(max+ f)) < +infty & integral+ (M,(max- f)) < +infty ) );

theorem Th96: :: MESFUNC5:96

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

( 0 <= integral+ (M,(max+ f)) & 0 <= integral+ (M,(max- f)) & -infty < Integral (M,f) & Integral (M,f) < +infty )

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

( 0 <= integral+ (M,(max+ f)) & 0 <= integral+ (M,(max- f)) & -infty < Integral (M,f) & Integral (M,f) < +infty )

proof end;

theorem Th97: :: MESFUNC5: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,ExtREAL

for A being Element of S st f is_integrable_on M holds

( integral+ (M,(max+ (f | A))) <= integral+ (M,(max+ f)) & integral+ (M,(max- (f | A))) <= integral+ (M,(max- f)) & f | A is_integrable_on M )

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for A being Element of S st f is_integrable_on M holds

( integral+ (M,(max+ (f | A))) <= integral+ (M,(max+ f)) & integral+ (M,(max- (f | A))) <= integral+ (M,(max- f)) & f | A is_integrable_on M )

proof end;

theorem Th98: :: MESFUNC5:98

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for A, 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)))

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

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

proof end;

theorem :: MESFUNC5:99

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for A, 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))) )

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

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

proof end;

theorem Th100: :: MESFUNC5:100

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

( A = dom f & f is_measurable_on A ) holds

( f is_integrable_on M iff |.f.| is_integrable_on M )

for S being SigmaField of X

for M being sigma_Measure of S

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

( A = dom f & f is_measurable_on A ) holds

( f is_integrable_on M iff |.f.| is_integrable_on M )

proof end;

theorem :: MESFUNC5:101

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

|.(Integral (M,f)).| <= Integral (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

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

proof end;

theorem Th102: :: MESFUNC5:102

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

( A = dom f & f is_measurable_on A ) & 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,|.f.|) <= Integral (M,g) )

for S being SigmaField of X

for M being sigma_Measure of S

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

( A = dom f & f is_measurable_on A ) & 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,|.f.|) <= Integral (M,g) )

proof end;

theorem Th103: :: MESFUNC5:103

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for r being Real st dom f in S & 0 <= r & dom f <> {} & ( for x being set st x in dom f holds

f . x = r ) holds

integral (X,S,M,f) = r * (M . (dom f))

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for r being Real st dom f in S & 0 <= r & dom f <> {} & ( for x being set st x in dom f holds

f . x = r ) holds

integral (X,S,M,f) = r * (M . (dom f))

proof end;

theorem Th104: :: MESFUNC5: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,ExtREAL

for r being Real st dom f in S & 0 <= r & ( for x being set st x in dom f holds

f . x = r ) holds

integral' (M,f) = (R_EAL r) * (M . (dom f))

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for r being Real st dom f in S & 0 <= r & ( for x being set st x in dom f holds

f . x = r ) holds

integral' (M,f) = (R_EAL r) * (M . (dom f))

proof end;

theorem Th105: :: MESFUNC5:105

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 " {+infty} in S & f " {-infty} in S & M . (f " {+infty}) = 0 & M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 )

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 " {+infty} in S & f " {-infty} in S & M . (f " {+infty}) = 0 & M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 )

proof end;

theorem Th106: :: MESFUNC5:106

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,ExtREAL 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,ExtREAL 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 Th107: :: MESFUNC5:107

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,ExtREAL 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,ExtREAL st f is_integrable_on M & g is_integrable_on M holds

dom (f + g) in S

proof end;

Lm11: 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,ExtREAL st ex E0 being Element of S st

( dom (f + g) = E0 & f + g is_measurable_on E0 ) & f is_integrable_on M & g is_integrable_on M holds

f + g is_integrable_on M

proof end;

theorem Th108: :: MESFUNC5:108

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,ExtREAL 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,ExtREAL st f is_integrable_on M & g is_integrable_on M holds

f + g is_integrable_on M

proof end;

Lm12: 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,ExtREAL st f is_integrable_on M & g is_integrable_on M & dom f = dom g holds

ex E, NFG, NFPG being Element of S st

( E c= dom f & NFG c= dom f & E = (dom f) \ NFG & f | E is V60() & E = dom (f | E) & f | E is_measurable_on E & f | E is_integrable_on M & Integral (M,f) = Integral (M,(f | E)) & E c= dom g & NFG c= dom g & E = (dom g) \ NFG & g | E is V60() & E = dom (g | E) & g | E is_measurable_on E & g | E is_integrable_on M & Integral (M,g) = Integral (M,(g | E)) & E c= dom (f + g) & NFPG c= dom (f + g) & E = (dom (f + g)) \ NFPG & M . NFG = 0 & M . NFPG = 0 & E = dom ((f + g) | E) & (f + g) | E is_measurable_on E & (f + g) | E is_integrable_on M & (f + g) | E = (f | E) + (g | E) & Integral (M,((f + g) | E)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )

proof end;

Lm13: 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,ExtREAL st f is_integrable_on M & g is_integrable_on M & dom f = dom g holds

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

proof end;

theorem :: MESFUNC5:109

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,ExtREAL 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,ExtREAL 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 Th110: :: MESFUNC5:110

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

( c (#) f is_integrable_on M & Integral (M,(c (#) f)) = (R_EAL c) * (Integral (M,f)) )

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for c being Real st f is_integrable_on M holds

( c (#) f is_integrable_on M & Integral (M,(c (#) f)) = (R_EAL c) * (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,ExtREAL;

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

let B be Element of S;

coherence

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

:: deftheorem defines Integral_on MESFUNC5:def 18 :

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

for B being Element of S holds Integral_on (M,B,f) = Integral (M,(f | B));

theorem :: MESFUNC5:111

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

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

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 :: MESFUNC5:112

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 c 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,(c (#) f)) = (R_EAL c) * (Integral_on (M,B,f)) )

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for c 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,(c (#) f)) = (R_EAL c) * (Integral_on (M,B,f)) )

proof end;

:: Integral of Measurable Function