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

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 b₁ being Function of X,(Y + Z) st
for x being Element of X holds b₁ . x = (F . x) + (G . x)

proof end;

uniqueness
for b₁, b₂ being Function of X,(Y + Z) st ( for x being Element of X holds b₁ . x = (F . x) + (G . x) ) & ( for x being Element of X holds b₂ . x = (F . x) + (G . x) ) holds
b₁ = b₂

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 b₆ being Function of X,(Y + Z) holds
( b₆ = F + G iff for x being Element of X holds b₆ . 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 b₁ being Function of X,(- Y) st
for x being Element of X holds b₁ . x = - (F . x)

proof end;

uniqueness
for b₁, b₂ being Function of X,(- Y) st ( for x being Element of X holds b₁ . x = - (F . x) ) & ( for x being Element of X holds b₂ . x = - (F . x) ) holds
b₁ = b₂

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 b₄ being Function of X,(- Y) holds
( b₄ = - F iff for x being Element of X holds b₄ . 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 b₁ being Function of X,Y st b₁ is bounded holds
( b₁ is bounded_above & b₁ is bounded_below ) ;

cluster Function-like V18(X,Y) bounded_above bounded_below -> bounded for Element of K19(K20(X,Y));

coherence
for b₁ being Function of X,Y st b₁ is bounded_above & b₁ is bounded_below holds
b₁ 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 Def5, Def6;

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 Th21, Th22;

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 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 & 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 Th27, Th28;

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 Th31, Th30;

theorem Th33: :: SUPINF_2:34

( 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 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 b₁ being non empty Subset of ExtREAL holds b₁ 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

cluster ext-real-membered V85() nonnegative for Element of K19(ExtREAL);

existence
ex b₁ being V85() Subset of ExtREAL st b₁ 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 b₁ being sequence of ExtREAL st
( b₁ . 0 = N . 0 & ( for n being Nat
for y being R_eal st y = b₁ . n holds
b₁ . (n + 1) = y + (N . (n + 1)) ) )

proof end;

uniqueness
for b₁, b₂ being sequence of ExtREAL st b₁ . 0 = N . 0 & ( for n being Nat
for y being R_eal st y = b₁ . n holds
b₁ . (n + 1) = y + (N . (n + 1)) ) & b₂ . 0 = N . 0 & ( for n being Nat
for y being R_eal st y = b₂ . n holds
b₂ . (n + 1) = y + (N . (n + 1)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines Ser SUPINF_2:def 10 :
for N, b₂ being sequence of ExtREAL holds
( b₂ = Ser N iff ( b₂ . 0 = N . 0 & ( for n being Nat
for y being R_eal st y = b₂ . n holds
b₂ . (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;

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