:: 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;