:: The Definition of Riemann Definite Integral and some Related Lemmas
::  by Noboru Endou and Artur Korni{\l}owicz
::
:: Received March 13, 1999
:: Copyright (c) 1999-2021 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 FINSEQ_1, RCOMP_1, ORDINAL2, ARYTM_1, RELAT_1, FUNCT_1, PARTFUN1,
      CARD_3, XBOOLE_0, FUNCT_3, ZFMISC_1, XXREAL_0, REAL_1, SUBSET_1,
      FINSEQ_2, RFINSEQ, JORDAN3, SEQ_4, CARD_1, INTEGRA1, FUNCOP_1, VALUED_0,
      NUMBERS, MEASURE7, ORDINAL4, XXREAL_1, XXREAL_2, NAT_1, ARYTM_3, TARSKI,
      MEMBER_1, MEASURE5, FUNCT_7, XCMPLX_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
      XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, NAT_D, RELAT_1, FUNCT_1,
      RELSET_1, VALUED_0, MEMBERED, MEMBER_1, VALUED_1, SEQ_4, XXREAL_2,
      COMSEQ_2, SEQ_2, RCOMP_1, FINSEQ_2, PARTFUN2, RFUNCT_1, RVSUM_1, RFINSEQ,
      FINSEQ_6, PARTFUN1, FINSEQ_1, FUNCT_2, MEASURE5, MEASURE6;
 constructors PARTFUN1, REAL_1, NAT_1, RCOMP_1, FINSOP_1, PARTFUN2, RFUNCT_1,
      REALSET1, RFINSEQ, BINARITH, FINSEQ_5, SEQM_3, MEASURE6, FINSEQ_6,
      BINOP_2, XXREAL_2, NAT_D, RVSUM_1, SEQ_4, RELSET_1, SEQ_2, MEMBER_1,
      XXREAL_3, MEASURE5, COMSEQ_2, NUMBERS;
 registrations SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0, NAT_1,
      MEMBERED, FINSEQ_1, FINSEQ_2, SEQM_3, VALUED_0, VALUED_1, FINSET_1,
      XXREAL_2, CARD_1, SEQ_2, RELSET_1, MEMBER_1, MEASURE5;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Definition of closed interval and its properties

reserve a,a1,b,b1,x,y for Real,
  F,G,H for FinSequence of REAL,
  i,j,k,n,m for Element of NAT,
  I for Subset of REAL,
  X for non empty set,
  x1,R,s for set;

reserve A for non empty closed_interval Subset of REAL;

registration
  cluster closed_interval -> compact for Subset of REAL;
end;

::$CT 2

theorem :: INTEGRA1:3
  A is bounded_below bounded_above;

registration
  cluster non empty closed_interval -> real-bounded for Subset of REAL;
end;

reserve A, B for non empty closed_interval Subset of REAL;

theorem :: INTEGRA1:4
  A = [. lower_bound A, upper_bound A .];

theorem :: INTEGRA1:5
  for a1,a2,b1,b2 being Real holds A=[.a1,b1.] & A=[.a2,b2.]
  implies a1=a2 & b1=b2;

begin :: Definition of division of closed interval and its properties

definition
::$CD
  let A be non empty compact Subset of REAL;
  mode Division of A -> non empty increasing FinSequence of REAL means
:: INTEGRA1:def 2

    rng it c= A & it.(len it) = upper_bound A;
end;

definition
  let A be non empty compact Subset of REAL;
  func divs A -> set means
:: INTEGRA1:def 3

  x1 in it iff x1 is Division of A;
end;

registration
  let A be non empty compact Subset of REAL;
  cluster divs A -> non empty;
end;

registration
  let A be non empty compact Subset of REAL;
  cluster -> Function-like Relation-like for Element of divs A;
end;

registration
  let A be non empty compact Subset of REAL;
  cluster -> real-valued FinSequence-like for Element of divs A;
end;

reserve r for Real;
reserve D, D1, D2 for Division of A;
reserve f, g for Function of A,REAL;

theorem :: INTEGRA1:6
  i in dom D implies D.i in A;

theorem :: INTEGRA1:7
  i in dom D & i<>1 implies i-1 in dom D & D.(i-1) in A & i-1 in NAT;

definition
  let A be non empty closed_interval Subset of REAL;
  let D be Division of A;
  let i be Nat;
  assume
 i in dom D;
  func divset(D,i) -> non empty closed_interval Subset of REAL means
:: INTEGRA1:def 4

  lower_bound it = lower_bound A & upper_bound it = D.i if i=1
  otherwise lower_bound it = D.(i-1) & upper_bound it = D.i;
end;

theorem :: INTEGRA1:8
  i in dom D implies divset(D,i) c= A;

definition
  let A be Subset of REAL;
  func vol(A) -> Real equals
:: INTEGRA1:def 5
  upper_bound A - lower_bound A;
end;

theorem :: INTEGRA1:9
  for A be real-bounded non empty Subset of REAL holds 0 <= vol(A);

begin :: Definitions of integrability and related topics

definition
  let A be non empty closed_interval Subset of REAL;
  let f be PartFunc of A,REAL;
  let D be Division of A;
  func upper_volume(f,D) -> FinSequence of REAL means
:: INTEGRA1:def 6

  len it = len D &
  for i be Nat st i in dom D holds it.i=(upper_bound rng (f|divset(D,i)))*vol
  divset(D,i);
  func lower_volume(f,D) -> FinSequence of REAL means
:: INTEGRA1:def 7

  len it = len D &
  for i be Nat st i in dom D holds it.i=(lower_bound rng (f|divset(D,i)))*vol
  divset(D,i);
end;

definition
  let A be non empty closed_interval Subset of REAL;
  let f be PartFunc of A,REAL;
  let D be Division of A;
  func upper_sum(f,D) -> Real equals
:: INTEGRA1:def 8
  Sum(upper_volume(f,D));
  func lower_sum(f,D) -> Real equals
:: INTEGRA1:def 9
  Sum(lower_volume(f,D));
end;

definition
  let A be non empty closed_interval Subset of REAL;
  let f be PartFunc of A,REAL;
  func upper_sum_set(f) -> Function of divs A,REAL means
:: INTEGRA1:def 10

  for D be Division of A holds it.D=upper_sum(f,D);
  func lower_sum_set(f) -> Function of divs A,REAL means
:: INTEGRA1:def 11

  for D be Division of A holds it.D=lower_sum(f,D);
end;

definition
  let A be non empty closed_interval Subset of REAL;
  let f be PartFunc of A,REAL;
  attr f is upper_integrable means
:: INTEGRA1:def 12
  rng upper_sum_set(f) is bounded_below;
  attr f is lower_integrable means
:: INTEGRA1:def 13
  rng lower_sum_set(f) is bounded_above;
end;

definition
  let A be non empty closed_interval Subset of REAL;
  let f be PartFunc of A,REAL;
  func upper_integral(f) -> Real equals
:: INTEGRA1:def 14
  lower_bound rng upper_sum_set(f);
end;

definition
  let A be non empty closed_interval Subset of REAL;
  let f be PartFunc of A,REAL;
  func lower_integral(f) -> Real equals
:: INTEGRA1:def 15
  upper_bound rng lower_sum_set(f);
end;

definition
  let A be non empty closed_interval Subset of REAL;
  let f be PartFunc of A,REAL;
  attr f is integrable means
:: INTEGRA1:def 16

  f is upper_integrable lower_integrable &
  upper_integral(f) = lower_integral(f);
end;

definition
  let A be non empty closed_interval Subset of REAL;
  let f be PartFunc of A,REAL;
  func integral(f) -> Real equals
:: INTEGRA1:def 17
  upper_integral(f);
end;

begin :: Real function's properties

theorem :: INTEGRA1:10
  for f,g be PartFunc of X,REAL holds rng(f+g) c= rng f ++ rng g;

theorem :: INTEGRA1:11
  for f be real-valued Function holds f is bounded_below implies
  rng f is bounded_below;

theorem :: INTEGRA1:12
  for f be real-valued Function st rng f is bounded_below holds
    f is bounded_below;

theorem :: INTEGRA1:13
  for f be real-valued Function st f is bounded_above holds
    rng f is bounded_above;

theorem :: INTEGRA1:14
  for f be real-valued Function st rng f is bounded_above holds
    f is bounded_above;

theorem :: INTEGRA1:15
  for f be real-valued Function holds f is bounded implies
    rng f is real-bounded;

begin :: Characteristic function's properties

theorem :: INTEGRA1:16
  for A be non empty set holds chi(A,A)|A is constant;

theorem :: INTEGRA1:17
  for A be non empty Subset of X holds rng chi(A,A) = {1};

theorem :: INTEGRA1:18
  for A be non empty Subset of X, B be set holds B meets dom chi(A
  ,A) implies rng (chi(A,A)|B) = {1};

theorem :: INTEGRA1:19
  i in dom D implies vol(divset(D,i))=lower_volume(chi(A,A),D).i;

theorem :: INTEGRA1:20
  i in dom D implies vol(divset(D,i))=upper_volume(chi(A,A),D).i;

theorem :: INTEGRA1:21
  len F = len G & len F = len H & (for k st k in dom F holds H.k = F/.k
  + G/.k) implies Sum(H) = Sum(F) + Sum(G);

theorem :: INTEGRA1:22
  len F = len G & len F = len H & (for k st k in dom F holds H.k =
  F/.k - G/.k) implies Sum(H) = Sum(F) - Sum(G);

theorem :: INTEGRA1:23
  Sum(lower_volume(chi(A,A),D))=vol(A);

theorem :: INTEGRA1:24
  Sum(upper_volume(chi(A,A),D))=vol(A);

begin :: Some properties of Darboux sum

registration
  let A be non empty closed_interval Subset of REAL;
  let f be PartFunc of A,REAL;
  let D be Division of A;
  cluster upper_volume(f,D) -> non empty;
  cluster lower_volume(f,D) -> non empty;
end;

theorem :: INTEGRA1:25
  f|A is bounded_below implies
  (lower_bound rng f)*vol(A) <= lower_sum(f,D);

theorem :: INTEGRA1:26
  f|A is bounded_above & i in dom D implies (upper_bound rng f)*vol(
  divset(D,i)) >= (upper_bound rng (f|divset(D,i)))*vol(divset(D,i));

theorem :: INTEGRA1:27
  f|A is bounded_above implies
  upper_sum(f,D) <= (upper_bound rng f)*vol(A);

theorem :: INTEGRA1:28
  f|A is bounded implies lower_sum(f,D) <= upper_sum(f,D);

definition
  let D1, D2 be FinSequence;

  pred D1 <= D2 means
:: INTEGRA1:def 18
  len D1 <= len D2 & rng D1 c= rng D2;
  reflexivity;
end;

notation
  let D1, D2 be FinSequence;
  synonym D2 >= D1 for D1 <= D2;
end;

theorem :: INTEGRA1:29
  len D1 = 1 implies D1 <= D2;

theorem :: INTEGRA1:30
  f|A is bounded_above & len D1 = 1 implies
    upper_sum(f,D1) >= upper_sum(f,D2);

theorem :: INTEGRA1:31
  f|A is bounded_below & len D1 = 1 implies
    lower_sum(f,D1) <= lower_sum(f,D2);

theorem :: INTEGRA1:32
  i in dom D implies ex A1,A2 be non empty closed_interval Subset of REAL
  st A1=[.lower_bound A,D.i .] & A2=[. D.i,upper_bound A.] & A=A1 \/ A2;

theorem :: INTEGRA1:33
  i in dom D1 & D1 <= D2 implies ex j st j in dom D2 & D1.i=D2.j;

definition
  let A, D1, D2;
  let i be Nat;
  assume
 D1 <= D2;
  func indx(D2,D1,i) -> Element of NAT means
:: INTEGRA1:def 19

  it in dom D2 & D1.i=D2.it
  if i in dom D1 otherwise it = 0;
end;

theorem :: INTEGRA1:34
  for p be increasing FinSequence of REAL, n be Element of NAT
  holds n <= len p implies p/^n is increasing FinSequence of REAL;

theorem :: INTEGRA1:35
  for p be increasing FinSequence of REAL, i,j be Element of NAT
holds j in dom p & i <= j implies mid(p,i,j) is increasing FinSequence of REAL;

theorem :: INTEGRA1:36
  i in dom D & j in dom D & i<=j implies
  ex B be non empty closed_interval Subset of REAL st
  lower_bound B = mid(D,i,j).1 & upper_bound B = mid(D,i,j).(len mid(D,i,j)) &
  mid(D,i,j) is Division of B;

theorem :: INTEGRA1:37
  i in dom D & j in dom D & i<=j & D.i>=lower_bound B & D.j=
  upper_bound B implies mid(D,i,j) is Division of B;

definition
  let p be FinSequence of REAL;
  func PartSums(p) -> FinSequence of REAL means
:: INTEGRA1:def 20

  len it = len p & for i be Nat st i in dom p holds it.i=Sum(p|i);
end;

theorem :: INTEGRA1:38
  D1 <= D2 & f|A is bounded_above implies for i be non zero
  Element of NAT holds (i in dom D1 implies Sum(upper_volume(f,D1)|i) >= Sum(
  upper_volume(f,D2)|indx(D2,D1,i)));

theorem :: INTEGRA1:39
  D1 <= D2 & f|A is bounded_below implies for i be non zero
  Element of NAT holds (i in dom D1 implies
  Sum(lower_volume(f,D1)|i) <= Sum(lower_volume(f,D2)|indx(D2,D1,i)));

theorem :: INTEGRA1:40
  D1 <= D2 & i in dom D1 & f|A is bounded_above implies (PartSums(
  upper_volume(f,D1))).i >= (PartSums(upper_volume(f,D2))).indx(D2,D1,i);

theorem :: INTEGRA1:41
  D1 <= D2 & i in dom D1 & f|A is bounded_below implies (PartSums(
  lower_volume(f,D1))).i <= (PartSums(lower_volume(f,D2))).indx(D2,D1,i);

theorem :: INTEGRA1:42
  (PartSums(upper_volume(f,D))).(len D) = upper_sum(f,D);

theorem :: INTEGRA1:43
  (PartSums(lower_volume(f,D))).(len D) = lower_sum(f,D);

theorem :: INTEGRA1:44
  D1 <= D2 implies indx(D2,D1,len D1) = len D2;

theorem :: INTEGRA1:45
  D1 <= D2 & f|A is bounded_above implies upper_sum(f,D2) <=
  upper_sum(f,D1);

theorem :: INTEGRA1:46
  D1 <= D2 & f|A is bounded_below implies lower_sum(f,D2) >=
  lower_sum(f,D1);

theorem :: INTEGRA1:47
  ex D be Division of A st D1 <= D & D2 <= D;

theorem :: INTEGRA1:48
  f|A is bounded implies lower_sum(f,D1) <= upper_sum(f,D2);

begin :: Additivity of integral

theorem :: INTEGRA1:49
  f|A is bounded implies upper_integral(f) >= lower_integral(f);

theorem :: INTEGRA1:50
  for X,Y be Subset of REAL holds (--X)++(--Y)=--(X++Y);

theorem :: INTEGRA1:51
  for X,Y being Subset of REAL st X is bounded_above & Y is
  bounded_above holds X++Y is bounded_above;

theorem :: INTEGRA1:52
  for X,Y be non empty Subset of REAL st
  X is bounded_above & Y is bounded_above holds
  upper_bound(X++Y) = upper_bound X + upper_bound Y;

theorem :: INTEGRA1:53
  i in dom D & f|A is bounded_above & g|A is bounded_above implies
  upper_volume(f+g,D).i <= upper_volume(f,D).i + upper_volume(g,D).i;

theorem :: INTEGRA1:54
  i in dom D & f|A is bounded_below & g|A is bounded_below implies
  lower_volume(f,D).i + lower_volume(g,D).i <= lower_volume(f+g,D).i;

theorem :: INTEGRA1:55
  f|A is bounded_above & g|A is bounded_above implies upper_sum(f+
  g,D) <= upper_sum(f,D) + upper_sum(g,D);

theorem :: INTEGRA1:56
  f|A is bounded_below & g|A is bounded_below implies lower_sum(f,
  D) + lower_sum(g,D) <= lower_sum(f+g,D);

theorem :: INTEGRA1:57
  f|A is bounded & g|A is bounded & f is integrable & g is integrable
  implies f+g is integrable & integral(f+g)=integral(f)+integral(g);

theorem :: INTEGRA1:58
  for f being FinSequence holds
  i in dom f & j in dom f & i<=j implies len mid(f,i,j) = j-i+1;