:: Series of Positive Real Numbers. Measure Theory
:: by J\'ozef Bia{\l}as
::
:: Copyright (c) 1990-2021 Association of Mizar Users

notation
synonym 0. for 0 ;
end;

definition
:: original: 0.
redefine func 0. -> R_eal;
coherence
0. is R_eal
by XXREAL_0:def 1;
let x be R_eal;
:: original: -
redefine func - x -> R_eal;
coherence
- x is R_eal
by XXREAL_0:def 1;
let y be R_eal;
:: original: +
redefine func x + y -> R_eal;
coherence
x + y is R_eal
by XXREAL_0:def 1;
:: original: -
redefine func x - y -> R_eal;
coherence
x - y is R_eal
by XXREAL_0:def 1;
end;

theorem :: SUPINF_2:1
for x, y being ExtReal
for a, b being Real st x = a & y = b holds
x + y = a + b by XXREAL_3:def 2;

theorem :: SUPINF_2:2
for x being ExtReal
for a being Real st x = a holds
- x = - a by XXREAL_3:def 3;

theorem :: SUPINF_2:3
for x, y being ExtReal
for a, b being Real st x = a & y = b holds
x - y = a - b
proof end;

notation
let X, Y be Subset of ExtREAL;
synonym X + Y for X ++ Y;
end;

definition
let X, Y be Subset of ExtREAL;
:: original: +
redefine func X + Y -> Subset of ExtREAL;
coherence
X + Y is Subset of ExtREAL
by MEMBERED:2;
end;

notation
let X be Subset of ExtREAL;
synonym - X for -- X;
end;

definition
let X be Subset of ExtREAL;
:: original: -
redefine func - X -> Subset of ExtREAL;
coherence
- X is Subset of ExtREAL
by MEMBERED:2;
end;

theorem :: SUPINF_2:4
canceled;

::$CT theorem :: SUPINF_2:5 for X being non empty Subset of ExtREAL for z being R_eal holds ( z in X iff - z in - X ) by MEMBER_1:1; theorem :: SUPINF_2:6 for X, Y being non empty Subset of ExtREAL holds ( X c= Y iff - X c= - Y ) by MEMBER_1:3; theorem :: SUPINF_2:7 for z being R_eal holds ( z in REAL iff - z in REAL ) proof end; definition let X be ext-real-membered set ; :: original: inf redefine func inf X -> R_eal; coherence inf X is R_eal by XXREAL_0:def 1; :: original: sup redefine func sup X -> R_eal; coherence sup X is R_eal by XXREAL_0:def 1; end; theorem Th7: :: SUPINF_2:8 for X, Y being non empty Subset of ExtREAL holds sup (X + Y) <= (sup X) + (sup Y) proof end; theorem Th8: :: SUPINF_2:9 for X, Y being non empty Subset of ExtREAL holds (inf X) + (inf Y) <= inf (X + Y) proof end; theorem :: SUPINF_2:10 for X, Y being non empty Subset of ExtREAL st X is bounded_above & Y is bounded_above holds sup (X + Y) <= (sup X) + (sup Y) by Th7; 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) by Th8; theorem Th11: :: SUPINF_2:12 for X being non empty Subset of ExtREAL for a being R_eal holds ( a is UpperBound of X iff - a is LowerBound of - X ) proof end; theorem Th12: :: SUPINF_2:13 for X being non empty Subset of ExtREAL for a being R_eal holds ( a is LowerBound of X iff - a is UpperBound of - X ) proof end; theorem Th13: :: SUPINF_2:14 for X being non empty Subset of ExtREAL holds inf (- X) = - (sup X) proof end; theorem Th14: :: SUPINF_2:15 for X being non empty Subset of ExtREAL holds sup (- X) = - (inf X) proof end; definition let X be non empty set ; let Y be non empty Subset of ExtREAL; let F be Function of X,Y; :: original: rng redefine func rng F -> non empty Subset of ExtREAL; coherence rng F is non empty Subset of ExtREAL proof 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 :: SUPINF_2:def 1 sup (rng F); coherence sup (rng F) is Element of ExtREAL ; func inf F -> Element of ExtREAL equals :: SUPINF_2:def 2 inf (rng F); coherence inf (rng F) is Element of ExtREAL ; end; :: deftheorem defines sup SUPINF_2:def 1 : for D being ext-real-membered set for X being set for Y being Subset of D for F being PartFunc of X,Y holds sup F = sup (rng F); :: deftheorem defines inf SUPINF_2:def 2 : for D being ext-real-membered set for X being set for Y being Subset of D for F being PartFunc of X,Y holds inf F = inf (rng F); definition let F be ext-real-valued Function; let x be set ; :: original: . redefine func F . x -> R_eal; coherence F . x is R_eal 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: :: SUPINF_2:def 3 for x being Element of X holds it . x = (F . x) + (G . x); existence ex b1 being Function of X,(Y + Z) st for x being Element of X holds b1 . x = (F . x) + (G . x) proof end; uniqueness for b1, b2 being Function of X,(Y + Z) st ( for x being Element of X holds b1 . x = (F . x) + (G . x) ) & ( for x being Element of X holds b2 . x = (F . x) + (G . x) ) holds b1 = b2 proof end; end; :: deftheorem Def3 defines + SUPINF_2:def 3 : for X being non empty set for Y, Z being non empty Subset of ExtREAL for F being Function of X,Y for G being Function of X,Z for b6 being Function of X,(Y + Z) holds ( b6 = F + G iff for x being Element of X holds b6 . x = (F . x) + (G . x) ); theorem Th15: :: SUPINF_2:16 for X being non empty set for Y, Z being non empty Subset of ExtREAL for F being Function of X,Y for G being Function of X,Z holds rng (F + G) c= (rng F) + (rng G) proof end; theorem Th16: :: SUPINF_2:17 for X being non empty set for 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 end; theorem Th17: :: SUPINF_2:18 for X being non empty set 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 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: :: SUPINF_2:def 4 for x being Element of X holds it . x = - (F . x); existence ex b1 being Function of X,(- Y) st for x being Element of X holds b1 . x = - (F . x) proof end; uniqueness for b1, b2 being Function of X,(- Y) st ( for x being Element of X holds b1 . x = - (F . x) ) & ( for x being Element of X holds b2 . x = - (F . x) ) holds b1 = b2 proof end; end; :: deftheorem Def4 defines - SUPINF_2:def 4 : for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y for b4 being Function of X,(- Y) holds ( b4 = - F iff for x being Element of X holds b4 . x = - (F . x) ); theorem Th18: :: SUPINF_2:19 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y holds rng (- F) = - (rng F) proof end; theorem Th19: :: SUPINF_2:20 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y holds ( inf (- F) = - (sup F) & sup (- F) = - (inf F) ) proof 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: :: SUPINF_2:def 5 sup F < +infty ; attr F is bounded_below means :Def6: :: SUPINF_2:def 6 -infty < inf F; end; :: deftheorem Def5 defines bounded_above SUPINF_2:def 5 : for X being set for Y being Subset of ExtREAL for F being Function of X,Y holds ( F is bounded_above iff sup F < +infty ); :: deftheorem Def6 defines bounded_below SUPINF_2:def 6 : for X being set for Y being Subset of ExtREAL for F being Function of X,Y holds ( F is bounded_below iff -infty < inf F ); definition let X be set ; let Y be Subset of ExtREAL; let F be Function of X,Y; attr F is bounded means :: SUPINF_2:def 7 ( F is bounded_above & F is bounded_below ); end; :: deftheorem defines bounded SUPINF_2:def 7 : for X being set for Y being Subset of ExtREAL for F being Function of X,Y holds ( F is bounded iff ( F is bounded_above & F is bounded_below ) ); registration let X be set ; let Y be Subset of ExtREAL; cluster Function-like V18(X,Y) bounded -> bounded_above bounded_below for Element of K19(K20(X,Y)); coherence for b1 being Function of X,Y st b1 is bounded holds ( b1 is bounded_above & b1 is bounded_below ) ; cluster Function-like V18(X,Y) bounded_above bounded_below -> bounded for Element of K19(K20(X,Y)); coherence for b1 being Function of X,Y st b1 is bounded_above & b1 is bounded_below holds b1 is bounded ; end; theorem :: SUPINF_2:21 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y holds ( F is bounded iff ( sup F < +infty & -infty < inf F ) ) by ; theorem Th21: :: SUPINF_2:22 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y holds ( F is bounded_above iff - F is bounded_below ) proof end; theorem Th22: :: SUPINF_2:23 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y holds ( F is bounded_below iff - F is bounded_above ) proof end; theorem :: SUPINF_2:24 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y holds ( F is bounded iff - F is bounded ) by ; theorem :: SUPINF_2:25 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y for x being Element of X holds ( -infty <= F . x & F . x <= +infty ) by ; theorem :: SUPINF_2:26 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y for x being Element of X st Y c= REAL holds ( -infty < F . x & F . x < +infty ) proof end; theorem Th26: :: SUPINF_2:27 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y for x being Element of X holds ( inf F <= F . x & F . x <= sup F ) proof end; theorem Th27: :: SUPINF_2:28 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y st Y c= REAL holds ( F is bounded_above iff sup F in REAL ) proof end; theorem Th28: :: SUPINF_2:29 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y st Y c= REAL holds ( F is bounded_below iff inf F in REAL ) proof end; theorem :: SUPINF_2:30 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y st Y c= REAL holds ( F is bounded iff ( inf F in REAL & sup F in REAL ) ) by ; theorem Th30: :: SUPINF_2:31 for X being non empty set for Y, Z being non empty Subset of ExtREAL for F1 being Function of X,Y for F2 being Function of X,Z st F1 is bounded_above & F2 is bounded_above holds F1 + F2 is bounded_above proof end; theorem Th31: :: SUPINF_2:32 for X being non empty set for Y, Z being non empty Subset of ExtREAL for F1 being Function of X,Y for F2 being Function of X,Z st F1 is bounded_below & F2 is bounded_below holds F1 + F2 is bounded_below proof end; theorem :: SUPINF_2:33 for X being non empty set for Y, Z being non empty Subset of ExtREAL for F1 being Function of X,Y for F2 being Function of X,Z st F1 is bounded & F2 is bounded holds F1 + F2 is bounded by ; theorem Th33: :: SUPINF_2:34 ( id NAT is sequence of ExtREAL & id NAT is one-to-one & NAT = rng () & rng () is non empty Subset of ExtREAL ) proof end; definition let D be non empty set ; let IT be Subset of D; :: original: countable redefine attr IT is countable means :Def8: :: SUPINF_2:def 8 ( IT is empty or ex F being sequence of D st IT = rng F ); compatibility ( IT is countable iff ( IT is empty or ex F being sequence of D st IT = rng F ) ) proof end; end; :: deftheorem Def8 defines countable SUPINF_2:def 8 : for D being non empty set for IT being Subset of D holds ( IT is countable iff ( IT is empty or ex F being sequence of D st IT = rng F ) ); registration cluster non empty ext-real-membered V85() for Element of K19(ExtREAL); existence not for b1 being non empty Subset of ExtREAL holds b1 is V85() proof end; end; definition let IT be set ; attr IT is nonnegative means :: SUPINF_2:def 9 for x being ExtReal st x in IT holds 0. <= x; end; :: deftheorem defines nonnegative SUPINF_2:def 9 : for IT being set holds ( IT is nonnegative iff for x being ExtReal st x in IT holds 0. <= x ); registration existence ex b1 being V85() Subset of ExtREAL st b1 is nonnegative proof end; end; canceled; ::$CD
:: Series of Elements of extended real numbers
definition
let F be sequence of ExtREAL;
:: original: rng
redefine func rng F -> non empty Subset of ExtREAL;
coherence
rng F is non empty Subset of ExtREAL
proof end;
end;

definition
let N be sequence of ExtREAL;
func Ser N -> sequence of ExtREAL means :Def11: :: SUPINF_2:def 10
( 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
ex b1 being sequence of ExtREAL st
( b1 . 0 = N . 0 & ( for n being Nat
for y being R_eal st y = b1 . n holds
b1 . (n + 1) = y + (N . (n + 1)) ) )
proof end;
uniqueness
for b1, b2 being sequence of ExtREAL st b1 . 0 = N . 0 & ( for n being Nat
for y being R_eal st y = b1 . n holds
b1 . (n + 1) = y + (N . (n + 1)) ) & b2 . 0 = N . 0 & ( for n being Nat
for y being R_eal st y = b2 . n holds
b2 . (n + 1) = y + (N . (n + 1)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines Ser SUPINF_2:def 10 :
for N, b2 being sequence of ExtREAL holds
( b2 = Ser N iff ( b2 . 0 = N . 0 & ( for n being Nat
for y being R_eal st y = b2 . n holds
b2 . (n + 1) = y + (N . (n + 1)) ) ) );

theorem :: SUPINF_2:35
canceled;

theorem :: SUPINF_2:36
canceled;

theorem :: SUPINF_2:37
canceled;

theorem :: SUPINF_2:38
canceled;

::$CT 4 definition let R be Relation; attr R is nonnegative means :: SUPINF_2:def 11 rng R is nonnegative ; end; :: deftheorem defines nonnegative SUPINF_2:def 11 : for R being Relation holds ( R is nonnegative iff rng R is nonnegative ); definition let F be sequence of ExtREAL; func SUM F -> R_eal equals :: SUPINF_2:def 12 sup (rng (Ser F)); coherence sup (rng (Ser F)) is R_eal ; end; :: deftheorem defines SUM SUPINF_2:def 12 : for F being sequence of ExtREAL holds SUM F = sup (rng (Ser F)); theorem Th38: :: SUPINF_2:39 for X being set for F being PartFunc of X,ExtREAL holds ( F is nonnegative iff for n being Element of X holds 0. <= F . n ) proof end; theorem Th39: :: SUPINF_2:40 for F being sequence of ExtREAL for n being Nat st F is nonnegative holds ( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n ) proof end; theorem Th40: :: 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) proof end; theorem Th41: :: 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 proof end; theorem Th42: :: 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 proof end; theorem :: SUPINF_2:44 canceled; ::$CT
theorem Th44: :: SUPINF_2:45
for F being sequence of ExtREAL st F is nonnegative & ex n being Element of NAT st F . n = +infty holds
SUM F = +infty
proof end;

definition
let F be sequence of ExtREAL;
attr F is summable means :: SUPINF_2:def 13
SUM F in REAL ;
end;

:: deftheorem defines summable SUPINF_2:def 13 :
for F being sequence of ExtREAL holds
( F is summable iff SUM F in REAL );

theorem :: SUPINF_2:46
for F being sequence of ExtREAL st F is nonnegative & ex n being Element of NAT st F . n = +infty holds
not F is summable by Th44;

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 ) & F2 is summable holds
F1 is summable
proof end;

theorem Th47: :: 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
proof end;

theorem Th48: :: 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
proof end;

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
proof end;

theorem :: SUPINF_2:51
for X being set
for F being PartFunc of X,ExtREAL holds
( F is nonnegative iff for n being object holds 0. <= F . n )
proof end;

theorem :: SUPINF_2:52
for X being set
for 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 end;

definition
func 1. -> R_eal equals :: SUPINF_2:def 14
1;
coherence
1 is R_eal
by XXREAL_0:def 1;
end;

:: deftheorem defines 1. SUPINF_2:def 14 :
1. = 1;