:: Series of Positive Real Numbers. Measure Theory
:: by J\'ozef Bia{\l}as
::
:: Received September 27, 1990
:: Copyright (c) 1990-2026 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;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, XCMPLX_0, XXREAL_0, XXREAL_3, MEMBER_1;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, FUNCT_1, FUNCT_2, NAT_1, RELSET_1, CARD_4, FUNCT_4, FUNCOP_1,
RELAT_1, ZFMISC_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1,
NUMBERS, XXREAL_2, XXREAL_3, CARD_3, MEMBER_1, MEMBERED, XREAL_0;
schemes FUNCT_2, RECDEF_1, NAT_1;
begin :: operations " + "," - " in R_eal numbers
notation
synonym 0. for 0;
end;
definition
redefine func 0. -> R_eal; :: redefines 0. (SUPINF_2, synonym) → 0 (ORDINAL1, definition)
coherence by XXREAL_0:def 1;
end;
theorem
for x,y being ExtReal, a,b being Real st x = a & y = b holds
x + y = a + b by XXREAL_3:def 2;
theorem
for x being ExtReal, a being Real st x = a holds - x = - a
by XXREAL_3:def 3;
theorem
for x,y being ExtReal, a,b being Real
st x = a & y = b holds x - y = a - b
proof
let x,y be ExtReal, a,b be Real;
assume
A1: x = a;
assume y = b;
then -y = -b by XXREAL_3:def 3;
hence thesis by A1,XXREAL_3:def 2;
end;
:: 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; :: redefines + (SUPINF_2, synonym) → ++ (MEMBER_1, definition)
coherence by MEMBERED:2;
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; :: redefines - (SUPINF_2, synonym) → -- (MEMBER_1, definition)
coherence by MEMBERED:2;
end;
::$CT
theorem
for X being non empty Subset of ExtREAL, z being R_eal holds
z in X iff - z in - X by MEMBER_1:1;
theorem
for X,Y being non empty Subset of ExtREAL holds X c= Y iff - X c= - Y
by MEMBER_1:3;
theorem
for z being R_eal holds z in REAL iff - z in REAL
proof
let z be R_eal;
A1: for z being R_eal holds z in REAL implies - z in REAL
proof
let z be R_eal;
A2: - z in REAL or - z in {-infty,+infty} by XBOOLE_0:def 3;
assume z in REAL;
hence thesis by A2,TARSKI:def 2;
end;
- z in REAL implies z in REAL
proof
assume -z in REAL;
then - -z in REAL by A1;
hence thesis;
end;
hence thesis by A1;
end;
definition
let X be ext-real-membered set;
redefine func inf X -> R_eal; :: redefines inf (XXREAL_2, definition)
coherence by XXREAL_0:def 1;
redefine func sup X -> R_eal; :: redefines sup (XXREAL_2, definition)
coherence by XXREAL_0:def 1;
end;
theorem Th7:
for X,Y being non empty Subset of ExtREAL holds sup (X + Y) <= sup X + sup Y
proof
let X,Y be non empty Subset of ExtREAL;
for z being ExtReal holds z in X + Y implies z <= sup X + sup Y
proof
let z be ExtReal;
assume z in X + Y;
then consider x,y being R_eal such that
A1: z = x + y and
A2: x in X and
A3: y in Y;
A4: y <= sup Y by A3,XXREAL_2:4;
x <= sup X by A2,XXREAL_2:4;
hence thesis by A1,A4,XXREAL_3:36;
end;
then sup X + sup Y is UpperBound of X + Y by XXREAL_2:def 1;
hence thesis by XXREAL_2:def 3;
end;
theorem Th8:
for X,Y being non empty Subset of ExtREAL holds inf X + inf Y <= inf (X + Y)
proof
let X,Y be non empty Subset of ExtREAL;
for z being ExtReal holds z in X + Y implies inf X + inf Y <= z
proof
let z be ExtReal;
assume z in X + Y;
then consider x,y being R_eal such that
A1: z = x + y and
A2: x in X and
A3: y in Y;
A4: inf Y <= y by A3,XXREAL_2:3;
inf X <= x by A2,XXREAL_2:3;
hence thesis by A1,A4,XXREAL_3:36;
end;
then inf X + inf Y is LowerBound of X + Y by XXREAL_2:def 2;
hence thesis by XXREAL_2:def 4;
end;
theorem
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 by Th7;
theorem
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) by Th8;
theorem Th11:
for X being non empty Subset of ExtREAL, a being R_eal holds
a is UpperBound of X iff - a is LowerBound of - X
proof
let X be non empty Subset of ExtREAL;
let a be R_eal;
hereby
assume
A1: a is UpperBound of X;
for x being ExtReal st x in - X holds -a <= x
proof
let x be ExtReal;
assume
A2: x in - X;
reconsider x as Element of ExtREAL by XXREAL_0:def 1;
- x in - -X by A2;
then - a <= - -x by XXREAL_3:38,A1,XXREAL_2:def 1;
hence thesis;
end;
hence - a is LowerBound of - X by XXREAL_2:def 2;
end;
assume
A3: - a is LowerBound of - X;
for x being ExtReal st x in X holds x <=a
proof
let x be ExtReal;
assume
A4: x in X;
reconsider x as Element of ExtREAL by XXREAL_0:def 1;
- x in - X by A4;
hence thesis by XXREAL_3:38,A3,XXREAL_2:def 2;
end;
hence thesis by XXREAL_2:def 1;
end;
theorem Th12:
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
proof
let X be non empty Subset of ExtREAL;
let a be R_eal;
hereby
assume
A1: a is LowerBound of X;
for x being ExtReal st x in - X holds x <= - a
proof
let x be ExtReal;
assume
A2: x in - X;
reconsider x as Element of ExtREAL by XXREAL_0:def 1;
- x in - (- X) by A2;
then - (- x) <= - a by XXREAL_3:38,A1,XXREAL_2:def 2;
hence thesis;
end;
hence - a is UpperBound of - X by XXREAL_2:def 1;
end;
assume
A3: - a is UpperBound of - X;
for x being ExtReal st x in X holds a <= x
proof
let x be ExtReal;
assume
A4: x in X;
reconsider x as Element of ExtREAL by XXREAL_0:def 1;
- x in - X by A4;
hence thesis by XXREAL_3:38,A3,XXREAL_2:def 1;
end;
hence thesis by XXREAL_2:def 2;
end;
theorem Th13:
for X being non empty Subset of ExtREAL holds inf(- X) = - sup X
proof
let X be non empty Subset of ExtREAL;
set a = inf(- X);
set b = sup X;
a is LowerBound of - X by XXREAL_2:def 4;
then - a is UpperBound of -(-X) by Th12; then
A1: - (- a) <= - b by XXREAL_3:38,XXREAL_2:def 3;
b is UpperBound of X by XXREAL_2:def 3;
then - b is LowerBound of - X by Th11;
then - b <= a by XXREAL_2:def 4;
hence thesis by A1,XXREAL_0:1;
end;
theorem Th14:
for X be non empty Subset of ExtREAL holds sup(- X) = - inf X
proof
let X be non empty Subset of ExtREAL;
set a = sup(- X);
set b = inf X;
a is UpperBound of - X by XXREAL_2:def 3;
then - a is LowerBound of - (- X) by Th11;
then
A1: - b <= - (-a) by XXREAL_3:38,XXREAL_2:def 4;
b is LowerBound of X by XXREAL_2:def 4;
then - b is UpperBound of - X by Th12;
then a <= - b by XXREAL_2:def 3;
hence thesis by A1,XXREAL_0:1;
end;
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; :: redefines rng (FUNCT_1, redefinition) → rng (RELAT_1, synonym) → proj2 (XTUPLE_0, definition)
coherence
proof
set x = the Element of X;
F.x in rng F by FUNCT_2:4;
hence thesis by XBOOLE_1:1;
end;
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
sup rng F;
coherence;
func inf F -> Element of ExtREAL equals
inf rng F;
coherence;
end;
definition
let F be ext-real-valued Function;
let x be set;
redefine func F.x -> R_eal; :: redefines . (FUNCT_1, definition)
coherence by XXREAL_0:def 1;
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
:Def3:
for x being Element of X holds it.x = F.x + G.x;
existence
proof
deffunc F(Element of X) = F.$1 + G.$1;
A1: for x being Element of X holds F(x) in Y + Z
proof
let x be Element of X;
A2: G.x in Z by FUNCT_2:5;
F.x in Y by FUNCT_2:5;
hence thesis by A2;
end;
ex H being Function of X,Y + Z st for x being Element of X holds H.x =
F(x) from FUNCT_2:sch 8(A1);
then consider H being Function of X,Y + Z such that
A3: for x being Element of X holds H.x = F.x + G.x;
take H;
thus thesis by A3;
end;
uniqueness
proof
let H1,H2 be Function of X,Y + Z such that
A4: for x being Element of X holds H1.x = F.x + G.x and
A5: for x being Element of X holds H2.x = F.x + G.x;
for x being object st x in X holds H1.x = H2.x
proof
let x be object;
assume x in X;
then reconsider x as Element of X;
H1.x = F.x + G.x by A4
.= H2.x by A5;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem Th15:
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
proof
let X be non empty set, Y,Z be non empty Subset of ExtREAL, F be Function of
X,Y, G be Function of X,Z;
A1: for x being object st x in X holds (F + G).x in rng F + rng G
proof
let x be object;
assume x in X;
then reconsider x as Element of X;
reconsider a = F.x, b = G.x as R_eal;
A2: a in rng F by FUNCT_2:4;
A3: b in rng G by FUNCT_2:4;
(F + G).x = a + b by Def3;
hence thesis by A2,A3;
end;
dom (F + G) = X by FUNCT_2:def 1;
then F + G is Function of X,rng F + rng G by A1,FUNCT_2:3;
hence thesis by RELAT_1:def 19;
end;
theorem Th16:
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
proof
let X be non empty set, Y,Z be non empty Subset of ExtREAL;
let F be Function of X,Y;
let G be Function of X,Z;
A1: sup(rng F + rng G) <= sup(rng F) + sup(rng G) by Th7;
sup(F + G) <= sup(rng F + rng G) by Th15,XXREAL_2:59;
hence thesis by A1,XXREAL_0:2;
end;
theorem Th17:
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)
proof
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;
A1: inf(rng F) + inf(rng G) <= inf(rng F + rng G) by Th8;
inf(rng F + rng G) <= inf(F + G) by Th15,XXREAL_2:60;
hence thesis by A1,XXREAL_0:2;
end;
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
:Def4:
for x being Element of X holds it.x = - F.x;
existence
proof
deffunc F(Element of X) = - F.$1;
A1: for x being Element of X holds F(x) in - Y
proof
let x be Element of X;
F.x in Y by FUNCT_2:5;
hence thesis;
end;
ex H being Function of X,- Y st for x being Element of X holds H.x = F
(x) from FUNCT_2:sch 8(A1);
then consider H being Function of X,- Y such that
A2: for x being Element of X holds H.x = - F.x;
take H;
thus thesis by A2;
end;
uniqueness
proof
let H1,H2 be Function of X,- Y such that
A3: for x being Element of X holds H1.x = - F.x and
A4: for x being Element of X holds H2.x = - F.x;
for x being object st x in X holds H1.x = H2.x
proof
let x be object;
assume x in X;
then reconsider x as Element of X;
H1.x = - F.x by A3
.= H2.x by A4;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem Th18:
for X being non empty set, Y being non empty Subset of ExtREAL,
F being Function of X,Y holds rng(- F) = - rng F
proof
let X be non empty set, Y be non empty Subset of ExtREAL, F be Function of X
,Y;
thus rng(- F) c= - rng F
proof
let y be object;
A1: dom F = X by FUNCT_2:def 1;
assume
A2: y in rng(- F);
then reconsider y as R_eal;
dom(- F) = X by FUNCT_2:def 1;
then consider a being object such that
A3: a in X and
A4: y = (- F).a by A2,FUNCT_1:def 3;
reconsider a as Element of X by A3;
y = - F.a by A4,Def4;
then - y in rng F by A1,FUNCT_1:def 3;
then - (- y) in - rng F;
hence thesis;
end;
let y be object;
assume
A5: y in - rng F;
then reconsider y as R_eal;
A6: - y in - (- rng F) by A5;
dom F = X by FUNCT_2:def 1;
then consider a being object such that
A7: a in X and
A8: - y = F.a by A6,FUNCT_1:def 3;
reconsider a as Element of X by A7;
y = - F.a by A8; then
A9: y = (- F).a by Def4;
dom (- F) = X by FUNCT_2:def 1;
hence thesis by A9,FUNCT_1:def 3;
end;
theorem Th19:
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
proof
let X be non empty set;
let Y be non empty Subset of ExtREAL;
let F be Function of X,Y;
thus inf(- F) = inf(- rng F) by Th18
.= - sup F by Th13;
thus sup(- F) = sup(- rng F) by Th18
.= - inf F by Th14;
end;
:: 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 :Def5:
sup F < +infty;
attr F is bounded_below means :Def6:
-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
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;
coherence;
cluster bounded_above bounded_below -> bounded for Function of X, Y;
coherence;
end;
theorem
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 <inf F
by Def5,Def6;
theorem Th21:
for X being non empty set, Y being non empty Subset of ExtREAL,
F being Function of X,Y holds F is bounded_above iff - F is bounded_below
proof
let X be non empty set, Y be non empty Subset of ExtREAL, F be Function of X
,Y;
hereby
assume F is bounded_above;
then
A1: - (+infty) <- sup F by XXREAL_3:38;
- (+infty) = -infty by XXREAL_3:def 3;
hence - F is bounded_below by A1,Th19;
end;
assume - F is bounded_below;
then - inf(- F) <- (-infty) by XXREAL_3:38;
then - (- sup F) <- (-infty) by Th19;
hence thesis by XXREAL_3:5;
end;
theorem Th22:
for X being non empty set, Y being non empty Subset of ExtREAL,
F being Function of X,Y holds F is bounded_below iff - F is bounded_above
proof
let X be non empty set, Y be non empty Subset of ExtREAL, F be Function of X
,Y;
hereby
assume F is bounded_below;
then - inf F <- (-infty) by XXREAL_3:38;
hence - F is bounded_above by Th19,XXREAL_3:5;
end;
assume - F is bounded_above;
then - inf F <+infty by Th19; then
- (+infty) <- (- inf F) by XXREAL_3:38;
hence thesis by XXREAL_3:def 3;
end;
theorem
for X being non empty set, Y being non empty Subset of ExtREAL, F
being Function of X,Y holds F is bounded iff - F is bounded by Th21,Th22;
theorem
for X being non empty set, Y being non empty Subset of ExtREAL, F
being Function of X,Y, x being Element of X holds -infty <= F.x & F.x <= +infty
by XXREAL_0:4,5;
theorem
for X being non empty set, Y being non empty Subset of ExtREAL, F
being Function of X,Y, x being Element of X st Y c= REAL holds -infty <F.x & F.
x <+infty
proof
let X be non empty set, Y be non empty Subset of ExtREAL, F be Function of X
,Y, x be Element of X;
A1: -infty <= F.x by XXREAL_0:5;
assume Y c= REAL;
hence thesis by A1,XXREAL_0:1,4;
end;
theorem Th26:
for X being non empty set, Y being non empty Subset of ExtREAL,
F being Function of X,Y, x being Element of X holds inf F <= F.x & F.x <= sup F
proof
let X be non empty set, Y be non empty Subset of ExtREAL, F be Function of X
,Y, x be Element of X;
X = dom F by FUNCT_2:def 1;
then F.x in rng F by FUNCT_1:def 3;
hence thesis by XXREAL_2:3,4;
end;
theorem Th27:
for X being non empty set, Y being non empty Subset of ExtREAL,
F being Function of X,Y holds Y c= REAL implies (F is bounded_above iff sup F
in REAL)
proof
let X be non empty set, Y be non empty Subset of ExtREAL, F be Function of X
,Y;
assume
A1: Y c= REAL;
hereby
set x = the Element of X;
X = dom F by FUNCT_2:def 1;
then
A2: F.x in rng F by FUNCT_1:def 3;
rng F c= Y by RELAT_1:def 19;
then F.x in Y by A2;
then
A3: not sup F = -infty by A1,Th26,XXREAL_0:12;
assume a4: F is bounded_above;
sup F in REAL or sup F in {-infty,+infty} by XBOOLE_0:def 3;
hence sup F in REAL by a4,A3,TARSKI:def 2;
end;
assume sup F in REAL;
hence thesis by XXREAL_0:9;
end;
theorem Th28:
for X being non empty set, Y being non empty Subset of ExtREAL,
F being Function of X,Y st Y c= REAL holds (F is bounded_below iff inf F in
REAL)
proof
let X be non empty set, Y be non empty Subset of ExtREAL, F be Function of X
,Y;
assume
A1: Y c= REAL;
thus F is bounded_below implies inf F in REAL
proof
set x = the Element of X;
X = dom F by FUNCT_2:def 1;
then
A2: F.x in rng F by FUNCT_1:def 3;
rng F c= Y by RELAT_1:def 19;
then F.x in Y by A2;
then
A3: not inf F = +infty by A1,Th26,XXREAL_0:9;
assume a4: F is bounded_below;
inf F in REAL or inf F in {-infty,+infty} by XBOOLE_0:def 3;
hence thesis by a4,A3,TARSKI:def 2;
end;
assume inf F in REAL;
hence thesis by XXREAL_0:12;
end;
theorem
for X being non empty set, Y being non empty Subset of ExtREAL, F
being Function of X,Y st Y c= REAL holds (F is bounded iff inf F in REAL & sup
F in REAL)
by Th27,Th28;
theorem Th30:
for X being non empty set, Y,Z being non empty Subset of ExtREAL
holds for F1 being Function of X,Y, F2 being Function of X,Z st F1 is
bounded_above & F2 is bounded_above holds F1 + F2 is bounded_above
proof
let X be non empty set, Y,Z be non empty Subset of ExtREAL;
let F1 be Function of X,Y, F2 be Function of X,Z;
assume that
A1: F1 is bounded_above and
A2: F2 is bounded_above;
A4: sup F1 in REAL & sup F2 in REAL implies sup F1 + sup F2 <+infty
proof
reconsider a = sup F1, b = sup F2 as R_eal;
assume that
A5: sup F1 in REAL and
A6: sup F2 in REAL;
reconsider a,b as Element of REAL by A5,A6;
sup F1 + sup F2 = a + b by XXREAL_3:def 2;
hence thesis by XXREAL_0:9;
end;
A7: sup F1 in REAL & sup F2 = -infty implies sup F1 + sup F2 <+infty by
XXREAL_0:7,XXREAL_3:def 2;
A8: sup F1 = -infty & sup F2 = -infty implies sup F1 + sup F2 <+infty by
XXREAL_0:7,XXREAL_3:def 2;
A9: sup F1 = -infty & sup F2 in REAL implies sup F1 + sup F2 <+infty by
XXREAL_0:7,XXREAL_3:def 2;
sup(F1 + F2) <+infty
proof
assume not sup(F1 + F2) <+infty;
then not sup(F1 + F2) <= +infty or sup(F1 + F2) = +infty by XXREAL_0:1;
hence thesis by A1,A2,A4,A7,A9,A8,Th16,XXREAL_0:4,XXREAL_3:def 1;
end;
hence thesis;
end;
theorem Th31:
for X being non empty set, Y,Z being non empty Subset of ExtREAL
holds for F1 being Function of X,Y, F2 being Function of X,Z st F1 is
bounded_below & F2 is bounded_below holds F1 + F2 is bounded_below
proof
let X be non empty set, Y,Z be non empty Subset of ExtREAL;
let F1 be Function of X,Y, F2 be Function of X,Z;
assume that
A1: F1 is bounded_below and
A2: F2 is bounded_below;
A4: inf F1 in REAL & inf F2 in REAL implies -infty <inf F1 + inf F2
proof
reconsider a = inf F1, b = inf F2 as R_eal;
assume that
A5: inf F1 in REAL and
A6: inf F2 in REAL;
reconsider a,b as Element of REAL by A5,A6;
inf F1 + inf F2 = a + b by XXREAL_3:def 2;
hence thesis by XXREAL_0:12;
end;
A7: inf F1 in REAL & inf F2 = +infty implies -infty <inf F1 + inf F2 by
XXREAL_0:7,XXREAL_3:def 2;
A8: inf F1 = +infty & inf F2 = +infty implies -infty <inf F1 + inf F2 by
XXREAL_0:7,XXREAL_3:def 2;
A9: inf F1 = +infty & inf F2 in REAL implies -infty <inf F1 + inf F2 by
XXREAL_0:7,XXREAL_3:def 2;
-infty <inf(F1 + F2)
proof
assume inf(F1 + F2) <= -infty;
then not -infty <= inf(F1 + F2) or inf(F1 + F2) = -infty by XXREAL_0:1;
hence thesis by A1,A2,A4,A7,A9,A8,Th17,XXREAL_0:6,XXREAL_3:def 1;
end;
hence thesis;
end;
theorem
for X being non empty set, Y,Z being non empty Subset of ExtREAL holds
for F1 being Function of X,Y, F2 being Function of X,Z st F1 is bounded & F2 is
bounded holds F1 + F2 is bounded by Th31,Th30;
theorem Th33:
id NAT is sequence of ExtREAL &
id NAT is one-to-one & NAT = rng id NAT &
rng id NAT is non empty Subset of ExtREAL
proof
NAT c= ExtREAL by NUMBERS:19,31;
then reconsider F = id NAT as sequence of ExtREAL by FUNCT_2:7;
rng F c= ExtREAL;
hence thesis;
end;
definition
let D be non empty set, IT be Subset of D;
redefine attr IT is countable means :Def8: :: redefines countable (CARD_3, definition)
IT is empty or ex F being sequence of D st IT = rng F;
compatibility
proof
thus IT is countable implies IT is empty or ex F being sequence of D
st IT = rng F
proof
assume that
A1: IT is countable and
A2: IT is not empty;
consider f being Function such that
A3: dom f = NAT and
A4: IT c= rng f by A1,CARD_3:93;
consider x being Element of D such that
A5: x in IT by A2;
set F = f|(f"IT) +* (NAT \ f"IT --> x);
A6: rng F = IT & dom F = NAT
proof
A7: f"IT c= NAT by A3,RELAT_1:132;
A8: dom(f|(f"IT)) = NAT /\ (f"IT) by A3,RELAT_1:61;
per cases;
suppose
A9: NAT = f"IT;
then
A10: NAT \ f"IT = {} by XBOOLE_1:37;
then dom(NAT \ f"IT --> x) = {};
then dom(f|(f"IT)) misses dom(NAT \ f"IT --> x);
then F = (f|(f"IT)) \/ (NAT \ f"IT --> x) by FUNCT_4:31;
hence rng F = rng(f|(f"IT)) \/ rng(NAT \ f"IT --> x) by RELAT_1:12
.= rng(f|(f"IT)) \/ {} by A10
.= f.:(f"IT) by RELAT_1:115
.= IT by A4,FUNCT_1:77;
thus dom F = dom(f|(f"IT)) \/ dom(NAT \ f"IT --> x) by FUNCT_4:def 1
.= dom(f|(f"IT)) \/ {} by A10
.= NAT by A3,A9;
end;
suppose NAT <> f"IT; then
A11: NAT \ f"IT is non empty by A7,XBOOLE_1:37;
dom(NAT \ f"IT --> x) = NAT \ f"IT by FUNCOP_1:13;
then F = (f|(f"IT)) \/ (NAT \ f"IT --> x)
by A8,FUNCT_4:31,XBOOLE_1:89;
hence rng F = rng(f|(f"IT)) \/ rng(NAT \ f"IT --> x) by RELAT_1:12
.= rng(f|(f"IT)) \/ {x} by A11,FUNCOP_1:8
.= f.:(f"IT) \/ {x} by RELAT_1:115
.= IT \/ {x} by A4,FUNCT_1:77
.= IT by A5,ZFMISC_1:40;
thus dom F = dom(f|(f"IT)) \/ dom(NAT \ f"IT --> x) by FUNCT_4:def 1
.= NAT /\ (f"IT) \/ (NAT \ f"IT) by A8,FUNCOP_1:13
.= NAT by XBOOLE_1:51;
end;
end;
then reconsider F as sequence of D by FUNCT_2:def 1,RELSET_1:4;
take F;
thus thesis by A6;
end;
assume
A12: IT is empty or ex F being sequence of D st IT = rng F;
per cases;
suppose
IT is empty;
hence thesis by CARD_4:1;
end;
suppose
IT is not empty;
then consider F being sequence of D such that
A13: IT = rng F by A12;
dom F = NAT by FUNCT_2:def 1;
hence thesis by A13,CARD_3:93;
end;
end;
end;
registration
cluster countable for non empty Subset of ExtREAL;
existence
proof
set F = the sequence of ExtREAL;
reconsider A = rng F as non empty Subset of ExtREAL;
take A;
assume A is non empty;
thus thesis;
end;
end;
definition
let IT be set;
attr IT is nonnegative means
for x being ExtReal holds x in IT implies 0. <= x;
end;
registration
cluster nonnegative for countable Subset of ExtREAL;
existence
proof
reconsider N = NAT as countable Subset of ExtREAL by Def8,Th33;
take N;
thus for x being ExtReal holds x in N implies 0. <= x;
end;
end;
::$CD
:: Series of Elements of extended real numbers
definition
let F be sequence of ExtREAL;
redefine func rng F -> non empty Subset of ExtREAL; :: redefines rng (FUNCT_1, redefinition) → rng (RELAT_1, synonym) → proj2 (XTUPLE_0, definition)
coherence
proof
rng F c= ExtREAL;
hence thesis;
end;
end;
definition
let N be sequence of ExtREAL;
func Ser(N) -> sequence of ExtREAL means :Def11:
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);
existence
proof
set D = rng N;
defpred P[set,set,set] means for a,b being R_eal,s being Element of NAT
holds (s = $1 & a = $2 & b = $3 implies b = a + N.(s+1));
reconsider A = N.0 as R_eal;
A1: for n being Nat for x being Element of ExtREAL ex y being
Element of ExtREAL st P[n,x,y]
proof
let n be Nat;
let x be Element of ExtREAL;
reconsider y = x + N.(n+1) as R_eal;
take y;
thus thesis;
end;
consider F being sequence of ExtREAL such that
A2: F.0 = A & for n being Nat holds P[n,F.n,F.(n+1)] from RECDEF_1:sch 2(A1);
take F;
thus F.0 = N.0 by A2;
let n be Nat;
reconsider n as Element of NAT by ORDINAL1:def 12;
P[n,F.n,F.(n+1)] by A2;
hence thesis;
end;
uniqueness
proof
let S1,S2 be sequence of ExtREAL such that
A3: S1.0 = N.0 and
A4: for n being Nat holds for y being R_eal st y = S1.n
holds S1.(n + 1) = y + N.(n + 1) and
A5: S2.0 = N.0 and
A6: for n being Nat holds for y being R_eal st y = S2.n
holds S2.(n + 1) = y + N.(n + 1);
defpred P[object] means S1.$1 = S2.$1;
for n being object holds n in NAT implies P[n]
proof
let n be object;
assume
A7: n in NAT;
then reconsider n as Element of REAL by NUMBERS:19;
reconsider n as Element of NAT by A7;
A8: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
reconsider y2 = S2.k as R_eal;
assume S1.k = S2.k;
hence S1.(k + 1) = y2 + N.(k + 1) by A4
.= S2.(k + 1) by A6;
end;
A9: P[0] by A3,A5;
for k being Nat holds P[k] from NAT_1:sch 2(A9, A8);
then S1.n = S2.n;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
end;
::$CT 4
definition
let R be Relation;
attr R is nonnegative means
rng R is nonnegative;
end;
definition
let F be sequence of ExtREAL;
func SUM(F) -> R_eal equals
sup rng Ser(F);
coherence;
end;
theorem Th38:
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
proof
let X be set, F be PartFunc of X,ExtREAL;
hereby
assume F is nonnegative;
then
A1: rng F is nonnegative;
let n be Element of X;
per cases;
suppose
n in dom F;
then F.n in rng F by FUNCT_1:def 3;
hence 0. <= F.n by A1;
end;
suppose
not n in dom F;
hence 0. <= F.n by FUNCT_1:def 2;
end;
end;
assume
A2: for n being Element of X holds 0. <= F.n;
let y be ExtReal;
assume y in rng F;
then ex x being object st x in dom F & y = F.x by FUNCT_1:def 3;
hence thesis by A2;
end;
theorem Th39:
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
proof
let F be sequence of ExtREAL, n be Nat;
assume A0: F is nonnegative;
set FF = Ser F;
defpred P[Nat] means FF.$1 <= FF.($1 + 1) & 0. <= FF.$1;
reconsider y = FF.0 as R_eal;
A1: FF.(0 + 1) = y + F.1 by Def11;
A2: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume that
A3: FF.k <= FF.(k + 1) and
A4: 0. <= FF.k;
FF.((k+1) + 1) = FF.(k + 1) + F.((k+1) + 1) by Def11;
hence thesis by A3,A4,Th38,A0,XXREAL_3:39;
end;
FF.0 = F.0 by Def11; then
A6: P[0] by A1,XXREAL_3:39,A0,Th38;
for n being Nat holds P[n] from NAT_1:sch 2(A6,A2);
hence thesis;
end;
theorem Th40:
for F being sequence of ExtREAL st F is nonnegative holds
for n,m being Nat holds Ser(F).n <= Ser(F).(n + m)
proof
let F be sequence of ExtREAL;
assume A0:F is nonnegative;
let n,m be Nat;
defpred P[Nat] means Ser(F).n <= Ser(F).(n + $1);
A1: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
Ser(F).(n + (k+1)) = Ser(F).((n + k) + 1); then
A2: Ser(F).(n + k) <= Ser(F).(n + (k+1)) by Th39,A0;
assume Ser(F).n <= Ser(F).(n + k);
hence thesis by A2,XXREAL_0:2;
end;
A3: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th41:
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
proof
let F1,F2 be sequence of ExtREAL;
defpred P[Nat] means Ser(F1).$1 <= Ser(F2).$1;
assume
A1: for n being Element of NAT holds F1.n <= F2.n;
let n be Element of NAT;
A3: Ser(F2).0 = F2.0 by Def11;
A5: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A6: Ser(F1).k <= Ser(F2).k;
A7: F1.(k+1) <= F2.(k+1) by A1;
A8: Ser(F2).(k+1) = Ser(F2).k + F2.(k+1) by Def11;
Ser(F1).(k+1) = Ser(F1).k + F1.(k+1) by Def11;
hence thesis by A6,A8,A7,XXREAL_3:36;
end;
Ser(F1).0 = F1.0 by Def11;
then
A9: P[0] by A1,A3;
for n being Nat holds P[n] from NAT_1:sch 2(A9,A5);
hence thesis;
end;
theorem Th42:
for F1,F2 being sequence of ExtREAL st
(for n being Element of NAT holds F1.n <= F2.n) holds SUM(F1) <= SUM(F2)
proof
let F1,F2 be sequence of ExtREAL;
assume
A1: for n being Element of NAT holds F1.n <= F2.n;
for x being ExtReal st x in rng Ser(F1) holds ex y being
ExtReal st y in rng Ser(F2) & x <= y
proof
let x be ExtReal;
A2: dom Ser(F1) = NAT by FUNCT_2:def 1;
assume x in rng Ser(F1);
then consider n being object such that
A3: n in NAT and
A4: x = Ser(F1).n by A2,FUNCT_1:def 3;
reconsider n as Element of NAT by A3;
reconsider y = Ser(F2).n as R_eal;
take y;
dom Ser(F2) = NAT by FUNCT_2:def 1;
hence thesis by A1,A4,Th41,FUNCT_1:def 3;
end;
hence thesis by XXREAL_2:63;
end;
::$CT
theorem Th44:
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
proof
let F be sequence of ExtREAL;
assume
A1: F is nonnegative;
given n being Element of NAT such that
A2: F.n = +infty;
A3: (ex k being Nat st n = k + 1) implies SUM(F) = +infty
proof
given k being Nat such that
A4: n = k + 1;
reconsider k as Element of NAT by ORDINAL1:def 12;
reconsider y = Ser(F).k as R_eal;
reconsider x = Ser(F).(k + 1) as R_eal;
A5: Ser(F).(k + 1) = y + F.(k + 1) by Def11;
Ser(F).k <> -infty by A1,Th39,XXREAL_0:6; then
A6: x = +infty by A2,A4,A5,XXREAL_3:def 2;
then x is UpperBound of rng Ser(F) by XXREAL_2:41;
hence thesis by A6,FUNCT_2:4,XXREAL_2:55;
end;
n = 0 implies SUM(F) = +infty
proof
reconsider x = Ser(F).0 as R_eal;
assume n = 0; then
A7: Ser(F).0 = +infty by A2,Def11;
then x is UpperBound of rng Ser(F) by XXREAL_2:41;
hence thesis by A7,FUNCT_2:4,XXREAL_2:55;
end;
hence thesis by A3,NAT_1:6;
end;
definition
let F be sequence of ExtREAL;
attr F is summable means
SUM F in REAL;
end;
theorem
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 by Th44;
theorem
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)
proof
let F1,F2 be sequence of ExtREAL;
assume F1 is nonnegative; then
A1: 0. <= Ser(F1).0 by Th39;
Ser(F1).0 <= sup rng Ser F1 by FUNCT_2:4,XXREAL_2:4; then
A2: SUM(F1) <> -infty by A1,XXREAL_0:6;
assume
A3: for n being Element of NAT holds F1.n <= F2.n;
assume F2 is summable; then
A4: not SUM(F1) = +infty by A3,Th42,XXREAL_0:9;
SUM(F1) in REAL or SUM(F1) in {-infty,+infty} by XBOOLE_0:def 3;
hence thesis by A4,A2,TARSKI:def 2;
end;
theorem Th47:
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
proof
let F be sequence of ExtREAL;
assume
A1: F is nonnegative;
let n be Nat;
reconsider n9=n as Element of NAT by ORDINAL1:def 12;
assume
A2: for r being Element of NAT st n <= r holds F.r = 0.;
A3: for r being Element of NAT st n <= r holds Ser(F).r <= Ser(F).n
proof
defpred P[Nat] means Ser(F).(n + $1) <= Ser(F).n;
let r be Element of NAT;
assume n <= r;
then
A4: ex m being Nat st r = n + m by NAT_1:10;
A5: for s being Nat st P[s] holds P[s+1]
proof
let s be Nat;
reconsider s9=s as Element of NAT by ORDINAL1:def 12;
reconsider y = Ser(F).(n + s) as R_eal;
n9 + (s9 + 1) = (n9 + s9) + 1; then
A6: Ser(F).(n9 + (s9 + 1)) = y + F.(n9 + (s9 + 1)) by Def11;
n + 0 <= n + (s+1) by XREAL_1:7; then
A7: F.(n9 + (s9+1)) = 0. by A2;
assume Ser(F).(n + s) <= Ser(F).n;
hence thesis by A6,A7,XXREAL_3:4;
end;
A8: P[0];
for m being Nat holds P[m] from NAT_1:sch 2(A8,A5);
hence thesis by A4;
end;
A9: for r being Element of NAT st r <= n holds Ser(F).r <= Ser(F).n
proof
let r be Element of NAT;
assume r <= n;
then consider m being Nat such that
A10: n = r + m by NAT_1:10;
reconsider m as Element of NAT by ORDINAL1:def 12;
thus thesis by A1,Th40,A10;
end;
for y being ExtReal st y in rng Ser(F) holds y <= Ser(F).n
proof
let y be ExtReal;
A11: dom Ser(F) = NAT by FUNCT_2:def 1;
assume y in rng Ser(F);
then consider m being object such that
A12: m in NAT and
A13: y = Ser(F).m by A11,FUNCT_1:def 3;
reconsider m as Element of NAT by A12;
m <= n or n <= m;
hence thesis by A3,A9,A13;
end;
then
A14: Ser(F).n is UpperBound of rng Ser(F) by XXREAL_2:def 1;
Ser(F).n9 in rng Ser(F) by FUNCT_2:4;
hence thesis by A14,XXREAL_2:55;
end;
theorem Th48:
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
proof
let F be sequence of ExtREAL;
defpred P[Nat] means Ser(F).$1 in REAL;
assume
A1: for n being Element of NAT holds F.n in REAL;
A2: for s being Nat st P[s] holds P[s+1]
proof
let s be Nat;
reconsider b = F.(s+1) as Element of REAL by A1;
reconsider y = Ser(F).s as R_eal;
assume Ser(F).s in REAL;
then reconsider a = y as Element of REAL;
A3: y + F.(s+1) = a + b by XXREAL_3:def 2;
Ser(F).(s+1) = y + F.(s+1) by Def11;
hence thesis by A3;
end;
Ser(F).0 = F.0 by Def11; then
A4: P[0] by A1;
thus for s being Nat holds P[s] from NAT_1:sch 2(A4,A2);
end;
theorem
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
proof
let F be sequence of ExtREAL;
assume
A1: F is nonnegative;
given n being Element of NAT such that
A2: for k being Element of NAT st n <= k holds F.k = 0. and
A3: for k being Element of NAT st k <= n holds F.k <> +infty;
for s being Element of NAT holds F.s in REAL
proof
let s be Element of NAT;
A4: s <= n implies F.s in REAL
proof
A5: F.s <> -infty by XXREAL_0:6,A1,Th38;
assume s <= n; then
A6: not F.s = +infty by A3;
F.s in REAL or F.s in {-infty,+infty} by XBOOLE_0:def 3;
hence thesis by A6,A5,TARSKI:def 2;
end;
n <= s implies F.s in REAL
proof
assume n <= s;
then F.s = 0. by A2;
hence thesis by XREAL_0:def 1;
end;
hence thesis by A4;
end; then
Ser(F).n in REAL by Th48;
hence thesis by A1,A2,Th47;
end;
:: Added by AK, 2006.02.06
theorem
for X being set, F being PartFunc of X,ExtREAL holds F is nonnegative
iff for n being object holds 0. <= F.n
proof
let X be set, F be PartFunc of X,ExtREAL;
hereby
assume F is nonnegative; then
A1: rng F is nonnegative;
let n be object;
per cases;
suppose
n in dom F;
then F.n in rng F by FUNCT_1:def 3;
hence 0. <= F.n by A1;
end;
suppose
not n in dom F;
hence 0. <= F.n by FUNCT_1:def 2;
end;
end;
assume
A2: for n being object holds 0. <= F.n;
let y be ExtReal;
assume y in rng F;
then ex x being object st x in dom F & y = F.x by FUNCT_1:def 3;
hence thesis by A2;
end;
theorem
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
proof
let X be set, F be PartFunc of X,ExtREAL such that
A1: for n being object st n in dom F holds 0. <= F.n;
let y be ExtReal;
assume y in rng F;
then ex x being object st x in dom F & y = F.x by FUNCT_1:def 3;
hence thesis by A1;
end;
definition
func 1. -> R_eal equals
1;
coherence by XXREAL_0:def 1;
end;