:: Series of Positive Real Numbers. Measure Theory :: by J\'ozef Bia{\l}as :: :: Received September 27, 1990 :: Copyright (c) 1990-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 CARD_1, SUPINF_1, ARYTM_3, REAL_1, ARYTM_1, XBOOLE_0, SUBSET_1, NUMBERS, TARSKI, XXREAL_0, MEMBERED, ORDINAL2, XXREAL_2, FUNCT_1, RELAT_1, VALUED_0, CARD_3, FUNCT_4, FUNCOP_1, PARTFUN1, NAT_1, SERIES_1, SUPINF_2, MEMBER_1, MESFUNC1; notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, MEMBERED, XXREAL_0, XXREAL_3, XCMPLX_0, XREAL_0, REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, FUNCOP_1, VALUED_0, FUNCT_4, NAT_1, CARD_3, XXREAL_2, SUPINF_1, MEMBER_1; constructors FUNCT_3, FUNCOP_1, FUNCT_4, FINSET_1, REAL_1, NAT_1, SUPINF_1, VALUED_1, XXREAL_2, XXREAL_3, CARD_3, RELSET_1, MEMBER_1, NUMBERS; registrations RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSET_1, NUMBERS, XREAL_0, MEMBERED, VALUED_0, XXREAL_3, RELSET_1, MEMBER_1, NAT_1; requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL; begin :: operations " + "," - " in R_eal numbers notation synonym 0. for 0; end; definition redefine func 0. -> R_eal; let x be R_eal; redefine func - x -> R_eal; let y be R_eal; redefine func x + y -> R_eal; redefine func x - y -> R_eal; end; theorem :: SUPINF_2:1 for x,y being ExtReal, a,b being Real st x = a & y = b holds x + y = a + b; theorem :: SUPINF_2:2 for x being ExtReal, a being Real st x = a holds - x = - a; theorem :: SUPINF_2:3 for x,y being ExtReal, a,b being Real st x = a & y = b holds x - y = a - b; :: Operations " + "," - " in a subset of ExtREAL notation let X,Y be Subset of ExtREAL; synonym X + Y for X ++ Y; end; definition let X,Y be Subset of ExtREAL; redefine func X + Y -> Subset of ExtREAL; end; notation let X be Subset of ExtREAL; synonym -X for --X; end; definition let X be Subset of ExtREAL; redefine func - X -> Subset of ExtREAL; end; ::$CT theorem :: SUPINF_2:5 for X being non empty Subset of ExtREAL, z being R_eal holds z in X iff - z in - X; theorem :: SUPINF_2:6 for X,Y being non empty Subset of ExtREAL holds X c= Y iff - X c= - Y; theorem :: SUPINF_2:7 for z being R_eal holds z in REAL iff - z in REAL; definition let X be ext-real-membered set; redefine func inf X -> R_eal; redefine func sup X -> R_eal; end; theorem :: SUPINF_2:8 for X,Y being non empty Subset of ExtREAL holds sup (X + Y) <= sup X + sup Y; theorem :: SUPINF_2:9 for X,Y being non empty Subset of ExtREAL holds inf X + inf Y <= inf (X + Y); theorem :: SUPINF_2:10 for X,Y being non empty Subset of ExtREAL holds X is bounded_above & Y is bounded_above implies sup (X + Y) <= sup X + sup Y; theorem :: SUPINF_2:11 for X,Y being non empty Subset of ExtREAL st X is bounded_below & Y is bounded_below holds inf X + inf Y <= inf (X + Y); theorem :: SUPINF_2:12 for X being non empty Subset of ExtREAL, a being R_eal holds a is UpperBound of X iff - a is LowerBound of - X; theorem :: SUPINF_2:13 for X being non empty Subset of ExtREAL holds for a being R_eal holds a is LowerBound of X iff - a is UpperBound of - X; theorem :: SUPINF_2:14 for X being non empty Subset of ExtREAL holds inf(- X) = - sup X; theorem :: SUPINF_2:15 for X be non empty Subset of ExtREAL holds sup(- X) = - inf X; definition let X be non empty set; let Y be non empty Subset of ExtREAL; let F be Function of X,Y; redefine func rng F -> non empty Subset of ExtREAL; end; :: sup F and inf F for Function of X,ExtREAL definition let D be ext-real-membered set; let X be set; let Y be Subset of D; let F be PartFunc of X,Y; func sup F -> Element of ExtREAL equals :: SUPINF_2:def 1 sup rng F; func inf F -> Element of ExtREAL equals :: SUPINF_2:def 2 inf rng F; end; definition let F be ext-real-valued Function; let x be set; redefine func F.x -> R_eal; end; definition let X be non empty set; let Y,Z be non empty Subset of ExtREAL; let F be Function of X,Y; let G be Function of X,Z; func F + G -> Function of X,Y + Z means :: SUPINF_2:def 3 for x being Element of X holds it.x = F.x + G.x; end; theorem :: SUPINF_2:16 for X being non empty set, Y,Z being non empty Subset of ExtREAL, F being Function of X,Y, G being Function of X,Z holds rng(F + G) c= rng F + rng G; theorem :: SUPINF_2:17 for X being non empty set, Y,Z being non empty Subset of ExtREAL for F being Function of X,Y for G being Function of X,Z holds sup(F + G) <= sup F + sup G; theorem :: SUPINF_2:18 for X being non empty set holds for Y,Z being non empty Subset of ExtREAL for F being Function of X,Y for G being Function of X,Z holds inf F + inf G <= inf(F + G); definition let X be non empty set; let Y be non empty Subset of ExtREAL; let F be Function of X,Y; func - F -> Function of X,- Y means :: SUPINF_2:def 4 for x being Element of X holds it.x = - F.x; end; theorem :: SUPINF_2:19 for X being non empty set, Y being non empty Subset of ExtREAL, F being Function of X,Y holds rng(- F) = - rng F; theorem :: SUPINF_2:20 for X being non empty set, Y being non empty Subset of ExtREAL for F being Function of X,Y holds inf(- F) = - sup F & sup(- F) = - inf F; :: Bounded Function of X,ExtREAL definition let X be set; let Y be Subset of ExtREAL; let F be Function of X,Y; attr F is bounded_above means :: SUPINF_2:def 5 sup F < +infty; attr F is bounded_below means :: SUPINF_2:def 6 -infty < inf F; end; definition let X be set, Y be Subset of ExtREAL, F be Function of X,Y; attr F is bounded means :: SUPINF_2:def 7 F is bounded_above bounded_below; end; registration let X be set; let Y be Subset of ExtREAL; cluster bounded -> bounded_above bounded_below for Function of X, Y; cluster bounded_above bounded_below -> bounded for Function of X, Y; end; theorem :: SUPINF_2:21 for X being non empty set, Y being non empty Subset of ExtREAL, F being Function of X,Y holds F is bounded iff sup F <+infty & -infty non empty Subset of ExtREAL; end; definition let N be sequence of ExtREAL; func Ser(N) -> sequence of ExtREAL means :: SUPINF_2:def 11 it.0 = N.0 & for n being Nat for y being R_eal st y = it.n holds it.(n + 1) = y + N.(n + 1); end; ::$CT 4 definition let R be Relation; attr R is nonnegative means :: SUPINF_2:def 12 rng R is nonnegative; end; definition let F be sequence of ExtREAL; func SUM(F) -> R_eal equals :: SUPINF_2:def 13 sup rng Ser(F); end; theorem :: SUPINF_2:39 for X being set, F being PartFunc of X,ExtREAL holds F is nonnegative iff for n being Element of X holds 0. <= F.n; theorem :: SUPINF_2:40 for F being sequence of ExtREAL, n being Nat st F is nonnegative holds (Ser F).n <= (Ser F).(n + 1) & 0. <= (Ser F).n; theorem :: SUPINF_2:41 for F being sequence of ExtREAL st F is nonnegative holds for n,m being Nat holds Ser(F).n <= Ser(F).(n + m); theorem :: SUPINF_2:42 for F1,F2 being sequence of ExtREAL st (for n being Element of NAT holds F1.n <= F2.n) holds for n being Element of NAT holds Ser(F1).n <= Ser(F2).n; theorem :: SUPINF_2:43 for F1,F2 being sequence of ExtREAL st (for n being Element of NAT holds F1.n <= F2.n) holds SUM(F1) <= SUM(F2); ::$CT theorem :: SUPINF_2:45 for F being sequence of ExtREAL st F is nonnegative holds (ex n being Element of NAT st F.n = +infty) implies SUM(F) = +infty; definition let F be sequence of ExtREAL; attr F is summable means :: SUPINF_2:def 14 SUM F in REAL; end; theorem :: SUPINF_2:46 for F being sequence of ExtREAL st F is nonnegative holds (ex n being Element of NAT st F.n = +infty) implies F is not summable; theorem :: SUPINF_2:47 for F1,F2 being sequence of ExtREAL st F1 is nonnegative & (for n being Element of NAT holds F1.n <= F2.n) holds (F2 is summable implies F1 is summable); theorem :: SUPINF_2:48 for F being sequence of ExtREAL st F is nonnegative holds for n being Nat st (for r being Element of NAT st n <= r holds F.r = 0.) holds SUM(F) = Ser(F).n; theorem :: SUPINF_2:49 for F being sequence of ExtREAL st (for n being Element of NAT holds F.n in REAL) holds for n being Nat holds Ser(F).n in REAL; theorem :: SUPINF_2:50 for F being sequence of ExtREAL st F is nonnegative & (ex n being Element of NAT st (for k being Element of NAT st n <= k holds F.k = 0.) & (for k being Element of NAT st k <= n holds F.k <> +infty)) holds F is summable; :: Added by AK, 2006.02.06 theorem :: SUPINF_2:51 for X being set, F being PartFunc of X,ExtREAL holds F is nonnegative iff for n being object holds 0. <= F.n; theorem :: SUPINF_2:52 for X being set, F being PartFunc of X,ExtREAL st for n being object st n in dom F holds 0. <= F.n holds F is nonnegative; definition func 1. -> R_eal equals :: SUPINF_2:def 15 1; end;