:: by Noboru Endou and Yasunari Shidama

::

:: Received September 14, 2005

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

theorem Th1: :: MESFUNC4:1

for F, G, H being FinSequence of ExtREAL st F is nonnegative & G is nonnegative & dom F = dom G & H = F + G holds

Sum H = (Sum F) + (Sum G)

Sum H = (Sum F) + (Sum G)

proof end;

theorem Th2: :: MESFUNC4:2

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for n being Nat

for f being PartFunc of X,ExtREAL

for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds

x . i = (a . i) * ((M * F) . i) ) & len F = n holds

integral (M,f) = Sum x

for S being SigmaField of X

for M being sigma_Measure of S

for n being Nat

for f being PartFunc of X,ExtREAL

for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds

x . i = (a . i) * ((M * F) . i) ) & len F = n holds

integral (M,f) = Sum x

proof end;

theorem Th3: :: MESFUNC4:3

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,ExtREAL

for M being sigma_Measure of S

for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds

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

integral (M,f) = Sum x

for S being SigmaField of X

for f being PartFunc of X,ExtREAL

for M being sigma_Measure of S

for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds

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

integral (M,f) = Sum x

proof end;

theorem Th4: :: MESFUNC4:4

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,ExtREAL

for M being sigma_Measure of S st f is_simple_func_in S & dom f <> {} & f is nonnegative holds

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

( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & integral (M,f) = Sum x )

for S being SigmaField of X

for f being PartFunc of X,ExtREAL

for M being sigma_Measure of S st f is_simple_func_in S & dom f <> {} & f is nonnegative holds

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

( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & integral (M,f) = Sum x )

proof end;

theorem :: MESFUNC4:5

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 holds

( f + g is_simple_func_in S & dom (f + g) <> {} & ( for x being object st x in dom (f + g) holds

0. <= (f + g) . x ) & integral (M,(f + g)) = (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 f is_simple_func_in S & dom f <> {} & f is nonnegative & g is_simple_func_in S & dom g = dom f & g is nonnegative holds

( f + g is_simple_func_in S & dom (f + g) <> {} & ( for x being object st x in dom (f + g) holds

0. <= (f + g) . x ) & integral (M,(f + g)) = (integral (M,f)) + (integral (M,g)) )

proof end;

theorem :: MESFUNC4:6

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 c being R_eal st f is_simple_func_in S & dom f <> {} & f is nonnegative & 0. <= c & c < +infty & dom g = dom f & ( for x being set st x in dom g holds

g . x = c * (f . x) ) holds

integral (M,g) = c * (integral (M,f))

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL

for c being R_eal st f is_simple_func_in S & dom f <> {} & f is nonnegative & 0. <= c & c < +infty & dom g = dom f & ( for x being set st x in dom g holds

g . x = c * (f . x) ) holds

integral (M,g) = c * (integral (M,f))

proof end;