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