:: Definition of Integrability for Partial Functions from REAL to
:: REAL and Integrability for Continuous Functions
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received March 23, 2000
:: Copyright (c) 2000-2026 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 NUMBERS, SUBSET_1, REAL_1, INTEGRA1, FINSEQ_1, ORDINAL4, CARD_3,
ARYTM_1, ARYTM_3, BINOP_2, RELAT_1, FUNCT_1, PARTFUN1, XXREAL_0,
FINSEQ_2, NAT_1, XBOOLE_0, REALSET1, VALUED_1, TARSKI, XXREAL_2,
ORDINAL2, FCONT_2, INTEGRA2, FUNCT_3, SEQ_2, CARD_1, SEQ_1, COMPLEX1,
MEASURE7, FDIFF_1, SEQ_4, XXREAL_1, ZFMISC_1, VALUED_0, SEQM_3, RCOMP_1,
INTEGRA5, MEASURE5, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
RELAT_1, COMPLEX1, XXREAL_2, ZFMISC_1, FUNCT_1, RELSET_1, FUNCT_2,
RCOMP_1, PARTFUN1, MEASURE6, FINSEQ_1, FUNCOP_1, VALUED_1, SEQ_1,
RFUNCT_1, FINSEQ_2, COMSEQ_2, SEQ_2, SEQ_4, BINOP_2, REAL_1, NAT_1,
FDIFF_1, RVSUM_1, MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3, FCONT_1,
FCONT_2, RFUNCT_2, XXREAL_0;
constructors PARTFUN1, REAL_1, NAT_1, BINOP_2, COMPLEX1, RFUNCT_1, RFUNCT_2,
FCONT_1, FCONT_2, FDIFF_1, ZFMISC_1, MEASURE6, INTEGRA2, XXREAL_2,
RVSUM_1, SEQ_4, RELSET_1, FUNCOP_1, SEQ_2, INTEGRA3, COMSEQ_2;
registrations XBOOLE_0, RELAT_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED,
FINSEQ_1, RCOMP_1, INTEGRA1, VALUED_0, VALUED_1, FUNCT_2, FINSET_1,
XXREAL_2, CARD_1, SEQ_2, RELSET_1, MEASURE5, RVSUM_1, ORDINAL1, FINSEQ_2;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions XXREAL_2;
equalities VALUED_1;
expansions XXREAL_2;
theorems SEQ_4, SUBSET_1, PARTFUN1, INTEGRA1, RFUNCT_1, FUNCT_1, FINSEQ_1,
RVSUM_1, SEQ_1, SEQ_2, FDIFF_1, ABSVALUE, NAT_1, TARSKI, INTEGRA2, NAT_2,
FINSEQ_2, RCOMP_1, FCONT_2, INTEGRA4, FCONT_1, ROLLE, RFUNCT_2, FDIFF_2,
RELAT_1, XREAL_0, FUNCT_2, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1,
XXREAL_0, ORDINAL1, VALUED_1, XXREAL_2, XXREAL_1, RELSET_1, INTEGRA3,
MEASURE5, INT_1;
schemes FINSEQ_2;
begin ::Some useful properties of finite sequence
reserve i,k,n,m for Element of NAT;
reserve a,b,r,r1,r2,s,x,x1,x2 for Real;
reserve A for non empty closed_interval Subset of REAL;
reserve X for set;
theorem Th1:
for F,F1,F2 being FinSequence of REAL, r1,r2 st (F1=<*r1*>^F or
F1=F^<*r1*>) & (F2=<*r2*>^F or F2=F^<*r2*>) holds Sum(F1-F2)=r1-r2
proof
let F,F1,F2 be FinSequence of REAL;
let r1,r2;
assume that
A1: F1=<*r1*>^F or F1=F^<*r1*> and
A2: F2=<*r2*>^F or F2=F^<*r2*>;
len F1=len F+len<*r1*> by A1,FINSEQ_1:22;
then
A3: len F1=len F+1 by FINSEQ_1:39;
len F2=len<*r2*>+len F by A2,FINSEQ_1:22;
then
A4: len F2=1+len F by FINSEQ_1:39;
F1-F2 = diffreal.:(F1,F2) by RVSUM_1:def 6;
then
A5: len F1 = len (F1-F2) by A3,A4,FINSEQ_2:72;
for k st k in dom F1 holds (F1-F2).k = F1/.k - F2/.k
proof
let k;
assume
A6: k in dom F1;
then
A7: F1.k = F1/.k by PARTFUN1:def 6;
A8: k in Seg len F1 by A6,FINSEQ_1:def 3;
then k in dom F2 by A3,A4,FINSEQ_1:def 3;
then
A9: F2.k = F2/.k by PARTFUN1:def 6;
k in dom (F1-F2) by A5,A8,FINSEQ_1:def 3;
hence thesis by A7,A9,VALUED_1:13;
end;
then
A10: Sum(F1-F2)=Sum F1-Sum F2 by A3,A4,A5,INTEGRA1:22;
Sum F1=r1+Sum F & Sum F2=Sum F+r2 by A1,A2,RVSUM_1:74,76;
hence thesis by A10;
end;
theorem Th2:
for F1,F2 being FinSequence of REAL st len F1 = len F2 holds len
(F1+F2)=len F1 & len (F1-F2)=len F1 & Sum(F1+F2)=Sum F1+Sum F2 & Sum(F1-F2)=
Sum F1-Sum F2
proof
let F1,F2 be FinSequence of REAL;
assume
A1: len F1=len F2;
F1+F2=addreal.:(F1,F2) by RVSUM_1:def 4;
hence
A2: len F1=len (F1+F2) by A1,FINSEQ_2:72;
F1-F2=diffreal.:(F1,F2) by RVSUM_1:def 6;
hence
A3: len F1=len (F1-F2) by A1,FINSEQ_2:72;
for k st k in dom F1 holds (F1+F2).k = F1/.k + F2/.k
proof
let k;
assume
A4: k in dom F1;
then
A5: F1.k = F1/.k by PARTFUN1:def 6;
A6: k in Seg len F1 by A4,FINSEQ_1:def 3;
then k in dom F2 by A1,FINSEQ_1:def 3;
then
A7: F2.k = F2/.k by PARTFUN1:def 6;
k in dom (F1+F2) by A2,A6,FINSEQ_1:def 3;
hence thesis by A5,A7,VALUED_1:def 1;
end;
hence Sum(F1+F2)=Sum F1 + Sum F2 by A1,A2,INTEGRA1:21;
for k st k in dom F1 holds (F1-F2).k = F1/.k - F2/.k
proof
let k;
assume
A8: k in dom F1;
then
A9: F1.k = F1/.k by PARTFUN1:def 6;
A10: k in Seg len F1 by A8,FINSEQ_1:def 3;
then k in dom F2 by A1,FINSEQ_1:def 3;
then
A11: F2.k = F2/.k by PARTFUN1:def 6;
k in dom (F1-F2) by A3,A10,FINSEQ_1:def 3;
hence thesis by A9,A11,VALUED_1:13;
end;
hence thesis by A1,A3,INTEGRA1:22;
end;
theorem Th3:
for F1,F2 being FinSequence of REAL st len F1 = len F2 & (for i
st i in dom F1 holds F1.i <= F2.i) holds Sum F1 <= Sum F2
proof
let F1,F2 be FinSequence of REAL;
assume that
A1: len F1 = len F2 and
A2: for i st i in dom F1 holds F1.i <= F2.i;
reconsider R1=F1 as Element of (len F1)-tuples_on REAL by FINSEQ_2:92;
reconsider R2=F2 as Element of (len F1)-tuples_on REAL by A1,FINSEQ_2:92;
for i be Nat st i in Seg len F1 holds R1.i <= R2.i
proof
let i be Nat;
assume i in Seg len F1;
then i in dom F1 by FINSEQ_1:def 3;
hence thesis by A2;
end;
hence thesis by RVSUM_1:82;
end;
begin :: Integrability for partial function of REAL,REAL
notation
let f be PartFunc of REAL,REAL;
let C be non empty Subset of REAL;
synonym f||C for f|C;
end;
definition
let f be PartFunc of REAL,REAL;
let C be non empty Subset of REAL;
redefine func f||C -> PartFunc of C,REAL; :: redefines || (INTEGRA5, synonym) → | (RELAT_1, definition)
correctness by PARTFUN1:10;
end;
theorem Th4:
for f,g being PartFunc of REAL,REAL, C being non empty Subset of
REAL holds (f||C)(#)(g||C) = (f(#)g)||C
proof
let f,g be PartFunc of REAL,REAL;
let C be non empty Subset of REAL;
A1: dom ((f(#)g)||C)= dom(f(#)g) /\ C by RELAT_1:61
.= (dom f /\ dom g) /\ C by VALUED_1:def 4;
A2: dom (f||C(#)g||C)= dom (f|C) /\ dom(g||C) by VALUED_1:def 4
.= (dom f /\ C) /\ dom (g|C) by RELAT_1:61
.= (dom f /\ C) /\ (dom g /\ C) by RELAT_1:61
.= ((dom f /\ C) /\ C) /\ dom g by XBOOLE_1:16
.= (dom f /\ (C /\ C)) /\ dom g by XBOOLE_1:16
.= (dom f /\ C) /\ dom g;
then
A3: dom (f||C(#)g||C) = dom ((f(#)g)||C) by A1,XBOOLE_1:16;
for c being Element of C st c in dom(f||C(#)g||C) holds (f||C(#)g||C).c
= ((f(#)g)||C).c
proof
let c be Element of C;
A4: (f||C(#)g||C).c =(f|C).c * (g|C).c by VALUED_1:5;
assume
A5: c in dom(f||C(#)g||C);
then
A6: c in dom (f||C) /\ dom (g||C) by VALUED_1:def 4;
then
A7: c in dom (f||C) by XBOOLE_0:def 4;
A8: c in dom (g||C) by A6,XBOOLE_0:def 4;
((f(#)g)||C).c =(f(#)g).c by A3,A5,FUNCT_1:47
.=f.c * g.c by VALUED_1:5
.= (f|C).c * g.c by A7,FUNCT_1:47;
hence thesis by A8,A4,FUNCT_1:47;
end;
hence thesis by A2,A1,PARTFUN1:5,XBOOLE_1:16;
end;
theorem Th5:
for f,g being PartFunc of REAL,REAL, C being non empty Subset of
REAL holds (f+g)||C = f||C + g||C
proof
let f,g be PartFunc of REAL,REAL;
let C be non empty Subset of REAL;
A1: dom (f||C+g||C) =dom (f|C) /\ dom (g||C) by VALUED_1:def 1
.= (dom f /\ C) /\ dom (g|C) by RELAT_1:61
.= (dom f /\ C) /\ (dom g /\ C) by RELAT_1:61
.= dom f /\ (C /\ (dom g /\ C)) by XBOOLE_1:16
.= dom f /\ (dom g /\ (C /\ C)) by XBOOLE_1:16
.= dom f /\ (dom g /\ C);
A2: dom ((f+g)||C) = dom (f+g) /\ C by RELAT_1:61
.= dom f /\ dom g /\ C by VALUED_1:def 1;
then
A3: dom ((f+g)||C) = dom (f||C + g||C) by A1,XBOOLE_1:16;
for c being Element of C st c in dom ((f+g)||C) holds (f+g)||C.c = (f||C
+ g||C).c
proof
let c be Element of C;
assume
A4: c in dom((f+g)||C);
then c in dom(f+g) /\ C by RELAT_1:61;
then
A5: c in dom(f+g) by XBOOLE_0:def 4;
A6: c in dom(f||C) /\ dom(g||C) by A3,A4,VALUED_1:def 1;
then
A7: c in dom(f||C) by XBOOLE_0:def 4;
A8: (f+g)||C.c = (f+g).c by A4,FUNCT_1:47
.= f.c + g.c by A5,VALUED_1:def 1;
A9: c in dom(g||C) by A6,XBOOLE_0:def 4;
(f||C+g||C).c =f|C.c + g||C.c by A3,A4,VALUED_1:def 1
.= f.c + g|C.c by A7,FUNCT_1:47;
hence thesis by A8,A9,FUNCT_1:47;
end;
hence thesis by A2,A1,PARTFUN1:5,XBOOLE_1:16;
end;
definition
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL,REAL;
pred f is_integrable_on A means
f||A is integrable;
end;
definition
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL,REAL;
func integral(f,A) -> Real equals
integral(f||A);
correctness;
end;
theorem Th6:
for f being PartFunc of REAL,REAL st A c= dom f holds f||A is
total
proof
let f be PartFunc of REAL,REAL;
assume
A1: A c= dom f;
dom (f||A) = dom f /\ A by RELAT_1:61
.= A by A1,XBOOLE_1:28;
hence thesis by PARTFUN1:def 2;
end;
theorem
for f being PartFunc of REAL,REAL st f|A is bounded_above holds f
||A|A is bounded_above;
theorem
for f being PartFunc of REAL,REAL st f|A is bounded_below holds f
||A|A is bounded_below;
theorem
for f being PartFunc of REAL,REAL st f|A is bounded holds f||A|A
is bounded;
begin :: Integrability for continuous function
theorem Th10:
for f being PartFunc of REAL,REAL st A c= dom f & f|A is
continuous holds f|A is bounded
proof
let f be PartFunc of REAL,REAL;
assume
A1: A c= dom f;
assume f|A is continuous;
then
A2: f.:A is real-bounded by A1,FCONT_1:29,RCOMP_1:10;
then consider a be Real such that
A3: a is UpperBound of f.:A by XXREAL_2:def 10;
A4: for r be Real st r in f.:A holds r <= a by A3,XXREAL_2:def 1;
consider b be Real such that
A5: b is LowerBound of f.:A by A2,XXREAL_2:def 9;
A6: for r be Real st r in f.:A holds b <= r by A5,XXREAL_2:def 2;
for x being object st x in A /\ dom f holds b <= f.x
proof
let x be object;
assume x in A /\ dom f;
then x in A & x in dom f by XBOOLE_0:def 4;
then f.x in f.:A by FUNCT_1:def 6;
hence thesis by A6;
end;
then
A7: f|A is bounded_below by RFUNCT_1:71;
for x being object st x in A /\ dom f holds f.x <= a
proof
let x be object;
assume x in A /\ dom f;
then x in A & x in dom f by XBOOLE_0:def 4;
then f.x in f.:A by FUNCT_1:def 6;
hence thesis by A4;
end;
then f|A is bounded_above by RFUNCT_1:70;
hence thesis by A7;
end;
theorem Th11:
for f being PartFunc of REAL,REAL st A c= dom f & f|A is
continuous holds f is_integrable_on A
proof
let f be PartFunc of REAL,REAL;
assume
A1: A c= dom f;
reconsider g=f|A as PartFunc of A,REAL by PARTFUN1:10;
A2: dom g = dom f /\ A by RELAT_1:61
.= A by A1,XBOOLE_1:28;
then
A3: g is total by PARTFUN1:def 2;
for y being object st y in f.:A holds y in rng g
proof
let y be object;
assume y in f.:A;
then consider x being object such that
x in dom f and
A4: x in A and
A5: y = f.x by FUNCT_1:def 6;
g.x in rng g by A2,A4,FUNCT_1:def 3;
hence thesis by A2,A4,A5,FUNCT_1:47;
end;
then
A6: f.:A c= rng g by TARSKI:def 3;
for y being object st y in rng g holds y in f.:A
proof
let y be object;
assume y in rng g;
then consider x being object such that
A7: x in dom g and
A8: y=g.x by FUNCT_1:def 3;
f.x in f.:A by A1,A2,A7,FUNCT_1:def 6;
hence thesis by A7,A8,FUNCT_1:47;
end;
then rng g c= f.:A by TARSKI:def 3;
then
A9: rng g = f.:A by A6,XBOOLE_0:def 10;
assume
A10: f|A is continuous;
then f.:A is real-bounded by A1,FCONT_1:29,RCOMP_1:10;
then
A11: g|A is bounded_above & g|A is bounded_below by A9,INTEGRA1:12,14;
reconsider g as Function of A,REAL by A3;
A12: f|A is uniformly_continuous by A1,A10,FCONT_2:11;
for T being DivSequence of A st delta(T) is convergent & lim delta(T)=0
holds lim upper_sum(g,T)-lim lower_sum(g,T)=0
proof
let T be DivSequence of A;
reconsider osc=upper_sum(g,T)-lower_sum(g,T) as Real_Sequence;
assume
A13: delta(T) is convergent & lim delta(T)=0;
A14: for r be Real st 0<r
ex n being Nat st for m being Nat st n<=m holds |.osc.m-0.|<
r
proof
let r be Real;
assume
A15: r>0;
ex r1 st r1>0 & r1*vol(A)<r
proof
per cases by INTEGRA1:9;
suppose
A16: vol(A)=0;
take 1;
r1*vol(A)<r by A15,A16;
hence thesis;
end;
suppose
A17: vol(A)>0;
then r/vol(A) > 0 by A15,XREAL_1:139;
then consider r1 being Real such that
A18: 0<r1 and
A19: r1<r/vol(A) by XREAL_1:5;
take r1;
r1*vol(A)<r by A17,A19,XREAL_1:79;
hence thesis by A18;
end;
end;
then consider r1 such that
A20: r1>0 and
A21: r1*vol(A) < r;
consider s such that
A22: 0<s and
A23: for x1,x2 st x1 in dom(f|A) & x2 in dom(f|A) & |.x1-x2.| < s
holds |.f.x1 - f.x2.| < r1 by A12,A20,FCONT_2:1;
consider n being Nat such that
A24: for m being Nat st n<=m
holds |.delta(T).m-0.|<s by A13,A22,SEQ_2:def 7;
A25: for m st n<=m holds upper_sum(g,T).m-lower_sum(g,T).m <=r1*vol(A)
proof
let m;
reconsider D=T.m as Division of A;
len upper_volume(g,D) = len D by INTEGRA1:def 6;
then reconsider
UV=upper_volume(g,D) as Element of (len D)-tuples_on REAL
by FINSEQ_2:92;
len lower_volume(g,D) = len D by INTEGRA1:def 7;
then reconsider
LV=lower_volume(g,D) as Element of (len D)-tuples_on REAL
by FINSEQ_2:92;
reconsider OSC=UV-LV as Element of (len D)-tuples_on REAL;
len upper_volume(chi(A,A),D) = len D by INTEGRA1:def 6;
then reconsider VOL=upper_volume(chi(A,A),D) as Element of (len D)
-tuples_on REAL by FINSEQ_2:92;
assume
A26: n<=m;
A27: for k st k in dom D holds upper_volume(g,D).k-lower_volume(g,D).k
<=r1*upper_volume(chi(A,A),D).k
proof
let k;
assume
A28: k in dom D;
reconsider h=g|divset(D,k) as PartFunc of divset(D,k),REAL by
PARTFUN1:10;
dom g = A by PARTFUN1:def 2;
then dom g /\ divset(D,k) = divset(D,k) by A28,INTEGRA1:8,XBOOLE_1:28
;
then dom h = divset(D,k) by RELAT_1:61;
then h is total by PARTFUN1:def 2;
then reconsider h as Function of divset(D,k),REAL;
A29: for x1,x2 st x1 in divset(D,k) & x2 in divset(D,k) holds |.h.
x1-h.x2.|<=r1
proof
upper_volume(chi(A,A),D).k=vol(divset(D,k)) by A28,INTEGRA1:20;
then
A30: upper_volume(chi(A,A),D).k>=0 by INTEGRA1:9;
k in Seg(len D) by A28,FINSEQ_1:def 3;
then k in Seg(len(upper_volume(chi(A,A),D))) by INTEGRA1:def 6;
then k in dom(upper_volume(chi(A,A),D)) by FINSEQ_1:def 3;
then
A31: upper_volume(chi(A,A),D).k in rng(upper_volume(chi(A,A),D))
by FUNCT_1:def 3;
dom h = dom g /\ divset(D,k) by RELAT_1:61;
then
A32: dom h c= dom g by XBOOLE_1:17;
let x1,x2;
assume that
A33: x1 in divset(D,k) and
A34: x2 in divset(D,k);
A35: x2 in dom h by A34,PARTFUN1:def 2;
then g.x2=h.x2 by FUNCT_1:47;
then
A36: f.x2=h.x2 by A35,A32,FUNCT_1:47;
A37: |.x1-x2.|<=delta(T).m
proof
now
per cases;
suppose
x1 >= x2;
then x1-x2>=0 by XREAL_1:48;
then
A38: |.x1-x2.|=x1-x2 by ABSVALUE:def 1;
x1<=upper_bound divset(D,k) & x2>=lower_bound divset(D,k)
by A33,A34,INTEGRA2:1;
then |.x1-x2.|<=
upper_bound divset(D,k)-lower_bound divset(D,k) by A38,
XREAL_1:13;
then
A39: |.x1-x2.|<=vol(divset(D,k)) by INTEGRA1:def 5;
k in Seg(len D) by A28,FINSEQ_1:def 3;
then k in Seg(len (upper_volume(chi(A,A),D))) by
INTEGRA1:def 6;
then k in dom(upper_volume(chi(A,A),D)) by FINSEQ_1:def 3;
then
upper_volume(chi(A,A),D).k in rng(upper_volume(chi(A,A)
,D)) by FUNCT_1:def 3;
then
upper_volume(chi(A,A),D).k<=max rng(upper_volume(chi(A,
A),D)) by XXREAL_2:def 8;
then
A40: upper_volume(chi(A,A),D).k<=delta(T.m) by INTEGRA3:def 1;
upper_volume(chi(A,A),D).k=vol(divset( D,k)) by A28,
INTEGRA1:20;
then |.x1-x2.|<=delta(T.m) by A39,A40,XXREAL_0:2;
hence thesis by INTEGRA3:def 2;
end;
suppose
x1<x2;
then x1-x2<0 by XREAL_1:49;
then |.x1-x2.|=-(x1-x2) by ABSVALUE:def 1;
then
A41: |.x1-x2.|=x2-x1;
x2<=upper_bound divset(D,k) & x1>=lower_bound divset(D,k)
by A33,A34,INTEGRA2:1;
then |.x1-x2.|<=
upper_bound divset(D,k)-lower_bound divset(D,k) by A41,
XREAL_1:13;
then
A42: |.x1-x2.|<=vol(divset(D,k)) by INTEGRA1:def 5;
k in Seg(len D) by A28,FINSEQ_1:def 3;
then k in Seg(len (upper_volume(chi(A,A),D))) by
INTEGRA1:def 6;
then k in dom(upper_volume(chi(A,A),D)) by FINSEQ_1:def 3;
then
upper_volume(chi(A,A),D).k in rng(upper_volume(chi(A,A)
,D)) by FUNCT_1:def 3;
then
upper_volume(chi(A,A),D).k<=max rng(upper_volume(chi(A,
A),D)) by XXREAL_2:def 8;
then
A43: upper_volume(chi(A,A),D).k<=delta(T.m) by INTEGRA3:def 1;
upper_volume(chi(A,A),D).k=vol(divset( D,k)) by A28,
INTEGRA1:20;
then |.x1-x2.|<=delta(T.m) by A42,A43,XXREAL_0:2;
hence thesis by INTEGRA3:def 2;
end;
end;
hence thesis;
end;
delta(T).m = delta(D) by INTEGRA3:def 2
.=max rng(upper_volume(chi(A,A),D)) by INTEGRA3:def 1;
then delta(T).m-0>=0 by A30,A31,XXREAL_2:def 8;
then
A44: |.x1-x2.|<=|.delta(T).m-0.| by A37,ABSVALUE:def 1;
|.delta(T).m-0.|<s by A24,A26;
then
A45: |.x1-x2.|<s by A44,XXREAL_0:2;
A46: x1 in dom h by A33,PARTFUN1:def 2;
then g.x1=h.x1 by FUNCT_1:47;
then f.x1=h.x1 by A46,A32,FUNCT_1:47;
hence thesis by A23,A45,A46,A35,A32,A36;
end;
vol(divset(D,k)) >= 0 by INTEGRA1:9;
then (upper_bound rng(g|divset(D,k))-
lower_bound rng(g|divset(D,k)))*vol(divset(D,k
) ) <=r1*vol(divset(D,k)) by A29,INTEGRA4:24,XREAL_1:64;
then upper_bound rng(g|divset(D,k))*vol(divset(D,k))
-lower_bound rng(g|divset(D,k)
)*vol(divset(D,k))<=r1*vol(divset(D,k));
then upper_volume(g,D).k -
lower_bound rng(g|divset(D,k))*vol(divset(D,k))<=
r1*vol(divset(D,k)) by A28,INTEGRA1:def 6;
then upper_volume(g,D).k-lower_volume(g,D).k<=r1*vol(divset(D,k))
by A28,INTEGRA1:def 7;
hence thesis by A28,INTEGRA1:20;
end;
for k be Nat st k in Seg len D holds OSC.k<=(r1*VOL).k
proof
let k be Nat;
assume k in Seg len D;
then
A47: k in dom D by FINSEQ_1:def 3;
OSC.k = upper_volume(g,D).k-lower_volume(g,D).k by RVSUM_1:27;
then OSC.k<=r1*VOL.k by A27,A47;
hence thesis by RVSUM_1:45;
end;
then Sum OSC <= Sum(r1*VOL) by RVSUM_1:82;
then Sum OSC <= r1*Sum VOL by RVSUM_1:87;
then Sum UV-Sum LV <= r1*Sum VOL by RVSUM_1:90;
then upper_sum(g,D)-Sum LV <= r1*Sum VOL by INTEGRA1:def 8;
then upper_sum(g,D)-lower_sum(g,D) <= r1*Sum VOL by INTEGRA1:def 9;
then upper_sum(g,D)-lower_sum(g,D) <= r1*vol(A) by INTEGRA1:24;
then upper_sum(g,T).m-lower_sum(g,D)<=r1*vol(A) by INTEGRA2:def 2;
hence thesis by INTEGRA2:def 3;
end;
take n;
let m be Nat;
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
reconsider D=T.mm as Division of A;
assume n<=m;
then upper_sum(g,T).mm-lower_sum(g,T).mm <= r1*vol(A) by A25;
then
A48: upper_sum(g,T).m-lower_sum(g,T).m < r by A21,XXREAL_0:2;
upper_sum(g,D)>=lower_sum(g,D) by A11,INTEGRA1:28;
then upper_sum(g,T).mm>=lower_sum(g,D) by INTEGRA2:def 2;
then upper_sum(g,T).mm>=lower_sum(g,T).mm by INTEGRA2:def 3;
then
A49: upper_sum(g,T).m-lower_sum(g,T).m >= 0 by XREAL_1:48;
osc.m=upper_sum(g,T).m+(-lower_sum(g,T)).m by SEQ_1:7
.=upper_sum(g,T).m+-lower_sum(g,T).m by SEQ_1:10
.=upper_sum(g,T).m-lower_sum(g,T).m;
hence thesis by A48,A49,ABSVALUE:def 1;
end;
then osc is convergent by SEQ_2:def 6;
then
A50: lim osc = 0 by A14,SEQ_2:def 7;
upper_sum(g,T) is convergent & lower_sum(g,T) is convergent by A11,A13,
INTEGRA4:8,9;
hence thesis by A50,SEQ_2:12;
end;
then g is integrable by A11,INTEGRA4:12;
hence thesis;
end;
theorem Th12:
for f being PartFunc of REAL,REAL, D being Division of A st A c=
X & f is_differentiable_on X & (f`|X)|A is bounded holds lower_sum((f`|X)||A,D)
<= f.(upper_bound A)-f.(lower_bound A) & f.(upper_bound A)-f.(lower_bound A)
<=upper_sum((f`|X)||A,D)
proof
let f be PartFunc of REAL,REAL;
let D be Division of A;
assume that
A1: A c= X and
A2: f is_differentiable_on X and
A3: (f`|X)|A is bounded;
len D - 1 in NAT
proof
ex j being Nat st len D = 1 + j by NAT_1:10,14;
hence thesis by ORDINAL1:def 12;
end;
then reconsider k1 =len D - 1 as Element of NAT;
deffunc G(Nat)=In(f.(lower_bound divset(D,$1+1)),REAL);
deffunc F(Nat)
=In(f.(upper_bound divset(D,$1))-f.(lower_bound divset(D,$1)),REAL);
consider p being FinSequence of REAL such that
A4: len p = len D & for i be Nat st i in dom p holds p.i = F(i) from
FINSEQ_2:sch 1;
X c= dom f by A2,FDIFF_1:def 6;
then
A5: A c= dom f by A1,XBOOLE_1:1;
A6: for k st k in dom D holds ex r st r in divset(D,k) &
f.(upper_bound divset(D,k))
-f.(lower_bound divset(D,k))=diff(f,r)*vol(divset(D,k))
proof
let k;
assume
A7: k in dom D;
now
per cases;
suppose
A8: lower_bound divset(D,k)=upper_bound divset(D,k);
consider r such that
A9: r = upper_bound divset(D,k);
A10: r in divset(D,k)
proof
ex a,b st a<=b & a=lower_bound divset(D,k) &
b=upper_bound divset(D,k) by SEQ_4:11;
hence thesis by A9,INTEGRA2:1;
end;
upper_bound divset(D,k)-lower_bound divset(D,k)=0 by A8;
then vol(divset(D,k))=0 by INTEGRA1:def 5;
then diff(f,r)*vol(divset(D,k)) = 0;
hence thesis by A8,A10;
end;
suppose
A11: lower_bound divset(D,k)<>upper_bound divset(D,k);
ex r1,r2 st r1<=r2 & r1=lower_bound divset(D,k) &
r2=upper_bound divset( D,k) by SEQ_4:11;
then
A12: lower_bound divset(D,k) < upper_bound divset(D,k) by A11,XXREAL_0:1;
f|X is continuous by A2,FDIFF_1:25;
then f|A is continuous by A1,FCONT_1:16;
then
A13: f|divset(D,k) is continuous by A7,FCONT_1:16,INTEGRA1:8;
A14: divset(D,k)=[.lower_bound divset(D,k),upper_bound divset(D,k).]
by INTEGRA1:4;
then
A15: ].lower_bound divset(D,k),upper_bound divset(D,k).[ c= divset(D,k)
by XXREAL_1:25;
A16: divset(D,k) c= A by A7,INTEGRA1:8;
then ].lower_bound divset(D,k),upper_bound divset(D,k).[ c= A
by A15,XBOOLE_1:1;
then
f is_differentiable_on ].lower_bound divset(D,k),
upper_bound divset(D,k).[ by A1,A2,FDIFF_1:26,XBOOLE_1:1;
then consider r such that
A17: r in ].lower_bound divset(D,k),upper_bound divset(D,k).[ and
A18: diff(f,r)=(f.(upper_bound divset(D,k))-f.(lower_bound divset(D,k)))/ (
upper_bound divset(D,k)-lower_bound divset(D,k)) by A5,A16,A13,A12,A14,
ROLLE:3,XBOOLE_1:1;
upper_bound divset(D,k)-lower_bound divset(D,k) > 0 by A12,XREAL_1:50;
then
diff(f,r)*(upper_bound divset(D,k)-lower_bound divset(D,k))
=f.(upper_bound divset(D,k))-
f.(lower_bound divset(D,k)) by A18,XCMPLX_1:87;
then
diff(f,r)*vol(divset(D,k)) =
f.(upper_bound divset(D,k))-f.(lower_bound divset(D,k
)) by INTEGRA1:def 5;
hence thesis by A15,A17;
end;
end;
hence thesis;
end;
A19: dom p = Seg len D by A4,FINSEQ_1:def 3;
A20: for i st i in Seg k1 holds upper_bound divset(D,i)
=lower_bound divset(D,i+1)
proof
let i;
assume
A21: i in Seg k1;
then i <= k1 by FINSEQ_1:1;
then
A22: i+1 <= k1+1 by XREAL_1:7;
1 <= i by A21,FINSEQ_1:1;
then 1+0 <= i+1 by XREAL_1:7;
then i+1 in Seg(len D) by A22,FINSEQ_1:1;
then
A23: i+1 in dom D by FINSEQ_1:def 3;
k1 + 1 = len D;
then k1 <= len D by NAT_1:11;
then Seg k1 c= Seg len D by FINSEQ_1:5;
then i in Seg (len D) by A21;
then
A24: i in dom D by FINSEQ_1:def 3;
A25: i+1-1=i;
now
per cases;
suppose
A26: i=1;
then upper_bound divset(D,i) = D.i by A24,INTEGRA1:def 4;
hence thesis by A23,A25,A26,INTEGRA1:def 4;
end;
suppose
A27: i<>1;
i >= 1 by A21,FINSEQ_1:1;
then i+1>=1+1 by XREAL_1:6;
then
A28: i+1 <> 1;
upper_bound divset(D,i) = D.i by A24,A27,INTEGRA1:def 4;
hence thesis by A23,A25,A28,INTEGRA1:def 4;
end;
end;
hence thesis;
end;
consider s2 being FinSequence of REAL such that
A29: len s2 = k1 & for i be Nat st i in dom s2 holds s2.i = G(i) from
FINSEQ_2:sch 1;
A30: for k st k in dom D holds rng(((f`|X)||A)|divset(D,k)) is real-bounded
proof
dom(f`|X) = X by A2,FDIFF_1:def 7;
then reconsider g=f`|X as PartFunc of X,REAL by RELSET_1:5;
let k;
assume k in dom D;
consider r1 be Real such that
A31: for x being object st x in A /\ dom(f`|X) holds (f`|X).x <= r1 by A3,
RFUNCT_1:70;
consider r2 be Real such that
A32: for x being object st x in A /\ dom(f`|X) holds (f`|X).x >= r2 by A3,
RFUNCT_1:71;
A33: dom((f`|X)|A) =dom(f`|X) /\ A by RELAT_1:61;
for x being object st x in A /\ dom((f`|X)||A) holds ((f`|X)||A).x>=r2
proof
let x be object;
A34: A /\ (A /\ dom(f`|X)) = (A /\ A) /\ dom(f`|X) by XBOOLE_1:16
.= A /\ dom(f`|X);
reconsider y=g.x as Real;
assume
A35: x in A /\ dom((f`|X)||A);
then y >= r2 by A32,A33,A34;
hence thesis by A33,A35,A34,FUNCT_1:47;
end;
then (f`|X)||A|A is bounded_below by RFUNCT_1:71;
then
A36: rng(((f`|X)||A)|divset(D,k)) is bounded_below by INTEGRA4:19;
for x being object st x in A /\ dom((f`|X)||A) holds ((f`|X)||A).x<=r1
proof
let x be object;
A37: A /\ (A /\ dom(f`|X)) = (A /\ A) /\ dom(f`|X) by XBOOLE_1:16
.= A /\ dom(f`|X);
reconsider y=g.x as Real;
assume
A38: x in A /\ dom((f`|X)||A);
then y <= r1 by A31,A33,A37;
hence thesis by A33,A38,A37,FUNCT_1:47;
end;
then (f`|X)||A|A is bounded_above by RFUNCT_1:70;
then rng(((f`|X)||A)|divset(D,k)) is bounded_above by INTEGRA4:18;
hence thesis by A36;
end;
deffunc F1(Nat)=In(f.(upper_bound divset(D,$1)),REAL);
consider s1 being FinSequence of REAL such that
A39: len s1 = k1 & for i be Nat st i in dom s1 holds s1.i = F1(i) from
FINSEQ_2:sch 1;
A40: dom s2 = Seg k1 by A29,FINSEQ_1:def 3;
reconsider flb = f.(lower_bound A), fub = f.(upper_bound A)
as Element of REAL by XREAL_0:def 1;
len (s1^<*f.(upper_bound A)*>) = len (<*f.(lower_bound A)*>^s2) &
len (s1^<*f.(upper_bound A)*>
) = len p & for i st i in dom (s1^<*fub*>)
holds p.i=((s1^<*fub*>)/.i) - ((<*flb*>^s2)/.i)
proof
dom(<*f.(upper_bound A)*>)=Seg 1 by FINSEQ_1:def 8;
then len(<*f.(upper_bound A)*>)=1 by FINSEQ_1:def 3;
then
A41: len(s1^<*f.(upper_bound A)*>)=k1+1 by A39,FINSEQ_1:22;
dom(<*f.(lower_bound A)*>)=Seg 1 by FINSEQ_1:def 8;
then len(<*f.(lower_bound A)*>)=1 by FINSEQ_1:def 3;
hence
A42: len (s1^<*f.(upper_bound A)*>) = len (<*f.(lower_bound A)*>^s2)
by A29,A41,FINSEQ_1:22;
thus len (s1^<*f.(upper_bound A)*>) = len p by A4,A41;
let i;
assume
A43: i in dom (s1^<*fub*>);
then
A44: (s1^<*fub*>)/.i=(s1^<*f.(upper_bound A)*>).i
by PARTFUN1:def 6;
i in Seg(len (s1^<*f.(upper_bound A)*>)) by A43,FINSEQ_1:def 3;
then i in dom (<*f.(lower_bound A)*>^s2) by A42,FINSEQ_1:def 3;
then
A45: (<*flb*>^s2)/.i=(<*flb*>^s2).i
by PARTFUN1:def 6;
A46: len D = 1 or len D is non trivial by NAT_2:def 1;
now
per cases by A46,NAT_2:29;
suppose
A47: len D = 1;
then
A48: i in Seg 1 by A41,A43,FINSEQ_1:def 3;
then
A49: i = 1 by FINSEQ_1:2,TARSKI:def 1;
s1={} by A39,A47;
then s1^<*f.(upper_bound A)*> = <*f.(upper_bound A)*> by FINSEQ_1:34;
then
A50: (s1^<*fub*>)/.i=f.(upper_bound A)
by A44,A49;
A51: i in dom D by A47,A48,FINSEQ_1:def 3;
s2={} by A29,A47;
then <*f.(lower_bound A)*>^s2 = <*f.(lower_bound A)*> by FINSEQ_1:34;
then
A52: (<*flb*>^s2)/.i=f.(lower_bound A)
by A45,A49;
D.i=upper_bound A by A47,A49,INTEGRA1:def 2;
then
A53: upper_bound divset(D,i)=upper_bound A by A49,A51,INTEGRA1:def 4;
p.i = F(i) by A4,A19,A47,A48
.=f.(upper_bound divset(D,i))-f.(lower_bound divset(D,i));
hence thesis by A49,A51,A50,A52,A53,INTEGRA1:def 4;
end;
suppose
A54: len D >= 2;
1 = 2 - 1;
then
A55: k1>=1 by A54,XREAL_1:9;
now
per cases;
suppose
A56: i=1;
then
A57: i in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then i in dom <*f.(lower_bound A)*> by FINSEQ_1:def 8;
then (<*f.(lower_bound A)*>^s2).i=<*f.(lower_bound A)*>.i
by FINSEQ_1:def 7;
then
A58: (<*f.(lower_bound A)*>^s2).i = f.(lower_bound A)
by A56;
Seg 1 c= Seg k1 by A55,FINSEQ_1:5;
then i in Seg k1 by A57;
then
A59: i in dom s1 by A39,FINSEQ_1:def 3;
then (s1^<*f.(upper_bound A)*>).i=s1.i by FINSEQ_1:def 7
.= F1(i) by A39,A59;
then
A60: (s1^<*f.(upper_bound A)*>).i=f.(upper_bound divset(D,i));
A61: i in Seg 2 by A56,FINSEQ_1:2,TARSKI:def 2;
A62: Seg 2 c= Seg len D by A54,FINSEQ_1:5;
then i in Seg(len D) by A61;
then
A63: i in dom D by FINSEQ_1:def 3;
p.i= F(i) by A4,A19,A62,A61
.= f.(upper_bound divset(D,i))-f.(lower_bound divset(D,i));
hence thesis by A44,A45,A56,A63,A60,A58,INTEGRA1:def 4;
end;
suppose
A64: i=len D;
then i-len s1 in Seg 1 by A39,FINSEQ_1:2,TARSKI:def 1;
then
A65: i-len s1 in dom <*f.(upper_bound A)*> by FINSEQ_1:def 8;
i=i-len s1 + len s1;
then (s1^<*f.(upper_bound A)*>).i=<*f.(upper_bound A)*>.(i-len s1)
by A65,FINSEQ_1:def 7;
then
A66: (s1^<*fub*>)/.i=f.(upper_bound A)
by A39,A44,A64;
A67: len <*f.(lower_bound A)*> = 1 by FINSEQ_1:40;
A68: i<>1 by A54,A64;
i in Seg(len D) by A64,FINSEQ_1:3;
then
A69: i in dom D by FINSEQ_1:def 3;
p.i = F(i) by A4,A19,A64,FINSEQ_1:3
.=f.(upper_bound divset(D,i))-f.(lower_bound divset(D,i));
then p.i=f.(upper_bound divset(D,i))-f.(D.(i-1))
by A69,A68,INTEGRA1:def 4;
then
A70: p.i=f.(D.i)-f.(D.(i-1)) by A69,A68,INTEGRA1:def 4;
i-1<>0 by A54,A64;
then
A71: i-1 in Seg k1 by A64,FINSEQ_1:3;
then reconsider i1 = i-1 as Nat;
A72: len <*f.(lower_bound A)*> + (i - len <*f.(lower_bound A)*>) = i &
i-len <*f.
(lower_bound A)*> in dom s2 by A29,A67,FINSEQ_1:def 3,A71;
then (<*f.(lower_bound A)*>^s2).i =
s2.(i1) by FINSEQ_1:def 7,A67
.= G(i1) by A29,A67,A72;
then (<*f.(lower_bound A)*>^s2).i
= f.(lower_bound divset(D,i));
then (<*f.(lower_bound A)*>^s2).i = f.(D.(i-1))
by A69,A68,INTEGRA1:def 4;
hence thesis by A45,A64,A66,A70,INTEGRA1:def 2;
end;
suppose
A73: i<>1 & i<>len D;
len s1+len <*f.(upper_bound A)*> = k1+1 by A39,FINSEQ_1:39;
then
A74: i in Seg(len D) by A43,FINSEQ_1:def 7;
A75: i in dom s1 & i in Seg k1 & i-1 in Seg k1 & i-1+1=i & i-len
<*f.(lower_bound A)*> in dom s2
proof
i <> 0 by A74,FINSEQ_1:1;
then i is non trivial by A73,NAT_2:def 1;
then i >= 1+1 by NAT_2:29;
then
A76: i-1 >= 1 by XREAL_1:19;
A77: 1 <= i by A74,FINSEQ_1:1;
i <= len D by A74,FINSEQ_1:1;
then
A78: i < k1 + 1 by A73,XXREAL_0:1;
then
A79: i <= k1 by NAT_1:13;
then i in Seg(len s1) by A39,A77,FINSEQ_1:1;
hence i in dom s1 by FINSEQ_1:def 3;
thus i in Seg k1 by A77,A79,FINSEQ_1:1;
i <= k1 by A78,NAT_1:13;
then i-1 <= k1-1 by XREAL_1:9;
then
A80: i-1+0 <= k1-1+1 by XREAL_1:7;
ex j being Nat st i = 1 + j by A77,NAT_1:10;
hence i-1 in Seg k1 by A76,A80,FINSEQ_1:1;
then
A81: i-len<*f.(lower_bound A)*> in Seg(len s2) by A29,FINSEQ_1:39;
thus i-1+1=i;
thus thesis by A81,FINSEQ_1:def 3;
end;
then
A82: i-len<*f.(lower_bound A)*> in Seg(len s2) by FINSEQ_1:def 3;
then i-len<*f.(lower_bound A)*><=len s2 by FINSEQ_1:1;
then
A83: i<=len<*f.(lower_bound A)*>+len s2 by XREAL_1:20;
i >= 1 by A74, FINSEQ_1:1;
then reconsider i1=i-1 as Element of NAT by INT_1:5;
1 <= i-len<*f.(lower_bound A)*> by A82,FINSEQ_1:1;
then len<*f.(lower_bound A)*>+1<=i by XREAL_1:19;
then (<*f.(lower_bound A)*>^s2).i=s2.(i-len<*f.(lower_bound A)*>)
by A83,FINSEQ_1:23;
then (<*f.(lower_bound A)*>^s2).i=s2.(i-1) by FINSEQ_1:39
.= G(i1) by A29,A40,A75;
then
A84: (<*f.(lower_bound A)*>^s2).i= f.(lower_bound divset(D,i));
(s1^<*f.(upper_bound A)*>).i = s1.i by A75,FINSEQ_1:def 7
.= F1(i) by A39,A75;
then
A85: (s1^<*f.(upper_bound A)*>).i = f.(upper_bound divset(D,i));
thus p.i=F(i) by A4,A19,A74
.= ((s1^<*fub*>)/.i) - ((<*flb*>^s2)/.i)
by A44,A45,A84,A85;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then Sum p=Sum(s1^<*f.(upper_bound A)*>)-Sum(<*f.(lower_bound A)*>^s2)
by INTEGRA1:22;
then Sum p=Sum s1 + f.(upper_bound A) -Sum(<*f.(lower_bound A)*>^s2)
by RVSUM_1:74;
then
A86: Sum p=Sum s1 + f.(upper_bound A) - (f.(lower_bound A) + Sum s2)
by RVSUM_1:76;
A87: dom s1 = Seg k1 by A39,FINSEQ_1:def 3;
A88: dom s1 = Seg k1 by A39,FINSEQ_1:def 3;
for i being Nat st i in dom s1 holds s1.i = s2.i
proof
let i be Nat;
assume
A89: i in dom s1;
then s1.i = F1(i) by A39
.=f.(upper_bound divset(D,i));
then s1.i=f.(lower_bound divset(D,i+1)) by A20,A87,A89
.= G(i);
hence thesis by A88,A29,A40,A89;
end;
then
A90: s1=s2 by A39,A29,FINSEQ_2:9;
A91: for k,r st k in dom D & r in divset(D,k) holds diff(f,r) in rng (((f`|X
)||A)|divset(D,k))
proof
A92: dom((f`|X)|A) = dom(f`|X) /\ A by RELAT_1:61
.= X /\ A by A2,FDIFF_1:def 7
.= A by A1,XBOOLE_1:28;
let k,r;
assume that
A93: k in dom D and
A94: r in divset(D,k);
A95: divset(D,k) c= A by A93,INTEGRA1:8;
then divset(D,k) c= X by A1,XBOOLE_1:1;
then (f`|X).r = diff(f,r) by A2,A94,FDIFF_1:def 7;
then
A96: diff(f,r)= ((f`|X)||A).r by A94,A95,A92,FUNCT_1:47;
A97: dom(((f`|X)||A)|divset(D,k))= A /\ divset(D,k) by A92,RELAT_1:61
.=divset(D,k) by A93,INTEGRA1:8,XBOOLE_1:28;
then ((f`|X)||A)|divset(D,k).r in rng(((f`|X)||A)|divset(D,k)) by A94,
FUNCT_1:def 3;
hence thesis by A94,A96,A97,FUNCT_1:47;
end;
A98: for k st k in dom D
holds f.(upper_bound divset(D,k))-f.(lower_bound divset(D,k))<=(
upper_volume((f`|X)||A,D)).k
proof
let k;
A99: vol(divset(D,k)) >= 0 by INTEGRA1:9;
assume
A100: k in dom D;
then consider r such that
A101: r in divset(D,k) and
A102: f.(upper_bound divset(D,k))-f.(lower_bound divset(D,k))
=diff(f,r)*vol(divset(D,k
)) by A6;
A103: rng(((f`|X)||A)|divset(D,k)) is real-bounded by A30,A100;
diff(f,r) in rng(((f`|X)||A)|divset(D,k)) by A91,A100,A101;
then diff(f,r) <= upper_bound rng(((f`|X)||A)|divset(D,k))
by A103,SEQ_4:def 1;
then diff(f,r)*vol(divset(D,k)) <=
(upper_bound rng(((f`|X)||A)|divset(D,k)))*vol(
divset(D,k)) by A99,XREAL_1:64;
hence thesis by A100,A102,INTEGRA1:def 6;
end;
A104: f.(upper_bound A)-f.(lower_bound A)<=upper_sum((f`|X)||A,D)
proof
len upper_volume((f`|X)||A,D)=len D by INTEGRA1:def 6;
then reconsider
q=(upper_volume((f`|X)||A,D)) as Element of (len D)-tuples_on
REAL by FINSEQ_2:92;
A105: for k be Nat st k in Seg len D holds p.k <= (upper_volume((f`|X)||A,
D)).k
proof
let k be Nat;
assume
A106: k in Seg len D;
A107: f.(upper_bound divset(D,k))-f.(lower_bound divset(D,k))
=F(k)
.=p.k by A4,A19,A106;
k in dom D by FINSEQ_1:def 3,A106;
hence thesis by A98,A107;
end;
reconsider p as Element of (len D)-tuples_on REAL by A4,FINSEQ_2:92;
Sum p<=Sum q by A105,RVSUM_1:82;
hence thesis by A90,A86,INTEGRA1:def 8;
end;
A108: for k st k in dom D
holds f.(upper_bound divset(D,k))-f.(lower_bound divset(D,k))>=(
lower_volume((f`|X)||A,D)).k
proof
let k;
assume
A109: k in dom D;
then
A110: vol(divset(D,k)) >= 0 & (lower_bound rng(((f`|X)||A)|divset(D,k)))*vol(
divset(D,k)) =(lower_volume((f`|X)||A,D)).k by INTEGRA1:9,def 7;
A111: rng(((f`|X)||A)|divset(D,k)) is real-bounded by A30,A109;
consider r such that
A112: r in divset(D,k) and
A113: f.(upper_bound divset(D,k))-f.(lower_bound divset(D,k))
=diff(f,r)*vol(divset(D,k
)) by A6,A109;
diff(f,r) in rng(((f`|X)||A)|divset(D,k)) by A91,A109,A112;
then diff(f,r) >= lower_bound rng(((f`|X)||A)|divset(D,k))
by A111,SEQ_4:def 2;
hence thesis by A113,A110,XREAL_1:64;
end;
f.(upper_bound A)-f.(lower_bound A)>=lower_sum((f`|X)||A,D)
proof
len lower_volume((f`|X)||A,D)=len D by INTEGRA1:def 7;
then reconsider
q=(lower_volume((f`|X)||A,D)) as Element of (len D)-tuples_on
REAL by FINSEQ_2:92;
A114: for k be Nat st k in Seg len D holds p.k >= (lower_volume((f`|X)||A,
D)).k
proof
let k be Nat;
assume
A115: k in Seg len D;
A116: f.(upper_bound divset(D,k))-f.(lower_bound divset(D,k))
= F(k)
.=p.k by A4,A19,A115;
k in dom D by FINSEQ_1:def 3,A115;
hence thesis by A108,A116;
end;
reconsider p as Element of (len D)-tuples_on REAL by A4,FINSEQ_2:92;
Sum q<=Sum p by A114,RVSUM_1:82;
hence thesis by A90,A86,INTEGRA1:def 9;
end;
hence thesis by A104;
end;
::$N Fundamental Theorem of Integral Calculus
::$L https://en.wikipedia.org/wiki/Fundamental_theorem_of_calculus Fundamental Theorem of Integral Calculus
theorem Th13:
for f being PartFunc of REAL,REAL st A c= X & f
is_differentiable_on X & f`|X is_integrable_on A & (f`|X)|A is bounded holds
integral(f`|X,A) = f.(upper_bound A)-f.(lower_bound A)
proof
let f be PartFunc of REAL,REAL;
assume that
A1: A c= X & f is_differentiable_on X and
A2: f`|X is_integrable_on A and
A3: (f`|X)|A is bounded;
(f`|X)||A is integrable by A2;
then
A4: upper_integral((f`|X)||A)=lower_integral((f`|X)||A) by INTEGRA1:def 16;
A5: for r be Real st r in rng upper_sum_set((f`|X)||A)
holds f.(upper_bound
A)-f.(lower_bound A) <= r
proof
let r be Real;
assume r in rng upper_sum_set((f`|X)||A);
then consider D being Element of divs A such that
A6: D in dom upper_sum_set((f`|X)||A) & r=(upper_sum_set((f`|X)||A)).
D by PARTFUN1:3;
reconsider D as Division of A by INTEGRA1:def 3;
r=upper_sum((f`|X)||A,D) by A6,INTEGRA1:def 10;
hence thesis by A1,A3,Th12;
end;
f.(upper_bound A)-f.(lower_bound A) <=
lower_bound rng upper_sum_set((f`|X)||A) by A5,SEQ_4:43;
then
A7: upper_integral((f`|X)||A) >= f.(upper_bound A)-f.(lower_bound A)
by INTEGRA1:def 14;
A8: for r be Real st r in rng lower_sum_set((f`|X)||A) holds r <= f.
(upper_bound A)-f.(lower_bound A)
proof
let r be Real;
assume r in rng lower_sum_set((f`|X)||A);
then consider D being Element of divs A such that
A9: D in dom lower_sum_set((f`|X)||A) & r=(lower_sum_set((f`|X)||A)).
D by PARTFUN1:3;
reconsider D as Division of A by INTEGRA1:def 3;
r=lower_sum((f`|X)||A,D) by A9,INTEGRA1:def 11;
hence thesis by A1,A3,Th12;
end;
upper_bound rng lower_sum_set((f`|X)||A) <=
f.(upper_bound A)-f.(lower_bound A) by A8,SEQ_4:45;
then upper_integral((f`|X)||A) <=
f.(upper_bound A)-f.(lower_bound A) by A4,INTEGRA1:def 15;
then upper_integral((f`|X)||A) =
f.(upper_bound A)-f.(lower_bound A) by A7,XXREAL_0:1;
hence thesis by INTEGRA1:def 17;
end;
theorem Th14:
for f being PartFunc of REAL,REAL st f|A is non-decreasing & A
c= dom f holds rng (f|A) is real-bounded
proof
let f be PartFunc of REAL,REAL;
assume that
A1: f|A is non-decreasing and
A2: A c= dom f;
A3: dom(f|A)=dom f /\ A by RELAT_1:61
.= A by A2,XBOOLE_1:28;
f.(lower_bound A) is LowerBound of rng (f|A)
proof
lower_bound A <= upper_bound A by SEQ_4:11;
then lower_bound A in dom(f|A) by A3,INTEGRA2:1;
then
A4: lower_bound A in dom f /\ A by RELAT_1:61;
let y be ExtReal;
assume y in rng (f|A);
then consider x being Element of REAL such that
A5: x in dom(f|A) and
A6: y=(f|A).x by PARTFUN1:3;
A7: x in dom f /\ A by A5,RELAT_1:61;
y=f.x & x >= lower_bound A by A5,A6,FUNCT_1:47,INTEGRA2:1;
hence thesis by A1,A7,A4,RFUNCT_2:24;
end;
then
A8: rng(f|A) is bounded_below;
f.(upper_bound A) is UpperBound of rng (f|A)
proof
lower_bound A <= upper_bound A by SEQ_4:11;
then upper_bound A in dom(f|A) by A3,INTEGRA2:1;
then
A9: upper_bound A in dom f /\ A by RELAT_1:61;
let y be ExtReal;
assume y in rng (f|A);
then consider x being Element of REAL such that
A10: x in dom(f|A) and
A11: y=(f|A).x by PARTFUN1:3;
A12: x in dom f /\ A by A10,RELAT_1:61;
y=f.x & x <= upper_bound A by A10,A11,FUNCT_1:47,INTEGRA2:1;
hence thesis by A1,A12,A9,RFUNCT_2:24;
end;
then rng(f|A) is bounded_above;
hence thesis by A8;
end;
theorem Th15:
for f being PartFunc of REAL,REAL st f|A is non-decreasing & A
c= dom f holds lower_bound rng (f|A) = f.(lower_bound A) &
upper_bound rng (f|A) = f.(upper_bound A)
proof
let f be PartFunc of REAL,REAL;
assume that
A1: f|A is non-decreasing and
A2: A c= dom f;
A3: dom(f|A) = dom f /\ A by RELAT_1:61
.= A by A2,XBOOLE_1:28;
then
A4: rng(f|A) <> {} by RELAT_1:42;
A5: lower_bound A <= upper_bound A by SEQ_4:11;
then
A6: upper_bound A in dom(f|A) by A3,INTEGRA2:1;
then
A7: upper_bound A in dom f /\ A by RELAT_1:61;
A8: for x be Real st x in rng(f|A) holds x <= f.(upper_bound A)
proof
let y be Real;
assume y in rng (f|A);
then consider x being Element of REAL such that
A9: x in dom (f|A) and
A10: y=(f|A).x by PARTFUN1:3;
x in dom f /\ A & upper_bound A >= x by A9,INTEGRA2:1,RELAT_1:61;
then f.(upper_bound A) >= f.x by A1,A7,RFUNCT_2:24;
hence thesis by A9,A10,FUNCT_1:47;
end;
A11: lower_bound A in dom(f|A) by A3,A5,INTEGRA2:1;
then
A12: lower_bound A in dom f /\ A by RELAT_1:61;
A13: for y be Real st y in rng(f|A) holds y >= f.(lower_bound A)
proof
let y be Real;
assume y in rng (f|A);
then consider x being Element of REAL such that
A14: x in dom (f|A) and
A15: y=(f|A).x by PARTFUN1:3;
x in dom f /\ A & lower_bound A <= x by A14,INTEGRA2:1,RELAT_1:61;
then f.(lower_bound A) <= f.x by A1,A12,RFUNCT_2:24;
hence thesis by A14,A15,FUNCT_1:47;
end;
for a be Real st for x be Real st x in rng(f|A) holds x>=
a holds f.(lower_bound A)>=a
proof
let a be Real;
assume
A16: for x be Real st x in rng(f|A) holds x>=a;
f.(lower_bound A) = (f|A).(lower_bound A) &
(f|A).(lower_bound A) in rng(f|A) by A11,FUNCT_1:47,def 3;
hence thesis by A16;
end;
hence lower_bound rng(f|A)=f.(lower_bound A) by A4,A13,SEQ_4:44;
for a be Real st for x be Real st x in rng(f|A) holds x<=
a holds f.(upper_bound A)<=a
proof
let a be Real;
assume
A17: for x be Real st x in rng(f|A) holds x<=a;
f.(upper_bound A) = (f|A).(upper_bound A) &
(f|A).(upper_bound A) in rng(f|A) by A6,FUNCT_1:47,def 3;
hence thesis by A17;
end;
hence thesis by A4,A8,SEQ_4:46;
end;
Lm1: for f being PartFunc of REAL,REAL st f|A is non-decreasing & A c= dom f
holds f is_integrable_on A
proof
let f be PartFunc of REAL,REAL;
assume that
A1: f|A is non-decreasing and
A2: A c= dom f;
A3: for D being Division of A, k st k in dom D holds 0 <= (upper_volume(f||A
,D)).k-(lower_volume(f||A,D)).k & (upper_volume(f||A,D)).k-(lower_volume(f||A,D
)).k <= (f.(upper_bound divset(D,k))-f.(lower_bound divset(D,k)))*delta(D)
proof
let D be Division of A;
let k;
assume
A4: k in dom D;
then
A5: (upper_volume(f||A,D)).k=
(upper_bound (rng((f||A)|divset(D,k))))*vol( divset(D
, k)) & (lower_volume(f||A,D)).k=
(lower_bound (rng((f||A)|divset(D,k))))*vol(divset(D,k
)) by INTEGRA1:def 6,def 7;
k in Seg len D by A4,FINSEQ_1:def 3;
then k in Seg len upper_volume(chi(A,A),D) by INTEGRA1:def 6;
then
A6: k in dom upper_volume(chi(A,A),D) by FINSEQ_1:def 3;
vol(divset(D,k))=upper_volume(chi(A,A),D).k by A4,INTEGRA1:20;
then vol(divset(D,k)) in rng upper_volume(chi(A,A),D) by A6,FUNCT_1:def 3;
then vol(divset(D,k)) <= max rng upper_volume(chi(A,A),D) by XXREAL_2:def 8
;
then
A7: vol(divset(D,k)) <= delta(D) by INTEGRA3:def 1;
A8: divset(D,k) c= A by A4,INTEGRA1:8;
then
A9: divset(D,k) c= dom f by A2,XBOOLE_1:1;
f|divset(D,k) is non-decreasing by A1,A4,INTEGRA1:8,RFUNCT_2:30;
then
A10: lower_bound rng (f|divset(D,k)) = f.(lower_bound divset(D,k)) &
upper_bound rng (f|divset(D,k)
) = f. (upper_bound divset(D,k)) by A9,Th15;
dom(f|divset(D,k)) = dom f /\ divset(D,k) by RELAT_1:61
.= divset(D,k) by A2,A8,XBOOLE_1:1,28;
then
A11: rng(f|divset(D,k)) <> {} by RELAT_1:42;
A12: rng (f|divset(D,k))=rng ((f||A)|divset(D,k)) by A8,FUNCT_1:51;
rng(f|A) is real-bounded by A1,A2,Th14;
then rng(f|divset(D,k)) is real-bounded by A12,RELAT_1:70,XXREAL_2:45;
then
A13: f.(upper_bound divset(D,k)) - f.(lower_bound divset(D,k)) >= 0
by A10,A11,SEQ_4:11,XREAL_1:48;
vol(divset(D,k)) >= 0 by INTEGRA1:9;
then
0*vol(divset(D,k)) <=
(f.(upper_bound divset(D,k)) - f.(lower_bound divset(D,k)))*vol
(divset(D,k)) by A13;
hence 0<=(upper_volume(f||A,D)).k-(lower_volume(f||A,D)).k by A10,A5,A12;
(upper_volume(f||A,D)).k-(lower_volume(f||A,D)).k
=(f.(upper_bound divset(D,k
))-f.(lower_bound divset(D,k)))*vol(divset(D,k)) by A10,A5,A12;
hence thesis by A13,A7,XREAL_1:64;
end;
A14: for D being Division of A holds upper_sum(f||A,D)-lower_sum(f||A,D) <=
delta(D)*(f.(upper_bound A)-f.(lower_bound A)) &
upper_sum(f||A,D)-lower_sum(f||A,D) >= 0
proof
let D be Division of A;
deffunc F2(Nat)=In(f.(upper_bound divset(D,$1)),REAL);
consider F1 being FinSequence of REAL such that
A15: len F1 = len D & for i be Nat st i in dom F1 holds F1.i = F2(i)
from FINSEQ_2:sch 1;
len D - 1 in NAT
proof
ex j being Nat st len D = 1 + j by NAT_1:10,14;
hence thesis by ORDINAL1:def 12;
end;
then consider k1 being Element of NAT such that
A16: k1=len D - 1;
deffunc G(Nat)=In(f.(lower_bound divset(D,$1)),REAL);
consider F2 being FinSequence of REAL such that
A17: len F2 = len D & for i be Nat st i in dom F2 holds F2.i = G(i)
from FINSEQ_2:sch 1;
deffunc G1(Nat)=In(f.(upper_bound divset(D,$1)),REAL);
A18: dom F2 = Seg len D by A17,FINSEQ_1:def 3;
consider F being FinSequence of REAL such that
A19: len F = k1 & for i be Nat st i in dom F holds F.i = G1(i) from
FINSEQ_2:sch 1;
A20: dom F = Seg k1 by A19,FINSEQ_1:def 3;
A21: for i be Nat st 1<=i & i<=len F2 holds F2.i=(<*f.(lower_bound A)*>^F).i
proof
let i be Nat;
assume that
A22: 1<=i and
A23: i<=len F2;
per cases;
suppose
A24: i=1;
A25: i in Seg len D by A17,A22,A23,FINSEQ_1:1;
then
A26: i in dom D by FINSEQ_1:def 3;
F2.i = G(i) by A17,A18,A25
.= f.(lower_bound divset(D,i))
.=f.(lower_bound A) by A24,A26,INTEGRA1:def 4;
hence thesis by A24,FINSEQ_1:41;
end;
suppose
A27: i<>1;
then
A28: i > 1 by A22,XXREAL_0:1;
then 1+1<=i by NAT_1:13;
then
A29: len <*f.(lower_bound A)*>+1<=i by FINSEQ_1:39;
A30: i in Seg len D by A17,A22,A23,FINSEQ_1:1;
then
A31: i in dom D by FINSEQ_1:def 3;
then reconsider k2=i-1 as Element of NAT by A27,INTEGRA1:7;
1+1 <= k2+1 by A28,NAT_1:13;
then
A32: 1 <= k2 by XREAL_1:19;
k2+1 <=len F2 by A23;
then
A33: k2 <= len D - 1 by A17,XREAL_1:19;
then
A34: k2 in Seg k1 by A16,A32,FINSEQ_1:1;
A35: upper_bound divset(D,k2)=D.(i-1)
proof
len D <= len D+1 by NAT_1:13;
then len D - 1 <= len D by XREAL_1:20;
then k2 <= len D by A33,XXREAL_0:2;
then k2 in Seg len D by A32,FINSEQ_1:1;
then
A36: k2 in dom D by FINSEQ_1:def 3;
per cases;
suppose
k2=1;
hence thesis by A36,INTEGRA1:def 4;
end;
suppose
k2<>1;
hence thesis by A36,INTEGRA1:def 4;
end;
end;
len F2= 1+(len D-1) by A17
.= len <*f.(lower_bound A)*>+len F by A16,A19,FINSEQ_1:39;
then
A37: (<*f.(lower_bound A)*>^F).i = F.(i-len<*f.(lower_bound A)*>)
by A23,A29,FINSEQ_1:23
.=F.(i-1) by FINSEQ_1:39;
F2.i = G(i)
by A17,A18,A30
.= f.(lower_bound divset(D,i))
.= f.(upper_bound divset(D,k2)) by A27,A31,INTEGRA1:def 4,A35
.= G1(k2);
hence thesis by A19,A20,A37,A34;
end;
end;
len (<*f.(lower_bound A)*>^F) = len <*f.(lower_bound A)*> + len F
by FINSEQ_1:22
.= 1 + (len D - 1) by A16,A19,FINSEQ_1:39
.= len D;
then
A38: F2=<*f.(lower_bound A)*>^F by A17,A21,FINSEQ_1:14;
len upper_volume(f||A,D) = len D & len lower_volume(f||A,D) = len D
by INTEGRA1:def 6,def 7;
then
A39: Sum(upper_volume(f||A,D)-lower_volume(f||A,D)) =Sum upper_volume(f||A
,D)-Sum lower_volume(f||A,D) by Th2
.=upper_sum(f||A,D)-Sum lower_volume(f||A,D) by INTEGRA1:def 8
.=upper_sum(f||A,D)-lower_sum(f||A,D) by INTEGRA1:def 9;
A40: dom F1 = Seg len D by A15,FINSEQ_1:def 3;
A41: for i be Nat st 1<=i & i<=len F1 holds F1.i=(F^<*f.(upper_bound A)*>).i
proof
let i be Nat;
assume that
A42: 1<=i and
A43: i<=len F1;
now
per cases;
suppose
i <= len F;
then
A44: i in Seg len F by A42,FINSEQ_1:1;
then
A45: F.i = G1(i) by A19,A20
.= f.(upper_bound divset(D,i));
A46: i in dom F by A19,A20,A44;
i in Seg len F1 by A42,A43,FINSEQ_1:1;
then F1.i = F2(i) by A15,A40
.= f.(upper_bound divset(D,i));
hence thesis by A46,A45,FINSEQ_1:def 7;
end;
suppose
i > len F;
then
A47: i >= len F + 1 by NAT_1:13;
then
A48: i =len F + 1 by A15,A16,A19,A43,XXREAL_0:1;
A49: i in Seg len F1 by A42,A43,FINSEQ_1:1;
then
A50: i in dom D by A15,FINSEQ_1:def 3;
A51: upper_bound divset(D,i) = D.i
proof
now
per cases;
suppose
i=1;
hence thesis by A50,INTEGRA1:def 4;
end;
suppose
i<>1;
hence thesis by A50,INTEGRA1:def 4;
end;
end;
hence thesis;
end;
F1.i = F2(i) by A15,A40,A49
.= f.(upper_bound divset(D,i));
then F1.i = f.(D.(len D)) by A15,A16,A19,A43,A47,A51,XXREAL_0:1
.= f.(upper_bound A) by INTEGRA1:def 2;
hence thesis by A48,FINSEQ_1:42;
end;
end;
hence thesis;
end;
len upper_volume(f||A,D)=len D & len lower_volume(f||A,D)=len D by
INTEGRA1:def 6,def 7;
then
A52: len (upper_volume(f||A,D)-lower_volume(f||A,D))=len D by Th2;
A53: len (F1-F2) = len D by A15,A17,Th2;
A54: for k st k in dom (upper_volume(f||A,D)-lower_volume(f||A,D)) holds (
upper_volume(f||A,D)-lower_volume(f||A,D)).k <= (delta(D)*(F1-F2)).k
proof
let k;
assume
A55: k in dom(upper_volume(f||A,D)-lower_volume(f||A,D));
then k in Seg len (F1-F2) by A52,A53,FINSEQ_1:def 3;
then
A56: k in dom (F1-F2) by FINSEQ_1:def 3;
A57: k in Seg len D by A52,A55,FINSEQ_1:def 3;
then k in dom D by FINSEQ_1:def 3;
then (upper_volume(f||A,D)).k-(lower_volume(f||A,D)).k <= (f.(upper_bound
divset(D,k))-f.(lower_bound divset(D,k)))*delta(D) by A3;
then
A58: (upper_volume(f||A,D)-lower_volume(f||A,D)).k <=
(f.(upper_bound divset(D,
k))-f.(lower_bound divset(D,k)))*delta(D) by A55,VALUED_1:13;
A59: F1.k= F2(k) by A15,A40,A57
.= f.(upper_bound divset(D,k));
F2.k = G(k) by A17,A18,A57
.=f.(lower_bound divset(D,k));
then (upper_volume(f||A,D)-lower_volume(f||A,D)).k <= delta(D)*(F1-F2).
k by A58,A56,VALUED_1:13,A59;
hence thesis by RVSUM_1:44;
end;
(delta(D)*(F1-F2))=(delta(D) multreal)*(F1-F2) by RVSUM_1:def 7;
then len (delta(D)*(F1-F2)) = len (F1-F2) by FINSEQ_2:33;
then len (upper_volume(f||A,D)-lower_volume(f||A,D)) = len (delta(D)*(F1-
F2)) by A15,A17,A52,Th2;
then
A60: Sum(upper_volume(f||A,D)-lower_volume(f||A,D))<=Sum(delta(D)*(F1-F2)
) by A54,Th3;
len (F^<*f.(upper_bound A)*>)= len F + len <*f.(upper_bound A)*>
by FINSEQ_1:22
.= len D - 1 + 1 by A16,A19,FINSEQ_1:39
.= len D;
then F1=F^<*f.(upper_bound A)*> by A15,A41,FINSEQ_1:14;
then Sum(F1-F2)=f.(upper_bound A)-f.(lower_bound A) by A38,Th1;
hence upper_sum(f||A,D)-lower_sum(f||A,D)<=
delta(D)*(f.(upper_bound A)-f.(lower_bound A))
by A39,A60,RVSUM_1:87;
for k be Nat st k in dom (upper_volume(f||A,D)-lower_volume(f||A,D))
holds 0<=(upper_volume(f||A,D)-lower_volume(f||A,D)).k
proof
let k be Nat;
set r = (upper_volume(f||A,D)-lower_volume(f||A,D)).k;
A61: len upper_volume(f||A,D)=len D & len lower_volume(f||A,D)=len D by
INTEGRA1:def 6,def 7;
assume
A62: k in dom (upper_volume(f||A,D)-lower_volume(f||A,D));
then k in Seg len (upper_volume(f||A,D)-lower_volume(f||A,D)) by
FINSEQ_1:def 3;
then k in Seg len D by A61,Th2;
then
A63: k in dom D by FINSEQ_1:def 3;
r = (upper_volume(f||A,D)).k-(lower_volume(f||A,D)).k by A62,VALUED_1:13;
hence thesis by A3,A63;
end;
hence thesis by A39,RVSUM_1:84;
end;
A64: f||A is total & f||A|A is bounded
proof
consider x being Element of REAL such that
A65: x in A by SUBSET_1:4;
A66: dom (f||A) = dom f /\ A by RELAT_1:61
.= A by A2,XBOOLE_1:28;
hence f||A is total by PARTFUN1:def 2;
lower_bound A <= x & x <= upper_bound A by A65,INTEGRA2:1;
then
A67: lower_bound A <= upper_bound A by XXREAL_0:2;
for x being object st x in A /\ dom (f||A) holds (f||A).x >= (f||A).(
lower_bound A)
proof
lower_bound A in A by A67,INTEGRA2:1;
then
A68: lower_bound A in A /\ dom f & f.(lower_bound A)=
(f|A).(lower_bound A) by A2,A66,FUNCT_1:47,XBOOLE_1:28;
let x be object;
assume
A69: x in A /\ dom (f||A);
then x in A;
then
A70: x in A /\ dom f by A2,XBOOLE_1:28;
reconsider x as Element of A by A69;
x >= lower_bound A & f.x = (f|A).x by A66,FUNCT_1:47,INTEGRA2:1;
hence thesis by A1,A70,A68,RFUNCT_2:24;
end;
then
A71: f||A|A is bounded_below by RFUNCT_1:71;
for x being object st x in A /\ dom (f||A) holds (f||A).x <= (f||A).(
upper_bound A)
proof
upper_bound A in A by A67,INTEGRA2:1;
then
A72: upper_bound A in A /\ dom f &
f.(upper_bound A)=(f|A).(upper_bound A) by A2,A66,FUNCT_1:47,XBOOLE_1:28;
let x be object;
assume
A73: x in A /\ dom (f||A);
then x in A;
then
A74: x in A /\ dom f by A2,XBOOLE_1:28;
reconsider x as Element of A by A73;
x <= upper_bound A & f.x = (f|A).x by A66,FUNCT_1:47,INTEGRA2:1;
hence thesis by A1,A74,A72,RFUNCT_2:24;
end;
then f||A|A is bounded_above by RFUNCT_1:70;
hence thesis by A71;
end;
for T being DivSequence of A st delta(T) is convergent & lim delta(T)=
0 holds lim upper_sum(f||A,T)-lim lower_sum(f||A,T)=0
proof
let T be DivSequence of A;
assume
A75: delta(T) is convergent & lim delta(T)=0;
A76: for r be Real st 0<r
ex n being Nat st for m being Nat st n<=m holds |.(
upper_sum(f||A,T)-lower_sum(f||A,T)).m-0.|<r
proof
consider x being Element of REAL such that
A77: x in A by SUBSET_1:4;
A78: A = A /\ dom f by A2,XBOOLE_1:28;
let r be Real;
assume
A79: 0<r;
lower_bound A <= x & x <= upper_bound A by A77,INTEGRA2:1;
then
A80: lower_bound A <= upper_bound A by XXREAL_0:2;
then lower_bound A in A & upper_bound A in A by INTEGRA2:1;
then
A81: f.(lower_bound A) <= f.(upper_bound A) by A1,A80,A78,RFUNCT_2:24;
per cases by A81,XXREAL_0:1;
suppose
A82: f.(lower_bound A)=f.(upper_bound A);
reconsider n=0 as Nat;
take n;
let m be Nat;
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
assume n<=m;
reconsider D1=T.mm as Division of A;
A83: (upper_sum(f||A,T)-lower_sum(f||A,T)).m =upper_sum(f||A,T).m
+(-lower_sum(f||A,T)).m by SEQ_1:7
.=upper_sum(f||A,T).m+-lower_sum(f||A,T).m by SEQ_1:10
.=upper_sum(f||A,D1)+-lower_sum(f||A,T).m by INTEGRA2:def 2
.=upper_sum(f||A,D1)+-lower_sum(f||A,D1) by INTEGRA2:def 3;
upper_sum(f||A,D1)-lower_sum(f||A,D1)<=
delta(D1)*(f.(upper_bound A)-
f.( lower_bound A) ) & upper_sum(f||A,D1)-lower_sum(f||A,D1)>=0
by A14;
hence thesis by A79,A82,A83,ABSVALUE:def 1;
end;
suppose
f.(lower_bound A)<f.(upper_bound A);
then
A84: f.(upper_bound A)-f.(lower_bound A) > 0 by XREAL_1:50;
then r/(f.(upper_bound A)-f.(lower_bound A)) > 0 by A79,XREAL_1:139;
then consider n being Nat such that
A85: for m being Nat st n<=m holds
|.delta(T).m-0.|<r/(f.(upper_bound A)-f.(lower_bound
A)) by A75,SEQ_2:def 7;
A86: for m st n<=m holds delta(T).m<
r/(f.(upper_bound A)-f.(lower_bound A))
proof
let m;
assume n<=m;
then
A87: |.delta(T).m-0.|<r/(f.(upper_bound A)-f.(lower_bound A)) by A85;
delta(T).m <= |.delta(T).m.| by ABSVALUE:4;
hence thesis by A87,XXREAL_0:2;
end;
take n;
let m be Nat;
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
reconsider D=T.mm as Division of A;
A88: |.upper_sum(f||A,D)-lower_sum(f||A,D).| =|.upper_sum(f||A
,T).mm-lower_sum(f||A,D)-0.| by INTEGRA2:def 2
.=|.upper_sum(f||A,T).mm-lower_sum(f||A,T).m-0.| by
INTEGRA2:def 3
.=|.upper_sum(f||A,T).m+-lower_sum(f||A,T).m-0.|
.=|.upper_sum(f||A,T).m+(-lower_sum(f||A,T)).m-0.| by SEQ_1:10
.=|.(upper_sum(f||A,T)-lower_sum(f||A,T)).m-0.| by SEQ_1:7;
assume n<=m;
then delta(T).mm<r/(f.(upper_bound A)-f.(lower_bound A))
by A86;
then delta(T).m*(f.(upper_bound A)-f.(lower_bound A)) < r
by A84,XREAL_1:79;
then
A89: delta(D)*(f.(upper_bound A)-f.(lower_bound A)) <r
by INTEGRA3:def 2;
upper_sum (f||A,D)-lower_sum(f||A,D) <=
delta(D)*(f.(upper_bound A)-
f.(lower_bound A)) by A14;
then
A90: upper_sum(f||A,D)-lower_sum(f||A,D) < r by A89,XXREAL_0:2;
upper_sum(f||A,D)-lower_sum(f||A,D) >=0 by A14;
hence thesis by A90,A88,ABSVALUE:def 1;
end;
end;
A91: upper_sum(f||A,T) is convergent & lower_sum(f||A,T) is convergent by A64
,A75,INTEGRA4:8,9;
then upper_sum(f||A,T)-lower_sum(f||A,T) is convergent;
then lim (upper_sum(f||A,T)-lower_sum(f||A,T)) = 0 by A76,SEQ_2:def 7;
hence thesis by A91,SEQ_2:12;
end;
then f||A is integrable by A64,INTEGRA4:12;
hence thesis;
end;
theorem
for f being PartFunc of REAL,REAL st f|A is monotone & A c= dom f
holds f is_integrable_on A
proof
let f be PartFunc of REAL,REAL;
assume that
A1: f|A is monotone and
A2: A c= dom f;
per cases by A1,RFUNCT_2:def 5;
suppose
f|A is non-decreasing;
hence thesis by A2,Lm1;
end;
suppose
f|A is non-increasing;
then
A3: ((-1)(#)f)|A is non-decreasing by RFUNCT_2:35;
A4: ((-f)||A) is total & (-f)||A|A is bounded
proof
consider x being Element of REAL such that
A5: x in A by SUBSET_1:4;
A6: dom ((-f)||A) = dom (-f) /\ A by RELAT_1:61
.= dom f /\ A by VALUED_1:8
.= A by A2,XBOOLE_1:28;
hence ((-f)||A) is total by PARTFUN1:def 2;
lower_bound A <= x & x <= upper_bound A by A5,INTEGRA2:1;
then
A7: lower_bound A <= upper_bound A by XXREAL_0:2;
for x being object st x in A /\ dom ((-f)||A) holds ((-f)||A).x >= ((-
f)||A).(lower_bound A)
proof
let x be object;
assume x in A /\ dom ((-f)||A);
then reconsider x as Element of A;
A8: x >= lower_bound A & (-f).x = ((-f)|A).x by A6,FUNCT_1:47,INTEGRA2:1;
lower_bound A in A by A7,INTEGRA2:1;
then
A9: (-f).(lower_bound A)=((-f)|A).(lower_bound A) by A6,FUNCT_1:47;
A10: A = A /\ dom f by A2,XBOOLE_1:28
.= A /\ dom (-f) by VALUED_1:8;
then lower_bound A in A /\ dom (-f) by A7,INTEGRA2:1;
hence thesis by A3,A10,A8,A9,RFUNCT_2:24;
end;
then
A11: (-f)||A|A is bounded_below by RFUNCT_1:71;
for x being object st x in A /\ dom ((-f)||A) holds ((-f)||A).x <= ((-
f)||A).(upper_bound A)
proof
let x be object;
assume x in A /\ dom ((-f)||A);
then reconsider x as Element of A;
A12: x <= upper_bound A & (-f).x = ((-f)|A).x by A6,FUNCT_1:47,INTEGRA2:1;
upper_bound A in A by A7,INTEGRA2:1;
then
A13: (-f).(upper_bound A)=((-f)|A).(upper_bound A) by A6,FUNCT_1:47;
A14: A = A /\ dom f by A2,XBOOLE_1:28
.= A /\ dom (-f) by VALUED_1:8;
then upper_bound A in A /\ dom (-f) by A7,INTEGRA2:1;
hence thesis by A3,A14,A12,A13,RFUNCT_2:24;
end;
then (-f)||A|A is bounded_above by RFUNCT_1:70;
hence thesis by A11;
end;
dom f = dom -f by VALUED_1:8;
then -f is_integrable_on A by A2,A3,Lm1;
then ((-f)||A) is integrable;
then
A15: (-1)(#)((-f)||A) is integrable by A4,INTEGRA2:31;
A16: dom ((-f)||A) = dom (-f) /\ A by RELAT_1:61
.= dom f /\ A by VALUED_1:8
.= A by A2,XBOOLE_1:28;
then
A17: A = dom ((-1)(#)((-f)||A)) by VALUED_1:def 5;
A18: dom (f||A) = dom f /\ A by RELAT_1:61;
then
A19: dom (f||A) = A by A2,XBOOLE_1:28;
A20: dom ((-1)(#)((-f)||A)) = A by A16,VALUED_1:def 5;
A21: for z being Element of A st z in A holds ((-1)(#)((-f)||A)).z = (f||
A ) . z
proof
let z be Element of A;
assume z in A;
((-f)||A).z = (-f).z by A16,FUNCT_1:47
.=-(f.z) by VALUED_1:8;
then ((-1)(#) ((-f)||A)).z =(-1)*(-(f.z)) by A20,VALUED_1:def 5
.= f.z;
hence thesis by A19,FUNCT_1:47;
end;
A = dom (f||A) by A2,A18,XBOOLE_1:28;
then (-1)(#)((-f)||A) = (f||A) by A21,A17,PARTFUN1:5;
hence thesis by A15;
end;
end;
theorem
for f being PartFunc of REAL,REAL,
A,B being non empty closed_interval Subset of
REAL st A c= dom f & f|A is continuous & B c= A holds f is_integrable_on B
proof
let f be PartFunc of REAL,REAL,
A,B be non empty closed_interval Subset of REAL such
that
A1: A c= dom f and
A2: f|A is continuous and
A3: B c= A;
f|B is continuous by A2,A3,FCONT_1:16;
hence thesis by A1,A3,Th11,XBOOLE_1:1;
end;
theorem
for f being PartFunc of REAL,REAL,
A,B,C being non empty closed_interval Subset
of REAL, X st A c= X & f is_differentiable_on X & (f`|X)|A is continuous
&lower_bound A
= lower_bound B & upper_bound B = lower_bound C & upper_bound C = upper_bound A
holds B c= A & C c= A & integral(f`|X,A
)=integral(f`|X,B)+integral(f`|X,C)
proof
let f be PartFunc of REAL,REAL;
let A,B,C be non empty closed_interval Subset of REAL;
let X;
assume that
A1: A c=X & f is_differentiable_on X and
A2: (f`|X)|A is continuous and
A3: lower_bound A=lower_bound B and
A4: upper_bound B=lower_bound C and
A5: upper_bound C=upper_bound A;
consider x being Element of REAL such that
A6: x in B by SUBSET_1:4;
lower_bound B <= x & x <= upper_bound B by A6,INTEGRA2:1;
then
A7: lower_bound B <= upper_bound B by XXREAL_0:2;
consider x being Element of REAL such that
A8: x in C by SUBSET_1:4;
lower_bound C <= x & x <= upper_bound C by A8,INTEGRA2:1;
then
A9: lower_bound C <= upper_bound C by XXREAL_0:2;
for x being object st x in B holds x in A
proof
let x be object;
assume
A10: x in B;
then reconsider x as Real;
x <= upper_bound B by A10,INTEGRA2:1;
then
A11: x <= upper_bound A by A4,A5,A9,XXREAL_0:2;
lower_bound A <= x by A3,A10,INTEGRA2:1;
hence thesis by A11,INTEGRA2:1;
end;
hence
A12: B c= A by TARSKI:def 3;
A13: A c= dom(f`|X) by A1,FDIFF_1:def 7;
then
A14: (f`|X)|A is bounded by A2,Th10;
then
A15: (f`|X)|B is bounded by A12,RFUNCT_1:74;
for x being object st x in C holds x in A
proof
let x be object;
assume
A16: x in C;
then reconsider x as Real;
lower_bound C <= x by A16,INTEGRA2:1;
then
A17: lower_bound A <= x by A3,A4,A7,XXREAL_0:2;
x <= upper_bound A by A5,A16,INTEGRA2:1;
hence thesis by A17,INTEGRA2:1;
end;
hence
A18: C c= A by TARSKI:def 3;
then
A19: (f`|X)|C is bounded by A14,RFUNCT_1:74;
(f`|X)|C is continuous by A2,A18,FCONT_1:16;
then f`|X is_integrable_on C by A13,A18,Th11,XBOOLE_1:1;
then
A20: integral(f`|X,C) = f.(upper_bound C)-f.(lower_bound C)
by A1,A18,A19,Th13,XBOOLE_1:1;
(f`|X)|B is continuous by A2,A12,FCONT_1:16;
then f`|X is_integrable_on B by A13,A12,Th11,XBOOLE_1:1;
then
A21: integral(f`|X,B) = f.(upper_bound B)-f.(lower_bound B)
by A1,A12,A15,Th13,XBOOLE_1:1;
f`|X is_integrable_on A by A2,A13,Th11;
then integral(f`|X,A) = f.(upper_bound A)-f.(lower_bound A)
by A1,A2,A13,Th10,Th13;
hence thesis by A3,A4,A5,A21,A20;
end;
definition
let a,b be Real;
assume
A1: a<=b;
func [' a,b '] -> non empty closed_interval Subset of REAL equals
:Def3:
[.a,b.];
correctness
by A1,MEASURE5:14;
end;
definition
let a,b be Real;
let f be PartFunc of REAL,REAL;
func integral(f,a,b) -> Real equals
:Def4:
integral(f,[' a,b ']) if a<=b
otherwise -integral(f,[' b,a ']);
correctness;
end;
theorem
for f being PartFunc of REAL,REAL,
A being non empty closed_interval Subset of
REAL, a,b st A=[.a,b.] holds integral(f,A)=integral(f,a,b)
proof
let f be PartFunc of REAL,REAL;
let A be non empty closed_interval Subset of REAL;
let a,b;
consider a1,b1 being Real such that
A1: a1 <= b1 and
A2: A = [.a1,b1.] by MEASURE5:14;
assume A = [.a,b.];
then
A3: a1=a & b1=b by A2,INTEGRA1:5;
then integral(f,a,b)=integral(f,[' a,b ']) by A1,Def4;
hence thesis by A1,A2,A3,Def3;
end;
theorem
for f being PartFunc of REAL,REAL,
A being non empty closed_interval Subset of
REAL, a,b st A=[.b,a.] holds -integral(f,A)=integral(f,a,b)
proof
let f be PartFunc of REAL,REAL;
let A be non empty closed_interval Subset of REAL;
let a,b;
consider a1,b1 being Real such that
A1: a1 <= b1 and
A2: A = [.a1,b1.] by MEASURE5:14;
assume
A3: A = [.b,a.];
then
A4: a1 = b & b1 = a by A2,INTEGRA1:5;
now
per cases by A1,A4,XXREAL_0:1;
suppose
A5: b < a;
then integral(f,a,b)=-integral(f,[' b,a ']) by Def4;
hence thesis by A3,A5,Def3;
end;
suppose
A6: b = a;
A=[.lower_bound A,upper_bound A.] by INTEGRA1:4;
then lower_bound A = b & upper_bound A = a by A3,INTEGRA1:5;
then vol(A)=upper_bound A-upper_bound A by A6,INTEGRA1:def 5
.=0;
then
A7: integral(f,A)=0 by INTEGRA4:6;
integral(f,a,b)=integral(f,[' a,b ']) by A6,Def4;
hence thesis by A3,A6,A7,Def3;
end;
end;
hence thesis;
end;
theorem
for f,g being PartFunc of REAL,REAL, X being open Subset of REAL st f
is_differentiable_on X & g is_differentiable_on X & A c= X & f`|X
is_integrable_on A & (f`|X)|A is bounded & g`|X is_integrable_on A & (g`|X)|A
is bounded holds integral((f`|X)(#)g,A) =
f.(upper_bound A)*g.(upper_bound A)-f.(lower_bound A)*g.(lower_bound A
)-integral(f(#)(g`|X),A)
proof
let f,g be PartFunc of REAL,REAL;
let X be open Subset of REAL;
assume that
A1: f is_differentiable_on X and
A2: g is_differentiable_on X and
A3: A c= X and
A4: f`|X is_integrable_on A and
A5: (f`|X)|A is bounded and
A6: g`|X is_integrable_on A and
A7: (g`|X)|A is bounded;
A8: (f(#)g)`|X = (f`|X)(#)g + f(#)(g`|X) by A1,A2,FDIFF_2:20;
g|X is continuous by A2,FDIFF_1:25;
then
A9: g|A is continuous by A3,FCONT_1:16;
X c= dom g by A2,FDIFF_1:def 6;
then
A10: A c= dom g by A3,XBOOLE_1:1;
then
A11: g||A is Function of A,REAL by Th6,FUNCT_2:68;
X c= dom g by A2,FDIFF_1:def 6;
then g is_integrable_on A by A3,A9,Th11,XBOOLE_1:1;
then
A12: g||A is integrable;
A13: A c= dom(g`|X) by A2,A3,FDIFF_1:def 7;
then
A14: (g`|X)||A is Function of A,REAL by Th6,FUNCT_2:68;
g|X is continuous by A2,FDIFF_1:25;
then g|A is bounded by A3,A10,Th10,FCONT_1:16;
then
A15: ((f`|X)(#)g)|(A /\ A) is bounded by A5,RFUNCT_1:84;
then
A16: ((f`|X)(#)g)||A|A is bounded;
f|X is continuous by A1,FDIFF_1:25;
then
A17: f|A is continuous by A3,FCONT_1:16;
X c= dom f by A1,FDIFF_1:def 6;
then f is_integrable_on A by A3,A17,Th11,XBOOLE_1:1;
then
A18: f||A is integrable;
A19: A c= dom(f`|X) by A1,A3,FDIFF_1:def 7;
then
A20: (f`|X)||A is Function of A,REAL by Th6,FUNCT_2:68;
A21: (g`|X)||A is integrable & (g`|X)||A|A is bounded by A6,A7;
A22: (f`|X)||A is integrable & (f`|X)||A|A is bounded by A4,A5;
dom ((f`|X)(#)g) = dom (f`|X) /\ dom g by VALUED_1:def 4;
then A c= dom((f`|X)(#)g) by A10,A19,XBOOLE_1:19;
then
A23: ((f`|X)(#)g)||A is Function of A, REAL by Th6,FUNCT_2:68;
X c= dom f by A1,FDIFF_1:def 6;
then
A24: A c= dom f by A3,XBOOLE_1:1;
then
A25: f||A is Function of A,REAL by Th6,FUNCT_2:68;
f|X is continuous by A1,FDIFF_1:25;
then f|A is bounded by A3,A24,Th10,FCONT_1:16;
then
A26: (f(#)(g`|X))|(A /\ A) is bounded by A7,RFUNCT_1:84;
then
A27: (f(#)(g`|X))||A|A is bounded;
((f`|X)(#)g + f(#)(g`|X))|(A /\ A) is bounded by A15,A26,RFUNCT_1:83;
then
A28: ((f(#)g)`|X)|A is bounded by A1,A2,FDIFF_2:20;
A29: (f(#)g).(upper_bound A)=f.(upper_bound A)*g.(upper_bound A) &
(f(#)g).(lower_bound A)=f.(lower_bound A)*g.(lower_bound
A) by VALUED_1:5;
dom (f(#)(g`|X)) = dom f /\ dom (g`|X) by VALUED_1:def 4;
then A c= dom(f(#)(g`|X)) by A24,A13,XBOOLE_1:19;
then
A30: (f(#)(g`|X))||A is Function of A, REAL by Th6,FUNCT_2:68;
g||A|A is bounded by A9,A10,Th10;
then ((f`|X)||A)(#)(g||A) is integrable by A12,A11,A20,A22,INTEGRA4:29;
then
A31: ((f`|X)(#)g)||A is integrable by Th4;
f||A|A is bounded by A17,A24,Th10;
then (f||A)(#)((g`|X)||A) is integrable by A18,A25,A14,A21,INTEGRA4:29;
then
A32: (f(#)(g`|X))||A is integrable by Th4;
then integral(((f`|X)(#)g)||A + (f(#)(g`|X))||A) =integral(((f`|X)(#)g)||A)
+ integral((f(#)(g`|X))||A) by A31,A23,A16,A30,A27,INTEGRA1:57;
then
A33: integral(((f`|X)(#)g+f(#)(g`|X))||A) =integral((f`|X)(#)g,A) + integral
(f(#)(g`|X),A) by Th5;
((f`|X)(#)g)||A+(f(#)(g`|X))||A is integrable by A31,A32,A23,A16,A30,A27,
INTEGRA1:57;
then ((f`|X)(#)g + f(#)(g`|X))||A is integrable by Th5;
then
A34: (f(#)g)`|X is_integrable_on A by A8;
integral(((f(#)g)`|X)||A)=integral((f(#)g)`|X,A)
.=(f(#)g).(upper_bound A)-(f(#)g).(lower_bound A)
by A1,A2,A3,A34,A28,Th13,FDIFF_2:20;
hence thesis by A8,A29,A33;
end;