:: Integrability and the Integral of Partial Functions from $\Bbb R$ into
:: $\Bbb R$
:: by Noboru Endou , Yasunari Shidama and Masahiko Yamazaki
::
:: Received November 17, 2006
:: Copyright (c) 2006-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, INTEGRA1, SUBSET_1, PARTFUN1, XXREAL_0, ARYTM_3,
XXREAL_1, ARYTM_1, TARSKI, RELAT_1, FUNCT_3, XBOOLE_0, FUNCT_1, MEASURE7,
INTEGRA5, ORDINAL2, COMPLEX1, CARD_1, REALSET1, XXREAL_2, REAL_1,
VALUED_1, FINSEQ_1, NAT_1, INTEGRA2, SEQ_2, INTEGRA4, INT_1, RFINSEQ,
ORDINAL4, CARD_3, FCONT_1, FDIFF_1, SEQ_1, FUNCT_2, FUNCOP_1, RCOMP_1,
VALUED_0, SEQ_4, MEASURE5, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, COMPLEX1, REAL_1, NAT_1, INT_1, FUNCT_1, PARTFUN1, FUNCT_2,
FUNCOP_1, RCOMP_1, FINSEQ_1, VALUED_0, VALUED_1, SEQ_1, RFUNCT_1, SEQ_2,
FDIFF_1, RFINSEQ, XXREAL_2, RVSUM_1, MEASURE5, INTEGRA1, INTEGRA2,
FCONT_1, INTEGRA3, INTEGRA4, INTEGRA5, XXREAL_0, SEQ_4;
constructors REAL_1, BINOP_2, COMPLEX1, RFUNCT_1, FCONT_1, FDIFF_1, RFINSEQ,
RSSPACE, INTEGRA2, INTEGRA4, INTEGRA5, RVSUM_1, SEQ_4, RELSET_1,
FUNCOP_1, SEQ_2, INTEGRA3, COMSEQ_2;
registrations XBOOLE_0, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XXREAL_0,
XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, RCOMP_1, FDIFF_1, SEQM_3,
INTEGRA1, VALUED_0, VALUED_1, FINSET_1, XXREAL_2, CARD_1, RELSET_1,
MEASURE5;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI;
equalities XCMPLX_0, INTEGRA1, FINSEQ_1, INTEGRA5, INTEGRA3;
expansions TARSKI, INTEGRA1, INTEGRA5;
theorems ORDINAL1, PARTFUN1, INTEGRA1, RFUNCT_1, FUNCT_1, FINSEQ_1, RVSUM_1,
SEQ_1, SEQ_2, FDIFF_1, ABSVALUE, NAT_1, INT_1, COMPLEX1, TARSKI,
INTEGRA2, INTEGRA3, RFINSEQ, INTEGRA4, FINSEQ_2, FINSEQ_3, RCOMP_1,
FCONT_1, XREAL_0, XXREAL_0, FUNCT_2, FINSEQ_5, XBOOLE_0, XBOOLE_1,
XCMPLX_1, XREAL_1, INTEGRA5, RELAT_1, VALUED_1, XXREAL_2, XXREAL_1,
SEQM_3, FUNCOP_1, RELSET_1;
schemes FUNCT_2, PARTFUN1, FINSEQ_2;
begin :: Preliminaries
reserve a,b,c,d,e,x,r for Real,
A for non empty closed_interval Subset of REAL,
f,g for PartFunc of REAL,REAL;
theorem Th1: ::: XREAL_0
a <= b & c <= d & a+c = b+d implies a = b & c = d
proof
assume that
A1: a <=b & c <=d and
A2: a+c =b+d;
assume not (a=b & c =d);
then a < b or c < d by A1,XXREAL_0:1;
hence contradiction by A1,A2,XREAL_1:8;
end;
theorem Th2: ::: XXREAL_1
a <= b implies ].x-a,x+a.[ c= ].x-b,x+b.[
proof
assume a <= b;
then x-b <= x - a & x+a <= x+b by XREAL_1:7,10;
hence thesis by XXREAL_1:46;
end;
theorem Th3:
for R be Relation, A,B,C be set st A c= B & A c= C holds (R|B)|A
= (R|C)|A
proof
let R be Relation, A,B,C be set;
assume that
A1: A c= B and
A2: A c= C;
(R|C)|A = R|A by A2,RELAT_1:74;
hence thesis by A1,RELAT_1:74;
end;
theorem Th4:
for A,B,C be set st A c= B & A c= C holds chi(B,B)|A = chi(C,C)|A
proof
let A,B,C be set;
assume that
A1: A c= B and
A2: A c= C;
A3: now
A4: dom(chi(C,C)|A) =dom(chi(C,C)) /\ A by RELAT_1:61;
assume
A5: A is non empty;
then C is non empty by A2,XBOOLE_1:58,61;
then dom(chi(C,C)|A) =C /\ A by A4,RFUNCT_1:61;
then
A6: dom(chi(C,C)|A) =A by A2,XBOOLE_1:28;
A7: dom(chi(B,B)|A) =dom(chi(B,B)) /\ A by RELAT_1:61;
B is non empty by A1,A5,XBOOLE_1:58,61;
then dom(chi(B,B)|A) =B /\ A by A7,RFUNCT_1:61;
then
A8: dom(chi(B,B)|A) =A by A1,XBOOLE_1:28;
now
let x be object;
assume
A9: x in A;
then (chi(B,B)|A).x =(chi(B,B)).x by A8,FUNCT_1:47;
then (chi(B,B)|A).x = 1 by A1,A9,RFUNCT_1:61;
then (chi(B,B)|A).x = (chi(C,C)).x by A2,A9,RFUNCT_1:61;
hence (chi(B,B)|A).x = (chi(C,C)|A).x by A6,A9,FUNCT_1:47;
end;
hence thesis by A8,A6,FUNCT_1:2;
end;
now
assume
A10: A is empty;
then chi(B,B)|A = {};
hence thesis by A10;
end;
hence thesis by A3;
end;
theorem Th5:
a <= b implies vol([' a,b '])=b-a
proof
assume a<=b;
then
A1: [' a,b '] = [.a,b.] by INTEGRA5:def 3;
then
A2: [.a,b.] = [.lower_bound [.a,b.], upper_bound [.a,b.].] by INTEGRA1:4;
then a=lower_bound([.a,b.]) by A1,INTEGRA1:5;
hence thesis by A1,A2,INTEGRA1:5;
end;
theorem Th6:
vol([' min(a,b),max(a,b) ']) = |.b-a.|
proof
per cases;
suppose
A1: a<= b;
then min(a,b) = a & max(a,b) = b by XXREAL_0:def 9,def 10;
then
A2: vol([' min(a,b),max(a,b) '])=b-a by Th5,XXREAL_0:25;
0 <= b-a by A1,XREAL_1:48;
hence thesis by A2,ABSVALUE:def 1;
end;
suppose
A3: not a<= b;
then 0 <= a-b by XREAL_1:48;
then
A4: a-b = |.a-b.| by ABSVALUE:def 1
.=|.b-a.| by COMPLEX1:60;
min(a,b) = b & max(a,b) = a by A3,XXREAL_0:def 9,def 10;
hence thesis by A4,Th5,XXREAL_0:17;
end;
end;
begin :: Integrability and The Integral of Partial Functions from REAL to REAL
Lm1: A c= dom f implies f||A is Function of A,REAL
proof
rng f c= REAL;
then
A1: f is Function of dom f,REAL by FUNCT_2:2;
assume A c= dom f;
hence thesis by A1,FUNCT_2:32;
end;
theorem Th7:
A c= dom f & f is_integrable_on A & f|A is bounded implies abs f
is_integrable_on A & |.integral(f,A).| <= integral(abs f,A)
proof
A1: |.f||A.| = abs(f)||A by RFUNCT_1:46;
assume A c= dom f;
then
A2: f||A is Function of A,REAL by Lm1;
assume f is_integrable_on A & f|A is bounded;
then
A3: f||A is integrable & f||A|A is bounded;
thus thesis by A3,A2,A1,INTEGRA4:23;
end;
theorem Th8:
a<=b & [' a,b '] c= dom f & f is_integrable_on [' a,b '] & f|[' a
,b '] is bounded implies |.integral(f,a,b).| <=integral(abs f,a,b)
proof
assume a<=b;
then
integral(f,a,b) = integral(f,[' a,b ']) & integral(abs f,a,b) = integral
(abs f,[' a,b ']) by INTEGRA5:def 4;
hence thesis by Th7;
end;
theorem Th9:
A c= dom f & f is_integrable_on A & f|A is
bounded implies
r(#)f is_integrable_on A & integral(r(#)f,A)=r*integral(f,A)
proof
assume that
A1: A c= dom f and
A2: f is_integrable_on A & f|A is bounded;
A3: f||A is integrable & f||A|A is bounded by A2;
rng f c= REAL;
then f is Function of dom f,REAL by FUNCT_2:2;
then
A4: f|A is Function of A,REAL by A1,FUNCT_2:32;
r(#)(f||A) =(r(#)f)|A by RFUNCT_1:49;
then (r(#)f)||A is integrable by A3,A4,INTEGRA2:31;
hence r(#)f is_integrable_on A;
integral((r(#)f),A) =integral(r(#)(f||A)) by RFUNCT_1:49;
hence thesis by A3,A4,INTEGRA2:31;
end;
theorem Th10:
a<=b & [' a,b '] c= dom f & f is_integrable_on [' a,b '] & f|['
a,b '] is bounded implies integral(c(#)f,a,b) =c*integral(f,a,b)
proof
assume that
A1: a<=b and
A2: [' a,b '] c= dom f & f is_integrable_on [' a,b '] & f|[' a,b '] is
bounded;
integral(f,a,b) = integral(f,[' a,b ']) & integral(c(#)f,a,b) = integral
(c (#)f,[' a,b ']) by A1,INTEGRA5:def 4;
hence thesis by A2,Th9;
end;
theorem Th11:
A c= dom f & A c= dom g & f is_integrable_on A & f|A is bounded
& g is_integrable_on A & g|A is bounded implies f+g is_integrable_on A & f-g
is_integrable_on A & integral(f+g,A) = integral(f,A) + integral(g,A) & integral
(f-g,A) = integral(f,A) - integral(g,A)
proof
assume that
A1: A c= dom f & A c= dom g and
A2: f is_integrable_on A and
A3: f|A is bounded and
A4: g is_integrable_on A and
A5: g|A is bounded;
A6: f||A|A is bounded & g||A|A is bounded by A3,A5;
A7: f||A is Function of A,REAL & g||A is Function of A,REAL by A1,Lm1;
A8: f||A + g||A = (f+g)||A & f||A - g||A = (f-g)||A by RFUNCT_1:44,47;
A9: f||A is integrable & g||A is integrable by A2,A4;
then f||A + g||A is integrable & f||A - g||A is integrable by A6,A7,
INTEGRA1:57,INTEGRA2:33;
hence f+g is_integrable_on A & f-g is_integrable_on A by A8;
thus thesis by A9,A6,A7,A8,INTEGRA1:57,INTEGRA2:33;
end;
theorem Th12:
a<=b & [' a,b '] c= dom f & [' a,b '] c= dom g & f
is_integrable_on [' a,b '] & g is_integrable_on [' a,b '] & f|[' a,b '] is
bounded & g|[' a,b '] is bounded implies integral(f+g,a,b) =integral(f,a,b) +
integral(g,a,b) & integral(f-g,a,b) =integral(f,a,b) - integral(g,a,b)
proof
assume that
A1: a<=b and
A2: [' a,b '] c= dom f & [' a,b '] c= dom g & f is_integrable_on [' a,b
'] & g is_integrable_on [' a,b '] & f|[' a,b '] is bounded & g|[' a,b '] is
bounded;
A3: integral(f+g,a,b) = integral(f+g,[' a,b ']) & integral(f-g,a,b) =
integral(f -g,[' a,b ']) by A1,INTEGRA5:def 4;
integral(f,a,b) = integral(f,[' a,b ']) & integral(g,a,b) = integral(g,
[' a, b ']) by A1,INTEGRA5:def 4;
hence thesis by A2,A3,Th11;
end;
theorem
f|A is bounded & g|A is bounded implies (f(#)g)|A is bounded
proof
assume f|A is bounded & g|A is bounded;
then (f(#)g)|(A /\ A) is bounded by RFUNCT_1:84;
hence thesis;
end;
theorem
A c= dom f & A c= dom g & f is_integrable_on A & f|A is bounded & g
is_integrable_on A & g|A is bounded implies f(#)g is_integrable_on A
proof
assume that
A1: A c= dom f & A c= dom g and
A2: f is_integrable_on A & f|A is bounded and
A3: g is_integrable_on A & g|A is bounded;
A4: f||A is integrable & f||A|A is bounded by A2;
A5: g||A is integrable & g||A|A is bounded by A3;
A6: (f||A)(#)(g||A) = (f(#)g)||A by INTEGRA5:4;
f||A is Function of A,REAL & g||A is Function of A,REAL by A1,Lm1;
then (f(#)g)||A is integrable by A4,A5,A6,INTEGRA4:29;
hence thesis;
end;
theorem Th15:
for n be Nat st n > 0 & vol A > 0 holds ex D being
Division of A st len D = n & for i be Nat st i in dom D holds D.i=
lower_bound A + vol(A)/n*i
proof
let n be Nat;
assume that
A1: n > 0 and
A2: vol A > 0;
deffunc F(Nat)=In(lower_bound A + vol(A)/n*$1,REAL);
consider D being FinSequence of REAL such that
A3: len D = n & for i be Nat st i in dom D holds D.i=F(i) from FINSEQ_2:
sch 1;
A4: for i,j be Nat st i in dom D & j in dom D & i<j holds D.i < D
.j
proof
let i,j be Nat;
assume that
A5: i in dom D and
A6: j in dom D and
A7: i < j;
vol(A)/n > 0 by A1,A2,XREAL_1:139;
then vol(A)/n*i < vol(A)/n*j by A7,XREAL_1:68;
then F(i) < F(j) by XREAL_1:6;
then D.i < F(j) by A3,A5;
hence thesis by A3,A6;
end;
A8: dom D = Seg n by A3,FINSEQ_1:def 3;
reconsider D as non empty increasing FinSequence of REAL by A1,A3,A4,
SEQM_3:def 1;
D.(len D)=F(n) by A3,A8,FINSEQ_1:3;
then
A9: D.(len D)=lower_bound A + vol(A) by A1,XCMPLX_1:87;
for x1 being object st x1 in rng D holds x1 in A
proof
let x1 be object;
assume x1 in rng D;
then consider i be Element of NAT such that
A10: i in dom D and
A11: D.i=x1 by PARTFUN1:3;
A12: 1 <= i by A10,FINSEQ_3:25;
i <= len D by A10,FINSEQ_3:25;
then vol(A)/n*i <= vol(A)/n*n by A2,A3,XREAL_1:64;
then vol(A)/n*i <= vol A by A1,XCMPLX_1:87;
then
A13: lower_bound A + vol(A)/n*i <= lower_bound A+ vol A by XREAL_1:6;
vol(A)/n>0 by A1,A2,XREAL_1:139;
then
A14: lower_bound A <= lower_bound A + vol(A)/n*i by A12,XREAL_1:29,129;
x1 = F(i) by A3,A10,A11;
hence thesis by A14,A13,INTEGRA2:1;
end;
then rng D c= A;
then reconsider D as Division of A by A9,INTEGRA1:def 2;
take D;
thus len D = n by A3;
let i be Nat;
assume i in dom D;
then D.i = F(i) by A3;
hence thesis;
end;
begin :: Integrability on a Subinterval
theorem Th16:
vol A > 0 implies ex T being DivSequence of A st delta T is
convergent & lim delta T = 0 & for n be Element of NAT holds ex Tn being
Division of A st Tn divide_into_equal n+1 & T.n =Tn
proof
defpred P[set,set] means ex n being Element of NAT, e being Division of A st
n = $1 & e = $2 & e divide_into_equal n+1;
assume
A1: vol A > 0;
A2: for n be Element of NAT ex D being Element of divs A st P[n,D]
proof
let n be Element of NAT;
consider D being Division of A such that
A3: len D = n+1 & for i be Nat st i in dom D holds D.i=lower_bound
A+vol(A)/( n+1)*i by A1,Th15;
reconsider D1=D as Element of divs A by INTEGRA1:def 3;
take D1;
D divide_into_equal n+1 by A3,INTEGRA4:def 1;
hence thesis;
end;
consider T being sequence of divs A such that
A4: for n be Element of NAT holds P[n,T.n] from FUNCT_2:sch 3(A2);
reconsider T as DivSequence of A;
A5: for n be Element of NAT holds ex Tn being Division of A st Tn
divide_into_equal n+1 & T.n =Tn
proof
let n be Element of NAT;
ex n1 be Element of NAT, Tn being Division of A st n1 = n & Tn = T.n &
Tn divide_into_equal n1+1 by A4;
hence thesis;
end;
A6: for i be Element of NAT holds (delta T).i = vol(A)/(i+1)
proof
let i be Element of NAT;
for x1 being object st x1 in rng upper_volume(chi(A,A),(T.i)) holds x1 in
{vol(A)/(i+1)}
proof
reconsider D = T.i as Division of A;
let x1 be object;
assume x1 in rng upper_volume(chi(A,A),(T.i));
then consider k be Element of NAT such that
A7: k in dom upper_volume(chi(A,A),(T.i)) and
A8: (upper_volume(chi(A,A),(T.i))).k=x1 by PARTFUN1:3;
k in Seg len upper_volume(chi(A,A),(T.i)) by A7,FINSEQ_1:def 3;
then k in Seg len D by INTEGRA1:def 6;
then
A9: k in dom D by FINSEQ_1:def 3;
A10: ex n being Element of NAT, e being Division of A st n = i & e = D &
e divide_into_equal n+1 by A4;
A11: upper_bound divset(D,k)-lower_bound divset(D,k)=vol(A)/(i+1)
proof
A12: now
A13: len D = i+1 by A10,INTEGRA4:def 1;
assume
A14: k=1;
then upper_bound divset(D,k)=D.1 by A9,INTEGRA1:def 4;
then upper_bound divset(D,k)=lower_bound A+vol(A)/(i+1)*1
by A10,A9,A14,A13,INTEGRA4:def 1;
then
upper_bound divset(D,k)-lower_bound divset(D,k)=
lower_bound A+vol(A)/(i+1)-lower_bound A by A9,A14,INTEGRA1:def 4;
hence thesis;
end;
now
assume
A15: k <> 1;
then k-1 in dom D by A9,INTEGRA1:7;
then
A16: D.(k-1)=lower_bound A + vol(A)/(len D)*(k-1) by A10,INTEGRA4:def 1;
A17: D.k = lower_bound A + vol(A)/(len D)* k by A10,A9,INTEGRA4:def 1;
lower_bound divset(D,k)=D.(k-1) & upper_bound divset(D,k)=D.k
by A9,A15,INTEGRA1:def 4;
hence thesis by A10,A16,A17,INTEGRA4:def 1;
end;
hence thesis by A12;
end;
x1=vol(divset(D,k)) by A8,A9,INTEGRA1:20;
hence thesis by A11,TARSKI:def 1;
end;
then
A18: rng upper_volume(chi(A,A),(T.i)) c= {vol(A)/(i+1)};
for x1 being object st x1 in {vol(A)/(i+1)} holds x1 in rng upper_volume
(chi(A,A),(T.i))
proof
reconsider D = T.i as Division of A;
let x1 be object;
assume x1 in {vol(A)/(i+1)};
then
A19: x1 = vol(A)/(i+1) by TARSKI:def 1;
A20: ex n being Element of NAT, e being Division of A st n = i & e = D &
e divide_into_equal n+1 by A4;
rng D <> {};
then
A21: 1 in dom D by FINSEQ_3:32;
then upper_bound divset(D,1)=D.1 by INTEGRA1:def 4;
then upper_bound divset(D,1)=lower_bound A+vol(A)/(len D)*1 by A21,A20,
INTEGRA4:def 1;
then
A22: vol(divset(D,1))=lower_bound A+vol(A)/(len D)-lower_bound A
by A21,INTEGRA1:def 4;
1 in Seg len D by A21,FINSEQ_1:def 3;
then 1 in Seg len upper_volume(chi(A,A),D) by INTEGRA1:def 6;
then 1 in dom upper_volume(chi(A,A),D) by FINSEQ_1:def 3;
then
A23: (upper_volume(chi(A,A),D)).1 in rng upper_volume(chi(A,A), D) by
FUNCT_1:def 3;
(upper_volume(chi(A,A),D)).1 = vol(divset(D,1)) by A21,INTEGRA1:20;
hence thesis by A19,A23,A20,A22,INTEGRA4:def 1;
end;
then {vol(A)/(i+1)} c= rng upper_volume(chi(A,A),(T.i)); then
(delta T).i = delta(T.i) & rng upper_volume(chi(A,A),(T.i))={vol(A)/(
i+1)} by A18,INTEGRA3:def 2,XBOOLE_0:def 10;
then (delta T).i in {vol(A)/(i+1)} by XXREAL_2:def 8;
hence thesis by TARSKI:def 1;
end;
A24: for a be Real st 0 < a ex i be Element of NAT st |.(delta T).i-0 .|<a
proof
let a be Real;
A25: vol A >= 0 by INTEGRA1:9;
reconsider i1=[\vol(A)/a/]+1 as Integer;
assume
A26: 0<a;
then [\vol(A)/a/]+1>0 by A25;
then reconsider i1 as Element of NAT by INT_1:3;
i1 < i1+1 by NAT_1:13;
then vol(A)/a < 1*(i1+1) by INT_1:29,XXREAL_0:2;
then
A27: vol(A)/(i1+1) < 1*a by A26,XREAL_1:113;
A28: (delta T).i1 = vol(A)/(i1+1) by A6;
vol(A)/(i1+1)-0 = |.vol(A)/(i1+1)-0 .| by A25,ABSVALUE:def 1;
hence thesis by A27,A28;
end;
A29: for i,j be Element of NAT st i <= j holds (delta T).i >= (delta T).j
proof
let i,j be Element of NAT;
assume i <= j;
then
A30: i+1 <= j+1 by XREAL_1:6;
vol A >= 0 by INTEGRA1:9;
then vol A/(i+1) >= vol(A)/(j+1) by A30,XREAL_1:118;
then (delta T).i >= vol(A)/(j+1) by A6;
hence thesis by A6;
end;
A31: for a be Real st 0<a ex i be Nat st
for j be Nat st i <= j holds |.(delta T).j-0 .|<a
proof
let a be Real;
assume
A32: 0<a;
consider i be Element of NAT such that
A33: |.(delta T).i-0 .|<a by A24,A32;
(delta T).i = delta(T.i) by INTEGRA3:def 2;
then (delta T).i >= 0 by INTEGRA3:9;
then
A34: (delta T).i < a by A33,ABSVALUE:def 1;
take i;
let j be Nat;
reconsider jj = j as Element of NAT by ORDINAL1:def 12;
assume i <= j;
then (delta T).jj <= (delta T).i by A29;
then
A35: (delta T).j < a by A34,XXREAL_0:2;
(delta T).j = delta(T.jj) by INTEGRA3:def 2;
then (delta T).j >= 0 by INTEGRA3:9;
hence |.(delta T).j-0 .|<a by A35,ABSVALUE:def 1;
end;
then
A36: delta T is convergent by SEQ_2:def 6;
then lim delta(T)=0 by A31,SEQ_2:def 7;
hence thesis by A5,A36;
end;
Lm2: a <= b & [' a,b '] c= dom f & f is_integrable_on [' a,b '] & f|[' a,b ']
is bounded & c in [' a,b '] & b <> c implies integral(f,a,b) = integral(f,a,c)
+ integral(f,c,b) & f is_integrable_on ['a,c '] & f is_integrable_on ['c,b ']
proof
assume that
A1: a <= b and
A2: [' a,b '] c= dom f and
A3: f is_integrable_on [' a,b '] and
A4: f|[' a,b '] is bounded and
A5: c in [' a,b '] and
A6: b <> c;
A7: [' a,b '] = [.a,b.] by A1,INTEGRA5:def 3;
then
A8: c <= b by A5,XXREAL_1:1;
then
A9: [' c,b '] = [.c,b.] by INTEGRA5:def 3;
then
A10: [.c,b.] = [.lower_bound([.c,b.]), upper_bound([.c,b.]).] by INTEGRA1:4;
then
A11: upper_bound [' c,b '] = b by A9,INTEGRA1:5;
set FAB = f||[' a,b '], FAC = f||[' a,c '], FCB = f||[' c,b '];
A12: FAB is Function of [' a,b '],REAL by A2,Lm1;
A13: a <= c by A5,A7,XXREAL_1:1;
then
A14: [' a,c '] = [.a,c.] by INTEGRA5:def 3;
then
A15: [.a,c.] = [.lower_bound([.a,c.]), upper_bound([.a,c.]).] by INTEGRA1:4;
then
A16: lower_bound [' a,c '] = a by A14,INTEGRA1:5;
A17: [' c,b '] c= [' a,b '] by A7,A13,A9,XXREAL_1:34;
then f|[' c,b '] is bounded by A4,RFUNCT_1:74;
then
A18: FCB|[' c,b '] is bounded;
A19: lower_bound [' c,b '] = c by A9,A10,INTEGRA1:5;
ex PS2 be DivSequence of [' c,b '] st delta PS2 is convergent & lim
delta PS2 = 0 & ex K be Element of NAT st for i be Element of NAT st K <= i ex
S2i be Division of [' c,b '] st S2i=PS2.i & 2 <= len S2i
proof
c < b by A6,A8,XXREAL_0:1;
then vol([' c,b '] ) > 0 by A19,A11,XREAL_1:50;
then consider T being DivSequence of [' c,b '] such that
A20: delta T is convergent & lim delta(T)=0 and
A21: for n be Element of NAT holds ex Tn being Division of [' c,b ']
st Tn divide_into_equal n+1 & T.n =Tn by Th16;
take T;
now
let i be Element of NAT;
assume
A22: 2 <= i;
consider Tn being Division of [' c,b '] such that
A23: Tn divide_into_equal i+1 and
A24: T.i =Tn by A21;
reconsider Tn as Division of [' c,b '];
take Tn;
thus Tn=T.i by A24;
len Tn = i+1 by A23,INTEGRA4:def 1;
then i <= len Tn by NAT_1:11;
hence 2 <= len Tn by A22,XXREAL_0:2;
end;
hence thesis by A20;
end;
then consider PS2 be DivSequence of [' c,b '] such that
A25: delta PS2 is convergent & lim delta PS2 = 0 and
A26: ex K be Element of NAT st for i be Element of NAT st K <= i ex S2i
be Division of [' c,b '] st S2i = PS2.i & 2 <= len S2i;
consider K be Element of NAT such that
A27: for i be Element of NAT st K <= i ex S2i be Division of [' c,b ']
st S2i=PS2.i & 2 <= len S2i by A26;
defpred Q[set,set] means ex n being Element of NAT, e being Division of [' c
,b '] st n = $1 & e = $2 & e = PS2.(n+K);
A28: for n be Element of NAT ex D being Element of divs [' c,b '] st Q[n,D]
proof
let n be Element of NAT;
reconsider D = PS2.(n+K) as Element of divs [' c,b '] by INTEGRA1:def 3;
take D;
thus thesis;
end;
consider S2 being sequence of divs [' c,b '] such that
A29: for n be Element of NAT holds Q[n,S2.n] from FUNCT_2:sch 3(A28);
reconsider S2 as DivSequence of [' c,b '];
defpred P1[Element of NAT, set] means ex S be Division of [' c,b '] st S =
S2.$1 & $2 = S/^1;
A30: now
let i be Element of NAT;
ex n being Element of NAT,e being Division of ['c,b '] st n = i & e =
S2.i & e = PS2.(n+K) by A29;
hence ex S2i be Division of [' c,b '] st S2i=S2.i & 2 <= len S2i by A27,
NAT_1:11;
end;
A31: for i be Element of NAT ex T be Element of divs [' c,b '] st P1[i,T]
proof
let i be Element of NAT;
consider S be Division of [' c,b '] such that
A32: S=S2.i and
A33: 2 <= len S by A30;
set T=S/^1;
A34: 1 <= len S by A33,XXREAL_0:2;
2-1 <= len S -1 by A33,XREAL_1:13;
then
A35: 1 <= len T by A34,RFINSEQ:def 1;
then len T in Seg (len T);
then len T in dom T by FINSEQ_1:def 3;
then T.(len T) =S.(len T+ 1) by A34,RFINSEQ:def 1;
then T.(len T) =S.(len S -1+ 1) by A34,RFINSEQ:def 1;
then
A36: T.(len T) = upper_bound [' c,b '] by INTEGRA1:def 2;
rng S c= [' c,b '] & rng T c= rng S by FINSEQ_5:33,INTEGRA1:def 2;
then
A37: rng T c= [' c,b '];
T is non empty increasing by A33,A35,INTEGRA1:34,XXREAL_0:2;
then T is Division of [' c,b '] by A37,A36,INTEGRA1:def 2;
then T is Element of divs [' c,b '] by INTEGRA1:def 3;
hence thesis by A32;
end;
consider T2 be DivSequence of [' c,b '] such that
A38: for i be Element of NAT holds P1[i,T2.i] from FUNCT_2:sch 3(A31);
A39: for n be Element of NAT holds ex D be Division of [' c,b '] st D = T2.n
& for i be Element of NAT st i in dom D holds c < D.i
proof
let n be Element of NAT;
reconsider D=T2.n as Division of [' c,b '];
take D;
consider E be Division of [' c,b '] such that
A40: E=S2.n and
A41: T2.n=E/^1 by A38;
A42: ex E1 be Division of [' c,b '] st E1=S2.n & 2 <= len E1 by A30;
then
A43: 2-1 <= len E -1 by A40,XREAL_1:13;
A44: 1 <= len E by A40,A42,XXREAL_0:2;
then 1 in Seg len E;
then
A45: 1 in dom E by FINSEQ_1:def 3;
then rng E c=[' c,b '] & E.1 in rng E by FUNCT_1:def 3,INTEGRA1:def 2;
then
A46: c <= E.1 by A9,XXREAL_1:1;
2 in Seg len E by A40,A42;
then 2 in dom E by FINSEQ_1:def 3;
then
A47: E.1 < E.2 by A45,SEQM_3:def 1;
len D = len E -1 by A41,A44,RFINSEQ:def 1;
then 1 in Seg len D by A43;
then
A48: 1 in dom D by FINSEQ_1:def 3;
then
A49: D.1 = E.(1+1) by A41,A44,RFINSEQ:def 1;
then
A50: c < D.1 by A46,A47,XXREAL_0:2;
now
let i be Element of NAT;
assume
A51: i in dom D;
then
A52: 1 <=i by FINSEQ_3:25;
thus now
assume i <> 1;
then 1 < i by A52,XXREAL_0:1;
then D.1 < D.i by A48,A51,SEQM_3:def 1;
hence c < D.i by A50,XXREAL_0:2;
end;
hence c < D.i by A49,A46,A47,XXREAL_0:2;
end;
hence thesis;
end;
set XAC = chi([' a,c '],[' a,c ']);
set XCB = chi(['c,b '],['c,b ']);
consider T1 be DivSequence of [' a,c '] such that
A53: delta T1 is convergent & lim delta T1 = 0 by INTEGRA4:11;
A54: for n be Element of NAT holds ex D be Division of [' c,b '] st D = T2.n
& 1 <= len D
proof
let n be Element of NAT;
reconsider D=T2.n as Division of [' c,b '];
take D;
consider E be Division of [' c,b '] such that
A55: E=S2.n and
A56: T2.n=E/^1 by A38;
ex E1 be Division of [' c,b '] st E1=S2.n & 2 <= len E1 by A30;
then 1 <= len E & 2-1 <= len E -1 by A55,XREAL_1:13,XXREAL_0:2;
hence thesis by A56,RFINSEQ:def 1;
end;
A57: integral(f,c,b) = integral(f,[' c,b ']) by A8,INTEGRA5:def 4
.= integral FCB;
A58: integral(f,a,c) = integral(f,[' a,c ']) by A13,INTEGRA5:def 4;
defpred P2[Element of NAT,set] means ex S1 be Division of [' a,c '], S2 be
Division of [' c,b '] st S1=T1.$1 & S2=T2.$1 & $2=S1^S2;
A59: [.a,b.] = [.lower_bound([.a,b.]), upper_bound([.a,b.]).] by A7,INTEGRA1:4;
then
A60: upper_bound [' a,b '] = b by A7,INTEGRA1:5;
A61: for i be Element of NAT ex T be Element of divs [' a,b '] st P2[i,T]
proof
let i0 be Element of NAT;
reconsider S1=T1.i0 as Division of [' a,c '];
reconsider S2=T2.i0 as Division of [' c,b '];
set T=S1^S2;
ex D be Division of [' c,b '] st D = T2.i0 & 1 <= len D by A54;
then len S2 in Seg len S2;
then
A62: len S2 in dom S2 by FINSEQ_1:def 3;
A63: rng S1 c= [' a,c '] by INTEGRA1:def 2;
now
let i,j be Nat;
assume that
A64: i in dom T and
A65: j in dom T and
A66: i < j;
A67: 1 <= i by A64,FINSEQ_3:25;
A68: j <= len T by A65,FINSEQ_3:25;
A69: i <= len T by A64,FINSEQ_3:25;
A70: now
j <= len S1 + len S2 by A68,FINSEQ_1:22;
then
A71: j-len S1 <= len S2 by XREAL_1:20;
assume
A72: j > len S1;
then
A73: T.j = S2.(j-len S1) by A68,FINSEQ_1:24;
A74: len S1 + 1 <=j by A72,NAT_1:13;
then consider m be Nat such that
A75: (len S1 + 1)+m=j by NAT_1:10;
reconsider m as Element of NAT by ORDINAL1:def 12;
1+m = j - len S1 by A75;
then 1 <= 1+m by A74,XREAL_1:19;
then 1+m in Seg len S2 by A75,A71;
then
A76: j - len S1 in dom S2 by A75,FINSEQ_1:def 3;
A77: now
i <= len S1 + len S2 by A69,FINSEQ_1:22;
then
A78: i-len S1 <= len S2 by XREAL_1:20;
A79: i - len S1 < j -len S1 by A66,XREAL_1:14;
assume
A80: i > len S1;
then
A81: len S1 + 1 <=i by NAT_1:13;
then consider m be Nat such that
A82: (len S1 + 1)+m=i by NAT_1:10;
reconsider m as Element of NAT by ORDINAL1:def 12;
1+m = i - len S1 by A82;
then 1 <= 1+m by A81,XREAL_1:19;
then 1+m in Seg len S2 by A82,A78;
then
A83: i - len S1 in dom S2 by A82,FINSEQ_1:def 3;
T.i = S2.(i-len S1) by A69,A80,FINSEQ_1:24;
hence T.i < T.j by A73,A76,A79,A83,SEQM_3:def 1;
end;
now
assume i <= len S1;
then
A84: i in dom S1 by A67,FINSEQ_3:25;
then T.i = S1.i by FINSEQ_1:def 7;
then T.i in rng S1 by A84,FUNCT_1:def 3;
then
A85: T.i <= c by A14,A63,XXREAL_1:1;
ex DD be Division of [' c,b '] st DD = T2.i0 & for k be
Element of NAT st k in dom DD holds c < DD.k by A39;
hence T.i < T.j by A73,A76,A85,XXREAL_0:2;
end;
hence T.i < T.j by A77;
end;
A86: 1 <= j by A65,FINSEQ_3:25;
now
assume
A87: j <= len S1;
then
A88: j in dom S1 by A86,FINSEQ_3:25;
then
A89: T.j = S1.j by FINSEQ_1:def 7;
i <= len S1 by A66,A87,XXREAL_0:2;
then
A90: i in dom S1 by A67,FINSEQ_3:25;
then T.i = S1.i by FINSEQ_1:def 7;
hence T.i < T.j by A66,A90,A88,A89,SEQM_3:def 1;
end;
hence T.i < T.j by A70;
end;
then
A91: T is non empty increasing FinSequence of REAL by SEQM_3:def 1;
rng S2 c= [' c,b '] by INTEGRA1:def 2;
then rng S1 \/ rng S2 c= [' a,c '] \/ [' c,b '] by A63,XBOOLE_1:13;
then rng S1 \/ rng S2 c=[.a,b.] by A13,A8,A14,A9,XXREAL_1:174;
then
A92: rng T c= [' a,b '] by A7,FINSEQ_1:31;
T.(len T) = T.(len S1 + len S2) by FINSEQ_1:22
.= S2.(len S2) by A62,FINSEQ_1:def 7
.= upper_bound [' a,b '] by A60,A11,INTEGRA1:def 2;
then T is Division of [' a,b '] by A92,A91,INTEGRA1:def 2;
then T is Element of divs [' a,b '] by INTEGRA1:def 3;
hence thesis;
end;
consider T be DivSequence of [' a,b '] such that
A93: for i be Element of NAT holds P2[i,T.i] from FUNCT_2:sch 3(A61);
A94: lower_bound [' a,b '] = a by A7,A59,INTEGRA1:5;
A95: for i, k be Element of NAT, S0 be Division of [' a,c '] st S0=T1.i & k
in Seg len S0 holds divset(T.i,k) = divset(T1.i,k)
proof
let i,k be Element of NAT, S0 be Division of [' a,c '];
assume
A96: S0=T1.i;
reconsider S=T.i as Division of [' a,b '];
A97: divset(T1.i,k) =
[. lower_bound divset(T1.i,k),upper_bound divset(T1.i,k).] by INTEGRA1:4;
consider S1 be Division of [' a,c '], S2 be Division of [' c,b '] such
that
A98: S1=T1.i and
S2=T2.i and
A99: T.i=S1^S2 by A93;
assume
A100: k in Seg len S0;
then
A101: k in dom S1 by A96,A98,FINSEQ_1:def 3;
len S = len S1 + len S2 by A99,FINSEQ_1:22;
then len S1 <= len S by NAT_1:11;
then Seg len S1 c= Seg len S by FINSEQ_1:5;
then k in Seg len S by A96,A100,A98;
then
A102: k in dom S by FINSEQ_1:def 3;
A103: divset(T.i,k) =
[.lower_bound divset(T.i,k),upper_bound divset(T.i,k).] by INTEGRA1:4;
A104: now
k <= len S1 & k-1 <= k -0 by A96,A100,A98,FINSEQ_1:1,XREAL_1:10;
then
A105: k-1 <= len S1 by XXREAL_0:2;
assume
A106: k <> 1;
1 <=k by A100,FINSEQ_1:1;
then
A107: 1 < k by A106,XXREAL_0:1;
then 1+1 <= k by NAT_1:13;
then
A108: 2-1 <= k-1 by XREAL_1:9;
k-1 is Element of NAT by A107,NAT_1:20;
then k-1 in Seg len S1 by A105,A108;
then
A109: k-1 in dom S1 by FINSEQ_1:def 3;
thus divset(T.i,k) =[. S.(k-1),upper_bound divset(T.i,k) .]
by A102,A103,A106,INTEGRA1:def 4
.=[. S.(k-1),S.k .] by A102,A106,INTEGRA1:def 4
.=[. S.(k-1),S1.k .] by A99,A101,FINSEQ_1:def 7
.=[. S1.(k-1),S1.k .] by A99,A109,FINSEQ_1:def 7
.=[. lower_bound divset(T1.i,k),S1.k .] by A98,A101,A106,INTEGRA1:def 4
.= divset(T1.i,k) by A98,A101,A97,A106,INTEGRA1:def 4;
end;
now
assume
A110: k=1;
hence divset(T.i,k) =[. lower_bound[' a,b '],upper_bound divset(T.i,k) .]
by A102,A103,INTEGRA1:def 4
.=[. lower_bound[' a,b '],S.k .] by A102,A110,INTEGRA1:def 4
.=[. lower_bound[' a,b '],S1.k .] by A99,A101,FINSEQ_1:def 7
.=[. lower_bound divset(T1.i,k),S1.1 .]
by A94,A16,A98,A101,A110,INTEGRA1:def 4
.= divset(T1.i,k) by A98,A101,A97,A110,INTEGRA1:def 4;
end;
hence thesis by A104;
end;
A111: upper_bound [' a,c '] = c by A14,A15,INTEGRA1:5;
A112: for i, k be Element of NAT, S01 be Division of [' a,c '], S02 be
Division of [' c,b '] st S01=T1.i & S02=T2.i & k in Seg len S02 holds divset(T.
i,(len S01 + k)) = divset(T2.i,k)
proof
let i,k be Element of NAT, S01 be Division of [' a,c '], S02 be Division
of [' c,b '];
assume that
A113: S01=T1.i and
A114: S02=T2.i;
reconsider S=T.i as Division of [' a,b '];
consider S1 be Division of [' a,c '], S2 be Division of [' c,b '] such
that
A115: S1=T1.i and
A116: S2=T2.i and
A117: T.i = S1^S2 by A93;
assume
A118: k in Seg len S02;
then
A119: k in dom S2 by A114,A116,FINSEQ_1:def 3;
then
A120: len S1 + k in dom S by A117,FINSEQ_1:28;
A121: divset(T2.i,k) =
[. lower_bound divset(T2.i,k), upper_bound divset(T2.i,k).] by INTEGRA1:4;
A122: divset(T.i,(len S1 + k)) =
[.lower_bound divset(T.i,(len S1 + k)), upper_bound divset
(T .i,(len S1 + k)).] by INTEGRA1:4;
A123: now
k <= len S2 & k-1 <= k -0 by A114,A118,A116,FINSEQ_1:1,XREAL_1:10;
then
A124: k-1 <= len S2 by XXREAL_0:2;
assume
A125: k <> 1;
A126: 1 <=k by A118,FINSEQ_1:1;
then
A127: 1 < k by A125,XXREAL_0:1;
then 1+1 <= k by NAT_1:13;
then
A128: 2-1 <= k-1 by XREAL_1:9;
k-1 is Element of NAT by A127,NAT_1:20;
then k-1 in Seg len S2 by A124,A128;
then
A129: k-1 in dom S2 by FINSEQ_1:def 3;
A130: 1+0 < k + len S1 by A126,XREAL_1:8;
hence divset(T.i,(len S1 + k)) =
[. S.(len S1 + k-1),upper_bound divset(T.i,len S1
+ k) .] by A120,A122,INTEGRA1:def 4
.=[. S.(len S1 + k-1),S.(len S1 + k) .] by A120,A130,INTEGRA1:def 4
.=[. S.(len S1 + (k-1)),S2.k .] by A117,A119,FINSEQ_1:def 7
.=[. S2.(k-1),S2.k .] by A117,A129,FINSEQ_1:def 7
.=[. lower_bound divset(T2.i,k), S2.k .]
by A116,A119,A125,INTEGRA1:def 4
.= divset(T2.i,k) by A116,A119,A121,A125,INTEGRA1:def 4;
end;
now
len S1 in Seg len S1 by FINSEQ_1:3;
then
A131: len S1 in dom S1 by FINSEQ_1:def 3;
assume
A132: k=1;
len S1 <> 0;
then
A133: len S1 + k <> 1 by A132;
hence
divset(T.i,(len S1 + k)) =
[. S.(len S1 + k-1),upper_bound divset(T.i,len S1
+ k) .] by A120,A122,INTEGRA1:def 4
.=[. S1.(len S1),upper_bound divset(T.i,len S1 +k) .]
by A117,A132,A131,FINSEQ_1:def 7
.=[. upper_bound ([' a,c ']), upper_bound divset(T.i,len S1 + k) .]
by INTEGRA1:def 2
.=[. lower_bound ([' c,b ']), S.(len S1 + k) .] by A19,A111,A120,A133,
INTEGRA1:def 4
.=[. lower_bound [' c,b '], S2.k .] by A117,A119,FINSEQ_1:def 7
.=[. lower_bound divset(T2.i,k), S2.1 .]
by A116,A119,A132,INTEGRA1:def 4
.= divset(T2.i,k) by A116,A119,A121,A132,INTEGRA1:def 4;
end;
hence thesis by A113,A115,A123;
end;
set XAB = chi([' a,b '],[' a,b ']);
A134: for i, k be Element of NAT, S0 be Division of [' c,b '] st S0=T2.i & k
in Seg len S0 holds divset(T2.i,k) c= [' c,b ']
proof
let i,k be Element of NAT, S0 be Division of [' c,b '];
assume that
A135: S0=T2.i and
A136: k in Seg len S0;
k in dom S0 by A136,FINSEQ_1:def 3;
hence thesis by A135,INTEGRA1:8;
end;
A137: [' a,c '] c= [' a,b '] by A7,A8,A14,XXREAL_1:34;
then f|[' a,c '] is bounded by A4,RFUNCT_1:74;
then
A138: FAC|[' a,c '] is bounded;
A139: for i,k be Element of NAT, S0 be Division of [' a,c '] st S0=T1.i & k
in Seg len S0 holds divset(T1.i,k) c= [' a,c ']
proof
let i,k be Element of NAT, S0 be Division of [' a,c '];
assume that
A140: S0=T1.i and
A141: k in Seg (len S0);
k in dom S0 by A141,FINSEQ_1:def 3;
hence thesis by A140,INTEGRA1:8;
end;
A142: for i be Element of NAT holds upper_volume(f||[' a,b '],T.i) = (
upper_volume(FAC,T1.i))^(upper_volume(FCB,T2.i))
proof
let i be Element of NAT;
reconsider F = upper_volume(FAB,T.i) as FinSequence of REAL;
reconsider F1 = upper_volume(FAC,T1.i) as FinSequence of REAL;
reconsider F2 = upper_volume(FCB,T2.i) as FinSequence of REAL;
reconsider S=T.i as Division of [' a,b '];
consider S1 be Division of [' a,c '], S2 be Division of [' c,b '] such
that
A143: S1=T1.i and
A144: S2=T2.i and
A145: T.i =S1^S2 by A93;
A146: len F = len S by INTEGRA1:def 6
.= len S1+ len S2 by A145,FINSEQ_1:22
.= len F1 + len S2 by A143,INTEGRA1:def 6
.= len F1 + len F2 by A144,INTEGRA1:def 6;
A147: now
let k be Nat;
assume
A148: k in dom F2;
then
A149: k in Seg len F2 by FINSEQ_1:def 3;
then 1 <=k by FINSEQ_1:1;
then
A150: 1 + len F1 <= k + len F1 by XREAL_1:6;
k <= len F2 by A149,FINSEQ_1:1;
then
A151: len F1 + k <= len F by A146,XREAL_1:6;
1 <= 1+ len F1 by NAT_1:11;
then 1 <= k + len F1 by A150,XXREAL_0:2;
then k+ len F1 in Seg len F by A151;
then len F1 + k in Seg len S by INTEGRA1:def 6;
then len F1 + k in dom S by FINSEQ_1:def 3;
then
A152: F.(len F1 + k) =(upper_bound rng(FAB|divset(T.i,(len F1 + k)))) * vol
divset(T.i,len F1 + k) by INTEGRA1:def 6;
k in Seg len F2 by A148,FINSEQ_1:def 3;
then
A153: k in Seg len S2 by A144,INTEGRA1:def 6;
then
A154: k in dom S2 by FINSEQ_1:def 3;
len F1= len S1 by A143,INTEGRA1:def 6;
then
A155: divset(T.i,len F1 + k) = divset(T2.i,k) by A112,A143,A144,A153;
then
A156: divset(T.i,len F1 + k) c= [' c,b '] by A134,A144,A153;
then divset(T.i,len F1 + k) c= [' a,b '] by A17;
then F.(len F1 + k)=
(upper_bound rng(FCB|divset(T2.i,k))) * vol divset(T2.i,k)
by A152,A155,A156,Th3;
hence F.(len F1 + k) =F2.k by A144,A154,INTEGRA1:def 6;
end;
A157: now
let k be Nat;
assume k in dom F1;
then
A158: k in Seg len F1 by FINSEQ_1:def 3;
then
A159: k in Seg(len S1) by A143,INTEGRA1:def 6;
then
A160: k in dom S1 by FINSEQ_1:def 3;
len F1 <= len F by A146,NAT_1:11;
then Seg len F1 c= Seg len F by FINSEQ_1:5;
then k in Seg len F by A158;
then k in Seg(len S) by INTEGRA1:def 6;
then k in dom S by FINSEQ_1:def 3;
then
A161: F.k = (upper_bound rng(FAB|divset(T.i,k)))*vol divset(T.i,k) by
INTEGRA1:def 6;
A162: divset(T.i,k) = divset(T1.i,k) by A95,A143,A159;
then
A163: divset(T.i,k) c= [' a,c '] by A139,A143,A159;
then divset(T.i,k) c= [' a,b '] by A137;
then F.k =
(upper_bound rng(FAC|divset(T1.i,k))) * vol divset(T1.i,k) by A161,A162
,A163,Th3;
hence F.k = F1.k by A143,A160,INTEGRA1:def 6;
end;
dom F = Seg (len F1 + len F2) by A146,FINSEQ_1:def 3;
hence thesis by A157,A147,FINSEQ_1:def 7;
end;
A164: for i be Element of NAT holds Sum upper_volume(FAB,T.i) = Sum
upper_volume(FAC,T1.i) + Sum upper_volume(FCB,T2.i)
proof
let i be Element of NAT;
upper_volume(FAB,T.i) = (upper_volume(FAC,T1.i))^(upper_volume(FCB,
T2.i) ) by A142;
hence thesis by RVSUM_1:75;
end;
now
let i be Nat;
reconsider ii=i as Element of NAT by ORDINAL1:def 12;
thus upper_sum(FAB,T).i =upper_sum(FAB,T.ii) by INTEGRA2:def 2
.=upper_sum(FAC,T1.ii) +Sum(upper_volume(FCB,T2.ii)) by A164
.=upper_sum(FAC,T1).i + upper_sum(FCB,T2.ii) by INTEGRA2:def 2
.=upper_sum(FAC,T1).i +upper_sum(FCB,T2).i by INTEGRA2:def 2;
end;
then
A165: upper_sum(FAB,T) = upper_sum(FAC,T1) +upper_sum(FCB,T2) by SEQ_1:7;
A166: FCB is Function of [' c,b '],REAL by A2,A17,Lm1,XBOOLE_1:1;
then
A167: lower_integral FCB <= upper_integral FCB by A18,INTEGRA1:49;
A168: now
let e be Real;
assume 0 < e;
then consider m be Nat such that
A169: for n be Nat st m <= n holds |.delta(PS2).n -0 .| < e
by A25,SEQ_2:def 7;
take m;
hereby
let n be Nat;
A170: n <=n+K by NAT_1:11;
assume m <=n;
then m <=n+K by A170,XXREAL_0:2;
then |.delta(PS2).(n+K) -0 .| < e by A169;
then
A171: |.delta(PS2.(n+K)) -0 .| < e by INTEGRA3:def 2;
n in NAT by ORDINAL1:def 12;
then ex k being Element of NAT, e1 being Division of [' c,b '] st k = n
& e1 =S2.n & e1 = PS2.(k+K) by A29;
hence |.delta(S2).n -0 .| < e by A171,INTEGRA3:def 2;
end;
end;
A172: now
let e be Real;
assume
A173: e > 0;
then consider m be Nat such that
A174: for n be Nat st m <=n holds |. delta(S2).n - 0 .| < e
/2 by A168,XREAL_1:215;
take m;
A175: e/2 < e by A173,XREAL_1:216;
let nn be Nat;
assume
A176: m <=nn;
reconsider n=nn as Element of NAT by ORDINAL1:def 12;
|. delta(S2).n - 0 .| < e/2 by A174,A176;
then 0 <= delta(S2.n) & |.delta(S2.n).| < e/2 by INTEGRA3:9,def 2;
then
A177: max rng upper_volume(XCB,S2.n) < e/2 by ABSVALUE:def 1;
A178: for y be Real st y in rng upper_volume(XCB,T2.n) holds y < e
proof
reconsider D=T2.n as Division of [' c,b '];
let y be Real;
assume y in rng upper_volume(XCB,T2.n);
then consider x be object such that
A179: x in dom upper_volume(XCB,T2.n) and
A180: y=(upper_volume(XCB,T2.n)).x by FUNCT_1:def 3;
reconsider i=x as Element of NAT by A179;
A181: x in Seg len upper_volume(XCB,T2.n) by A179,FINSEQ_1:def 3;
consider E1 be Division of [' c,b '] such that
A182: E1=S2.n and
A183: 2 <= len E1 by A30;
set i1=i+1;
consider E be Division of [' c,b '] such that
A184: E=S2.n and
A185: T2.n=E/^1 by A38;
A186: 1 <= len E1 by A183,XXREAL_0:2;
then
A187: len D = len E -1 by A184,A185,A182,RFINSEQ:def 1;
A188: len (upper_volume(XCB,T2.n)) = len D by INTEGRA1:def 6;
then
A189: dom (upper_volume(XCB,T2.n)) = dom D by FINSEQ_3:29;
A190: now
len(upper_volume(XCB,S2.n)) = len E by A184,INTEGRA1:def 6;
then 2 in Seg len (upper_volume(XCB,S2.n)) by A184,A182,A183;
then 2 in dom upper_volume(XCB,S2.n) by FINSEQ_1:def 3;
then (upper_volume(XCB,S2.n)).2 in rng upper_volume(XCB,S2.n) by
FUNCT_1:def 3;
then (upper_volume(XCB,S2.n)).2 <= max rng upper_volume(XCB,S2.n)
by XXREAL_2:def 8;
then
A191: (upper_volume(XCB,S2.n)).2 < e/2 by A177,XXREAL_0:2;
assume
A192: i = 1;
then
A193: 1 in dom D by A181,A188,FINSEQ_1:def 3;
len(upper_volume(XCB,S2.n))= len D + 1 by A184,A187,INTEGRA1:def 6;
then len(upper_volume(XCB,S2.n)) = len (upper_volume(XCB,T2.n)) + 1
by INTEGRA1:def 6;
then 1 in Seg len(upper_volume(XCB,S2.n)) by A181,A192,FINSEQ_2:8;
then 1 in dom upper_volume(XCB,S2.n) by FINSEQ_1:def 3;
then (upper_volume(XCB,S2.n)).1 in rng upper_volume(XCB,S2.n) by
FUNCT_1:def 3;
then (upper_volume(XCB,S2.n)).1 <= max rng upper_volume(XCB,S2.n)
by XXREAL_2:def 8;
then
A194: (upper_volume(XCB,S2.n)).1 < e/2 by A177,XXREAL_0:2;
A195: 2 in dom E by A184,A182,A183,FINSEQ_3:25;
1 in Seg len E by A184,A182,A186;
then
A196: 1 in dom E by FINSEQ_1:def 3;
divset(S2.n,1) =
[. lower_bound divset(S2.n,1),upper_bound divset(S2.n,1) .]
by INTEGRA1:4;
then
A197: divset(S2.n,1) =
[. lower_bound([' c,b ']),upper_bound divset(S2.n,1) .] by A184,A196,
INTEGRA1:def 4;
then
A198: [. lower_bound([' c,b ']),upper_bound divset(S2.n,1) .]
= [.lower_bound([. lower_bound([' c,b
']),upper_bound divset(S2.n,1) .]), upper_bound([. lower_bound([' c,b ']),
upper_bound divset(S2.n,1) .]).] by INTEGRA1:4;
A199: divset((T2.n),i) =
[. lower_bound(divset((T2.n),1)),upper_bound(divset((T2.n),
1)) .] by A192,INTEGRA1:4
.= [. lower_bound([' c,b ']),upper_bound(divset((T2.n),1)) .]
by A193,INTEGRA1:def 4
.= [. lower_bound([' c,b ']),D.1 .] by A193,INTEGRA1:def 4
.= [. lower_bound([' c,b ']),E.(1+1) .]
by A184,A185,A182,A186,A193,RFINSEQ:def 1
.= [. lower_bound([' c,b ']),upper_bound(divset((S2.n),2)) .]
by A184,A195,INTEGRA1:def 4;
then [. lower_bound([' c,b ']),upper_bound(divset((S2.n),2)) .]
= [.lower_bound([. lower_bound([' c
,b ']),upper_bound(divset((S2.n),2)) .]),
upper_bound([. lower_bound([' c,b ']),upper_bound(divset((S2.n),2))
.]).] by INTEGRA1:4;
then
A200: lower_bound([' c,b '])=lower_bound([. lower_bound([' c,b ']),
upper_bound(divset(( S2.n),2)) .]
) & upper_bound(divset ((S2.n),2)) =upper_bound([. lower_bound([' c,b ']),
upper_bound(divset((S2.n),2)) .]) by A199,INTEGRA1:5;
y =vol divset(T2.n,1) by A179,A180,A189,A192,INTEGRA1:20;
then y =(upper_bound divset(S2.n,2)-upper_bound divset(S2.n,1)) +
(upper_bound([. lower_bound([' c,
b ']),upper_bound divset(S2.n,1) .])-lower_bound([' c,b ']))
by A192,A199,A200,A197;
then
A201: y =(upper_bound divset(S2.n,2) - upper_bound divset(S2.n,1))
+ vol divset(S2.n
,1) by A197,A198,INTEGRA1:5;
divset(S2.n,2) = [. lower_bound divset(S2.n,2),
upper_bound divset(S2.n,2) .] by INTEGRA1:4;
then divset(S2.n,2) = [. E.(2-1),upper_bound divset(S2.n,2) .]
by A184,A195,INTEGRA1:def 4;
then
A202: divset(S2.n,2) = [. upper_bound divset(S2.n,1),
upper_bound divset( S2.n,2) .]
by A184,A196,INTEGRA1:def 4;
then [. upper_bound divset(S2.n,1) ,upper_bound divset(S2.n,2) .]
= [.lower_bound([. upper_bound
divset(S2.n,1) ,upper_bound divset(S2.n,2) .]),
upper_bound([. upper_bound divset(S2.n,1) ,upper_bound divset(
S2.n,2) .]).] by INTEGRA1:4;
then y = vol divset(S2.n,2) + vol divset(S2.n,1) by A202,A201,
INTEGRA1:5;
then y = (upper_volume(XCB,S2.n)).2 + vol divset(S2.n,1) by A184,A195
,INTEGRA1:20;
then y = (upper_volume(XCB,S2.n)).2 + (upper_volume(XCB,S2.n)).1 by
A184,A196,INTEGRA1:20;
then y < (e/2)+(e/2) by A191,A194,XREAL_1:8;
hence thesis;
end;
A203: y=( upper_bound rng(XCB|divset(T2.n,i)) ) * vol divset(T2.n,i) by A179
,A180,A189,INTEGRA1:def 6;
now
len upper_volume(XCB,S2.n) = len D +1 by A184,A187,INTEGRA1:def 6;
then len upper_volume(XCB,S2.n) = len (upper_volume(XCB,T2.n)) + 1
by INTEGRA1:def 6;
then
A204: i1 in Seg len (upper_volume(XCB,S2.n)) by A181,FINSEQ_1:60;
then
A205: i1 in dom upper_volume(XCB,S2.n) by FINSEQ_1:def 3;
A206: i1 in dom upper_volume(XCB,S2.n) by A204,FINSEQ_1:def 3;
A207: i in dom D by A181,A188,FINSEQ_1:def 3;
Seg (len D + 1) = Seg len E by A187;
then i1 in Seg len E by A181,A188,FINSEQ_1:60;
then
A208: i1 in dom E by FINSEQ_1:def 3;
len upper_volume(XCB,S2.n) = len E by A184,INTEGRA1:def 6;
then
A209: dom upper_volume(XCB,S2.n) = dom E by FINSEQ_3:29;
assume
A210: i <> 1;
i in Seg len D by A179,A188,FINSEQ_1:def 3;
then 1 <= i by FINSEQ_1:1;
then
A211: 1 < i by A210,XXREAL_0:1;
then
A212: i-1 in Seg len D by A181,A188,FINSEQ_3:12;
then
A213: i-1 in dom D by FINSEQ_1:def 3;
reconsider i9 = i-1 as Element of NAT by A212;
1+1 < i+1 by A211,XREAL_1:8;
then
A214: i1 <> 1;
divset(T2.n,i) = [. lower_bound divset(T2.n,i),
upper_bound divset(T2.n,i) .] by INTEGRA1:4
.= [. D.(i-1),upper_bound divset(T2.n,i) .]
by A210,A207,INTEGRA1:def 4
.= [. D.(i-1),D.i .] by A210,A207,INTEGRA1:def 4
.= [. E.(i9+1),D.i .] by A184,A185,A182,A186,A213,RFINSEQ:def 1
.= [. E.((i-1)+1),E.(i+1) .] by A184,A185,A182,A186,A207,
RFINSEQ:def 1
.= [. E.(i1-1),upper_bound divset(S2.n,i1) .]
by A184,A214,A208,INTEGRA1:def 4
.= [. lower_bound divset(S2.n,i1),upper_bound divset(S2.n,i1) .]
by A184,A214,A208,INTEGRA1:def 4
.= divset(S2.n,i1) by INTEGRA1:4;
then y = (upper_volume(XCB,S2.n)).i1 by A203,A184,A205,A209,
INTEGRA1:def 6;
then y in rng upper_volume(XCB,S2.n) by A206,FUNCT_1:def 3;
then y <= max rng upper_volume(XCB,S2.n) by XXREAL_2:def 8;
then y < e/2 by A177,XXREAL_0:2;
hence thesis by A175,XXREAL_0:2;
end;
hence thesis by A190;
end;
max rng upper_volume(XCB,T2.n) in rng upper_volume(XCB,T2.n) by
XXREAL_2:def 8;
then 0 <= delta(T2.n) & delta(T2.n) < e by A178,INTEGRA3:9;
then |.delta(T2.n).| < e by ABSVALUE:def 1;
hence |.delta(T2).nn-0 .| < e by INTEGRA3:def 2;
end;
then
A215: delta T2 is convergent by SEQ_2:def 6;
then
A216: lim delta T2 =0 by A172,SEQ_2:def 7;
then
A217: upper_sum(FCB,T2) is convergent & lim upper_sum(FCB,T2) =
upper_integral FCB by A166,A18,A215,INTEGRA4:9;
A218: now
let e be Real;
assume
A219: 0 < e;
then consider n1 be Nat such that
A220: for m be Nat st n1 <= m holds |.delta(T1).m -0 .| < e by A53,SEQ_2:def 7;
consider n2 be Nat such that
A221: for m be Nat st n2 <= m holds |.delta(T2).m -0 .| < e by A172,A219;
reconsider n = max(n1,n2) as Nat by TARSKI:1;
take n;
let mm be Nat;
assume
A222: n <=mm;
reconsider m=mm as Element of NAT by ORDINAL1:def 12;
n2 <= n by XXREAL_0:25;
then n2 <= m by A222,XXREAL_0:2;
then |.delta(T2).m -0 .| < e by A221;
then
A223: |.delta(T2.m) .| < e by INTEGRA3:def 2;
0 <= delta(T2.m) by INTEGRA3:9;
then
A224: max rng upper_volume(XCB,T2.m) < e by A223,ABSVALUE:def 1;
n1 <= n by XXREAL_0:25;
then n1 <= m by A222,XXREAL_0:2;
then |.delta(T1).m -0 .| < e by A220;
then
A225: |.delta(T1.m) .| < e by INTEGRA3:def 2;
0 <= delta(T1.m) by INTEGRA3:9;
then
A226: max rng upper_volume(XAC,T1.m) < e by A225,ABSVALUE:def 1;
A227: for r be Real st r in rng upper_volume(XAB,T.m) holds r < e
proof
reconsider Tm=T.m as Division of [' a,b '];
let y be Real;
assume y in rng upper_volume(XAB,T.m);
then consider x be object such that
A228: x in dom upper_volume(XAB,T.m) and
A229: y = (upper_volume(XAB,T.m)).x by FUNCT_1:def 3;
reconsider i=x as Element of NAT by A228;
A230: x in Seg len (upper_volume(XAB,T.m)) by A228,FINSEQ_1:def 3;
then
A231: 1 <= i by FINSEQ_1:1;
A232: len(upper_volume(XAB,T.m)) =len Tm by INTEGRA1:def 6;
then
A233: i <= len Tm by A230,FINSEQ_1:1;
dom(upper_volume(XAB,T.m)) =dom Tm by A232,FINSEQ_3:29;
then
A234: y=(upper_bound rng(XAB|divset(T.m,i))) * vol divset(T.m,i)
by A228,A229,INTEGRA1:def 6;
consider S1 be Division of [' a,c '], S2 be Division of [' c,b '] such
that
A235: S1=T1.m and
A236: S2=T2.m and
A237: T.m = S1^S2 by A93;
A238: len Tm = len S1 + len S2 by A237,FINSEQ_1:22;
per cases;
suppose
i <= len S1;
then
A239: i in Seg len S1 by A231;
then
A240: i in dom S1 by FINSEQ_1:def 3;
len (upper_volume(XAC,T1.m)) = len S1 by A235,INTEGRA1:def 6;
then
A241: i in dom (upper_volume(XAC,T1.m)) by A239,FINSEQ_1:def 3;
A242: divset(T1.m,i) = divset(T.m,i) by A95,A235,A239;
A243: divset(T1.m,i) c= [' a,c '] by A139,A235,A239;
then divset(T1.m,i) c= [' a,b '] by A137;
then XAC|divset(T1.m,i) = XAB|divset(T.m,i) by A242,A243,Th4;
then y=(upper_volume(XAC,T1.m)).i by A234,A235,A240,A242,
INTEGRA1:def 6;
then y in rng upper_volume(XAC,T1.m) by A241,FUNCT_1:def 3;
then y <= max rng upper_volume(XAC,T1.m) by XXREAL_2:def 8;
hence thesis by A226,XXREAL_0:2;
end;
suppose
i > len S1;
then
A244: len S1 + 1 <=i by NAT_1:13;
then consider k be Nat such that
A245: (len S1 + 1)+k=i by NAT_1:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
set i1=1+k;
A246: i-len S1 <= len S2 by A238,A233,XREAL_1:20;
1+k = i - len S1 by A245;
then 1 <= 1+k by A244,XREAL_1:19;
then
A247: 1+k in Seg len S2 by A245,A246;
then
A248: 1+k in dom S2 by FINSEQ_1:def 3;
A249: divset(T2.m,i1) =divset(T.m,len S1 + i1) by A112,A235,A236,A247;
A250: divset(T2.m,i1) c= [' c,b '] by A134,A236,A247;
then divset(T2.m,i1) c= [' a,b '] by A17;
then y=(upper_bound rng(XCB|divset(T2.m,i1))) * vol divset(T2.m,i1)
by A234,A245,A249,A250,Th4;
then
A251: y=(upper_volume(XCB,T2.m)).i1 by A236,A248,INTEGRA1:def 6;
len (upper_volume(XCB,T2.m)) = len S2 by A236,INTEGRA1:def 6;
then i1 in dom (upper_volume(XCB,T2.m)) by A247,FINSEQ_1:def 3;
then y in rng upper_volume(XCB,T2.m) by A251,FUNCT_1:def 3;
then y <= max rng upper_volume(XCB,T2.m) by XXREAL_2:def 8;
hence thesis by A224,XXREAL_0:2;
end;
end;
A252: 0 <= delta(T.m) by INTEGRA3:9;
max rng upper_volume(XAB,T.m) in rng upper_volume(XAB,T.m) by
XXREAL_2:def 8;
then delta(T.m) < e by A227;
then |. delta(T.m) .| < e by A252,ABSVALUE:def 1;
hence |.delta(T).mm -0 .| < e by INTEGRA3:def 2;
end;
then
A253: delta T is convergent by SEQ_2:def 6;
then
A254: lim delta(T)=0 by A218,SEQ_2:def 7;
FAB|[' a,b '] is bounded by A4;
then
A255: upper_integral FAB = lim upper_sum(FAB,T) by A12,A253,A254,INTEGRA4:9;
A256: for i be Element of NAT holds lower_volume(FAB,T.i) =(lower_volume(FAC
,T1.i))^(lower_volume(FCB,T2.i))
proof
let i be Element of NAT;
reconsider F = lower_volume(FAB,T.i) as FinSequence of REAL;
reconsider F1 = lower_volume(FAC,T1.i) as FinSequence of REAL;
reconsider F2 = lower_volume(FCB,T2.i) as FinSequence of REAL;
reconsider S=T.i as Division of [' a,b '];
consider S1 be Division of [' a,c '], S2 be Division of [' c,b '] such
that
A257: S1=T1.i and
A258: S2=T2.i and
A259: T.i = S1^S2 by A93;
A260: len F = len S by INTEGRA1:def 7
.= len S1+ len S2 by A259,FINSEQ_1:22
.= len F1 + len S2 by A257,INTEGRA1:def 7;
then
A261: len F = len F1 + len F2 by A258,INTEGRA1:def 7;
A262: now
let k be Nat;
assume k in dom F2;
then
A263: k in Seg len F2 by FINSEQ_1:def 3;
then 1 <=k by FINSEQ_1:1;
then
A264: 1 + len F1 <= k + len F1 by XREAL_1:6;
k <= len F2 by A263,FINSEQ_1:1;
then
A265: len F1 + k <= len F by A261,XREAL_1:6;
1 <= 1+ len F1 by NAT_1:11;
then 1 <= k + len F1 by A264,XXREAL_0:2;
then k+ len F1 in Seg len F by A265;
then len F1 + k in Seg len S by INTEGRA1:def 7;
then len F1 + k in dom S by FINSEQ_1:def 3;
then
A266: F.(len F1 + k) = (lower_bound rng(FAB|divset(T.i,len F1 + k))) * vol
divset(T.i,(len F1 + k)) by INTEGRA1:def 7;
A267: k in Seg len S2 by A258,A263,INTEGRA1:def 7;
then
A268: k in dom S2 by FINSEQ_1:def 3;
len F1= len S1 by A257,INTEGRA1:def 7;
then
A269: divset(T.i,len F1 + k) = divset(T2.i,k) by A112,A257,A258,A267;
A270: divset(T2.i,k) c= [' c,b '] by A134,A258,A267;
then divset(T.i,len F1 + k) c= [' a,b '] by A17,A269;
then F.(len F1 + k)=
(lower_bound rng(FCB|divset(T2.i,k))) * vol divset(T2.i,k)
by A266,A269,A270,Th3;
hence F.(len F1 + k)=F2.k by A258,A268,INTEGRA1:def 7;
end;
A271: now
let k be Nat;
len lower_volume(FAB,T.i) = len S by INTEGRA1:def 7;
then
A272: dom lower_volume(FAB,T.i) = dom S by FINSEQ_3:29;
assume
A273: k in dom F1;
then k in Seg len F1 by FINSEQ_1:def 3;
then
A274: k in Seg len S1 by A257,INTEGRA1:def 7;
then
A275: k in dom S1 by FINSEQ_1:def 3;
len F1 <= len F by A260,NAT_1:11;
then dom F1 c= dom F by FINSEQ_3:30;
then
A276: F.k=(lower_bound rng(FAB|divset(T.i,k))) * vol divset(T.i,k) by A273,A272
,INTEGRA1:def 7;
A277: divset(T.i,k) = divset(T1.i,k) & divset(T1.i,k) c=[' a,c '] by A139,A95
,A257,A274;
then divset(T.i,k) c= [' a,b '] by A137;
then F.k=(lower_bound rng(FAC|divset(T1.i,k))) * vol divset(T1.i,k)
by A276,A277,Th3;
hence F.k=F1.k by A257,A275,INTEGRA1:def 7;
end;
dom F = Seg (len F1 + len F2) by A261,FINSEQ_1:def 3;
hence thesis by A271,A262,FINSEQ_1:def 7;
end;
A278: for i be Element of NAT holds Sum lower_volume(FAB,T.i) = Sum
lower_volume(FAC,T1.i) + Sum lower_volume(FCB,T2.i)
proof
let i be Element of NAT;
lower_volume(FAB,T.i) = (lower_volume(FAC,T1.i))^(lower_volume(FCB,
T2.i)) by A256;
hence thesis by RVSUM_1:75;
end;
now
let i be Nat;
reconsider ii=i as Element of NAT by ORDINAL1:def 12;
thus lower_sum(FAB,T).i =lower_sum(FAB,T.ii) by INTEGRA2:def 3
.=lower_sum(FAC,T1.ii) + Sum lower_volume(FCB,T2.ii) by A278
.=lower_sum(FAC,T1).i + lower_sum(FCB,T2.ii) by INTEGRA2:def 3
.=lower_sum(FAC,T1).i + lower_sum(FCB,T2).i by INTEGRA2:def 3;
end;
then
A279: lower_sum(FAB,T) = lower_sum(FAC,T1) + lower_sum(FCB,T2) by SEQ_1:7;
A280: FAC is Function of [' a,c '],REAL by A2,A137,Lm1,XBOOLE_1:1;
then
A281: FAC is upper_integrable & FAC is lower_integrable by A138,INTEGRA4:10;
A282: upper_sum(FAC,T1) is convergent & lim upper_sum(FAC,T1) =
upper_integral FAC by A280,A138,A53,INTEGRA4:9;
then
A283: upper_integral FAC + upper_integral FCB = upper_integral FAB by A165,A217
,A255,SEQ_2:6;
A284: lower_sum(FAC,T1) is convergent & lim lower_sum(FAC,T1) =
lower_integral FAC by A280,A138,A53,INTEGRA4:8;
FAB|[' a,b '] is bounded by A4;
then
A285: lower_integral FAB = lim lower_sum(FAB,T) by A12,A253,A254,INTEGRA4:8;
lower_sum(FCB,T2) is convergent & lim lower_sum(FCB,T2) =
lower_integral FCB by A166,A18,A215,A216,INTEGRA4:8;
then
A286: lower_integral FAC + lower_integral FCB = lower_integral FAB by A279,A284
,A285,SEQ_2:6;
integral(f,a,b) = integral(f,[' a,b ']) by A1,INTEGRA5:def 4
.= integral FAC + integral FCB by A165,A282,A217,A255,SEQ_2:6;
hence integral(f,a,b) = integral(f,a,c) + integral(f,c,b) by A58,A57;
FAB is integrable by A3;
then
A287: upper_integral FAB = lower_integral FAB;
A288: FCB is upper_integrable & FCB is lower_integrable by A166,A18,INTEGRA4:10
;
A289: lower_integral FAC <= upper_integral FAC by A280,A138,INTEGRA1:49;
then lower_integral FCB = upper_integral FCB by A287,A283,A286,A167,Th1;
then
A290: FCB is integrable by A288;
lower_integral FAC = upper_integral FAC by A287,A283,A286,A289,A167,Th1;
then FAC is integrable by A281;
hence thesis by A290;
end;
theorem Th17:
a <= b & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded &
[' a,b '] c= dom f & c in [' a,b '] implies f is_integrable_on ['a,c '] & f
is_integrable_on ['c,b '] & integral(f,a,b )=integral(f,a,c )+integral(f,c,b)
proof
assume that
A1: a <= b and
A2: f is_integrable_on [' a,b '] and
A3: f|[' a,b '] is bounded & [' a,b '] c= dom f & c in [' a,b '];
now
assume
A4: b=c;
then
A5: [' c,b ']= [.c,b.] by INTEGRA5:def 3;
thus f is_integrable_on ['a,c '] by A2,A4;
[' c,b ']= [. lower_bound([' c,b ']),upper_bound([' c,b ']) .]
by INTEGRA1:4;
then lower_bound([' c,b ']) = c & upper_bound([' c,b ']) = b
by A5,INTEGRA1:5;
then
A6: vol(['c,b ']) =0 by A4;
then f||['c,b '] is integrable by INTEGRA4:6;
hence f is_integrable_on ['c,b '];
integral(f,c,b ) = integral(f,[' c,b '] ) by A5,INTEGRA5:19;
then integral(f,c,b ) =0 by A6,INTEGRA4:6;
hence integral(f, a,b )= integral(f,a,c ) +integral(f,c,b) by A4;
end;
hence thesis by A1,A2,A3,Lm2;
end;
Lm3: for a,b,c be Real st a <= c & c <= b holds c in [' a,b '] & [' a,c
'] c= [' a,b '] & [' c,b '] c= [' a,b ']
proof
let a,b,c be Real;
assume that
A1: a <= c and
A2: c <= b;
A3: c in [.a,b.] by A1,A2,XXREAL_1:1;
hence c in [' a,b '] by A1,A2,INTEGRA5:def 3,XXREAL_0:2;
A4: [' c,b '] = [.c,b.] by A2,INTEGRA5:def 3;
a <= b by A1,A2,XXREAL_0:2;
then
A5: a in [.a,b.] & b in [.a,b.] by XXREAL_1:1;
[' a,b '] = [.a,b.] & [' a,c '] = [.a,c.] by A1,A2,INTEGRA5:def 3,XXREAL_0:2;
hence thesis by A4,A3,A5,XXREAL_2:def 12;
end;
theorem Th18:
a <= c & c <= d & d <= b & f is_integrable_on [' a,b '] & f|[' a
,b '] is bounded & [' a,b '] c= dom f implies f is_integrable_on ['c,d '] & f|
[' c,d '] is bounded & ['c,d '] c= dom f
proof
assume that
A1: a <= c and
A2: c <= d and
A3: d <= b and
A4: f is_integrable_on [' a,b '] and
A5: f|[' a,b '] is bounded and
A6: [' a,b '] c= dom f;
a <= d by A1,A2,XXREAL_0:2;
then
A7: a <= b by A3,XXREAL_0:2;
A8: c <= b by A2,A3,XXREAL_0:2;
then c in [' a,b '] by A1,Lm3;
then
A9: f is_integrable_on ['c,b '] by A4,A5,A6,A7,Th17;
A10: d in [' c,b '] by A2,A3,Lm3;
A11: ['c,b '] c= [' a,b '] by A1,A8,Lm3;
then ['c,b '] c= dom f & f|[' c,b '] is bounded by A5,A6,RFUNCT_1:74;
hence f is_integrable_on ['c,d '] by A8,A10,A9,Th17;
[' c,d '] c= [' c,b '] by A2,A3,Lm3;
then
A12: [' c,d '] c= [' a,b '] by A11;
hence f|[' c,d '] is bounded by A5,RFUNCT_1:74;
thus thesis by A6,A12;
end;
theorem
a <= c & c <= d & d <= b & f is_integrable_on [' a,b '] & g
is_integrable_on [' a,b '] & f|[' a,b '] is bounded & g|[' a,b '] is bounded &
[' a,b '] c= dom f & [' a,b '] c= dom g implies f+g is_integrable_on ['c,d '] &
(f+g)|[' c,d '] is bounded
proof
assume that
A1: a <= c and
A2: c <= d & d <= b and
A3: f is_integrable_on [' a,b '] & g is_integrable_on [' a,b '] & f|[' a
,b '] is bounded & g|[' a,b '] is bounded and
A4: [' a,b '] c= dom f and
A5: [' a,b '] c= dom g;
A6: [' c,d '] c= [' c,b '] by A2,Lm3;
A7: f|[' c,d '] is bounded & g|[' c,d '] is bounded by A1,A2,A3,A4,A5,Th18;
c <=b by A2,XXREAL_0:2;
then
A8: ['c,b '] c= [' a,b '] by A1,Lm3;
then ['c,b '] c= dom f by A4;
then
A9: [' c,d '] c= dom f by A6;
['c,b '] c= dom g by A5,A8;
then
A10: [' c,d '] c= dom g by A6;
f is_integrable_on ['c,d '] & g is_integrable_on ['c,d '] by A1,A2,A3,A4,A5
,Th18;
hence f+g is_integrable_on ['c,d '] by A7,A9,A10,Th11;
(f+g)|([' c,d '] /\ ['c,d ']) is bounded by A7,RFUNCT_1:83;
hence thesis;
end;
Lm4: for a,b,c,d be Real, f be PartFunc of REAL,REAL st a<=b & c <=d &
f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & [' a,b '] c= dom f & c
in [' a,b '] & d in [' a,b '] holds integral(f,a,d)=integral(f,a,c)+integral(f,
c,d)
proof
let a,b,c,d be Real, f be PartFunc of REAL,REAL;
assume that
A1: a<=b and
A2: c <= d and
A3: f is_integrable_on [' a,b '] & f|[' a,b '] is bounded and
A4: [' a,b '] c= dom f and
A5: c in [' a,b '] and
A6: d in [' a,b '];
A7: f is_integrable_on [' a,d '] by A1,A3,A4,A6,Th17;
A8: [' a,b '] = [.a,b.] by A1,INTEGRA5:def 3;
then
A9: a <= d by A6,XXREAL_1:1;
A10: d <= b by A6,A8,XXREAL_1:1;
then [' a,d '] c= [' a,b '] by A9,Lm3;
then
A11: [' a,d '] c= dom f by A4;
a <= c by A5,A8,XXREAL_1:1;
then
A12: c in [' a,d '] by A2,Lm3;
f|[' a,d '] is bounded by A3,A4,A9,A10,Th18;
hence thesis by A9,A12,A11,A7,Th17;
end;
theorem Th20:
a<=b & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded &
[' a,b '] c= dom f & c in [' a,b '] & d in [' a,b '] implies integral(f,a,d)=
integral(f,a,c)+integral(f,c,d)
proof
assume
A1: a<=b & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & [' a,
b '] c= dom f & c in [' a,b '] & d in [' a,b '];
now
assume
A2: not c <= d;
then integral(f,a,c)=integral(f,a,d)+integral(f,d,c) by A1,Lm4;
then
A3: integral(f,a,d) =integral(f,a,c) - integral(f,d,c);
integral(f,c,d) = -integral(f,[' d,c ']) by A2,INTEGRA5:def 4;
hence thesis by A2,A3,INTEGRA5:def 4;
end;
hence thesis by A1,Lm4;
end;
Lm5: for a,b,c,d be Real, f be PartFunc of REAL,REAL st a <= b & c <=d
& f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & [' a,b '] c= dom f &
c in [' a,b '] & d in [' a,b '] holds [' c,d '] c= dom abs f & abs f
is_integrable_on [' c,d '] & abs f|[' c,d '] is bounded & |.integral(f,c,d).|
<= integral(abs f,c,d)
proof
let a,b,c,d be Real, f be PartFunc of REAL,REAL such that
A1: a <= b and
A2: c <= d and
A3: f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & [' a,b '] c=
dom f and
A4: c in [' a,b '] & d in [' a,b '];
[' a,b '] = [.a,b.] by A1,INTEGRA5:def 3;
then
A5: a<=c & d <= b by A4,XXREAL_1:1;
then
A6: f|[' c,d '] is bounded by A2,A3,Th18;
[' c,d '] c= dom f & f is_integrable_on [' c,d '] by A2,A3,A5,Th18;
hence thesis by A2,A6,Th7,Th8,RFUNCT_1:82,VALUED_1:def 11;
end;
theorem Th21:
a <= b & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded &
[' a,b '] c= dom f & c in [' a,b '] & d in [' a,b '] implies [' min(c,d),max(c,
d) '] c= dom (abs f) & abs f is_integrable_on [' min(c,d),max(c,d) '] & abs f|
[' min(c,d),max(c,d) '] is bounded & |.integral(f,c,d).| <= integral(abs f,min(
c,d),max(c,d))
proof
assume
A1: a <= b & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & ['
a,b '] c= dom f & c in [' a,b '] & d in [' a,b '];
A2: now
assume
A3: not c <= d;
then integral(f,c,d) = -integral(f,[' d,c ']) by INTEGRA5:def 4;
then integral(f,c,d) = -integral(f,d,c) by A3,INTEGRA5:def 4;
then
A4: |.integral(f,c,d).| = |.integral(f,d,c).| by COMPLEX1:52;
d = min(c,d) & c = max(c,d) by A3,XXREAL_0:def 9,def 10;
hence thesis by A1,A3,A4,Lm5;
end;
now
assume
A5: c <= d;
then c = min(c,d) & d = max(c,d) by XXREAL_0:def 9,def 10;
hence thesis by A1,A5,Lm5;
end;
hence thesis by A2;
end;
Lm6: a <= b & c <= d & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded &
[' a,b '] c= dom f & c in [' a,b '] & d in [' a,b '] implies [' c,d '] c= dom (
abs f) & abs f is_integrable_on [' c,d '] & abs f|[' c,d '] is bounded &
|.integral(f,c,d).| <= integral(abs f,c,d)
proof
assume that
A1: a<=b and
A2: c <= d and
A3: f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & [' a,b '] c=
dom f & c in [' a,b '] & d in [' a,b '];
min(c,d) = c & max(c,d) = d by A2,XXREAL_0:def 9,def 10;
hence thesis by A1,A3,Th21;
end;
Lm7: a <= b & c <= d & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded &
[' a,b '] c= dom f & c in [' a,b '] & d in [' a,b '] implies |.integral(f,d,c)
.| <= integral(abs f,c,d)
proof
assume that
A1: a<=b and
A2: c <= d and
A3: f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & [' a,b '] c=
dom f & c in [' a,b '] and
A4: d in [' a,b '];
A5: |.integral(f,c,d).| <= integral(abs f,c,d) & integral(f,c,d) = integral(
f,[' c,d ']) by A1,A2,A3,A4,Lm6,INTEGRA5:def 4;
per cases;
suppose
c = d;
hence thesis by A1,A3,Lm6;
end;
suppose
c <> d;
then c < d by A2,XXREAL_0:1;
then integral(f,d,c) = -integral(f,[' c,d ']) by INTEGRA5:def 4;
hence thesis by A5,COMPLEX1:52;
end;
end;
theorem
a <= b & c <= d & f is_integrable_on [' a,b '] & f|[' a,b '] is
bounded & [' a,b '] c= dom f & c in [' a,b '] & d in [' a,b '] implies [' c,d
'] c= dom (abs f) & abs f is_integrable_on [' c,d '] & abs f|[' c,d '] is
bounded & |.integral(f,c,d).| <= integral(abs f,c,d) & |.integral(f,d,c).| <=
integral(abs f,c,d) by Lm6,Lm7;
Lm8: ( a<=b & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & [' a,b
'] c= dom f & c in [' a,b '] & d in [' a,b '] & for x be Real st x in ['
min(c,d),max(c,d) '] holds |.f.x.| <= e ) implies |.integral(f,c,d).| <= e *
|.d-c.|
proof
set A = [' min(c,d),max(c,d) '];
assume that
A1: a<=b & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & [' a,
b '] c= dom f & c in [' a,b '] & d in [' a,b '] and
A2: for x be Real st x in [' min(c,d),max(c,d) '] holds |.f.x.|
<= e;
rng abs f c= REAL;
then
A3: abs f is Function of dom abs f,REAL by FUNCT_2:2;
[' min(c,d),max(c,d) '] c= dom (abs f) by A1,Th21;
then reconsider g =abs(f)||A as Function of A,REAL by A3,FUNCT_2:32;
A4: vol A = |.d-c.| by Th6;
abs f is_integrable_on A by A1,Th21;
then
A5: g is integrable;
reconsider e as Real;
consider h be Function of A,REAL such that
A6: rng h = {e} and
A7: h|A is bounded by INTEGRA4:5;
A8: now
let x be Real;
assume
A9: x in A;
then g.x = (abs f).x by FUNCT_1:49;
then
A10: g.x = |.f.x.| by VALUED_1:18;
h.x in {e} by A6,A9,FUNCT_2:4;
then h.x =e by TARSKI:def 1;
hence g.x <= h.x by A2,A9,A10;
end;
A11: |.integral(f,c,d).| <= integral(abs f,min(c,d),max(c,d)) by A1,Th21;
min(c,d) <= c & c <= max(c,d) by XXREAL_0:17,25;
then min(c,d) <= max(c,d) by XXREAL_0:2;
then
A12: integral(abs f,min(c,d),max(c,d)) = integral(abs f,A) by INTEGRA5:def 4;
abs f|A is bounded by A1,Th21;
then
A13: g|A is bounded;
h is integrable & integral h = e*vol A by A6,INTEGRA4:4;
then
integral(abs f,min(c,d),max(c,d)) <= e * |.d-c.| by A12,A7,A8,A5,A13,A4,
INTEGRA2:34;
hence thesis by A11,XXREAL_0:2;
end;
Lm9: ( a<=b & c <= d & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded &
[' a,b '] c= dom f & c in [' a,b '] & d in [' a,b '] & for x be Real st
x in [' c,d '] holds |.f.x.| <= e ) implies |.integral(f,c,d).| <= e * (d-c)
proof
assume that
A1: a<=b and
A2: c <= d and
A3: f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & [' a,b '] c=
dom f & c in [' a,b '] &( d in [' a,b '] & for x be Real st x in [' c,d
'] holds |.f.x.| <= e);
0 <= d - c by A2,XREAL_1:48;
then
A4: |.d-c.| = d-c by ABSVALUE:def 1;
min(c,d) = c & max(c,d) = d by A2,XXREAL_0:def 9,def 10;
hence thesis by A1,A3,A4,Lm8;
end;
Lm10: ( a<=b & c <= d & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded
& [' a,b '] c= dom f & c in [' a,b '] & d in [' a,b '] & for x be Real
st x in [' c,d '] holds |.f.x.| <= e ) implies |.integral(f,d,c).| <= e * (d-c
)
proof
assume that
A1: a<=b and
A2: c <= d and
A3: f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & [' a,b '] c=
dom f & c in [' a,b '] and
A4: d in [' a,b '] and
A5: for x be Real st x in [' c,d '] holds |.f.x.| <= e;
A6: |.integral(f,c,d).| <= e * (d-c) & integral(f,c,d) = integral(f,[' c,d
']) by A1,A2,A3,A4,A5,Lm9,INTEGRA5:def 4;
per cases;
suppose
c = d;
hence thesis by A1,A3,A5,Lm9;
end;
suppose
c <> d;
then c < d by A2,XXREAL_0:1;
then integral(f,d,c) = -integral(f,[' c,d ']) by INTEGRA5:def 4;
hence thesis by A6,COMPLEX1:52;
end;
end;
theorem
( a<=b & c <= d & f is_integrable_on [' a,b '] & f|[' a,b '] is
bounded & [' a,b '] c= dom f & c in [' a,b '] & d in [' a,b '] & for x be Real
st x in [' c,d '] holds |.f.x.| <= e ) implies |.integral(f,c,d).| <= e
* (d-c) & |.integral(f,d,c).| <= e * (d-c) by Lm9,Lm10;
Lm11: for a,b,c,d be Real, f,g be PartFunc of REAL,REAL st a <= b & c
<= d & f is_integrable_on [' a,b '] & g is_integrable_on [' a,b '] & f|[' a,b
'] is bounded & g|[' a,b '] is bounded & [' a,b '] c= dom f & [' a,b '] c= dom
g & c in ['a,b '] & d in ['a,b '] holds f+g is_integrable_on ['c,d '] & (f+g)|
[' c,d '] is bounded & integral(f+g,c,d) =integral(f,c,d)+integral(g,c,d) & f-g
is_integrable_on ['c,d '] & (f-g)|[' c,d '] is bounded & integral(f-g,c,d) =
integral(f,c,d)-integral(g,c,d)
proof
let a,b,c,d be Real, f,g be PartFunc of REAL,REAL;
assume that
A1: a <= b and
A2: c <= d and
A3: f is_integrable_on [' a,b '] and
A4: g is_integrable_on [' a,b '] and
A5: f|[' a,b '] is bounded and
A6: g|[' a,b '] is bounded and
A7: [' a,b '] c= dom f and
A8: [' a,b '] c= dom g and
A9: c in ['a,b '] & d in ['a,b '];
['a,b '] = [.a,b.] by A1,INTEGRA5:def 3;
then
A10: a<=c & d <= b by A9,XXREAL_1:1;
then
A11: f is_integrable_on ['c,d '] & ['c,d '] c= dom f by A2,A3,A5,A7,Th18;
A12: g is_integrable_on ['c,d '] & ['c,d '] c= dom g by A2,A4,A6,A8,A10,Th18;
A13: f|[' c,d '] is bounded & g|[' c,d '] is bounded by A2,A3,A4,A5,A6,A7,A8
,A10,Th18;
then (f+g)|([' c,d '] /\ ['c,d ']) is bounded by RFUNCT_1:83;
hence thesis by A2,A11,A13,A12,Th11,Th12,RFUNCT_1:84;
end;
theorem Th24:
a <= b & f is_integrable_on [' a,b '] & g is_integrable_on [' a,
b '] & f|[' a,b '] is bounded & g|[' a,b '] is bounded & [' a,b '] c= dom f &
[' a,b '] c= dom g & c in ['a,b '] & d in ['a,b '] implies integral(f+g,c,d) =
integral(f,c,d) + integral(g,c,d) & integral(f-g,c,d) = integral(f,c,d) -
integral(g,c,d)
proof
assume
A1: a <= b & f is_integrable_on [' a,b '] & g is_integrable_on [' a,b ']
& f| [' a,b '] is bounded & g|[' a,b '] is bounded & [' a,b '] c= dom f & [' a,
b '] c= dom g & c in ['a,b '] & d in ['a,b '];
now
assume
A2: not c <= d;
then
A3: integral(f,c,d) = -integral(f,[' d,c ']) by INTEGRA5:def 4;
A4: integral(g,c,d) = -integral(g,[' d,c ']) by A2,INTEGRA5:def 4;
integral(f+g,c,d) = -integral(f+g,[' d,c ']) by A2,INTEGRA5:def 4;
hence integral(f+g,c,d) = -integral(f+g,d,c) by A2,INTEGRA5:def 4
.= -(integral(f,d,c)+integral(g,d,c)) by A1,A2,Lm11
.= -integral(f,d,c)-integral(g,d,c)
.= integral(f,c,d) -integral(g,d,c) by A2,A3,INTEGRA5:def 4
.= integral(f,c,d) +integral(g,c,d) by A2,A4,INTEGRA5:def 4;
integral(f-g,c,d) = -integral(f-g,[' d,c ']) by A2,INTEGRA5:def 4;
hence integral(f-g,c,d) =-integral(f-g,d,c) by A2,INTEGRA5:def 4
.= -(integral(f,d,c)-integral(g,d,c)) by A1,A2,Lm11
.= -(integral(f,d,c)+integral(g,c,d)) by A2,A4,INTEGRA5:def 4
.=-integral(f,d,c)-integral(g,c,d)
.= integral(f,c,d) -integral(g,c,d) by A2,A3,INTEGRA5:def 4;
end;
hence thesis by A1,Lm11;
end;
Lm12: for a,b,c,d,e be Real, f be PartFunc of REAL,REAL st a <= b & c
<= d & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & [' a,b '] c= dom
f & c in ['a,b '] & d in ['a,b '] holds integral(e(#)f,c,d)=e*integral(f,c,d)
proof
let a,b,c,d,e be Real, f be PartFunc of REAL,REAL;
assume that
A1: a <= b and
A2: c <= d and
A3: f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & [' a,b '] c=
dom f and
A4: c in ['a,b '] & d in ['a,b '];
['a,b '] = [.a,b.] by A1,INTEGRA5:def 3;
then
A5: a <= c & d <= b by A4,XXREAL_1:1;
then
A6: ['c,d '] c= dom f by A2,A3,Th18;
f is_integrable_on ['c,d '] & f|[' c,d '] is bounded by A2,A3,A5,Th18;
hence thesis by A2,A6,Th10;
end;
theorem
a <= b & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded &
[' a,b '] c= dom f & c in ['a,b '] & d in ['a,b '] implies
integral(e(#)f,c,d) = e*integral(f,c,d)
proof
assume
A1: a <= b & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & ['
a,b '] c= dom f & c in ['a,b '] & d in ['a,b '];
now
assume
A2: not c <= d;
then
A3: integral(f,c,d) = -integral(f,[' d,c ']) by INTEGRA5:def 4;
thus integral(e(#)f,c,d) = -integral(e(#)f,[' d,c ']) by A2,INTEGRA5:def 4
.= -integral(e(#)f,d,c) by A2,INTEGRA5:def 4
.= -e*integral(f,d,c) by A1,A2,Lm12
.= e*(-integral(f,d,c))
.= e*integral(f,c,d) by A2,A3,INTEGRA5:def 4;
end;
hence thesis by A1,Lm12;
end;
theorem Th26:
for a,b,r be Real, f be PartFunc of REAL,REAL
st a <= b & ['a,b'] c= dom f
& for t be Real st t in ['a,b'] holds f.t = r
holds
f | ['a,b'] is continuous
& f | ['a,b'] is bounded
& f is_integrable_on ['a,b']
& integral(f,a,b) = r*(b-a)
proof
let a,b,r be Real, f be PartFunc of REAL,REAL;
assume
A1: a <= b & ['a,b'] c= dom f
& for t be Real st t in ['a,b'] holds f.t = r;
A2: dom(f | ['a,b']) = ['a,b'] by A1,RELAT_1:62;
for y be object
holds y in rng(f | ['a,b']) iff y in {r}
proof
let y be object;
hereby
assume y in rng(f | ['a,b']);
then consider x be object such that
A3: x in dom(f | ['a,b'])
& y = (f | ['a,b']).x by FUNCT_1:def 3;
reconsider x as Real by A2,A3;
y = f.x by A2,A3,FUNCT_1:49
.= r by A1,A2,A3;
hence y in {r} by TARSKI:def 1;
end;
assume y in {r}; then
A4: y = r by TARSKI:def 1;
A5: ['a,b'] = [.a,b.] by A1,INTEGRA5:def 3; then
y = f.a by A1,A4,XXREAL_1:1
.= (f | ['a,b']).a by A1,A5,FUNCT_1:49,XXREAL_1:1;
hence y in rng(f | ['a,b']) by A1,A2,A5,FUNCT_1:3,XXREAL_1:1;
end; then
A7: rng(f | ['a,b']) = {r} by TARSKI:2;
rng(f | ['a,b']) c= REAL; then
reconsider g = f || ['a,b'] as Function of ['a,b'],REAL by A2,FUNCT_2:2;
integral(g) = r * vol([' a,b ']) by A7,INTEGRA4:4
.= r * (b-a) by A1,Th5; then
integral(f,['a,b']) = r * (b-a);
hence thesis by A1,A7,FCONT_1:39,INTEGRA5:10,11,def 4;
end;
theorem Th27:
a <= b & (for x be Real st x in [' a,b '] holds f.x=e) &
[' a,b '] c= dom f & c in ['a,b '] & d in ['a,b '] implies
integral(f,c,d) = e*(d-c)
proof
assume that
A1: a<=b and
A2: for x be Real st x in [' a,b '] holds f.x=e and
A3: [' a,b '] c= dom f and
A4: c in ['a,b '] and
A5: d in ['a,b '];
A6: f is_integrable_on ['a,b '] & f|[' a,b '] is bounded by A1,A2,A3,Th26;
A7: ['a,b '] = [.a,b.] by A1,INTEGRA5:def 3;
then
A8: c <= b by A4,XXREAL_1:1;
A9: a <= c by A4,A7,XXREAL_1:1;
then
A10: ['c,b '] c= [' a,b '] by A8,Lm3;
A11: d <= b by A5,A7,XXREAL_1:1;
A12: a <= d by A5,A7,XXREAL_1:1;
A13: ['a,c '] c= [' a,b '] by A9,A8,Lm3;
per cases;
suppose
A14: c <= d;
then ['c,d '] c= [' c,b '] by A11,Lm3;
then ['c,d '] c= ['a,b '] by A10;
then
A15: for x be Real st x in ['c,d '] holds f.x=e by A2;
['c,d '] c= dom f by A3,A9,A11,A6,A14,Th18;
hence thesis by A14,A15,Th26;
end;
suppose
A16: not c <= d;
then ['d,c '] c= [' a,c '] by A12,Lm3;
then ['d,c '] c= ['a,b '] by A13;
then
A17: for x be Real st x in ['d,c '] holds f.x=e by A2;
integral(f,c,d) = -integral(f,[' d,c ']) by A16,INTEGRA5:def 4;
then
A18: integral(f,c,d) = -integral(f,d,c) by A16,INTEGRA5:def 4;
['d,c '] c= dom f by A3,A12,A8,A6,A16,Th18;
then integral(f,d,c) = e*(c-d) by A16,A17,Th26;
hence thesis by A18;
end;
end;
begin :: Fundamental Theorem of Calculus
theorem Th28:
for x0 be Real, F be PartFunc of REAL,REAL st a <= b & f
is_integrable_on [' a,b '] & f|[' a,b '] is bounded & [' a,b '] c= dom f & ].a,
b.[ c= dom F & (for x be Real st x in ].a,b.[ holds F.x = integral(f,a,x
)) & x0 in ].a,b.[ & f is_continuous_in x0 holds F is_differentiable_in x0 &
diff(F,x0)=f.x0
proof
deffunc F2(object) = 0;
let x0 be Real, F be PartFunc of REAL,REAL;
assume that
A1: a <= b and
A2: f is_integrable_on [' a,b '] and
A3: f|[' a,b '] is bounded and
A4: [' a,b '] c= dom f and
A5: ].a,b.[ c= dom F and
A6: for x be Real st x in ].a,b.[ holds F.x = integral(f,a,x) and
A7: x0 in ].a,b.[ and
A8: f is_continuous_in x0;
defpred C1[object] means (x0+In($1,REAL)) in ].a,b.[;
deffunc F0(Real)=In((f.x0)*$1,REAL);
consider L be Function of REAL,REAL such that
A9: for h be Element of REAL holds L.h=F0(h) from FUNCT_2:sch 4;
A10: for h be Real holds L.h=(f.x0)*h
proof let h be Real;
reconsider h as Element of REAL by XREAL_0:def 1;
L.h=F0(h) by A9;
hence thesis;
end;
reconsider L as PartFunc of REAL,REAL;
deffunc F1(object) = F.(x0+In($1,REAL))-F.x0-L.In($1,REAL);
reconsider L as LinearFunc by A10,FDIFF_1:def 3;
consider R be Function such that
A11: dom R=REAL & for x be object st x in REAL holds (C1[x] implies R.x =
F1(x)) & (not C1[x] implies R.x = F2(x)) from PARTFUN1:sch 1;
rng R c= REAL
proof
let y be object;
assume y in rng R;
then consider x be object such that
A12: x in dom R and
A13: y=R.x by FUNCT_1:def 3;
A14: not C1[x] implies R.x = F2(x) by A11,A12;
C1[x] implies R.x = F1(x) by A11,A12;
hence thesis by A13,A14,XREAL_0:def 1;
end;
then reconsider R as PartFunc of REAL,REAL by A11,RELSET_1:4;
A15: R is total by A11,PARTFUN1:def 2;
A16: [' a,b '] = [.a,b.] by A1,INTEGRA5:def 3;
A17: for h be 0-convergent non-zero Real_Sequence holds (h")(#)(R/*h) is
convergent & lim ((h")(#)(R/*h)) = 0
proof
let h be 0-convergent non-zero Real_Sequence;
A18: for e be Real st 0<e ex n be Nat st
for m be Nat st n <= m holds |.((h")(#)(R/*h)).m - 0 .| < e
proof
reconsider fx0 = f.x0 as Element of REAL by XREAL_0:def 1;
set g = REAL --> fx0;
let e0 be Real;
set e=e0/2;
A19: h is convergent & lim(h) = 0;
assume
A20: 0 < e0;
then 0 < e by XREAL_1:215;
then consider p be Real such that
A21: 0 < p and
A22: for t be Real st t in dom f & |.t - x0.| < p holds |.
f.t - f.x0.| < e by A8,FCONT_1:3;
A23: 0 < p/2 by A21,XREAL_1:215;
A24: p/2 < p by A21,XREAL_1:216;
consider N be Neighbourhood of x0 such that
A25: N c= ].a,b.[ by A7,RCOMP_1:18;
consider q be Real such that
A26: 0<q and
A27: N = ].x0-q,x0+q.[ by RCOMP_1:def 6;
A28: q/2 < q by A26,XREAL_1:216;
set r=min(p/2,q/2);
0 < q/2 by A26,XREAL_1:215;
then 0 < r by A23,XXREAL_0:15;
then consider n be Nat such that
A29: for m be Nat st n <= m holds |.h.m - 0 .|<r by A19,SEQ_2:def 7;
take n;
let m be Nat;
r <= q/2 by XXREAL_0:17;
then
A30: ].x0-r,x0+r.[ c= ].x0-q,x0+q.[ by A28,Th2,XXREAL_0:2;
assume n <= m;
then
A31: |.h.m - 0 .| < r by A29;
then |.(x0 + h.m)-x0.| < r;
then x0 + h.m in ].x0-r,x0+r.[ by RCOMP_1:1;
then
A32: x0 + h.m in ].x0-q,x0+q.[ by A30;
then
A33: x0+h.m in ].a,b.[ by A25,A27;
then x0+In(h.m,REAL) in ].a,b.[;
then R.(h.m)=F.(x0+In(h.m,REAL))-F.x0-L.In(h.m,REAL) by A11;
then R.(h.m)=F.(x0+h.m)-F.x0-L.In(h.m,REAL);
then R.(h.m) = F.(x0+h.m)-F.x0-L.(h.m);
then
A34: R.(h.m) = F.(x0+h.m)-F.x0-(f.x0)*h.m by A10;
F.(x0+h.m) = integral(f,a,x0+h.m) by A6,A25,A27,A32;
then
A35: R.(h.m) =integral(f,a,x0+h.m ) -integral(f,a,x0) -(f.x0)*h.m by A6,A7,A34
;
A36: dom g = REAL by FUNCT_2:def 1;
then [' a,b '] /\ [' a,b '] c= dom f /\ dom g by A4,XBOOLE_1:27;
then
A37: [' a,b '] c= dom (f-g) by VALUED_1:12;
A38: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
then
A39: integral(f,a,x0+h.m) = integral(f,a,x0) +integral(f,x0,x0+h.m) by A1,A2
,A3,A4,A7,A16,A33,Th20;
A40: r <= p/2 by XXREAL_0:17;
A41: for x be Real st x in [' min(x0,x0+h.m),max(x0,x0+h.m) ']
holds |.(f-g).x.| <= e
proof
let x be Real;
reconsider x1 = x as Real;
A42: min(x0,x0+h.m) <= x0 & x0 <= max(x0,x0+h.m) by XXREAL_0:17,25;
assume x in [' min(x0,x0+h.m),max(x0,x0+h.m) '];
then
A43: x in [. min(x0,x0+h.m),max(x0,x0+h.m) .] by A42,INTEGRA5:def 3
,XXREAL_0:2;
|.x-x0.| <=|.h.m.|
proof
per cases;
suppose
x0<= x0+h.m;
then x0 = min(x0,x0+h.m) & x0+h.m = max(x0,x0+h.m) by
XXREAL_0:def 9,def 10;
then x in {z where z is Real:
x0<=z & z<=x0+h.m } by A43,
RCOMP_1:def 1;
then
A44: ex z be Real st x=z & x0<=z & z<=x0+h.m;
then 0 <= x-x0 by XREAL_1:48;
then
A45: |.x-x0.| = x-x0 by ABSVALUE:def 1;
A46: x-x0 <= x0+h.m - x0 by A44,XREAL_1:9;
then 0 <= h.m by A44,XREAL_1:48;
hence thesis by A46,A45,ABSVALUE:def 1;
end;
suppose
A47: not x0<=x0 +h.m;
then x0 = max(x0,x0+h.m) & x0+h.m = min(x0,x0+h.m) by
XXREAL_0:def 9,def 10;
then x in {z where z is Real:
x0+h.m<=z & z<=x0 } by A43,
RCOMP_1:def 1;
then
A48: ex z be Real st x=z & x0+h.m<=z & z<=x0;
then
A49: x0 +h.m -x0 <= x-x0 by XREAL_1:9;
per cases;
suppose
A50: x-x0 <> 0;
x0 + h.m - x0 < x0-x0 by A47,XREAL_1:14;
then
A51: |.h.m.| = -(h.m) by ABSVALUE:def 1;
x-x0 < 0 by A48,A50,XREAL_1:47;
then |.x-x0.| = -(x-x0) by ABSVALUE:def 1;
hence thesis by A49,A51,XREAL_1:24;
end;
suppose
x-x0 = 0;
then |.x-x0.| = 0 by ABSVALUE:def 1;
hence thesis by COMPLEX1:46;
end;
end;
end;
then
A52: |.x-x0.| < r by A31,XXREAL_0:2;
then x in ].x0-r,x0+r.[ by RCOMP_1:1;
then x in ].x0-q,x0+q.[ by A30;
then x in ].a,b.[ by A25,A27;
then
A53: x in [.a,b.] by A38;
A54: x1 in REAL by XREAL_0:def 1;
|.x-x0.| < p/2 by A40,A52,XXREAL_0:2;
then |.x-x0.| < p by A24,XXREAL_0:2;
then |.f.x- f.x0.|<=e by A4,A16,A22,A53;
then |.f.x1- g.x1.|<=e by FUNCOP_1:7,A54;
hence thesis by A16,A37,A53,VALUED_1:13;
end;
A55: for x be Real st x in [' a,b '] holds g.x = f.x0 by FUNCOP_1:7;
then
A56: g|[' a,b '] is bounded by A1,A36,Th26;
then
A57: (f-g)|(['a,b '] /\ ['a,b ']) is bounded by A3,RFUNCT_1:84;
A58: m in NAT by ORDINAL1:def 12;
rng h c= dom R by A11;
then R.(h.m)/(h.m) =(R/*h).m /(h.m) by FUNCT_2:108,A58;
then R.(h.m)/(h.m) =((R/*h).m) *((h").m) by VALUED_1:10;
then
A59: R.(h.m)/(h.m) = ((h")(#)(R/*h)).m by SEQ_1:8;
h.m <> 0 by SEQ_1:4,A58;
then
A60: 0 < |.h.m.| by COMPLEX1:47;
A61: g is_integrable_on [' a,b '] by A1,A36,A55,Th26;
then f-g is_integrable_on [' a,b '] by A2,A3,A4,A36,A56,Th11;
then
A62: |.integral(f-g,x0,x0+h.m).| <= e*|.x0+h.m-x0.| by A1,A7,A16,A38,A33,A57
,A37,A41,Lm8;
integral(g,x0,x0+h.m)=(f.x0)*((x0+h.m)-x0) by A1,A7,A16,A38,A33,A36,A55
,Th27;
then R.(h.m) =integral(f-g,x0,x0+h.m) by A1,A2,A3,A4,A7,A16,A38,A33,A35
,A36,A61,A56,A39,Th24;
then |.R.(h.m)/(h.m).| = |.R.(h.m).|/|.h.m.| & |.R.(h.m).|/|.h.m.|
<= e*|. h.m.|/|.h.m.| by A62,A60,COMPLEX1:67,XREAL_1:72;
then
A63: |.R.(h.m)/(h.m).| <= e by A60,XCMPLX_1:89;
e < e0 by A20,XREAL_1:216;
hence thesis by A63,A59,XXREAL_0:2;
end;
hence (h")(#)(R/*h) is convergent by SEQ_2:def 6;
hence thesis by A18,SEQ_2:def 7;
end;
consider N be Neighbourhood of x0 such that
A64: N c= ].a,b.[ by A7,RCOMP_1:18;
reconsider R as RestFunc by A15,A17,FDIFF_1:def 2;
A65: for x be Real st x in N holds F.x-F.x0 = L.(x-x0) + R.(x-x0)
proof
let x be Real;
assume x in N;
then
A66:x0 + (x-x0) in N;
reconsider x as Real;
A67: x0+(x-x0) in N by A66;
C1[x-x0] by A67,A64;
then R.(x-x0) = F1(x-x0) by A11;
hence thesis;
end;
A68: N c= dom F by A5,A64;
hence
A69: F is_differentiable_in x0 by A65,FDIFF_1:def 4;
L.1=(f.x0)*1 by A10;
hence thesis by A68,A65,A69,FDIFF_1:def 5;
end;
Lm13: for a,b be Real, f be PartFunc of REAL,REAL holds ex F be
PartFunc of REAL,REAL st ].a,b.[ c= dom F & for x be Real st x in ].a,b
.[ holds F.x = integral(f,a,x)
proof
deffunc G(Real) = 0;
let a,b be Real;
let f be PartFunc of REAL,REAL;
defpred C[set] means $1 in ].a,b.[;
deffunc F(Real) = integral(f,a,$1);
consider F be Function such that
A1: dom F = REAL & for x be Element of REAL holds (C[x] implies F.x = F(
x)) & (not C[x] implies F.x = G(x)) from PARTFUN1:sch 4;
now
let y be object;
assume y in rng F;
then consider x be object such that
A2: x in dom F and
A3: y = F.x by FUNCT_1:def 3;
reconsider x as Element of REAL by A1,A2;
A4: now
assume not x in ].a,b.[;
then F.x = In(0,REAL) by A1;
hence y in REAL by A3;
end;
now
assume x in ].a,b.[;
then F.x = integral(f,a,x) by A1;
hence y in REAL by A3,XREAL_0:def 1;
end;
hence y in REAL by A4;
end;
then rng F c= REAL;
then reconsider F as PartFunc of REAL,REAL by A1,RELSET_1:4;
take F;
thus thesis by A1;
end;
theorem
for x0 be Real st a <= b & f is_integrable_on [' a,b '] & f|['
a,b '] is bounded & [' a,b '] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0
holds ex F be PartFunc of REAL,REAL st ].a,b.[ c= dom F & (for x be Real
st x in ].a,b.[ holds F.x = integral(f,a,x)) & F is_differentiable_in x0 & diff
(F,x0)=f.x0
proof
let x0 be Real;
consider F be PartFunc of REAL,REAL such that
A1: ].a,b.[ c= dom F & for x be Real st x in ].a,b.[ holds F.x =
integral (f,a,x) by Lm13;
assume a <= b & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & ['
a,b '] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0;
then F is_differentiable_in x0 & diff(F,x0)=f.x0 by A1,Th28;
hence thesis by A1;
end;