:: by Noboru Endou

::

:: Received September 3, 2017

:: Copyright (c) 2017-2018 Association of Mizar Users

registration

let X be non empty set ;

let f be nonnegative PartFunc of X,ExtREAL;

correctness

coherence

- f is nonpositive ;

end;
let f be nonnegative PartFunc of X,ExtREAL;

correctness

coherence

- f is nonpositive ;

proof end;

registration

let X be non empty set ;

let f be nonpositive PartFunc of X,ExtREAL;

correctness

coherence

- f is nonnegative ;

end;
let f be nonpositive PartFunc of X,ExtREAL;

correctness

coherence

- f is nonnegative ;

proof end;

theorem Th1: :: MESFUN11:1

for X being non empty set

for f being nonpositive PartFunc of X,ExtREAL

for E being set holds f | E is nonpositive

for f being nonpositive PartFunc of X,ExtREAL

for E being set holds f | E is nonpositive

proof end;

theorem Th2: :: MESFUN11:2

for X being non empty set

for A being set

for r being Real

for f being PartFunc of X,ExtREAL holds (r (#) f) | A = r (#) (f | A)

for A being set

for r being Real

for f being PartFunc of X,ExtREAL holds (r (#) f) | A = r (#) (f | A)

proof end;

theorem Th3: :: MESFUN11:3

for X being non empty set

for A being set

for f being PartFunc of X,ExtREAL holds - (f | A) = (- f) | A

for A being set

for f being PartFunc of X,ExtREAL holds - (f | A) = (- f) | A

proof end;

theorem Th4: :: MESFUN11:4

for X being non empty set

for f being PartFunc of X,ExtREAL

for c being Real st f is nonpositive holds

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

for f being PartFunc of X,ExtREAL

for c being Real st f is nonpositive holds

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

proof end;

theorem Th5: :: MESFUN11: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,ExtREAL holds

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

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 :: MESFUN11:6

for X being non empty set

for f being PartFunc of X,ExtREAL

for x being object holds

( f . x <= (max+ f) . x & f . x >= - ((max- f) . x) )

for f being PartFunc of X,ExtREAL

for x being object holds

( f . x <= (max+ f) . x & f . x >= - ((max- f) . x) )

proof end;

Lm1: for X being non empty set

for f being PartFunc of X,ExtREAL

for r being Real holds

( ( r > 0 implies less_dom (f,r) = less_dom ((max+ f),r) ) & ( r <= 0 implies less_dom (f,r) = great_dom ((max- f),(- r)) ) )

proof end;

theorem :: MESFUN11:7

theorem :: MESFUN11:8

theorem Th9: :: MESFUN11:9

for X being non empty set

for f, g being PartFunc of X,ExtREAL

for a being ExtReal

for r being Real st r <> 0 & g = r (#) f holds

eq_dom (f,a) = eq_dom (g,(a * r))

for f, g being PartFunc of X,ExtREAL

for a being ExtReal

for r being Real st r <> 0 & g = r (#) f holds

eq_dom (f,a) = eq_dom (g,(a * r))

proof end;

theorem Th10: :: MESFUN11:10

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 st A c= dom f holds

( f is_measurable_on A iff ( max+ f is_measurable_on A & max- f is_measurable_on A ) )

for S being SigmaField of X

for f being PartFunc of X,ExtREAL

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

( f is_measurable_on A iff ( max+ f is_measurable_on A & max- f is_measurable_on A ) )

proof end;

Lm2: for i, j being Nat st i <= j holds

ex k being Nat st j = i + k

proof end;

definition

let X be non empty set ;

let f be Function of X,ExtREAL;

let r be Real;

:: original: (#)

redefine func r (#) f -> Function of X,ExtREAL;

correctness

coherence

r (#) f is Function of X,ExtREAL;

end;
let f be Function of X,ExtREAL;

let r be Real;

:: original: (#)

redefine func r (#) f -> Function of X,ExtREAL;

correctness

coherence

r (#) f is Function of X,ExtREAL;

proof end;

theorem Th11: :: MESFUN11:11

for X being non empty set

for r being Real

for f being V121() Function of X,ExtREAL st r >= 0 holds

r (#) f is V121()

for r being Real

for f being V121() Function of X,ExtREAL st r >= 0 holds

r (#) f is V121()

proof end;

registration

let X be non empty set ;

let f be V121() Function of X,ExtREAL;

let r be non negative Real;

coherence

for b_{1} being Function of X,ExtREAL st b_{1} = r (#) f holds

b_{1} is without+infty
by Th11;

end;
let f be V121() Function of X,ExtREAL;

let r be non negative Real;

coherence

for b

b

theorem Th12: :: MESFUN11:12

for X being non empty set

for r being Real

for f being V121() Function of X,ExtREAL st r <= 0 holds

r (#) f is V120()

for r being Real

for f being V121() Function of X,ExtREAL st r <= 0 holds

r (#) f is V120()

proof end;

registration

let X be non empty set ;

let f be V121() Function of X,ExtREAL;

let r be non positive Real;

correctness

coherence

r (#) f is without-infty ;

by Th12;

end;
let f be V121() Function of X,ExtREAL;

let r be non positive Real;

correctness

coherence

r (#) f is without-infty ;

by Th12;

theorem Th13: :: MESFUN11:13

for X being non empty set

for r being Real

for f being V120() Function of X,ExtREAL st r >= 0 holds

r (#) f is V120()

for r being Real

for f being V120() Function of X,ExtREAL st r >= 0 holds

r (#) f is V120()

proof end;

registration

let X be non empty set ;

let f be V120() Function of X,ExtREAL;

let r be non negative Real;

correctness

coherence

r (#) f is without-infty ;

by Th13;

end;
let f be V120() Function of X,ExtREAL;

let r be non negative Real;

correctness

coherence

r (#) f is without-infty ;

by Th13;

theorem Th14: :: MESFUN11:14

for X being non empty set

for r being Real

for f being V120() Function of X,ExtREAL st r <= 0 holds

r (#) f is V121()

for r being Real

for f being V120() Function of X,ExtREAL st r <= 0 holds

r (#) f is V121()

proof end;

registration

let X be non empty set ;

let f be V120() Function of X,ExtREAL;

let r be non positive Real;

correctness

coherence

r (#) f is without+infty ;

by Th14;

end;
let f be V120() Function of X,ExtREAL;

let r be non positive Real;

correctness

coherence

r (#) f is without+infty ;

by Th14;

theorem Th15: :: MESFUN11:15

for X being non empty set

for r being Real

for f being V120() V121() Function of X,ExtREAL holds

( r (#) f is V120() & r (#) f is V121() )

for r being Real

for f being V120() V121() Function of X,ExtREAL holds

( r (#) f is V120() & r (#) f is V121() )

proof end;

registration

let X be non empty set ;

let f be V120() V121() Function of X,ExtREAL;

let r be Real;

correctness

coherence

( r (#) f is without-infty & r (#) f is without+infty );

by Th15;

end;
let f be V120() V121() Function of X,ExtREAL;

let r be Real;

correctness

coherence

( r (#) f is without-infty & r (#) f is without+infty );

by Th15;

theorem Th16: :: MESFUN11:16

for X being non empty set

for r being positive Real

for f being Function of X,ExtREAL holds

( f is V121() iff r (#) f is V121() )

for r being positive Real

for f being Function of X,ExtREAL holds

( f is V121() iff r (#) f is V121() )

proof end;

theorem Th17: :: MESFUN11:17

for X being non empty set

for r being negative Real

for f being Function of X,ExtREAL holds

( f is V121() iff r (#) f is V120() )

for r being negative Real

for f being Function of X,ExtREAL holds

( f is V121() iff r (#) f is V120() )

proof end;

theorem Th18: :: MESFUN11:18

for X being non empty set

for r being positive Real

for f being Function of X,ExtREAL holds

( f is V120() iff r (#) f is V120() )

for r being positive Real

for f being Function of X,ExtREAL holds

( f is V120() iff r (#) f is V120() )

proof end;

theorem Th19: :: MESFUN11:19

for X being non empty set

for r being negative Real

for f being Function of X,ExtREAL holds

( f is V120() iff r (#) f is V121() )

for r being negative Real

for f being Function of X,ExtREAL holds

( f is V120() iff r (#) f is V121() )

proof end;

theorem :: MESFUN11:20

for X being non empty set

for r being non zero Real

for f being Function of X,ExtREAL holds

( f is V120() & f is V121() iff ( r (#) f is V120() & r (#) f is V121() ) )

for r being non zero Real

for f being Function of X,ExtREAL holds

( f is V120() & f is V121() iff ( r (#) f is V120() & r (#) f is V121() ) )

proof end;

theorem Th21: :: MESFUN11:21

for X, Y being non empty set

for f being PartFunc of X,ExtREAL

for r being Real st f = Y --> r holds

( f is V120() & f is V121() )

for f being PartFunc of X,ExtREAL

for r being Real st f = Y --> r holds

( f is V120() & f is V121() )

proof end;

theorem :: MESFUN11:22

for X being non empty set

for f being Function of X,ExtREAL holds

( 0 (#) f = X --> 0 & 0 (#) f is V120() & 0 (#) f is V121() )

for f being Function of X,ExtREAL holds

( 0 (#) f = X --> 0 & 0 (#) f is V120() & 0 (#) f is V121() )

proof end;

theorem Th23: :: MESFUN11:23

for X being non empty set

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

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

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

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

proof end;

theorem :: MESFUN11:24

for X being non empty set

for f1, f2 being Function of X,ExtREAL st f2 is V120() & f2 is V121() holds

( f1 + f2 is Function of X,ExtREAL & ( for x being Element of X holds (f1 + f2) . x = (f1 . x) + (f2 . x) ) )

for f1, f2 being Function of X,ExtREAL st f2 is V120() & f2 is V121() holds

( f1 + f2 is Function of X,ExtREAL & ( for x being Element of X holds (f1 + f2) . x = (f1 . x) + (f2 . x) ) )

proof end;

theorem :: MESFUN11:25

for X being non empty set

for f1, f2 being Function of X,ExtREAL st f1 is V120() & f1 is V121() holds

( f1 - f2 is Function of X,ExtREAL & ( for x being Element of X holds (f1 - f2) . x = (f1 . x) - (f2 . x) ) )

for f1, f2 being Function of X,ExtREAL st f1 is V120() & f1 is V121() holds

( f1 - f2 is Function of X,ExtREAL & ( for x being Element of X holds (f1 - f2) . x = (f1 . x) - (f2 . x) ) )

proof end;

theorem :: MESFUN11:26

for X being non empty set

for f1, f2 being Function of X,ExtREAL st f2 is V120() & f2 is V121() holds

( f1 - f2 is Function of X,ExtREAL & ( for x being Element of X holds (f1 - f2) . x = (f1 . x) - (f2 . x) ) )

for f1, f2 being Function of X,ExtREAL st f2 is V120() & f2 is V121() holds

( f1 - f2 is Function of X,ExtREAL & ( for x being Element of X holds (f1 - f2) . x = (f1 . x) - (f2 . x) ) )

proof end;

theorem :: MESFUN11:27

for X, Y being non empty set

for f1, f2 being PartFunc of X,ExtREAL st dom f1 c= Y & f2 = Y --> 0 holds

( f1 + f2 = f1 & f1 - f2 = f1 & f2 - f1 = - f1 )

for f1, f2 being PartFunc of X,ExtREAL st dom f1 c= Y & f2 = Y --> 0 holds

( f1 + f2 = f1 & f1 - f2 = f1 & f2 - f1 = - f1 )

proof end;

theorem Th28: :: MESFUN11:28

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

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

f + g is_simple_func_in S

proof end;

theorem :: MESFUN11:29

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 holds

f - g is_simple_func_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_simple_func_in S & g is_simple_func_in S holds

f - g is_simple_func_in S

proof end;

theorem Th30: :: MESFUN11:30

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_simple_func_in S

for S being SigmaField of X

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

- f is_simple_func_in S

proof end;

theorem Th33: :: MESFUN11:33

for C being non empty set

for f being PartFunc of C,ExtREAL

for c being Real st c <= 0 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 c <= 0 holds

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

proof end;

theorem Th35: :: MESFUN11:35

for X being non empty set

for f being PartFunc of X,ExtREAL

for r1, r2 being Real holds r1 (#) (r2 (#) f) = (r1 * r2) (#) f

for f being PartFunc of X,ExtREAL

for r1, r2 being Real holds r1 (#) (r2 (#) f) = (r1 * r2) (#) f

proof end;

definition

let X be non empty set ;

let F be Functional_Sequence of X,ExtREAL;

let r be Real;

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

for n being Nat holds b_{1} . n = r (#) (F . n)

for b_{1}, b_{2} being Functional_Sequence of X,ExtREAL st ( for n being Nat holds b_{1} . n = r (#) (F . n) ) & ( for n being Nat holds b_{2} . n = r (#) (F . n) ) holds

b_{1} = b_{2}

end;
let F be Functional_Sequence of X,ExtREAL;

let r be Real;

func r (#) F -> Functional_Sequence of X,ExtREAL means :Def1: :: MESFUN11:def 1

for n being Nat holds it . n = r (#) (F . n);

existence for n being Nat holds it . n = r (#) (F . n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines (#) MESFUN11:def 1 :

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for r being Real

for b_{4} being Functional_Sequence of X,ExtREAL holds

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

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for r being Real

for b

( b

definition

let X be non empty set ;

let F be Functional_Sequence of X,ExtREAL;

correctness

coherence

(- 1) (#) F is Functional_Sequence of X,ExtREAL;

;

end;
let F be Functional_Sequence of X,ExtREAL;

correctness

coherence

(- 1) (#) F is Functional_Sequence of X,ExtREAL;

;

:: deftheorem defines - MESFUN11:def 2 :

for X being non empty set

for F being Functional_Sequence of X,ExtREAL holds - F = (- 1) (#) F;

for X being non empty set

for F being Functional_Sequence of X,ExtREAL holds - F = (- 1) (#) F;

theorem Th37: :: MESFUN11:37

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for n being Nat holds (- F) . n = - (F . n)

for F being Functional_Sequence of X,ExtREAL

for n being Nat holds (- F) . n = - (F . n)

proof end;

theorem Th38: :: MESFUN11:38

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for x being Element of X holds (- F) # x = - (F # x)

for F being Functional_Sequence of X,ExtREAL

for x being Element of X holds (- F) # x = - (F # x)

proof end;

theorem Th39: :: MESFUN11:39

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for x being Element of X holds

( ( F # x is convergent_to_+infty implies (- F) # x is convergent_to_-infty ) & ( (- F) # x is convergent_to_-infty implies F # x is convergent_to_+infty ) & ( F # x is convergent_to_-infty implies (- F) # x is convergent_to_+infty ) & ( (- F) # x is convergent_to_+infty implies F # x is convergent_to_-infty ) & ( F # x is convergent_to_finite_number implies (- F) # x is convergent_to_finite_number ) & ( (- F) # x is convergent_to_finite_number implies F # x is convergent_to_finite_number ) & ( F # x is convergent implies (- F) # x is convergent ) & ( (- F) # x is convergent implies F # x is convergent ) & ( F # x is convergent implies lim ((- F) # x) = - (lim (F # x)) ) )

for F being Functional_Sequence of X,ExtREAL

for x being Element of X holds

( ( F # x is convergent_to_+infty implies (- F) # x is convergent_to_-infty ) & ( (- F) # x is convergent_to_-infty implies F # x is convergent_to_+infty ) & ( F # x is convergent_to_-infty implies (- F) # x is convergent_to_+infty ) & ( (- F) # x is convergent_to_+infty implies F # x is convergent_to_-infty ) & ( F # x is convergent_to_finite_number implies (- F) # x is convergent_to_finite_number ) & ( (- F) # x is convergent_to_finite_number implies F # x is convergent_to_finite_number ) & ( F # x is convergent implies (- F) # x is convergent ) & ( (- F) # x is convergent implies F # x is convergent ) & ( F # x is convergent implies lim ((- F) # x) = - (lim (F # x)) ) )

proof end;

theorem Th40: :: MESFUN11:40

for X being non empty set

for F being Functional_Sequence of X,ExtREAL st F is with_the_same_dom holds

- F is with_the_same_dom

for F being Functional_Sequence of X,ExtREAL st F is with_the_same_dom holds

- F is with_the_same_dom

proof end;

theorem Th41: :: MESFUN11:41

for X being non empty set

for F being Functional_Sequence of X,ExtREAL st F is additive holds

- F is additive

for F being Functional_Sequence of X,ExtREAL st F is additive holds

- F is additive

proof end;

theorem Th42: :: MESFUN11:42

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for n being Nat holds (Partial_Sums (- F)) . n = (- (Partial_Sums F)) . n

for F being Functional_Sequence of X,ExtREAL

for n being Nat holds (Partial_Sums (- F)) . n = (- (Partial_Sums F)) . n

proof end;

theorem Th43: :: MESFUN11:43

for seq being ExtREAL_sequence

for n being Nat holds (Partial_Sums (- seq)) . n = - ((Partial_Sums seq) . n)

for n being Nat holds (Partial_Sums (- seq)) . n = - ((Partial_Sums seq) . n)

proof end;

theorem Th46: :: MESFUN11:46

for X being non empty set

for F being Functional_Sequence of X,ExtREAL st ( for n being Nat holds F . n is V121() ) holds

F is additive

for F being Functional_Sequence of X,ExtREAL st ( for n being Nat holds F . n is V121() ) holds

F is additive

proof end;

theorem Th47: :: MESFUN11:47

for X being non empty set

for F being Functional_Sequence of X,ExtREAL st ( for n being Nat holds F . n is V120() ) holds

F is additive

for F being Functional_Sequence of X,ExtREAL st ( for n being Nat holds F . n is V120() ) holds

F is additive

proof end;

theorem Th48: :: MESFUN11:48

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for x being Element of X st F # x is summable holds

( (- F) # x is summable & Sum ((- F) # x) = - (Sum (F # x)) )

for F being Functional_Sequence of X,ExtREAL

for x being Element of X st F # x is summable holds

( (- F) # x is summable & Sum ((- F) # x) = - (Sum (F # x)) )

proof end;

theorem Th49: :: MESFUN11:49

for X being non empty set

for S being SigmaField of X

for F being Functional_Sequence of X,ExtREAL st F is additive & F is with_the_same_dom & ( for x being Element of X st x in dom (F . 0) holds

F # x is summable ) holds

lim (Partial_Sums (- F)) = - (lim (Partial_Sums F))

for S being SigmaField of X

for F being Functional_Sequence of X,ExtREAL st F is additive & F is with_the_same_dom & ( for x being Element of X st x in dom (F . 0) holds

F # x is summable ) holds

lim (Partial_Sums (- F)) = - (lim (Partial_Sums F))

proof end;

theorem Th50: :: MESFUN11:50

for X being non empty set

for S being SigmaField of X

for F, G being Functional_Sequence of X,ExtREAL

for E being Element of S st E c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds G . n = (F . n) | E ) holds

lim (Partial_Sums G) = (lim (Partial_Sums F)) | E

for S being SigmaField of X

for F, G being Functional_Sequence of X,ExtREAL

for E being Element of S st E c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds G . n = (F . n) | E ) holds

lim (Partial_Sums G) = (lim (Partial_Sums F)) | E

proof end;

theorem :: MESFUN11:51

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f being nonnegative PartFunc of X,ExtREAL holds integral' (M,(max- (- f))) = integral' (M,f)

for S being SigmaField of X

for M being sigma_Measure of S

for f being nonnegative PartFunc of X,ExtREAL holds integral' (M,(max- (- f))) = integral' (M,f)

proof end;

theorem Th52: :: MESFUN11:52

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 A = dom f & f is_measurable_on A 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

for A being Element of S st A = dom f & f is_measurable_on A holds

Integral (M,(- f)) = - (Integral (M,f))

proof end;

theorem :: MESFUN11:53

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f being nonnegative PartFunc of X,ExtREAL

for E being Element of S st E = dom f & f is_measurable_on E holds

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

for S being SigmaField of X

for M being sigma_Measure of S

for f being nonnegative PartFunc of X,ExtREAL

for E being Element of S st E = dom f & f is_measurable_on E holds

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

proof end;

theorem :: MESFUN11:54

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for E being Element of S st E = dom f & f is_measurable_on E holds

Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f)))

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for E being Element of S st E = dom f & f is_measurable_on E holds

Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f)))

proof end;

theorem Th55: :: MESFUN11:55

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for E being Element of S st E c= dom f & f is_measurable_on E holds

Integral (M,((- f) | E)) = - (Integral (M,(f | E)))

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for E being Element of S st E c= dom f & f is_measurable_on E holds

Integral (M,((- f) | E)) = - (Integral (M,(f | E)))

proof end;

theorem Th56: :: MESFUN11:56

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 nonpositive 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 nonpositive ) & ( 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 nonpositive 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 nonpositive ) & ( 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;

theorem Th57: :: MESFUN11:57

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

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

( A = dom f & f is_measurable_on A ) holds

( Integral (M,f) = - (integral+ (M,(max- f))) & 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 E being Element of S

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

( A = dom f & f is_measurable_on A ) holds

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

proof end;

theorem Th58: :: MESFUN11:58

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

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

( Integral (M,f) = - (integral' (M,(- f))) & Integral (M,f) = - (integral' (M,(max- f))) )

for S being SigmaField of X

for M being sigma_Measure of S

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

( Integral (M,f) = - (integral' (M,(- f))) & Integral (M,f) = - (integral' (M,(max- f))) )

proof end;

Lm3: 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 nonpositive & 0 <= c holds

( Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) & Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) )

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

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

proof end;

theorem Th59: :: MESFUN11:59

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 holds

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

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

proof end;

theorem :: MESFUN11:60

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 nonpositive holds

( Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) & Integral (M,(c (#) f)) = - (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 nonpositive holds

( Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) & Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) )

proof end;

theorem Th61: :: MESFUN11:61

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 nonpositive 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 nonpositive holds

0 >= Integral (M,f)

proof end;

theorem :: MESFUN11:62

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, E being Element of S st E = dom f & f is_measurable_on E & f is nonpositive & 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, E being Element of S st E = dom f & f is_measurable_on E & f is nonpositive & A misses B holds

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

proof end;

theorem :: MESFUN11:63

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

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

proof end;

theorem :: MESFUN11:64

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, E being Element of S st E = dom f & f is_measurable_on E & f is nonpositive & 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, E being Element of S st E = dom f & f is_measurable_on E & f is nonpositive & A c= B holds

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

proof end;

theorem :: MESFUN11:65

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f being PartFunc of X,ExtREAL st E = dom f & f is_measurable_on E & f is nonpositive & M . (E /\ (eq_dom (f,-infty))) <> 0 holds

Integral (M,f) = -infty

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f being PartFunc of X,ExtREAL st E = dom f & f is_measurable_on E & f is nonpositive & M . (E /\ (eq_dom (f,-infty))) <> 0 holds

Integral (M,f) = -infty

proof end;

theorem :: MESFUN11:66

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f, g being PartFunc of X,ExtREAL st E c= dom f & E c= dom g & f is_measurable_on E & g is_measurable_on E & f is nonpositive & ( for x being Element of X st x in E holds

g . x <= f . x ) holds

Integral (M,(g | E)) <= Integral (M,(f | E))

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f, g being PartFunc of X,ExtREAL st E c= dom f & E c= dom g & f is_measurable_on E & g is_measurable_on E & f is nonpositive & ( for x being Element of X st x in E holds

g . x <= f . x ) holds

Integral (M,(g | E)) <= Integral (M,(f | E))

proof end;

theorem Th67: :: MESFUN11:67

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for S being SigmaField of X

for E being Element of S

for m being Nat st F is with_the_same_dom & E = dom (F . 0) & ( for n being Nat holds

( F . n is_measurable_on E & F . n is V121() ) ) holds

(Partial_Sums F) . m is_measurable_on E

for F being Functional_Sequence of X,ExtREAL

for S being SigmaField of X

for E being Element of S

for m being Nat st F is with_the_same_dom & E = dom (F . 0) & ( for n being Nat holds

( F . n is_measurable_on E & F . n is V121() ) ) holds

(Partial_Sums F) . m is_measurable_on E

proof end;

theorem :: MESFUN11:68

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S

for I being ExtREAL_sequence

for m being Nat st E = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds

( F . n is_measurable_on E & F . n is nonpositive & I . n = Integral (M,(F . n)) ) ) holds

Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m

for S being SigmaField of X

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S

for I being ExtREAL_sequence

for m being Nat st E = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds

( F . n is_measurable_on E & F . n is nonpositive & I . n = Integral (M,(F . n)) ) ) holds

Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m

proof end;

theorem :: MESFUN11:69

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S

for f being PartFunc of X,ExtREAL st E c= dom f & f is nonpositive & f is_measurable_on E & ( for n being Nat holds

( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds

( F # x is summable & f . x = Sum (F # x) ) ) holds

ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I )

for S being SigmaField of X

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S

for f being PartFunc of X,ExtREAL st E c= dom f & f is nonpositive & f is_measurable_on E & ( for n being Nat holds

( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds

( F # x is summable & f . x = Sum (F # x) ) ) holds

ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I )

proof end;

theorem :: MESFUN11:70

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f being PartFunc of X,ExtREAL st E c= dom f & f is nonpositive & f is_measurable_on E holds

ex F being Functional_Sequence of X,ExtREAL st

( F is additive & ( for n being Nat holds

( F . n is_simple_func_in S & F . n is nonpositive & F . n is_measurable_on E ) ) & ( for x being Element of X st x in E holds

( F # x is summable & f . x = Sum (F # x) ) ) & ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I ) )

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f being PartFunc of X,ExtREAL st E c= dom f & f is nonpositive & f is_measurable_on E holds

ex F being Functional_Sequence of X,ExtREAL st

( F is additive & ( for n being Nat holds

( F . n is_simple_func_in S & F . n is nonpositive & F . n is_measurable_on E ) ) & ( for x being Element of X st x in E holds

( F # x is summable & f . x = Sum (F # x) ) ) & ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I ) )

proof end;

theorem :: MESFUN11:71

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E = dom (F . 0) & F is with_the_same_dom & ( for n being Nat holds

( F . n is nonpositive & F . n is_measurable_on E ) ) holds

ex FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) st

for n being Nat holds

( ( for m being Nat holds

( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) )

for S being SigmaField of X

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E = dom (F . 0) & F is with_the_same_dom & ( for n being Nat holds

( F . n is nonpositive & F . n is_measurable_on E ) ) holds

ex FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) st

for n being Nat holds

( ( for m being Nat holds

( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds

for x being Element of X st x in dom (F . n) holds

((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds

( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) )

proof end;

theorem :: MESFUN11:72

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds

( F . n is_measurable_on E & F . n is nonpositive ) ) holds

ex I being ExtREAL_sequence st

for n being Nat holds

( I . n = Integral (M,(F . n)) & Integral (M,((Partial_Sums F) . n)) = (Partial_Sums I) . n )

for S being SigmaField of X

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds

( F . n is_measurable_on E & F . n is nonpositive ) ) holds

ex I being ExtREAL_sequence st

for n being Nat holds

( I . n = Integral (M,(F . n)) & Integral (M,((Partial_Sums F) . n)) = (Partial_Sums I) . n )

proof end;

theorem :: MESFUN11:73

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds

( F . n is nonpositive & F . n is_measurable_on E ) ) & ( for x being Element of X st x in E holds

F # x is summable ) holds

ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )

for S being SigmaField of X

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds

( F . n is nonpositive & F . n is_measurable_on E ) ) & ( for x being Element of X st x in E holds

F # x is summable ) holds

ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )

proof end;

theorem :: MESFUN11:74

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E = dom (F . 0) & F . 0 is nonpositive & F is with_the_same_dom & ( for n being Nat holds F . n is_measurable_on E ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in E holds

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

F # x is convergent ) holds

ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I )

for S being SigmaField of X

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E = dom (F . 0) & F . 0 is nonpositive & F is with_the_same_dom & ( for n being Nat holds F . n is_measurable_on E ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in E holds

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

F # x is convergent ) holds

ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I )

proof end;