begin
begin
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 )
begin
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
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) <> {} )
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
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))
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 )
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 )
begin
Lm8:
for J being ExtREAL_sequence holds
( not J is () or sup (rng J) in REAL or sup (rng J) = +infty )
begin
begin
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)) )
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
;
existence
ex b1 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 & b1 = lim K )
uniqueness
for b1, b2 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 & b1 = 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 & b2 = lim K ) holds
b1 = b2
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))
begin
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
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))) )
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)) )
:: Integral of Measurable Function