:: Linearity of {L}ebesgue Integral of Simple Valued Function
:: by Noboru Endou and Yasunari Shidama
::
:: Received September 14, 2005
:: Copyright (c) 2005-2012 Association of Mizar Users


begin

theorem Th1: :: MESFUNC4:1
for F, G, H being FinSequence of ExtREAL st ( for i being Nat st i in dom F holds
0. <= F . i ) & ( for i being Nat st i in dom G holds
0. <= G . i ) & dom F = dom G & H = F + G holds
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 <> {} & ( for x being set st x in dom f holds
0. <= f . x ) & 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 (X,S,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 <> {} & ( for x being set st x in dom f holds
0. <= f . x ) & 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 (X,S,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 <> {} & ( for x being set st x in dom f holds
0. <= f . x ) 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 (X,S,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 <> {} & ( for x being set st x in dom f holds
0. <= f . x ) & g is_simple_func_in S & dom g = dom f & ( for x being set st x in dom g holds
0. <= g . x ) holds
( f + g is_simple_func_in S & dom (f + g) <> {} & ( for x being set st x in dom (f + g) holds
0. <= (f + g) . x ) & integral (X,S,M,(f + g)) = (integral (X,S,M,f)) + (integral (X,S,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 <> {} & ( for x being set st x in dom f holds
0. <= f . x ) & 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 (X,S,M,g) = c * (integral (X,S,M,f))
proof end;