:: Linearity of {L}ebesgue Integral of Simple Valued Function :: by Noboru Endou and Yasunari Shidama :: :: Received September 14, 2005 :: Copyright (c) 2005-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies 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 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; constructors PARTFUN1, REAL_1, NAT_1, NAT_D, FINSEQOP, EXTREAL1, MESFUNC1, BINARITH, MESFUNC2, MESFUNC3, SUPINF_1, RELSET_1, NUMBERS; registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, MEASURE1, VALUED_0, MEMBERED, CARD_1, XXREAL_3; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin :: Linearity of Lebesgue Integral of Simple Valued Function theorem :: MESFUNC4:1 for F,G,H be FinSequence of ExtREAL st F is nonnegative & G is nonnegative & dom F = dom G & H = F + G holds Sum(H)=Sum(F)+Sum(G); theorem :: MESFUNC4:2 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S holds for n be Nat, f be PartFunc of X,ExtREAL, F be Finite_Sep_Sequence of S, a,x be 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 be Nat st i in dom x holds x.i=a.i*(M*F).i) & len F = n holds integral(M,f)=Sum(x); theorem :: MESFUNC4:3 for X be non empty set, S be SigmaField of X, f be PartFunc of X, ExtREAL, M be sigma_Measure of S, F be Finite_Sep_Sequence of S, a,x be 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 be Nat st n in dom x holds x.n=a.n*(M*F).n) holds integral(M,f)=Sum( x); theorem :: MESFUNC4:4 for X be non empty set, S be SigmaField of X, f be PartFunc of X, ExtREAL, M be sigma_Measure of S st f is_simple_func_in S & dom f <> {} & f is nonnegative ex F be Finite_Sep_Sequence of S, a,x be FinSequence of ExtREAL st F,a are_Re-presentation_of f & dom x = dom F & (for n be Nat st n in dom x holds x.n=a.n*(M*F).n) & integral(M,f)=Sum(x); theorem :: MESFUNC4:5 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be 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 be object st x in dom (f+g) holds 0. <= (f+g).x) & integral( M,f+g)=integral(M,f)+integral(M,g); theorem :: MESFUNC4:6 for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X,ExtREAL, c be R_eal st f is_simple_func_in S & dom f <> {} & f is nonnegative & 0. <= c & c < +infty & dom g = dom f & (for x be set st x in dom g holds g.x=c*f.x) holds integral(M,g)=c* integral(M,f);