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


begin

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 funcx + y ->  R_eal;
coherence
 x + y is R_eal by XXREAL_0:def_1;
:: original:-
redefine funcx - y ->  R_eal;
coherence
 x - y is R_eal by XXREAL_0:def_1;
end;

theorem :: SUPINF_2:1
for x, y being R_eal
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 R_eal
for a being Real st x = a holds
- x = - a by XXREAL_3:def_3;

theorem :: SUPINF_2:3
for x, y being R_eal
for a, b being Real st x = a & y = b holds
x - y = a - b
proofend;

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 funcX + 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;

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 )
proofend;

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 Th8: :: SUPINF_2:8
for X, Y being non empty Subset of ExtREAL holds sup (X + Y) <= (sup X) + (sup Y)
proofend;

theorem Th9: :: SUPINF_2:9
for X, Y being non empty Subset of ExtREAL holds (inf X) + (inf Y) <= inf (X + Y)
proofend;

theorem :: SUPINF_2:10
for X, Y being non empty Subset of ExtREAL st X is bounded_above &amp; Y is bounded_above holds
sup (X + Y) <= (sup X) + (sup Y) by Th8;

theorem :: SUPINF_2:11
for X, Y being non empty Subset of ExtREAL st X is bounded_below &amp; Y is bounded_below holds
(inf X) + (inf Y) <= inf (X + Y) by Th9;

theorem Th12: :: 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 )
proofend;

theorem Th13: :: 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 )
proofend;

theorem Th14: :: SUPINF_2:14
for X being non empty Subset of ExtREAL holds inf (- X) = - (sup X)
proofend;

theorem Th15: :: SUPINF_2:15
for X being non empty Subset of ExtREAL holds sup (- X) = - (inf X)
proofend;

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
proofend;
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 funcF . 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;
funcF + 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)
proofend;
uniqueness
 for b1, b2 being Function of X,(Y + Z) st ( for x being Element of X holds b1 . x = (F . x) + (G . x) ) &amp; ( for x being Element of X holds b2 . x = (F . x) + (G . x) ) holds
b1 = b2
proofend;
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 Th16: :: 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)
proofend;

theorem Th17: :: 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)
proofend;

theorem Th18: :: 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)
proofend;

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)
proofend;
uniqueness
 for b1, b2 being Function of X,(- Y) st ( for x being Element of X holds b1 . x = - (F . x) ) &amp; ( for x being Element of X holds b2 . x = - (F . x) ) holds
b1 = b2
proofend;
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 Th19: :: 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)
proofend;

theorem Th20: :: 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) &amp; sup (- F) = - (inf F) )
proofend;

::
:: Bounded Function of X,ExtREAL
::
definition
let X be set ;
let Y be Subset of ExtREAL;
let F be Function of X,Y;
attrF is bounded_above  means :Def5: :: SUPINF_2:def 5
 sup F < +infty ;
attrF 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;
attrF is bounded  means :Def7: :: SUPINF_2:def 7
( F is bounded_above &amp; F is bounded_below );
end;

:: deftheorem Def7 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 &amp; 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 &amp; b1 is bounded_below ) by Def7;
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 &amp; b1 is bounded_below holds
b1 is bounded by Def7;
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 &amp; -infty < inf F ) )
proofend;

theorem Th22: :: 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 )
proofend;

theorem Th23: :: 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 )
proofend;

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 )
proofend;

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 &amp; F . x <= +infty ) by XXREAL_0:4, XXREAL_0:5;

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 &amp; F . x < +infty )
proofend;

theorem Th27: :: 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 &amp; F . x <= sup F )
proofend;

theorem Th28: :: 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 )
proofend;

theorem Th29: :: 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 )
proofend;

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 &amp; sup F in REAL ) )
proofend;

theorem Th31: :: 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 &amp; F2 is bounded_above holds
F1 + F2 is bounded_above
proofend;

theorem Th32: :: 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 &amp; F2 is bounded_below holds
F1 + F2 is bounded_below
proofend;

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 &amp; F2 is bounded holds
F1 + F2 is bounded
proofend;

theorem Th34: :: SUPINF_2:34
( incl NAT is Function of NAT,ExtREAL &amp; incl NAT is one-to-one &amp; NAT = rng (incl NAT) &amp; rng (incl NAT) is non empty Subset of ExtREAL )
proofend;

::
:: Series of Elements of ExtREAL numbers
::
definition
let D be non empty set ;
let IT be Subset of D;
:: original:countable
redefine attrIT is countable  means :Def8: :: SUPINF_2:def 8
( IT is empty or ex F being Function of NAT,D st IT = rng F );
compatibility
 ( IT is countable iff ( IT is empty or ex F being Function of NAT,D st IT = rng F ) )
proofend;
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 Function of NAT,D st IT = rng F ) );

registration
cluster non empty ext-real-membered V78() for Element of K19(ExtREAL);
existence
 not for b1 being non empty Subset of ExtREAL holds b1 is V78()
proofend;
end;

definition
mode Denum_Set_of_R_EAL is non empty V78() Subset of ExtREAL;
end;

definition
let IT be set ;
attrIT is nonnegative  means :Def9: :: SUPINF_2:def 9
 for x being R_eal st x in IT holds
0. <= x;
end;

:: deftheorem Def9 defines nonnegative SUPINF_2:def_9_:_
 for IT being set holds
( IT is nonnegative iff for x being R_eal st x in IT holds
0. <= x );

registration
cluster non empty ext-real-membered countable nonnegative for Element of K19(ExtREAL);
existence
 ex b1 being Denum_Set_of_R_EAL st b1 is nonnegative
proofend;
end;

definition
mode Pos_Denum_Set_of_R_EAL is nonnegative Denum_Set_of_R_EAL;
end;

definition
let D be Denum_Set_of_R_EAL;
mode Num of D ->  Function of NAT,ExtREAL means :Def10: :: SUPINF_2:def 10
D = rng it;
existence
 ex b1 being Function of NAT,ExtREAL st D = rng b1 by Def8;
end;

:: deftheorem Def10 defines Num SUPINF_2:def_10_:_
 for D being Denum_Set_of_R_EAL
for b2 being Function of NAT,ExtREAL holds
( b2 is Num of D iff D = rng b2 );

definition
let D be Denum_Set_of_R_EAL;
let N be Num of D;
func Ser (D,N) ->  Function of NAT,ExtREAL means :Def11: :: SUPINF_2:def 11
( it . 0 = N . 0 &amp; ( for n being Element of NAT
for y being R_eal st y = it . n holds
it . (n + 1) = y + (N . (n + 1)) ) );
existence
 ex b1 being Function of NAT,ExtREAL st
( b1 . 0 = N . 0 &amp; ( for n being Element of NAT
for y being R_eal st y = b1 . n holds
b1 . (n + 1) = y + (N . (n + 1)) ) )
proofend;
uniqueness
 for b1, b2 being Function of NAT,ExtREAL st b1 . 0 = N . 0 &amp; ( for n being Element of NAT
for y being R_eal st y = b1 . n holds
b1 . (n + 1) = y + (N . (n + 1)) ) &amp; b2 . 0 = N . 0 &amp; ( for n being Element of NAT
for y being R_eal st y = b2 . n holds
b2 . (n + 1) = y + (N . (n + 1)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines Ser SUPINF_2:def_11_:_
 for D being Denum_Set_of_R_EAL
for N being Num of D
for b3 being Function of NAT,ExtREAL holds
( b3 = Ser (D,N) iff ( b3 . 0 = N . 0 &amp; ( for n being Element of NAT
for y being R_eal st y = b3 . n holds
b3 . (n + 1) = y + (N . (n + 1)) ) ) );

theorem Th35: :: SUPINF_2:35
for D being Pos_Denum_Set_of_R_EAL
for N being Num of D
for n being Element of NAT holds 0. <= N . n
proofend;

theorem Th36: :: SUPINF_2:36
for D being Pos_Denum_Set_of_R_EAL
for N being Num of D
for n being Element of NAT holds
( (Ser (D,N)) . n <= (Ser (D,N)) . (n + 1) &amp; 0. <= (Ser (D,N)) . n )
proofend;

theorem Th37: :: SUPINF_2:37
for D being Pos_Denum_Set_of_R_EAL
for N being Num of D
for n, m being Element of NAT holds (Ser (D,N)) . n <= (Ser (D,N)) . (n + m)
proofend;

definition
let D be Denum_Set_of_R_EAL;
mode Set_of_Series of D ->  non empty Subset of ExtREAL means :: SUPINF_2:def 12
 ex N being Num of D st it = rng (Ser (D,N));
existence
 ex b1 being non empty Subset of ExtREAL ex N being Num of D st b1 = rng (Ser (D,N))
proofend;
end;

:: deftheorem  defines Set_of_Series SUPINF_2:def_12_:_
 for D being Denum_Set_of_R_EAL
for b2 being non empty Subset of ExtREAL holds
( b2 is Set_of_Series of D iff ex N being Num of D st b2 = rng (Ser (D,N)) );

definition
let D be Pos_Denum_Set_of_R_EAL;
let N be Num of D;
func SUM (D,N) ->  R_eal equals :: SUPINF_2:def 13
 sup (rng (Ser (D,N)));
coherence
 sup (rng (Ser (D,N))) is R_eal ;
end;

:: deftheorem  defines SUM SUPINF_2:def_13_:_
 for D being Pos_Denum_Set_of_R_EAL
for N being Num of D holds SUM (D,N) = sup (rng (Ser (D,N)));

definition
let D be Pos_Denum_Set_of_R_EAL;
let N be Num of D;
predD is_sumable N means :: SUPINF_2:def 14
 SUM (D,N) in REAL ;
end;

:: deftheorem  defines is_sumable SUPINF_2:def_14_:_
 for D being Pos_Denum_Set_of_R_EAL
for N being Num of D holds
( D is_sumable N iff SUM (D,N) in REAL );

theorem Th38: :: SUPINF_2:38
for F being Function of NAT,ExtREAL holds rng F is Denum_Set_of_R_EAL by Def8;

definition
let F be Function of NAT,ExtREAL;
:: original:rng
redefine func rng F ->  Denum_Set_of_R_EAL;
coherence
 rng F is Denum_Set_of_R_EAL by Th38;
end;

definition
let F be Function of NAT,ExtREAL;
func Ser F ->  Function of NAT,ExtREAL means :Def15: :: SUPINF_2:def 15
 for N being Num of rng F st N = F holds
it = Ser ((rng F),N);
existence
 ex b1 being Function of NAT,ExtREAL st
for N being Num of rng F st N = F holds
b1 = Ser ((rng F),N)
proofend;
uniqueness
 for b1, b2 being Function of NAT,ExtREAL st ( for N being Num of rng F st N = F holds
b1 = Ser ((rng F),N) ) &amp; ( for N being Num of rng F st N = F holds
b2 = Ser ((rng F),N) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def15 defines Ser SUPINF_2:def_15_:_
 for F, b2 being Function of NAT,ExtREAL holds
( b2 = Ser F iff for N being Num of rng F st N = F holds
b2 = Ser ((rng F),N) );

definition
let R be Relation;
attrR is nonnegative  means :Def16: :: SUPINF_2:def 16
 rng R is nonnegative ;
end;

:: deftheorem Def16 defines nonnegative SUPINF_2:def_16_:_
 for R being Relation holds
( R is nonnegative iff rng R is nonnegative );

definition
let F be Function of NAT,ExtREAL;
func SUM F ->  R_eal equals :: SUPINF_2:def 17
 sup (rng (Ser F));
coherence
 sup (rng (Ser F)) is R_eal ;
end;

:: deftheorem  defines SUM SUPINF_2:def_17_:_
 for F being Function of NAT,ExtREAL holds SUM F = sup (rng (Ser F));

theorem Th39: :: 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 )
proofend;

theorem Th40: :: SUPINF_2:40
for F being Function of NAT,ExtREAL
for n being Element of NAT st F is nonnegative holds
( (Ser F) . n <= (Ser F) . (n + 1) &amp; 0. <= (Ser F) . n )
proofend;

theorem Th41: :: SUPINF_2:41
for F being Function of NAT,ExtREAL st F is nonnegative holds
for n, m being Element of NAT holds (Ser F) . n <= (Ser F) . (n + m)
proofend;

theorem Th42: :: SUPINF_2:42
for F1, F2 being Function of NAT,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
proofend;

theorem Th43: :: SUPINF_2:43
for F1, F2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds F1 . n <= F2 . n ) holds
SUM F1 <= SUM F2
proofend;

theorem Th44: :: SUPINF_2:44
for F being Function of NAT,ExtREAL holds
( (Ser F) . 0 = F . 0 &amp; ( for n being Element of NAT
for y being R_eal st y = (Ser F) . n holds
(Ser F) . (n + 1) = y + (F . (n + 1)) ) )
proofend;

theorem Th45: :: SUPINF_2:45
for F being Function of NAT,ExtREAL st F is nonnegative &amp; ex n being Element of NAT st F . n = +infty holds
SUM F = +infty
proofend;

definition
let F be Function of NAT,ExtREAL;
attrF is summable  means :Def18: :: SUPINF_2:def 18
 SUM F in REAL ;
end;

:: deftheorem Def18 defines summable SUPINF_2:def_18_:_
 for F being Function of NAT,ExtREAL holds
( F is summable iff SUM F in REAL );

theorem :: SUPINF_2:46
for F being Function of NAT,ExtREAL st F is nonnegative &amp; ex n being Element of NAT st F . n = +infty holds
not F is summable
proofend;

theorem :: SUPINF_2:47
for F1, F2 being Function of NAT,ExtREAL st F1 is nonnegative &amp; ( for n being Element of NAT holds F1 . n <= F2 . n ) &amp; F2 is summable holds
F1 is summable
proofend;

theorem Th48: :: SUPINF_2:48
for F being Function of NAT,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
proofend;

theorem Th49: :: SUPINF_2:49
for F being Function of NAT,ExtREAL st ( for n being Element of NAT holds F . n in REAL ) holds
for n being Element of NAT holds (Ser F) . n in REAL
proofend;

theorem :: SUPINF_2:50
for F being Function of NAT,ExtREAL st F is nonnegative &amp; ex n being Element of NAT st
( ( for k being Element of NAT st n <= k holds
F . k = 0. ) &amp; ( for k being Element of NAT st k <= n holds
F . k <> +infty ) ) holds
F is summable
proofend;

:: Added by AK, 2006.02.06
theorem :: SUPINF_2:51
for X being set
for F being PartFunc of X,ExtREAL holds
( F is nonnegative iff for n being set holds 0. <= F . n )
proofend;

theorem :: SUPINF_2:52
for X being set
for F being PartFunc of X,ExtREAL st ( for n being set st n in dom F holds
0. <= F . n ) holds
F is nonnegative
proofend;