MESFUNC4: Linearity of {L}ebesgue Integral of Simple Valued Function

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

environ

vocabularies HIDDEN, NUMBERS, FINSEQ_1, NAT_1, RELAT_1, SUPINF_2, XXREAL_0, FUNCT_1, ARYTM_3, CARD_3, SUBSET_1, XBOOLE_0, CARD_1, PROB_1, MEASURE1, PARTFUN1, MESFUNC2, MESFUNC3, INTEGRA1, VALUED_0, TARSKI, COMPLEX1, MESFUNC1, ORDINAL4, ARYTM_1, INT_1, SUPINF_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, XXREAL_3, EXTREAL1, XCMPLX_0, XREAL_0, NAT_1, NAT_D, PROB_1, SUPINF_1, SUPINF_2, MEASURE1, MESFUNC1, MESFUNC2, MESFUNC3;
definitions TARSKI, XBOOLE_0;
theorems MEASURE1, TARSKI, FUNCT_1, NAT_1, MESFUNC1, ZFMISC_1, FINSEQ_1, FINSEQ_2, FINSEQ_5, PROB_2, XBOOLE_0, XBOOLE_1, RELAT_1, MESFUNC2, EXTREAL1, MESFUNC3, XREAL_1, NAT_2, FINSEQ_3, XXREAL_0, PROB_1, FINSUB_1, ORDINAL1, NAT_D, VALUED_0, XXREAL_3, NUMBERS, SUPINF_2;
schemes FINSEQ_1, FINSEQ_2, NAT_1;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, MEASURE1, VALUED_0, MEMBERED, CARD_1, XXREAL_3;
constructors HIDDEN, PARTFUN1, REAL_1, NAT_1, NAT_D, FINSEQOP, EXTREAL1, MESFUNC1, BINARITH, MESFUNC2, MESFUNC3, SUPINF_1, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, SUPINF_2;
expansions TARSKI, XBOOLE_0;

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)

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

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

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 )

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

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

proof end;