:: 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
::           (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, ORDINAL1, XXREAL_2,
      FUNCT_1, RELAT_1, VALUED_0, FUNCT_3, CARD_3, FUNCT_4, FUNCOP_1, PARTFUN1,
      NAT_1, SERIES_1, SUPINF_2, MEMBER_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, MEMBERED, XXREAL_0,
      XXREAL_3, XCMPLX_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;
 registrations RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSET_1, NUMBERS, XREAL_0,
      MEMBERED, VALUED_0, XXREAL_3, RELSET_1, MEMBER_1;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


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 R_eal, a,b being Real st x = a & y = b holds
  x + y = a + b;

theorem :: SUPINF_2:2
  for x being R_eal, a being Real st x = a holds - x = - a;

theorem :: SUPINF_2:3
  for x,y being R_eal, 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;

canceled;

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 <inf F;

theorem :: SUPINF_2:22
  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;

theorem :: SUPINF_2:23
  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;

theorem :: SUPINF_2:24
  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;

theorem :: SUPINF_2:25
  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
;

theorem :: SUPINF_2:26
  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;

theorem :: SUPINF_2:27
  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
;

theorem :: SUPINF_2:28
  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);

theorem :: SUPINF_2:29
  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);

theorem :: SUPINF_2:30
  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);

theorem :: SUPINF_2:31
  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;

theorem :: SUPINF_2:32
  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;

theorem :: SUPINF_2:33
  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;

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

::
::       Series of Elements of ExtREAL numbers
::

definition
  let D be non empty set, IT be Subset of D;
  redefine attr IT is countable means
:: SUPINF_2:def 8

  IT is empty or ex F being Function of NAT,D st IT = rng F;
end;

registration
  cluster countable for non empty Subset of ExtREAL;
end;

definition
  mode Denum_Set_of_R_EAL is countable non empty Subset of ExtREAL;
end;

definition
  let IT be set;
  attr IT is nonnegative means
:: SUPINF_2:def 9

  for x being R_eal holds x in IT implies 0. <= x;
end;

registration
  cluster nonnegative for Denum_Set_of_R_EAL;
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
:: SUPINF_2:def 10

    D = rng it;
end;

definition
  let D be Denum_Set_of_R_EAL;
  let N be Num of D;
  func Ser(D,N) -> Function of NAT,ExtREAL means
:: SUPINF_2:def 11

  it.0 = N.0 &
  for n being Element of NAT for y being R_eal st y = it.n holds
  it.(n + 1) = y + N.(n + 1);
end;

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

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

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

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

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

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

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

definition
  let F be Function of NAT,ExtREAL;
  redefine func rng F -> Denum_Set_of_R_EAL;
end;

definition
  let F be Function of NAT,ExtREAL;
  func Ser(F) -> Function of NAT,ExtREAL means
:: SUPINF_2:def 15

  for N being Num of rng F st N = F holds it = Ser(rng F,N);
end;

definition
  let R be Relation;
  attr R is nonnegative means
:: SUPINF_2:def 16

  rng R is nonnegative;
end;

definition
  let F be Function of NAT,ExtREAL;
  func SUM(F) -> R_eal equals
:: SUPINF_2:def 17
  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 Function of NAT,ExtREAL, n being Element of NAT st F
  is nonnegative holds (Ser F).n <= (Ser F).(n + 1) & 0. <= (Ser F).n;

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

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

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

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

theorem :: SUPINF_2:45
  for F being Function of NAT,ExtREAL st F is nonnegative holds (
  ex n being Element of NAT st F.n = +infty) implies SUM(F) = +infty;

definition
  let F be Function of NAT,ExtREAL;
  attr F is summable means
:: SUPINF_2:def 18

  SUM(F) in REAL;
end;

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

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

theorem :: SUPINF_2:50
  for F being Function of NAT,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 set holds 0. <= F.n;

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