The abstract of the Mizar article:

The Definition of the Riemann Definite Integral and some Related Lemmas

by

Noboru Endou, and

Artur Kornilowicz

Received March 13, 1999

MML identifier: INTEGRA1

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_1, RCOMP_1, COMPTS_1, SEQ_2, LATTICES, ORDINAL2, ARYTM,
      ARYTM_1, RELAT_1, FUNCT_1, MEASURE5, PARTFUN1, RLVECT_1, SUBSET_1, BOOLE,
      RFUNCT_1, FUNCT_3, PARTFUN2, FINSEQ_4, FINSEQ_2, VECTSP_1, RVSUM_1,
      FINSET_1, SQUARE_1, RFINSEQ, JORDAN3, SEQ_4, CARD_1, INTEGRA1, REALSET1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XREAL_0, REAL_1, NAT_1, FUNCT_1, REALSET1, RELSET_1, SEQ_1, SEQ_4,
      GOBOARD1, RCOMP_1, PSCOMP_1, FINSET_1, FINSEQ_1, FUNCOP_1, VECTSP_1,
      FINSEQ_2, FINSEQ_4, PARTFUN2, RFUNCT_1, PRE_CIRC, RVSUM_1, COMPLSP1,
      RFINSEQ, BINARITH, JORDAN3, CARD_1, PARTFUN1, TOPREAL1, FUNCT_2;
 constructors REAL_1, FINSEQOP, FINSEQ_4, PARTFUN1, PSCOMP_1, PARTFUN2,
      RFUNCT_1, RCOMP_1, PRE_CIRC, COMPLSP1, GOBOARD9, BINARITH, RFINSEQ,
      JORDAN3, GOBOARD1, INT_1, REALSET1;
 clusters SUBSET_1, XREAL_0, RELSET_1, FINSEQ_1, NAT_2, PSCOMP_1, FINSEQ_2,
      GOBOARD1, GROUP_2, FINSEQ_5, FUNCT_2, XBOOLE_0, NAT_1, MEMBERED, NUMBERS,
      ORDINAL2;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Definition of closed interval and its properties

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

definition let IT be Subset of REAL;
 attr IT is closed-interval means
:: INTEGRA1:def 1
ex a,b being Real st a <= b & IT=[.a,b.];
end;

definition
 cluster closed-interval Subset of REAL;
end;

reserve A for closed-interval Subset of REAL;

theorem :: INTEGRA1:1
A is compact;

theorem :: INTEGRA1:2
A is non empty;

definition
 cluster closed-interval -> non empty compact Subset of REAL;
end;

theorem :: INTEGRA1:3
A is bounded_below & A is bounded_above;

definition
 cluster closed-interval -> bounded Subset of REAL;
end;

definition
 cluster closed-interval Subset of REAL;
end;

reserve A for closed-interval Subset of REAL;

theorem :: INTEGRA1:4
ex a,b st a<=b & a=inf A & b=sup A;

theorem :: INTEGRA1:5
A = [. inf A, sup A .];

theorem :: INTEGRA1:6
for a1,a2,b1,b2 being real number holds
 A=[.a1,b1.] & A=[.a2,b2.] implies a1=a2 & b1=b2;

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

definition let A be non empty compact Subset of REAL;
 mode DivisionPoint of A -> non empty increasing FinSequence of REAL means
:: INTEGRA1:def 2
 rng it c= A & it.(len it) = sup A;
end;

definition let A be non empty compact Subset of REAL;
 func divs A means
:: INTEGRA1:def 3
  x1 in it iff x1 is DivisionPoint of A;
end;

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

definition let A be non empty compact Subset of REAL;
 mode Division of A -> non empty set means
:: INTEGRA1:def 4
  x1 in it iff x1 is DivisionPoint of A;
end;

definition let A be non empty compact Subset of REAL;
 cluster non empty Division of A;
end;

definition let A be non empty compact Subset of REAL,
 S be non empty Division of A;
 redefine mode Element of S -> DivisionPoint of A;
end;

reserve r for Real;
reserve S for non empty Division of A;
reserve D for Element of S;

canceled;

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

theorem :: INTEGRA1:9
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 closed-interval Subset of REAL;
 let S be non empty Division of A;
 let D be Element of S;
 let i be Nat;
 assume i in dom D;
 func divset(D,i) -> closed-interval Subset of REAL means
:: INTEGRA1:def 5
  inf it = inf A & sup it = D.i if i=1
 otherwise inf it = D.(i-1) & sup it = D.i;
end;

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

definition let A be Subset of REAL;
func vol(A) -> Real equals
:: INTEGRA1:def 6
 sup A - inf A;
end;

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

begin :: Definitions of integrability and related topics

definition let A be closed-interval Subset of REAL;
 let f be PartFunc of A,REAL;
 let S be non empty Division of A;
 let D be Element of S;
 func upper_volume(f,D) -> FinSequence of REAL means
:: INTEGRA1:def 7
  len it = len D & for i st i in Seg(len D) holds
 it.i=(sup (rng (f|divset(D,i))))*vol(divset(D,i));

 func lower_volume(f,D) -> FinSequence of REAL means
:: INTEGRA1:def 8
  len it = len D & for i st i in Seg(len D) holds
 it.i=(inf (rng (f|divset(D,i))))*vol(divset(D,i));
end;

definition let A be closed-interval Subset of REAL;
 let f be PartFunc of A,REAL;
 let S be non empty Division of A;
 let D be Element of S;
 func upper_sum(f,D) -> Real equals
:: INTEGRA1:def 9
  Sum(upper_volume(f,D));

 func lower_sum(f,D) -> Real equals
:: INTEGRA1:def 10
  Sum(lower_volume(f,D));
end;

definition let A be closed-interval Subset of REAL;
 redefine func divs A -> Division of A;
end;

definition let A be closed-interval Subset of REAL;
 let f be PartFunc of A,REAL;
 func upper_sum_set(f) -> PartFunc of divs A,REAL means
:: INTEGRA1:def 11
  dom it = divs A &
 for D be Element of divs A st D in dom it holds it.D=upper_sum(f,D);

 func lower_sum_set(f) -> PartFunc of divs A,REAL means
:: INTEGRA1:def 12
  dom it = divs A &
 for D be Element of divs A st D in dom it holds it.D=lower_sum(f,D);
end;

definition let A be closed-interval Subset of REAL;
 let f be PartFunc of A,REAL;
 pred f is_upper_integrable_on A means
:: INTEGRA1:def 13
  rng upper_sum_set(f) is bounded_below;

 pred f is_lower_integrable_on A means
:: INTEGRA1:def 14
  rng lower_sum_set(f) is bounded_above;
end;

definition let A be closed-interval Subset of REAL;
 let f be PartFunc of A,REAL;
 func upper_integral(f) -> Real equals
:: INTEGRA1:def 15
  inf rng upper_sum_set(f);
end;

definition let A be closed-interval Subset of REAL;
 let f be PartFunc of A,REAL;
 func lower_integral(f) -> Real equals
:: INTEGRA1:def 16
  sup rng lower_sum_set(f);
end;

definition let A be closed-interval Subset of REAL;
 let f be PartFunc of A,REAL;
 pred f is_integrable_on A means
:: INTEGRA1:def 17
  f is_upper_integrable_on A & f is_lower_integrable_on A &
 upper_integral(f) = lower_integral(f);
end;

definition let A be closed-interval Subset of REAL;
 let f be PartFunc of A,REAL;
 func integral(f) -> Real equals
:: INTEGRA1:def 18
  upper_integral(f);
end;

begin :: Real function's properties

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

theorem :: INTEGRA1:13
 for f be PartFunc of X,REAL holds
 f is_bounded_below_on X implies rng f is bounded_below;

theorem :: INTEGRA1:14
   for f be PartFunc of X,REAL
 st rng f is bounded_below holds f is_bounded_below_on X;

theorem :: INTEGRA1:15
 for f be PartFunc of X,REAL
 st f is_bounded_above_on X holds rng f is bounded_above;

theorem :: INTEGRA1:16
   for f be PartFunc of X,REAL
 st rng f is bounded_above holds f is_bounded_above_on X;

theorem :: INTEGRA1:17
   for f be PartFunc of X,REAL holds
 f is_bounded_on X implies rng f is bounded;

begin :: Characteristic function's properties

theorem :: INTEGRA1:18
 for A be non empty set holds
 chi(A,A) is_constant_on A;

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

theorem :: INTEGRA1:20
 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:21
 i in Seg(len D) implies vol(divset(D,i))=lower_volume(chi(A,A),D).i;

theorem :: INTEGRA1:22
 i in Seg(len D) implies vol(divset(D,i))=upper_volume(chi(A,A),D).i;

theorem :: INTEGRA1:23
   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:24
 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:25
 for A be closed-interval Subset of REAL,
 S being non empty Division of A,
 D being Element of S holds
 Sum(lower_volume(chi(A,A),D))=vol(A);

theorem :: INTEGRA1:26
 for A be closed-interval Subset of REAL,
 S being non empty Division of A,
 D being Element of S holds
 Sum(upper_volume(chi(A,A),D))=vol(A);

begin :: Some properties of Darboux sum

definition let A be closed-interval Subset of REAL;
 let f be PartFunc of A,REAL;
 let S be non empty Division of A;
 let D be Element of S;
 redefine func upper_volume(f,D) -> non empty FinSequence of REAL;
end;

definition let A be closed-interval Subset of REAL;
 let f be PartFunc of A,REAL;
 let S be non empty Division of A;
 let D be Element of S;
 redefine func lower_volume(f,D) -> non empty FinSequence of REAL;
end;

theorem :: INTEGRA1:27
 for A being closed-interval Subset of REAL,
 f being Function of A,REAL,
 S being non empty Division of A,
 D being Element of S holds
 (f is_bounded_below_on A implies
 (inf rng f)*vol(A) <= lower_sum(f,D));

theorem :: INTEGRA1:28
   for A being closed-interval Subset of REAL,
 f being Function of A,REAL,
 S being non empty Division of A,
 D being Element of S,
 i being Nat
 holds
 f is_bounded_above_on A & i in Seg(len D)implies
 (sup rng f)*vol(divset(D,i)) >= (sup rng (f|divset(D,i)))*vol(divset(D,i));

theorem :: INTEGRA1:29
 for A being closed-interval Subset of REAL,
 f being Function of A,REAL,
 S being non empty Division of A,
 D being Element of S
 holds
 (f is_bounded_above_on A implies
 upper_sum(f,D) <= (sup rng f)*vol(A));

theorem :: INTEGRA1:30
 for A being closed-interval Subset of REAL,
 f being Function of A,REAL,
 S being non empty Division of A,
 D being Element of S
 holds
 f is_bounded_on A implies
 lower_sum(f,D) <= upper_sum(f,D);

definition let x be non empty FinSequence of REAL;
 redefine func rng x -> finite non empty Subset of REAL;
end;

definition let A be closed-interval Subset of REAL;
 let D be Element of divs A;
 func delta(D) -> Real equals
:: INTEGRA1:def 19
   max rng upper_volume(chi(A,A),D);
end;

definition let A be closed-interval Subset of REAL;
 let S be non empty Division of A;
 let D1,D2 be Element of S;
 pred D1 <= D2 means
:: INTEGRA1:def 20
  len D1 <= len D2 & rng D1 c= rng D2;
 synonym D2 >= D1;
end;

theorem :: INTEGRA1:31
 for A be closed-interval Subset of REAL,
 S be non empty Division of A,
 D1,D2 be Element of S
 holds len D1 = 1 implies D1 <= D2;

theorem :: INTEGRA1:32
 for A be closed-interval Subset of REAL, f be Function of A,REAL,
 S be non empty Division of A, D1,D2 be Element of S
 holds f is_bounded_above_on A & len D1 = 1
 implies upper_sum(f,D1) >= upper_sum(f,D2);

theorem :: INTEGRA1:33
 for A be closed-interval Subset of REAL, f be Function of A,REAL,
 S be non empty Division of A, D1,D2 be Element of S
 holds f is_bounded_below_on A & len D1 = 1
 implies lower_sum(f,D1) <= lower_sum(f,D2);

theorem :: INTEGRA1:34
   for A be closed-interval Subset of REAL, S be non empty Division of A,
 D be Element of S st i in dom D holds
 ex A1,A2 be closed-interval Subset of REAL
  st A1=[.inf A,D.i .] & A2=[. D.i,sup A.] & A=A1 \/ A2;

theorem :: INTEGRA1:35
 for A be closed-interval Subset of REAL, S be non empty Division of A,
 D1,D2 be Element of S st i in dom D1
 holds D1 <= D2 implies ex j st j in dom D2 & D1.i=D2.j;

definition let A be closed-interval Subset of REAL;
 let S be non empty Division of A;
 let D1,D2 be Element of S;
 let i be Nat;
 assume D1 <= D2;
 func indx(D2,D1,i) -> Nat means
:: INTEGRA1:def 21
  it in dom D2 & D1.i=D2.it if i in dom D1 otherwise it = 0;
end;

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

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

theorem :: INTEGRA1:38
for A be closed-interval Subset of REAL,
 S be non empty Division of A, D be Element of S, i,j be Nat holds
 i in dom D & j in dom D & i<=j implies ex B be closed-interval Subset of REAL
 st inf B=mid(D,i,j).1 & sup B=mid(D,i,j).(len mid(D,i,j))
 & len mid(D,i,j)=j-i+1 & mid(D,i,j) is DivisionPoint of B;

theorem :: INTEGRA1:39
for A,B be closed-interval Subset of REAL,
 S be non empty Division of A, S1 be non empty Division of B,
 D be Element of S,
 i,j be Nat
 holds i in dom D & j in dom D & i<=j & D.i>=inf B & D.j=sup B
 implies mid(D,i,j) is Element of S1;

definition let p be FinSequence of REAL;
 func PartSums(p) -> FinSequence of REAL means
:: INTEGRA1:def 22
  len it = len p & for i st i in Seg(len p) holds it.i=Sum(p|i);
end;

theorem :: INTEGRA1:40
for A be closed-interval Subset of REAL,
 f be Function of A,REAL, S be non empty Division of A,
 D1,D2 be Element of S st D1 <= D2 & f is_bounded_above_on A
 holds for i be non empty Nat holds (i in dom D1 implies
 Sum(upper_volume(f,D1)|i) >= Sum(upper_volume(f,D2)|indx(D2,D1,i)));

theorem :: INTEGRA1:41
 for A be closed-interval Subset of REAL,
 f be Function of A,REAL, S be non empty Division of A,
 D1,D2 be Element of S st D1 <= D2 & f is_bounded_below_on A
 holds for i be non empty Nat holds (i in dom D1 implies
 Sum(lower_volume(f,D1)|i) <= Sum(lower_volume(f,D2)|indx(D2,D1,i)));

theorem :: INTEGRA1:42
for A be closed-interval Subset of REAL,
 f be Function of A,REAL,
 S be non empty Division of A, D1,D2 be Element of S, i be Nat
 holds D1 <= D2 & i in dom D1 & f is_bounded_above_on A
 implies
 (PartSums(upper_volume(f,D1))).i >=
 (PartSums(upper_volume(f,D2))).indx(D2,D1,i);

theorem :: INTEGRA1:43
for A be closed-interval Subset of REAL,
 f be Function of A,REAL,
 S be non empty Division of A, D1,D2 be Element of S, i be Nat
 holds D1 <= D2 & i in dom D1 & f is_bounded_below_on A
 implies
 (PartSums(lower_volume(f,D1))).i <=
 (PartSums(lower_volume(f,D2))).indx(D2,D1,i);

theorem :: INTEGRA1:44
for A be closed-interval Subset of REAL,
 f be PartFunc of A,REAL, S be non empty Division of A,
 D be Element of S
 holds (PartSums(upper_volume(f,D))).(len D) = upper_sum(f,D);

theorem :: INTEGRA1:45
for A be closed-interval Subset of REAL,
 f be PartFunc of A,REAL, S be non empty Division of A,
 D be Element of S
 holds (PartSums(lower_volume(f,D))).(len D) = lower_sum(f,D);

theorem :: INTEGRA1:46
for A be closed-interval Subset of REAL,
 S be non empty Division of A, D1,D2 be Element of S
 holds D1 <= D2 implies indx(D2,D1,len D1) = len D2;

theorem :: INTEGRA1:47
for A be closed-interval Subset of REAL,
 f be Function of A,REAL,
 S be non empty Division of A, D1,D2 be Element of S
 holds D1 <= D2 & f is_bounded_above_on A implies
 upper_sum(f,D2) <= upper_sum(f,D1);

theorem :: INTEGRA1:48
for A be closed-interval Subset of REAL,
 f be Function of A,REAL,
 S be non empty Division of A, D1,D2 be Element of S
 holds D1 <= D2 & f is_bounded_below_on A implies
 lower_sum(f,D2) >= lower_sum(f,D1);

theorem :: INTEGRA1:49
for A be closed-interval Subset of REAL,
 S be non empty Division of A, D1,D2 be Element of S
 holds ex D be Element of S st D1 <= D & D2 <= D;

theorem :: INTEGRA1:50
for A be closed-interval Subset of REAL,
 f be Function of A,REAL,
 S be non empty Division of A,
 D1,D2 be Element of S st f is_bounded_on A
 holds lower_sum(f,D1) <= upper_sum(f,D2);

begin :: Additivity of integral

theorem :: INTEGRA1:51
for A be closed-interval Subset of REAL,
 f be Function of A,REAL st
 f is_bounded_on A
 holds upper_integral(f) >= lower_integral(f);

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

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

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

theorem :: INTEGRA1:55
 for A be closed-interval Subset of REAL,
 f,g be Function of A,REAL,
 S be non empty Division of A,
 D be Element of S st i in Seg(len D) & f is_bounded_above_on A &
 g is_bounded_above_on A
 holds upper_volume(f+g,D).i <= upper_volume(f,D).i + upper_volume(g,D).i;

theorem :: INTEGRA1:56
 for A be closed-interval Subset of REAL,
 f,g be Function of A,REAL,
 S be non empty Division of A,
 D be Element of S st i in Seg(len D) & f is_bounded_below_on A
 & g is_bounded_below_on A
 holds lower_volume(f,D).i + lower_volume(g,D).i <= lower_volume(f+g,D).i;

theorem :: INTEGRA1:57
for A be closed-interval Subset of REAL,
 f,g be Function of A,REAL,
 S be non empty Division of A,
 D be Element of S st f is_bounded_above_on A
 & g is_bounded_above_on A
 holds upper_sum(f+g,D) <= upper_sum(f,D) + upper_sum(g,D);

theorem :: INTEGRA1:58
for A be closed-interval Subset of REAL,
 f,g be Function of A,REAL,
 S be non empty Division of A,
 D be Element of S st f is_bounded_below_on A
 & g is_bounded_below_on A
 holds lower_sum(f,D) + lower_sum(g,D) <= lower_sum(f+g,D);

theorem :: INTEGRA1:59
   for A be closed-interval Subset of REAL,
 f,g be Function of A,REAL st
 f is_bounded_on A & g is_bounded_on A &
 f is_integrable_on A & g is_integrable_on A
 holds f+g is_integrable_on A & integral(f+g)=integral(f)+integral(g);