:: Integrability of Bounded Total Functions
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received February 1, 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, XBOOLE_0, MEASURE7, CARD_1,
FINSEQ_1, RELAT_1, XXREAL_0, FUNCT_1, SEQ_4, ARYTM_3, ARYTM_1, FUNCT_3,
TARSKI, PARTFUN1, CARD_3, VALUED_1, XXREAL_2, XXREAL_1, INTEGRA2, SEQ_2,
ORDINAL2, FINSET_1, NAT_1, FINSEQ_2, VALUED_0, FDIFF_1, COMPLEX1, INT_1,
ZFMISC_1, RFUNCT_3, SEQ_1, ORDINAL4, SQUARE_1, INTEGRA4, MEASURE5,
FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
COMPLEX1, REAL_1, NAT_1, INT_1, XXREAL_2, VALUED_0, ZFMISC_1, FUNCT_1,
RELSET_1, FINSET_1, FUNCT_2, FINSEQ_1, VALUED_1, SEQ_1, RFUNCT_1,
FINSEQ_2, COMSEQ_2, SEQ_2, SEQ_4, RCOMP_1, FDIFF_1, SQUARE_1, RVSUM_1,
MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3, RFUNCT_3, PARTFUN1, XXREAL_0;
constructors REAL_1, SQUARE_1, NAT_1, BINOP_2, COMPLEX1, FINSEQOP, FINSOP_1,
PARTFUN2, FDIFF_1, ZFMISC_1, RFUNCT_3, INTEGRA2, XXREAL_2, RVSUM_1,
SEQ_4, RELSET_1, SEQ_2, INTEGRA3, COMSEQ_2;
registrations XBOOLE_0, RELAT_1, ORDINAL1, FUNCT_2, FINSET_1, NUMBERS,
XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, FINSEQ_2, INTEGRA1, VALUED_0,
VALUED_1, XXREAL_2, CARD_1, SEQ_2, RELSET_1, SEQM_3, MEASURE5, SQUARE_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions XXREAL_2;
equalities SQUARE_1, RVSUM_1, FINSEQ_2, 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, FINSEQ_3,
INTEGRA2, INTEGRA3, SEQM_3, PARTFUN2, NAT_2, INT_1, FINSEQ_2, RFUNCT_3,
RELAT_1, XREAL_0, FUNCT_2, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1,
XREAL_1, COMPLEX1, XXREAL_0, FINSOP_1, FUNCOP_1, VALUED_1, XXREAL_2,
VALUED_0, ORDINAL1, RELSET_1, CARD_1;
schemes FINSEQ_2, FUNCT_2;
begin :: Basic integrable functions and first mean value theorem
reserve i,j,k,n,n1,n2,m for Nat;
reserve a,r,x,y for Real;
reserve A for non empty closed_interval Subset of REAL;
reserve C for non empty set;
reserve X for set;
theorem Th1:
for D being Division of A st vol(A)=0 holds len D=1
proof
let D be Division of A;
assume that
A1: vol(A)=0 and
A2: len D<>1;
rng D <> {};
then
A3: 1 in dom D by FINSEQ_3:32;
then
A4: 1 <= len D by FINSEQ_3:25;
then
A5: len D in dom D by FINSEQ_3:25;
D.1 in A by A3,INTEGRA1:6;
then
A6: lower_bound A <= D.1 by INTEGRA2:1;
1 < len D by A2,A4,XXREAL_0:1;
then
A7: D.1 < D.(len D) by A3,A5,SEQM_3:def 1;
upper_bound A-lower_bound A=0 by A1,INTEGRA1:def 5;
hence contradiction by A7,A6,INTEGRA1:def 2;
end;
theorem Th2:
chi(A,A) is integrable & integral(chi(A,A))=vol(A)
proof
divs A /\ dom upper_sum_set(chi(A,A))=divs A /\ divs A by FUNCT_2:def 1;
then
A1: divs A meets dom upper_sum_set(chi(A,A)) by XBOOLE_0:def 7;
reconsider vA = vol A as Element of REAL by XREAL_0:def 1;
A2: for D1 being Element of divs A st D1 in divs A /\ dom upper_sum_set(chi(
A,A)) holds (upper_sum_set(chi(A,A)))/.D1=vA
proof
let D1 be Element of divs A;
reconsider D2 = D1 as Division of A by INTEGRA1:def 3;
assume D1 in divs A /\ dom upper_sum_set(chi(A,A));
(upper_sum_set(chi(A,A)))/.D1=(upper_sum_set(chi(A,A))).D1
.=upper_sum(chi(A,A),D2) by INTEGRA1:def 10
.=Sum(upper_volume(chi(A,A),D2)) by INTEGRA1:def 8;
hence thesis by INTEGRA1:24;
end;
then (upper_sum_set chi(A,A))|divs A is constant by PARTFUN2:35;
then consider x being Element of REAL such that
A3: rng((upper_sum_set(chi(A,A)))|(divs A))={x} by A1,PARTFUN2:37;
A4: chi(A,A) is upper_integrable by A3,INTEGRA1:def 12;
vol(A) in rng upper_sum_set(chi(A,A))
proof
set D1 = the Element of divs A;
D1 in divs A;
then
A5: D1 in dom upper_sum_set(chi(A,A)) by FUNCT_2:def 1;
then
A6: (upper_sum_set(chi(A,A))).D1 in rng upper_sum_set(chi(A,A)) by
FUNCT_1:def 3;
A7: (upper_sum_set(chi(A,A))).D1 = (upper_sum_set(chi(A,A)))/.D1;
D1 in divs A /\ dom upper_sum_set(chi(A,A)) by A5,XBOOLE_0:def 4;
hence thesis by A2,A6,A7;
end;
then
A8: x=vol(A) by A3,TARSKI:def 1;
rng upper_sum_set(chi(A,A))={x} by A3;
then lower_bound rng upper_sum_set(chi(A,A))=vol(A) by A8,SEQ_4:9;
then
A9: upper_integral(chi(A,A))=vol(A) by INTEGRA1:def 14;
divs A /\ dom lower_sum_set(chi(A,A))=divs A /\ divs A by FUNCT_2:def 1;
then
A10: divs A meets dom lower_sum_set(chi(A,A)) by XBOOLE_0:def 7;
reconsider vA = vol A as Element of REAL by XREAL_0:def 1;
A11: for D1 being Element of divs A st D1 in divs A /\ dom lower_sum_set(chi
(A,A)) holds (lower_sum_set(chi(A,A)))/.D1=vA
proof
let D1 be Element of divs A;
reconsider D2 = D1 as Division of A by INTEGRA1:def 3;
assume D1 in divs A /\ dom lower_sum_set(chi(A,A));
(lower_sum_set(chi(A,A)))/.D1=(lower_sum_set(chi(A,A))).D1
.=lower_sum(chi(A,A),D2) by INTEGRA1:def 11
.=Sum(lower_volume(chi(A,A),D2)) by INTEGRA1:def 9;
hence thesis by INTEGRA1:23;
end;
then (lower_sum_set chi(A,A))|divs A is constant by PARTFUN2:35;
then consider x being Element of REAL such that
A12: rng((lower_sum_set(chi(A,A)))|(divs A))={x} by A10,PARTFUN2:37;
vol(A) in rng lower_sum_set(chi(A,A))
proof
set D1 = the Element of divs A;
D1 in divs A;
then
A13: D1 in dom lower_sum_set(chi(A,A)) by FUNCT_2:def 1;
then
A14: (lower_sum_set(chi(A,A))).D1 in rng lower_sum_set(chi(A,A)) by
FUNCT_1:def 3;
A15: (lower_sum_set(chi(A,A))).D1 = (lower_sum_set(chi(A,A)))/.D1;
D1 in divs A /\ dom lower_sum_set(chi(A,A)) by A13,XBOOLE_0:def 4;
hence thesis by A11,A14,A15;
end;
then
A16: x=vol(A) by A12,TARSKI:def 1;
rng lower_sum_set(chi(A,A))={x} by A12;
then upper_bound rng lower_sum_set(chi(A,A))=vol(A) by A16,SEQ_4:9;
then
A17: lower_integral(chi(A,A))=vol(A) by INTEGRA1:def 15;
chi(A,A) is lower_integrable by A12,INTEGRA1:def 13;
hence thesis by A4,A9,A17,INTEGRA1:def 16,def 17;
end;
theorem Th3:
for f being PartFunc of A,REAL, r holds f is total & rng f = {r}
iff f=r(#)chi(A,A)
proof
let f be PartFunc of A,REAL;
let r;
A1: f=r(#)chi(A,A) implies f is total & rng f={r}
proof
assume
A2: f=r(#)chi(A,A);
A3: chi(A,A) is total by RFUNCT_1:62;
hence f is total by A2;
A4: dom f = A by A2,A3,PARTFUN1:def 2;
for x being object st x in {r} holds x in rng f
proof
let x be object;
assume x in {r};
then
A5: x = r by TARSKI:def 1;
consider a being Element of REAL such that
A6: a in dom f by A4,SUBSET_1:4;
chi(A,A).a = 1 by A6,RFUNCT_1:63;
then f.a = r*1 by A2,A6,VALUED_1:def 5;
hence thesis by A5,A6,FUNCT_1:def 3;
end;
then
A7: {r} c= rng f by TARSKI:def 3;
for x being object st x in rng f holds x in {r}
proof
let x be object;
assume x in rng f;
then consider a being Element of A such that
A8: a in dom f and
A9: f.a=x by PARTFUN1:3;
chi(A,A).a = 1 by RFUNCT_1:63;
then x = r*1 by A2,A8,A9,VALUED_1:def 5
.= r;
hence thesis by TARSKI:def 1;
end;
then rng f c= {r} by TARSKI:def 3;
hence thesis by A7,XBOOLE_0:def 10;
end;
f is total & rng f={r} implies f=r(#)chi(A,A)
proof
reconsider g=r(#)chi(A,A) as PartFunc of A,REAL;
assume
A10: f is total;
A11: chi(A,A) is total by RFUNCT_1:62;
A12: dom g = dom chi(A,A) by VALUED_1:def 5
.= A by A11,PARTFUN1:def 2;
assume
A13: rng f = {r};
A14: for x being Element of A st x in dom f holds f/.x=g/.x
proof
let x be Element of A;
assume
A15: x in dom f;
then f/.x=f.x by PARTFUN1:def 6;
then
A16: f/.x in rng f by A15,FUNCT_1:def 3;
g/.x=g.x by A12,PARTFUN1:def 6
.= r*chi(A,A).x by A12,VALUED_1:def 5
.= r*1 by RFUNCT_1:63
.= r;
hence thesis by A13,A16,TARSKI:def 1;
end;
dom f = dom g by A10,A12,PARTFUN1:def 2;
hence thesis by A14,PARTFUN2:1;
end;
hence thesis by A1;
end;
theorem Th4:
for f being Function of A,REAL, r st rng f = {r} holds f is
integrable & integral(f)=r*vol(A)
proof
let f be Function of A,REAL;
let r;
A1: chi(A,A) is Function of A, REAL by FUNCT_2:68,RFUNCT_1:62;
A2: integral(chi(A,A))=vol(A) by Th2;
assume rng f={r};
then
A3: f=r(#)chi(A,A) by Th3;
A4: rng chi(A,A) is real-bounded by INTEGRA1:17;
then
A5: chi(A,A)|A is bounded_above by INTEGRA1:14;
A6: chi(A,A)|A is bounded_below by A4,INTEGRA1:12;
chi(A,A) is integrable by Th2;
hence thesis by A3,A2,A1,A5,A6,INTEGRA2:31;
end;
theorem Th5:
for r holds ex f being Function of A,REAL st rng f = {r} & f|A is
bounded
proof
let r;
r(#)chi(A,A) is total by Th3;
then reconsider f=r(#)chi(A,A) as Function of A,REAL;
A1: rng f = {r} by Th3;
then
A2: f|A is bounded_below by INTEGRA1:12;
f|A is bounded_above by A1,INTEGRA1:14;
hence thesis by A1,A2;
end;
Lm1: 0 in REAL by XREAL_0:def 1;
Lm2: for f being PartFunc of A,REAL, D being Element of divs A st vol(A)=0
holds f is upper_integrable & upper_integral(f)=0
proof
let f be PartFunc of A,REAL;
let D be Element of divs A;
divs A /\ dom upper_sum_set(f)=divs A /\ divs A by FUNCT_2:def 1;
then
A1: divs A meets dom upper_sum_set(f) by XBOOLE_0:def 7;
assume
A2: vol(A)=0;
A3: for D1 being Element of divs A st D1 in divs A /\ dom upper_sum_set(f)
holds (upper_sum_set(f))/.D1=0
proof
let D1 be Element of divs A;
reconsider D2 = D1 as Division of A by INTEGRA1:def 3;
A4: len upper_volume(f,D2)=len D2 by INTEGRA1:def 6
.= 1 by A2,Th1;
A5: len D2 = 1 by A2,Th1;
then 1 in Seg len D1 by FINSEQ_1:1;
then
A6: 1 in dom D1 by FINSEQ_1:def 3;
rng D2 <> {};
then
A7: 1 in dom D2 by FINSEQ_3:32;
then
A8: upper_bound divset(D2,len D2)=D2.len D2 by A5,INTEGRA1:def 4
.= upper_bound A by INTEGRA1:def 2;
divset(D2,1)=[.lower_bound divset(D2,len D2), upper_bound divset(D2,
len D2).] by A5,INTEGRA1:4
.=[.lower_bound A, upper_bound A.] by A5,A7,A8,INTEGRA1:def 4;
then divset(D2,1)=A by INTEGRA1:4;
then upper_volume(f,D2).1=(upper_bound rng(f|divset(D2,1)))*vol(A) by A6,
INTEGRA1:def 6
.=0 by A2;
then
A9: upper_volume(f,D2)=<*(0 qua Real)*> by A4,FINSEQ_1:40;
assume D1 in divs A /\ dom upper_sum_set(f);
(upper_sum_set(f))/.D1=(upper_sum_set(f)).D1
.=upper_sum(f,D2) by INTEGRA1:def 10
.=Sum(upper_volume(f,D2)) by INTEGRA1:def 8;
hence thesis by A9,FINSOP_1:11,Lm1;
end;
then (upper_sum_set f)|divs A is constant by PARTFUN2:35,Lm1;
then consider x being Element of REAL such that
A10: rng((upper_sum_set(f))|(divs A))={x} by A1,PARTFUN2:37;
thus f is upper_integrable by A10,INTEGRA1:def 12;
0 in rng upper_sum_set(f)
proof
set D1 = the Element of divs A;
D1 in divs A;
then
A11: D1 in dom upper_sum_set(f) by FUNCT_2:def 1;
then
A12: (upper_sum_set(f)).D1 in rng upper_sum_set(f) by FUNCT_1:def 3;
A13: (upper_sum_set(f)).D1 = (upper_sum_set(f))/.D1;
D1 in divs A /\ dom upper_sum_set(f) by A11,XBOOLE_0:def 4;
hence thesis by A3,A12,A13;
end;
then
A14: x=0 by A10,TARSKI:def 1;
rng upper_sum_set(f)={x} by A10;
then lower_bound rng upper_sum_set(f)=0 by A14,SEQ_4:9;
hence thesis by INTEGRA1:def 14;
end;
Lm3: for f being PartFunc of A,REAL, D being Element of divs A st vol(A)=0
holds f is lower_integrable & lower_integral(f)=0
proof
let f be PartFunc of A,REAL;
let D be Element of divs A;
divs A /\ dom lower_sum_set(f)=divs A /\ divs A by FUNCT_2:def 1;
then
A1: divs A meets dom lower_sum_set(f) by XBOOLE_0:def 7;
assume
A2: vol(A)=0;
A3: for D1 being Element of divs A st D1 in divs A /\ dom lower_sum_set(f)
holds (lower_sum_set(f))/.D1=In(0,REAL)
proof
let D1 be Element of divs A;
reconsider D2 = D1 as Division of A by INTEGRA1:def 3;
A4: len lower_volume(f,D2)=len D2 by INTEGRA1:def 7
.= 1 by A2,Th1;
A5: len D2 = 1 by A2,Th1;
then 1 in Seg len D2 by FINSEQ_1:1;
then
A6: 1 in dom D2 by FINSEQ_1:def 3;
rng D2 <> {};
then
A7: 1 in dom D2 by FINSEQ_3:32;
then
A8: upper_bound divset(D2,len D2)=D2.len D2 by A5,INTEGRA1:def 4
.= upper_bound A by INTEGRA1:def 2;
divset(D2,1)=[.lower_bound divset(D2,len D2), upper_bound divset(D2,
len D2).] by A5,INTEGRA1:4
.=[.lower_bound A, upper_bound A.] by A5,A7,A8,INTEGRA1:def 4;
then divset(D2,1)=A by INTEGRA1:4;
then lower_volume(f,D2).1=(lower_bound rng(f|divset(D2,1)))*vol(A) by A6,
INTEGRA1:def 7
.=0 by A2;
then
A9: lower_volume(f,D2)=<*In(0,REAL)*> by A4,FINSEQ_1:40;
assume D1 in divs A /\ dom lower_sum_set(f);
(lower_sum_set(f))/.D1=(lower_sum_set(f)).D1
.=lower_sum(f,D2) by INTEGRA1:def 11
.=Sum(lower_volume(f,D2)) by INTEGRA1:def 9;
hence thesis by A9,FINSOP_1:11;
end;
then (lower_sum_set f)|divs A is constant by PARTFUN2:35;
then consider x being Element of REAL such that
A10: rng((lower_sum_set(f))|(divs A))={x} by A1,PARTFUN2:37;
thus f is lower_integrable by A10,INTEGRA1:def 13;
0 in rng lower_sum_set(f)
proof
set D1 = the Element of divs A;
D1 in divs A;
then
A11: D1 in dom lower_sum_set(f) by FUNCT_2:def 1;
then
A12: (lower_sum_set(f)).D1 in rng lower_sum_set(f) by FUNCT_1:def 3;
A13: (lower_sum_set(f)).D1 = (lower_sum_set(f))/.D1;
D1 in divs A /\ dom lower_sum_set(f) by A11,XBOOLE_0:def 4;
hence thesis by A3,A12,A13;
end;
then
A14: x=0 by A10,TARSKI:def 1;
rng lower_sum_set(f)={x} by A10;
then upper_bound rng lower_sum_set(f)=0 by A14,SEQ_4:9;
hence thesis by INTEGRA1:def 15;
end;
theorem Th6:
for f being PartFunc of A,REAL st vol(A)=0 holds
f is integrable & integral(f)=0
proof
let f be PartFunc of A,REAL;
assume
A1: vol(A)=0;
then
A2: upper_integral(f)=0 by Lm2;
A3: lower_integral(f)=0 by A1,Lm3;
A4: f is lower_integrable by A1,Lm3;
f is upper_integrable by A1,Lm2;
hence thesis by A2,A4,A3,INTEGRA1:def 16,def 17;
end;
theorem
for f being Function of A,REAL st f|A is bounded & f is integrable
holds ex a st lower_bound rng f <= a & a <= upper_bound rng f & integral(f)=a*
vol(A)
proof
let f be Function of A,REAL;
consider g being Function of A,REAL such that
A1: rng g = {lower_bound rng f} and
A2: g|A is bounded by Th5;
consider h being Function of A,REAL such that
A3: rng h = {upper_bound rng f} and
A4: h|A is bounded by Th5;
A5: integral(g)=(lower_bound rng f)*vol(A) by A1,Th4;
assume
A6: f|A is bounded;
A7: for x st x in dom f holds lower_bound rng f <= f.x & f.x <= upper_bound
rng f
proof
let x;
assume x in dom f;
then
A8: f.x in rng f by FUNCT_1:def 3;
A9: rng f is bounded_below by A6,INTEGRA1:11;
rng f is bounded_above by A6,INTEGRA1:13;
hence thesis by A9,A8,SEQ_4:def 1,def 2;
end;
A10: for x st x in A holds f.x <= h.x
proof
let x;
assume
A11: x in A;
dom h = A by FUNCT_2:def 1;
then
A12: h.x in rng h by A11,FUNCT_1:def 3;
dom f = A by FUNCT_2:def 1;
then f.x <= upper_bound rng f by A7,A11;
hence thesis by A3,A12,TARSKI:def 1;
end;
A13: for x st x in A holds g.x <= f.x
proof
let x;
assume
A14: x in A;
dom g = A by FUNCT_2:def 1;
then
A15: g.x in rng g by A14,FUNCT_1:def 3;
dom f = A by FUNCT_2:def 1;
then lower_bound rng f <= f.x by A7,A14;
hence thesis by A1,A15,TARSKI:def 1;
end;
assume
A16: f is integrable;
A17: integral(h)=(upper_bound rng f)*vol(A) by A3,Th4;
A18: h is integrable by A3,Th4;
A19: g is integrable by A1,Th4;
now
per cases;
suppose
A20: vol(A)<>0;
reconsider a=integral(f)/vol(A) as Real;
A21: integral(f)=a*vol(A) by A20,XCMPLX_1:87;
A22: vol(A) >= 0 by INTEGRA1:9;
then
A23: integral(f)/vol(A) <= (upper_bound rng f) by A6,A16,A4,A18,A17,A10,A20,
INTEGRA2:34,XREAL_1:79;
(lower_bound rng f) <= integral(f)/vol(A) by A6,A16,A2,A19,A5,A13,A20,A22
,INTEGRA2:34,XREAL_1:77;
hence thesis by A23,A21;
end;
suppose
A24: vol(A)=0;
A25: lower_bound rng f <= upper_bound rng f
proof
dom f = A by FUNCT_2:def 1;
then consider x being Element of REAL such that
A26: x in dom f by SUBSET_1:4;
A27: f.x <= upper_bound rng f by A7,A26;
lower_bound rng f <= f.x by A7,A26;
hence thesis by A27,XXREAL_0:2;
end;
integral(f)=(lower_bound rng f)*vol(A) by A24,Th6;
hence thesis by A25;
end;
end;
hence thesis;
end;
begin :: Integrability of Bounded Total Functions
theorem Th8:
for f being Function of A,REAL, T being DivSequence of A st
f|A is bounded & delta(T) is convergent & lim delta(T)=0 holds
lower_sum(f,T) is convergent & lim lower_sum(f,T) = lower_integral(f)
proof
let f be Function of A,REAL;
let T be DivSequence of A;
assume
A1: f|A is bounded;
assume
A2: delta(T) is convergent;
assume
A3: lim delta(T)=0;
now
per cases;
suppose
A4: vol(A)<>0;
for n being Nat holds (delta T).n<>0
proof
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
reconsider mm = rng upper_volume(chi(A,A),T.nn)
as non empty finite
Subset of REAL;
reconsider D=T.nn as Division of A;
assume (delta T).n=0;
then delta(T.nn)=0 by INTEGRA3:def 2;
then
A5: max mm=0 by INTEGRA3:def 1;
A6: for k being Element of NAT st k in dom D holds vol(divset(D,k))=0
proof
let k be Element of NAT;
assume
A7: k in dom D;
then k in Seg len D by 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 <= 0 by A5,XXREAL_2:def 8;
then vol(divset(D,k))<=0 by A7,INTEGRA1:20;
hence thesis by INTEGRA1:9;
end;
A8: for j be Nat holds 1 <= j & j <= len upper_volume(chi(A,A),D)
implies (upper_volume(chi(A,A),D)).j=((len D)|->(0 qua Real)).j
proof
let j be Nat;
assume that
A9: 1<=j and
A10: j<=len upper_volume(chi(A,A),D);
j in Seg len upper_volume(chi(A,A),D) by A9,A10,FINSEQ_1:1;
then
A11: j in Seg len D by INTEGRA1:def 6;
then j in dom D by FINSEQ_1:def 3;
then
A12: upper_volume(chi(A,A),D).j=vol(divset(D,j)) by INTEGRA1:20;
j in dom D by A11,FINSEQ_1:def 3;
then upper_volume(chi(A,A),D).j=0 by A6,A12;
hence thesis by A11,FUNCOP_1:7;
end;
len upper_volume(chi(A,A),D)=len D by INTEGRA1:def 6;
then len upper_volume(chi(A,A),D)=len ((len D)|->(0 qua Real)) by
CARD_1:def 7;
then upper_volume(chi(A,A),D)=((len D) |-> (0 qua Real)) by A8,
FINSEQ_1:14;
then Sum(upper_volume(chi(A,A),D))=0 by RVSUM_1:81;
hence contradiction by A4,INTEGRA1:24;
end;
then delta(T) is non-zero by SEQ_1:5;
then delta(T) is 0-convergent non-zero by A2,A3,FDIFF_1:def 1;
hence thesis by A1,A4,INTEGRA3:25;
end;
suppose
A13: vol(A)=0;
A14: for n being Nat holds lower_sum(f,T).n = In(0,REAL)
proof
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
reconsider D=T.nn as Division of A;
A15: len D=1 by A13,Th1;
then
A16: len lower_volume(f,D)=1 by INTEGRA1:def 7;
rng D <> {};
then
A17: 1 in dom D by FINSEQ_3:32;
then
A18: upper_bound divset(D,len D)=D.(len D) by A15,INTEGRA1:def 4
.= upper_bound A by INTEGRA1:def 2;
1 in Seg len D by A15,FINSEQ_1:1;
then
A19: 1 in dom D by FINSEQ_1:def 3;
divset(D,1)=[.lower_bound divset(D,len D), upper_bound divset(D,
len D).] by A15,INTEGRA1:4
.=[.lower_bound A, upper_bound A.] by A15,A17,A18,INTEGRA1:def 4;
then divset(D,1)=A by INTEGRA1:4;
then lower_volume(f,D).1=(lower_bound rng(f|divset(D,1)))*vol(A) by A19
,INTEGRA1:def 7
.=0 by A13;
then lower_volume(f,D)=<*(0 qua Real)*> by A16,FINSEQ_1:40;
then Sum(lower_volume(f,D))=In(0,REAL) by FINSOP_1:11;
then lower_sum(f,D)=0 by INTEGRA1:def 9;
hence thesis by INTEGRA2:def 3;
end;
then
A20: lower_sum(f,T) is constant by VALUED_0:def 18;
hence lower_sum(f,T) is convergent;
lower_sum(f,T).1 = 0 by A14;
then lim lower_sum(f,T)=0 by A20,SEQ_4:25;
hence lim lower_sum(f,T)=lower_integral(f) by A13,Lm3;
end;
end;
hence thesis;
end;
theorem Th9:
for f being Function of A,REAL, T being DivSequence of A st f|A
is bounded & delta(T) is convergent & lim delta(T)=0 holds upper_sum(f,T) is
convergent & lim upper_sum(f,T) = upper_integral(f)
proof
let f be Function of A,REAL;
let T be DivSequence of A;
assume
A1: f|A is bounded;
assume
A2: delta(T) is convergent;
assume
A3: lim delta(T)=0;
now
per cases;
suppose
A4: vol(A)<>0;
for n being Nat holds (delta(T)).n<>0
proof
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
reconsider D=T.nn as Division of A;
assume (delta(T)).n=0;
then delta(T.nn)=0 by INTEGRA3:def 2;
then
A5: max rng upper_volume(chi(A,A),T.nn)=0 by INTEGRA3:def 1;
A6: for k being Element of NAT st k in dom D holds vol(divset(D,k))=0
proof
let k be Element of NAT;
assume
A7: k in dom D;
then k in Seg len D by 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 <= 0 by A5,XXREAL_2:def 8;
then vol(divset(D,k))<=0 by A7,INTEGRA1:20;
hence thesis by INTEGRA1:9;
end;
A8: for j be Nat holds 1 <= j & j <= len upper_volume(chi(A,A),D)
implies (upper_volume(chi(A,A),D)).j=((len D)|->(0 qua Real)).j
proof
let j be Nat;
assume that
A9: 1<=j and
A10: j<=len upper_volume(chi(A,A),D);
j in Seg len upper_volume(chi(A,A),D) by A9,A10,FINSEQ_1:1;
then
A11: j in Seg len D by INTEGRA1:def 6;
then j in dom D by FINSEQ_1:def 3;
then
A12: upper_volume(chi(A,A),D).j=vol(divset(D,j)) by INTEGRA1:20;
j in dom D by A11,FINSEQ_1:def 3;
then upper_volume(chi(A,A),D).j=0 by A6,A12;
hence thesis by A11,FUNCOP_1:7;
end;
len upper_volume(chi(A,A),D)=len D by INTEGRA1:def 6;
then len upper_volume(chi(A,A),D)=len ((len D)|->(0 qua Real)) by
CARD_1:def 7;
then upper_volume(chi(A,A),D)=((len D) |-> (0 qua Real)) by A8,
FINSEQ_1:14;
then Sum(upper_volume(chi(A,A),D))=0 by RVSUM_1:81;
hence contradiction by A4,INTEGRA1:24;
end;
then delta(T) is non-zero by SEQ_1:5;
then delta(T) is 0-convergent non-zero by A2,A3,FDIFF_1:def 1;
hence thesis by A1,A4,INTEGRA3:26;
end;
suppose
A13: vol(A)=0;
A14: for n being Nat holds upper_sum(f,T).n = In(0,REAL)
proof
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
reconsider D=T.nn as Division of A;
A15: len D=1 by A13,Th1;
then
A16: len upper_volume(f,D)=1 by INTEGRA1:def 6;
rng D <> {};
then
A17: 1 in dom D by FINSEQ_3:32;
then
A18: upper_bound divset(D,len D)=D.(len D) by A15,INTEGRA1:def 4
.= upper_bound A by INTEGRA1:def 2;
1 in Seg len D by A15,FINSEQ_1:1;
then
A19: 1 in dom D by FINSEQ_1:def 3;
divset(D,1)=[.lower_bound divset(D,len D), upper_bound divset(D,
len D).] by A15,INTEGRA1:4
.=[.lower_bound A, upper_bound A.] by A15,A17,A18,INTEGRA1:def 4;
then divset(D,1)=A by INTEGRA1:4;
then upper_volume(f,D).1=(upper_bound rng(f|divset(D,1)))*vol(A) by A19
,INTEGRA1:def 6
.=0 by A13;
then upper_volume(f,D)=<*(0 qua Real)*> by A16,FINSEQ_1:40;
then Sum(upper_volume(f,D))=In(0,REAL) by FINSOP_1:11;
then upper_sum(f,D)=0 by INTEGRA1:def 8;
hence thesis by INTEGRA2:def 2;
end;
then
A20: upper_sum(f,T) is constant by VALUED_0:def 18;
hence upper_sum(f,T) is convergent;
upper_sum(f,T).1 = 0 by A14;
then lim upper_sum(f,T)=0 by A20,SEQ_4:25;
hence lim upper_sum(f,T)=upper_integral(f) by A13,Lm2;
end;
end;
hence thesis;
end;
theorem Th10:
for f being Function of A,REAL st f|A is bounded holds f is
upper_integrable & f is lower_integrable
proof
let f be Function of A,REAL;
assume
A1: f|A is bounded;
(lower_bound rng f)*vol(A) is LowerBound of rng upper_sum_set(f)
proof
let r be ExtReal;
assume r in rng upper_sum_set(f);
then consider D being Element of divs A such that
D in dom upper_sum_set(f) and
A2: (upper_sum_set(f)).D=r by PARTFUN1:3;
reconsider D as Division of A by INTEGRA1:def 3;
r = upper_sum(f,D) by A2,INTEGRA1:def 10;
then
A3: lower_sum(f,D) <= r by A1,INTEGRA1:28;
(lower_bound rng f)*vol(A)<=lower_sum(f,D) by A1,INTEGRA1:25;
hence thesis by A3,XXREAL_0:2;
end;
then rng upper_sum_set(f) is bounded_below;
hence f is upper_integrable by INTEGRA1:def 12;
(upper_bound rng f)*vol(A) is UpperBound of rng lower_sum_set(f)
proof
let r be ExtReal;
assume r in rng lower_sum_set(f);
then consider D being Element of divs A such that
D in dom lower_sum_set(f) and
A4: (lower_sum_set(f)).D=r by PARTFUN1:3;
reconsider D as Division of A by INTEGRA1:def 3;
r = lower_sum(f,D) by A4,INTEGRA1:def 11;
then
A5: upper_sum(f,D) >= r by A1,INTEGRA1:28;
(upper_bound rng f)*vol(A)>=upper_sum(f,D) by A1,INTEGRA1:27;
hence thesis by A5,XXREAL_0:2;
end;
then rng lower_sum_set(f) is bounded_above;
hence thesis by INTEGRA1:def 13;
end;
definition
let A be non empty closed_interval Subset of REAL, IT be Division of A, n;
pred IT divide_into_equal n means
len IT = n & for i st i in dom IT
holds IT.i=lower_bound A + vol(A)/(len IT)*i;
end;
Lm4: for n st n > 0 & vol(A)>0 holds ex D being Division of A st len D = n &
for i st i in dom D holds D.i=lower_bound A + vol(A)/n*i
proof
let n;
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 being 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) < lower_bound A + vol(A)/n*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;
A10: lower_bound A + vol(A)=lower_bound A + (upper_bound A - lower_bound A
) by INTEGRA1:def 5
.= upper_bound A;
assume
A11: x1 in rng D;
then reconsider x1 as Real;
consider i being Element of NAT such that
A12: i in dom D and
A13: D.i=x1 by A11,PARTFUN1:3;
A14: 1 <= i by A12,FINSEQ_3:25;
i <= len D by A12,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
A15: 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
A16: lower_bound A <= lower_bound A + vol(A)/n*i by A14,XREAL_1:29,129;
x1 = F(i) by A3,A12,A13;
hence thesis by A16,A15,A10,INTEGRA2:1;
end;
then
A17: rng D c= A by TARSKI:def 3;
vol(A)=upper_bound A-lower_bound A by INTEGRA1:def 5;
then reconsider D as Division of A by A17,A9,INTEGRA1:def 2;
take D;
thus len D = n by A3;
let i;
assume i in dom D;
then D.i = F(i) by A3;
hence thesis;
end;
Lm5: vol(A)>0 implies ex T being DivSequence of A st delta(T) is convergent &
lim delta(T)=0
proof
defpred P[set,set] means ex n being 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 being 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 and
A4: for i st i in dom D holds D.i=lower_bound A+vol(A)/(n+1)*i by A1,Lm4;
A5: D is Element of divs A by INTEGRA1:def 3;
D divide_into_equal n+1 by A3,A4;
hence thesis by A5;
end;
consider T being sequence of divs A such that
A6: for n being Element of NAT holds P[n,T.n] from FUNCT_2:sch 3(A2);
reconsider T as DivSequence of A;
A7: for i being Element of NAT holds (delta(T)).i = vol(A)/(i+1)
proof
let i be Element of NAT ;
(delta(T)).i = delta(T.i) by INTEGRA3:def 2;
then
A8: (delta(T)).i = max rng upper_volume(chi(A,A),(T.i)) by INTEGRA3:def 1;
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 being Element of NAT such that
A9: k in dom upper_volume(chi(A,A),(T.i)) and
A10: (upper_volume(chi(A,A),(T.i))).k=x1 by PARTFUN1:3;
A11: ex n being Nat, e being Division of A st n = i & e = D &
e divide_into_equal n+1 by A6;
k in Seg len upper_volume(chi(A,A),(T.i)) by A9,FINSEQ_1:def 3;
then
A12: k in Seg len D by INTEGRA1:def 6;
A13: upper_bound divset(D,k)-lower_bound divset(D,k)=vol(A)/(i+1)
proof
A14: 1 <= k by A9,FINSEQ_3:25;
now
per cases by A14,XXREAL_0:1;
suppose
A15: k=1;
A16: 1 in dom D by A12,A15,FINSEQ_1:def 3;
then upper_bound divset(D,k)=D.1 by A15,INTEGRA1:def 4;
then upper_bound divset(D,k)=lower_bound A+vol(A)/(i+1)*1 by A11
,A16;
then upper_bound divset(D,k)-lower_bound divset(D,k)= lower_bound
A+vol(A)/(i+1)-lower_bound A by A15,A16,INTEGRA1:def 4
.=vol(A)/(i+1)-(lower_bound A-lower_bound A);
hence thesis;
end;
suppose
A17: k>1;
A18: k in dom D by A12,FINSEQ_1:def 3;
then
A19: lower_bound divset(D,k)=D.(k-1) by A17,INTEGRA1:def 4;
k-1 in dom D by A17,A18,INTEGRA1:7;
then
A20: D.(k-1)=lower_bound A + vol(A)/(len D)*(k-1) by A11;
A21: upper_bound divset(D,k)=D.k by A17,A18,INTEGRA1:def 4;
D.k = lower_bound A + vol(A)/( len D)* k by A11,A18;
hence thesis by A11,A19,A21,A20;
end;
end;
hence thesis;
end;
k in dom D by A12,FINSEQ_1:def 3;
then x1=vol(divset(D,k)) by A10,INTEGRA1:20;
then x1=upper_bound divset(D,k) - lower_bound divset(D,k) by
INTEGRA1:def 5;
hence thesis by A13,TARSKI:def 1;
end;
then
A22: rng upper_volume(chi(A,A),(T.i)) c= {vol(A)/(i+1)} by TARSKI:def 3;
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;
A23: vol(divset(D,1))=upper_bound divset(D,1) - lower_bound divset(D,1)
by INTEGRA1:def 5;
A24: ex n being Nat, e being Division of A st n = i & e = D &
e divide_into_equal n+1 by A6;
rng D <> {};
then
A25: 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 A25,A24;
then
A26: vol(divset(D,1))=lower_bound A+vol(A)/(len D)-lower_bound A by A25,A23,
INTEGRA1:def 4
.=vol(A)/(len D);
assume x1 in {vol(A)/(i+1)};
then
A27: x1 = vol(A)/(i+1) by TARSKI:def 1;
1 in Seg len D by A25,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
A28: (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 A25,INTEGRA1:20;
hence thesis by A27,A28,A24,A26;
end;
then {vol(A)/(i+1)} c= rng upper_volume(chi(A,A),(T.i)) by TARSKI:def 3;
then rng upper_volume(chi(A,A),(T.i))={vol(A)/(i+1)} by A22,XBOOLE_0:def 10
;
then (delta(T)).i in {vol(A)/(i+1)} by A8,XXREAL_2:def 8;
hence thesis by TARSKI:def 1;
end;
A29: for a st 0<a ex i st |.(delta(T)).i-0.|<a
proof
let a;
A30: vol(A) >= 0 by INTEGRA1:9;
reconsider i1=[\vol(A)/a/]+1 as Integer;
assume
A31: 0<a;
then [\vol(A)/a/]+1>0 by A30;
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
A32: vol(A)/(i1+1) < 1*a by A31,XREAL_1:113;
A33: (delta(T)).i1 = vol(A)/(i1+1) by A7;
vol(A)/(i1+1)-0 = |.vol(A)/(i1+1)-0.| by A30,ABSVALUE:def 1;
hence thesis by A32,A33;
end;
A34: for i being Nat holds (delta(T)).i >= 0
proof
let i be Nat;
reconsider ii=i as Element of NAT by ORDINAL1:def 12;
(delta(T)).i = delta(T.ii) by INTEGRA3:def 2;
hence thesis by INTEGRA3:9;
end;
A35: for i,j being Nat st i <= j holds (delta(T)).i >= (delta(T)).j
proof
let i,j be Nat;
assume i <= j;
then
A36: i+1 <= j+1 by XREAL_1:6;
A37: i in NAT & j in NAT by ORDINAL1:def 12;
vol(A) >= 0 by INTEGRA1:9;
then vol(A)/(i+1) >= vol(A)/(j+1) by A36,XREAL_1:118;
then (delta(T)).i >= vol(A)/(j+1) by A7,A37;
hence thesis by A7,A37;
end;
A38: for a be Real st 0<a
ex i being Nat st for j being Nat st i <= j holds |.(delta(T)
).j-0.|<a
proof
let a be Real;
assume
A39: 0<a;
consider i such that
A40: |.(delta(T)).i-0.|<a by A29,A39;
(delta(T)).i >= 0 by A34;
then
A41: (delta(T)).i < a by A40,ABSVALUE:def 1;
for j being Nat st i <= j holds |.(delta(T)).j-0.|<a
proof
let j be Nat;
assume i <= j;
then (delta(T)).j <= (delta(T)).i by A35;
then
A42: (delta(T)).j < a by A41,XXREAL_0:2;
(delta(T)).j >= 0 by A34;
hence thesis by A42,ABSVALUE:def 1;
end;
hence thesis;
end;
then
A43: delta(T) is convergent by SEQ_2:def 6;
then lim delta(T)=0 by A38,SEQ_2:def 7;
hence thesis by A43;
end;
Lm6: vol(A)=0 implies ex T being DivSequence of A st delta(T) is convergent &
lim delta(T)=0
proof
set T = the DivSequence of A;
assume
A1: vol(A)=0;
A2: for i being Nat holds (delta(T)).i=In(0,REAL)
proof
let i be Nat;
reconsider ii=i as Element of NAT by ORDINAL1:def 12;
reconsider D = T.ii as Division of A;
A3: (delta(T)).i=delta(D) by INTEGRA3:def 2
.= max rng upper_volume(chi(A,A),D) by INTEGRA3:def 1;
A4: len D = 1
proof
assume len D <> 1;
then len D is non trivial by NAT_2:def 1;
then
A5: len D >= 2 by NAT_2:29;
then 1 <= len D by XXREAL_0:2;
then
A6: 1 in dom D by FINSEQ_3:25;
then
A7: D.1 in A by INTEGRA1:6;
then
A8: lower_bound A <= D.1 by INTEGRA2:1;
A9: 2 in dom D by A5,FINSEQ_3:25;
then D.2 in A by INTEGRA1:6;
then
A10: D.2 <= upper_bound A by INTEGRA2:1;
A11: D.1 <= upper_bound A by A7,INTEGRA2:1;
A12: upper_bound A-lower_bound A=0 by A1,INTEGRA1:def 5;
D.1 < D.2 by A6,A9,SEQM_3:def 1;
hence contradiction by A8,A11,A10,A12,XXREAL_0:1;
end;
for x1 being object st x1 in {0} holds x1 in rng upper_volume(chi(A,A),
D )
proof
let x1 be object;
A13: 1 in Seg len D by A4,FINSEQ_1:3;
then 1 in dom D by FINSEQ_1:def 3;
then
A14: (upper_volume(chi(A,A),D)).1 = vol(divset(D,1)) by INTEGRA1:20;
1 in Seg len upper_volume(chi(A,A),D) by A13,INTEGRA1:def 6;
then 1 in dom upper_volume(chi(A,A),D) by FINSEQ_1:def 3;
then
A15: (upper_volume(chi(A,A),D)).1 in rng upper_volume(chi(A,A), D) by
FUNCT_1:def 3;
A16: 1 in dom D by A13,FINSEQ_1:def 3;
then upper_bound divset(D,1)=D.(len D) by A4,INTEGRA1:def 4;
then
A17: upper_bound divset(D,1)=upper_bound A by INTEGRA1:def 2;
lower_bound divset(D,1)= lower_bound A by A16,INTEGRA1:def 4;
then
A18: vol(divset(D,1))=upper_bound A-lower_bound A by A17,INTEGRA1:def 5
.=0 by A1,INTEGRA1:def 5;
assume x1 in {0};
hence thesis by A15,A14,A18,TARSKI:def 1;
end;
then
A19: {0} c= rng upper_volume(chi(A,A),D) by TARSKI:def 3;
for x1 being object st x1 in rng upper_volume(chi(A,A),D) holds x1 in {
0 }
proof
let x1 be object;
assume
A20: x1 in rng upper_volume(chi(A,A),D);
then consider k being Element of NAT such that
A21: k in dom upper_volume(chi(A,A),D) and
A22: (upper_volume(chi(A,A),D)).k=x1 by PARTFUN1:3;
reconsider x1 as Real by A20;
k in Seg len upper_volume(chi(A,A),D) by A21,FINSEQ_1:def 3;
then
A23: k in Seg len D by INTEGRA1:def 6;
then
A24: k in dom D by FINSEQ_1:def 3;
k in dom D by A23,FINSEQ_1:def 3;
then
A25: x1=vol(divset(D,k)) by A22,INTEGRA1:20;
then x1 >= 0 by INTEGRA1:9;
then x1 = 0 by A1,A25,A24,INTEGRA1:8,INTEGRA2:38;
hence thesis by TARSKI:def 1;
end;
then rng upper_volume(chi(A,A),D) c= {0} by TARSKI:def 3;
then rng upper_volume(chi(A,A),D)={0} by A19,XBOOLE_0:def 10;
then (delta(T)).i in {0} by A3,XXREAL_2:def 8;
hence thesis by TARSKI:def 1;
end;
then
A26: delta(T) is constant by VALUED_0:def 18;
(delta(T)).1 = 0 by A2;
then lim delta(T)=0 by A26,SEQ_4:25;
hence thesis by A26;
end;
theorem Th11:
ex T being DivSequence of A st delta(T) is convergent & lim
delta(T)=0
proof
now
per cases;
suppose
A1: vol(A)<>0;
vol(A) >= 0 by INTEGRA1:9;
hence thesis by A1,Lm5;
end;
suppose
vol(A)=0;
hence thesis by Lm6;
end;
end;
hence thesis;
end;
theorem Th12:
for f being Function of A,REAL st f|A is bounded holds f is
integrable iff for T being DivSequence of A st delta(T) is convergent & lim
delta(T)=0 holds lim upper_sum(f,T)-lim lower_sum(f,T)=0
proof
let f be Function of A,REAL;
assume
A1: f|A is bounded;
A2: f is integrable implies for T being DivSequence of A st delta(T) is
convergent & lim delta(T)=0 holds lim upper_sum(f,T)-lim lower_sum(f,T)=0
proof
assume
A3: f is integrable;
for T being DivSequence of A st delta(T) is convergent & lim delta(T)
= 0 holds lim upper_sum(f,T)-lim lower_sum(f,T)=0
proof
A4: upper_integral(f)=lower_integral(f) by A3,INTEGRA1:def 16;
let T be DivSequence of A;
assume that
A5: delta(T) is convergent and
A6: lim delta(T)=0;
A7: lim lower_sum(f,T)=lower_integral(f) by A1,A5,A6,Th8;
lim upper_sum(f,T)=upper_integral(f) by A1,A5,A6,Th9;
hence thesis by A7,A4;
end;
hence thesis;
end;
(for T being DivSequence of A st delta(T) is convergent & lim delta(T)
= 0 holds lim upper_sum(f,T)-lim lower_sum(f,T)=0) implies f is integrable
proof
consider T being DivSequence of A such that
A8: delta(T) is convergent and
A9: lim delta(T)=0 by Th11;
assume for T being DivSequence of A st delta(T) is convergent & lim
delta(T)=0 holds lim upper_sum(f,T)-lim lower_sum(f,T)=0;
then lim upper_sum(f,T)-lim lower_sum(f,T)=0 by A8,A9;
then upper_integral(f)-lim lower_sum(f,T)=0 by A1,A8,A9,Th9;
then
A10: upper_integral(f)-lower_integral(f)=0 by A1,A8,A9,Th8;
A11: f is lower_integrable by A1,Th10;
f is upper_integrable by A1,Th10;
hence thesis by A11,A10,INTEGRA1:def 16;
end;
hence thesis by A2;
end;
theorem Th13:
for f being Function of C,REAL holds max+(f) is total & max-(f)
is total
proof
let f be Function of C,REAL;
A1: dom f = C by FUNCT_2:def 1;
then
A2: dom max-(f) = C by RFUNCT_3:def 11;
dom max+(f) = C by A1,RFUNCT_3:def 10;
hence thesis by A2,PARTFUN1:def 2;
end;
theorem Th14:
for f being PartFunc of C,REAL st f|X is bounded_above holds (
max+f)|X is bounded_above
proof
let f be PartFunc of C,REAL;
assume f|X is bounded_above;
then consider b being Real such that
A1: for c being object st c in X /\ dom f holds f.c <= b by RFUNCT_1:70;
A2: dom max+(f) = dom f by RFUNCT_3:def 10;
ex r st for c being object st c in X /\ dom max+(f) holds max+(f).c <= r
proof
now
per cases;
suppose
A3: b < 0;
for c being object st c in X /\ dom max+(f) holds max+(f).c <= 0
proof
let c be object;
assume c in X /\ dom max+(f);
then
A4: c in X /\ dom f by RFUNCT_3:def 10;
then f.c <= b by A1;
then max(f.c,0) = 0 by A3,XXREAL_0:def 10;
then
A5: max+(f.c) = 0 by RFUNCT_3:def 1;
c in dom f by A4,XBOOLE_0:def 4;
hence thesis by A2,A5,RFUNCT_3:def 10;
end;
hence thesis;
end;
suppose
A6: b >= 0;
for c being object st c in X /\ dom max+(f) holds max+(f).c <= b
proof
let c be object;
assume c in X /\ dom max+(f);
then
A7: c in X /\ dom f by RFUNCT_3:def 10;
then f.c <= b by A1;
then max(f.c,0) <= b by A6,XXREAL_0:28;
then
A8: max+(f.c) <= b by RFUNCT_3:def 1;
c in dom f by A7,XBOOLE_0:def 4;
hence thesis by A2,A8,RFUNCT_3:def 10;
end;
then consider r be Real such that
r = b and
A9: for c being object st c in X /\ dom max+(f) holds max+(f).c <= r;
thus thesis by A9;
end;
end;
hence thesis;
end;
hence thesis by RFUNCT_1:70;
end;
theorem Th15:
for f being PartFunc of C,REAL holds (max+f)|X is bounded_below
proof
let f be PartFunc of C,REAL;
for c being object st c in X /\ dom max+(f) holds max+(f).c >= 0
by RFUNCT_3:37;
hence thesis by RFUNCT_1:71;
end;
theorem Th16:
for f being PartFunc of C,REAL st f|X is bounded_below holds (
max-f)|X is bounded_above
proof
let f be PartFunc of C,REAL;
assume f|X is bounded_below;
then consider b be Real such that
A1: for c being object st c in X /\ dom f holds f.c >= b by RFUNCT_1:71;
A2: dom max-(f) = dom f by RFUNCT_3:def 11;
ex r st for c being object st c in X /\ dom max-(f) holds max-(f).c <= r
proof
now
per cases;
suppose
A3: b > 0;
for c being object st c in X /\ dom max-(f) holds max-(f).c <= 0
proof
let c be object;
assume c in X /\ dom max-(f);
then
A4: c in X /\ dom f by RFUNCT_3:def 11;
then f.c >= b by A1;
then max(-f.c,0) = 0 by A3,XXREAL_0:def 10;
then
A5: max-(f.c) = 0 by RFUNCT_3:def 2;
c in dom f by A4,XBOOLE_0:def 4;
hence thesis by A2,A5,RFUNCT_3:def 11;
end;
hence thesis;
end;
suppose
A6: b <= 0;
for c being object st c in X /\ dom max-(f) holds max-(f).c <= -b
proof
let c be object;
assume c in X /\ dom max-(f);
then
A7: c in X /\ dom f by RFUNCT_3:def 11;
then f.c >= b by A1;
then -f.c <= -b by XREAL_1:24;
then max(-f.c,0) <= -b by A6,XXREAL_0:28;
then
A8: max-(f.c) <= -b by RFUNCT_3:def 2;
c in dom f by A7,XBOOLE_0:def 4;
hence thesis by A2,A8,RFUNCT_3:def 11;
end;
then consider r be Real such that
r = -b and
A9: for c being object st c in X /\ dom max-(f) holds max-(f).c <= r;
thus thesis by A9;
end;
end;
hence thesis;
end;
hence thesis by RFUNCT_1:70;
end;
theorem Th17:
for f being PartFunc of C,REAL holds (max-f)|X is bounded_below
proof
let f be PartFunc of C,REAL;
for c being object st c in X /\ dom max-(f) holds max-(f).c >= 0
by RFUNCT_3:40;
hence thesis by RFUNCT_1:71;
end;
theorem Th18:
for f being PartFunc of A,REAL st f|A is bounded_above holds rng
(f|X) is bounded_above
proof
let f be PartFunc of A,REAL;
assume f|A is bounded_above;
then rng f is bounded_above by INTEGRA1:13;
hence thesis by RELAT_1:70,XXREAL_2:43;
end;
theorem Th19:
for f being PartFunc of A,REAL st f|A is bounded_below holds rng
(f|X) is bounded_below
proof
let f be PartFunc of A,REAL;
assume f|A is bounded_below;
then rng f is bounded_below by INTEGRA1:11;
hence thesis by RELAT_1:70,XXREAL_2:44;
end;
theorem Th20:
for f being Function of A,REAL st f|A is bounded & f is
integrable holds max+(f) is integrable
proof
let f be Function of A,REAL;
assume that
A1: f|A is bounded and
A2: f is integrable;
A3: max+(f) is total by Th13;
A4: (max+f)|A is bounded_below by Th15;
A5: (max+f)|A is bounded_above by A1,Th14;
for T being DivSequence of A st delta(T) is convergent & lim delta(T)= 0
holds lim upper_sum(max+(f),T)-lim lower_sum(max+(f),T)=0
proof
let T be DivSequence of A;
assume that
A6: delta(T) is convergent and
A7: lim delta(T)=0;
A8: lower_sum(f,T) is convergent by A1,A6,A7,Th8;
A9: upper_sum(f,T) is convergent by A1,A6,A7,Th9;
then
A10: upper_sum(f,T)-lower_sum(f,T) is convergent by A8;
reconsider osc1=upper_sum(max+(f),T)-lower_sum(max+(f),T) as Real_Sequence;
reconsider osc=upper_sum(f,T)-lower_sum(f,T) as Real_Sequence;
lim upper_sum(f,T)-lim lower_sum(f,T)=0 by A1,A2,A6,A7,Th12;
then
A11: lim(upper_sum(f,T)-lower_sum(f,T))=0 by A9,A8,SEQ_2:12;
A12: for a be Real st 0<a
ex n being Nat st for m being Nat st n <= m holds |.osc1.m-0.|<a
proof
let a be Real;
assume 0 < a;
then consider n being Nat such that
A13: for m being Nat st n <= m
holds |. osc.m - 0 .|<a by A10,A11,SEQ_2:def 7;
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;
len upper_volume(f,D)=len D by INTEGRA1:def 6;
then reconsider
UV=upper_volume(f,D) as Element of (len D)-tuples_on REAL
by FINSEQ_2:133;
len lower_volume(f,D)=len D by INTEGRA1:def 7;
then reconsider
LV=lower_volume(f,D) as Element of (len D)-tuples_on REAL
by FINSEQ_2:133;
len upper_volume(max+(f),D) = len D by INTEGRA1:def 6;
then reconsider
UV1=upper_volume(max+(f),D) as Element of (len D)-tuples_on
REAL by FINSEQ_2:133;
len lower_volume(max+(f),D) = len D by INTEGRA1:def 7;
then reconsider
LV1=lower_volume(max+(f),D) as Element of (len D)-tuples_on
REAL by FINSEQ_2:133;
reconsider F = UV1-LV1 as FinSequence of REAL;
osc1.m=(upper_sum(max+(f),T)).m+(-lower_sum(max+(f),T)).m by SEQ_1:7
.=(upper_sum(max+(f),T)).m+-(lower_sum(max+(f),T)).m by SEQ_1:10
.=(upper_sum(max+(f),T)).m-(lower_sum(max+(f),T)).m
.=upper_sum(max+(f),T.mm)
-(lower_sum(max+(f),T)).m by INTEGRA2:def 2
.=upper_sum(max+(f),T.mm)
-lower_sum(max+(f),T.mm) by INTEGRA2:def 3
.=Sum(upper_volume(max+(f),D))-lower_sum(max+(f),T.mm) by
INTEGRA1:def 8
.=Sum(upper_volume(max+(f),D))-Sum(lower_volume(max+(f),D)) by
INTEGRA1:def 9;
then
A14: osc1.m=Sum(UV1-LV1) by RVSUM_1:90;
A15: for j be Nat st j in Seg (len D) holds (UV1-LV1).j <= (UV-LV).j
proof
let j be Nat;
set x=(UV1-LV1).j, y=(UV-LV).j;
assume
A16: j in Seg (len D);
then
A17: j in dom D by FINSEQ_1:def 3;
then
A18: LV1.j=(lower_bound (rng (max+(f)|divset(D,j))))*vol(divset(D,j)
) by INTEGRA1:def 7;
A19: rng (f|divset(D,j)) is real-bounded & ex r st r in rng (f|divset(D,j
))
proof
A20: rng f is bounded_below by A1,INTEGRA1:11;
rng f is bounded_above by A1,INTEGRA1:13;
hence rng (f|divset(D,j)) is real-bounded
by A20,RELAT_1:70,XXREAL_2:45;
consider r being Element of REAL such that
A21: r in divset(D,j) by SUBSET_1:4;
j in dom D by A16,FINSEQ_1:def 3;
then divset(D,j) c= A by INTEGRA1:8;
then r in A by A21;
then r in dom f by FUNCT_2:def 1;
then f.r in rng(f|divset(D,j)) by A21,FUNCT_1:50;
hence thesis;
end;
A22: upper_bound rng (f|divset(D,j))-lower_bound rng (f|divset(D,j))
>= upper_bound rng (max+(f)|divset(D,j))- lower_bound rng (max+(f)|divset(D,j))
proof
set m1=lower_bound rng (max+(f)|divset(D,j));
set M1=upper_bound rng (max+(f)|divset(D,j));
set m=lower_bound rng (f|divset(D,j));
set M=upper_bound rng (f|divset(D,j));
A23: dom f = dom max+(f) by RFUNCT_3:def 10;
A24: j in dom D by A16,FINSEQ_1:def 3;
A25: rng (f|divset(D,j)) is bounded_above by A1,Th18;
dom (f|divset(D,j)) = dom f /\ divset(D,j) by RELAT_1:61;
then dom (f|divset(D,j)) = A /\ divset(D,j) by FUNCT_2:def 1;
then dom (f|divset(D,j)) <> {} by A24,INTEGRA1:8,XBOOLE_1:28;
then
A26: rng (f|divset(D,j)) <> {} by RELAT_1:42;
dom f = A by FUNCT_2:def 1;
then dom (max+(f)|divset(D,j)) = A /\ divset(D,j) by A23,RELAT_1:61
;
then dom (max+(f)|divset(D,j)) <> {} by A24,INTEGRA1:8,XBOOLE_1:28;
then
A27: rng (max+(f)|divset(D,j)) <> {} by RELAT_1:42;
(max+f)|A is bounded_below by Th15;
then
A28: rng (max+(f)|divset(D,j)) is bounded_below by Th19;
A29: rng (f|divset(D,j)) is bounded_below by A1,Th19;
(max+f)|A is bounded_above by A1,Th14;
then
A30: rng (max+(f)|divset(D,j)) is bounded_above by Th18;
now
per cases by A19,SEQ_4:11;
suppose
A31: M > 0 & m >=0;
A32: for r be Real st r in rng (max+(f)|divset(D,j))
holds r <= M
proof
let r be Real;
assume r in rng(max+(f)|divset(D,j));
then consider x being Element of A such that
A33: x in dom(max+(f)|divset(D,j)) and
A34: r=(max+(f)|divset(D,j)).x by PARTFUN1:3;
A35: r=(max+(f|divset(D,j))).x by A34,RFUNCT_3:44;
A36: x in dom(max+(f|divset(D,j))) by A33,RFUNCT_3:44;
then
A37: x in dom(f|divset(D,j)) by RFUNCT_3:def 10;
now
per cases by A35,RFUNCT_3:37;
suppose
r=0;
hence thesis by A31;
end;
suppose
A38: r>0;
r=max+((f|divset(D,j)).x) by A35,A36,RFUNCT_3:def 10;
then r=max((f|divset(D,j)).x,0) by RFUNCT_3:def 1;
then r=(f|divset(D,j)).x by A38,XXREAL_0:def 10;
then r in rng(f|divset(D,j)) by A37,FUNCT_1:def 3;
hence thesis by A25,SEQ_4:def 1;
end;
end;
hence thesis;
end;
A39: for s be Real st 0<s ex r be Real st r in
rng (max+(f)|divset(D,j)) & r<m+s
proof
let s be Real;
assume 0<s;
then consider r be Real such that
A40: r in rng (f|divset(D,j)) and
A41: r<m+s by A26,A29,SEQ_4:def 2;
reconsider r as Real;
r in rng (max+(f)|divset(D,j))
proof
A42: r >= m by A29,A40,SEQ_4:def 2;
consider x being Element of A such that
A43: x in dom(f|divset(D,j)) and
A44: r=(f|divset(D,j)).x by A40,PARTFUN1:3;
A45: x in dom(max+(f|divset(D,j))) by A43,RFUNCT_3:def 10;
then (max+(f|divset(D,j))).x=max+(r) by A44,RFUNCT_3:def 10
.=max(r,0) by RFUNCT_3:def 1
.= r by A31,A42,XXREAL_0:def 10;
then r in rng (max+(f|divset(D,j))) by A45,FUNCT_1:def 3;
hence thesis by RFUNCT_3:44;
end;
hence thesis by A41;
end;
A46: for r be Real st r in rng (max+(f)|divset(D,j))
holds m<=r
proof
let r be Real;
assume r in rng(max+(f)|divset(D,j));
then consider x being Element of A such that
A47: x in dom(max+(f)|divset(D,j)) and
A48: r=(max+(f)|divset(D,j)).x by PARTFUN1:3;
A49: x in dom(max+(f|divset(D,j))) by A47,RFUNCT_3:44;
x in dom(max+(f|divset(D,j))) by A47,RFUNCT_3:44;
then x in dom(f|divset(D,j)) by RFUNCT_3:def 10;
then (f|divset(D,j)).x in rng (f|divset(D,j)) by
FUNCT_1:def 3;
then
A50: (f|divset(D,j)).x >= m by A29,SEQ_4:def 2;
r=(max+(f|divset(D,j))).x by A48,RFUNCT_3:44
.=max+((f|divset(D,j)).x) by A49,RFUNCT_3:def 10
.=max((f|divset(D,j)).x,0) by RFUNCT_3:def 1;
hence thesis by A31,A50,XXREAL_0:def 10;
end;
for s be Real st 0<s ex r be Real st r in
rng (max+(f)|divset(D,j)) & M-s<r
proof
let s be Real;
assume 0<s;
then consider r be Real such that
A51: r in rng (f|divset(D,j)) and
A52: M-s<r by A26,A25,SEQ_4:def 1;
r in rng (max+(f)|divset(D,j))
proof
reconsider r1 = r as Real;
consider x being Element of A such that
A53: x in dom(f|divset(D,j)) and
A54: r=(f|divset(D,j)).x by A51,PARTFUN1:3;
A55: r >= m by A29,A51,SEQ_4:def 2;
A56: x in dom(max+(f|divset(D,j))) by A53,RFUNCT_3:def 10;
then (max+(f|divset(D,j))).x=max+(r1) by A54,
RFUNCT_3:def 10
.=max(r,0) by RFUNCT_3:def 1
.= r by A31,A55,XXREAL_0:def 10;
then r in rng (max+(f|divset(D,j))) by A56,FUNCT_1:def 3;
hence thesis by RFUNCT_3:44;
end;
hence thesis by A52;
end;
then M1=M by A27,A30,A32,SEQ_4:def 1;
hence thesis by A27,A28,A46,A39,SEQ_4:def 2;
end;
suppose
A57: M > 0 & m <= 0;
A58: for s be Real st 0<s ex r be Real st r in
rng (max+(f)|divset(D,j)) & r<0+s
proof
let s be Real;
assume
A59: s>0;
then consider r be Real such that
A60: r in rng (f|divset(D,j)) and
A61: r<m+s by A26,A29,SEQ_4:def 2;
consider x being Element of A such that
A62: x in dom (f|divset(D,j)) and
A63: r=(f|divset(D,j)).x by A60,PARTFUN1:3;
A64: x in dom (max+(f|divset(D,j))) by A62,RFUNCT_3:def 10;
then
A65: (max+(f|divset(D,j))).x = max+((f|divset(D,j)).x) by
RFUNCT_3:def 10
.= max((f|divset(D,j)).x,0) by RFUNCT_3:def 1;
(max+(f|divset(D,j))).x in rng (max+(f|divset(D,j)) )
by A64,FUNCT_1:def 3;
then
A66: (max+(f|divset(D,j))).x in rng (max+(f)|divset(D,j))
by RFUNCT_3:44;
A67: r-s < m by A61,XREAL_1:19;
now
per cases;
suppose
r < 0;
then 0 in rng(max+(f)|divset(D,j)) by A63,A66,A65,
XXREAL_0:def 10;
hence ex r st r in rng (max+(f)|divset(D,j)) & r<0+s by
A59;
end;
suppose
A68: r >=0;
A69: r<0+s by A57,A67,XREAL_1:19;
r in rng(max+(f)|divset(D,j)) by A63,A66,A65,A68,
XXREAL_0:def 10;
hence
ex r st r in rng (max+(f)|divset(D,j)) & r < 0+s by A69;
end;
end;
hence thesis;
end;
for r be Real st r in rng (max+(f)|divset(D,j))
holds 0<=r
proof
let r be Real;
assume r in rng (max+(f)|divset(D,j));
then r in rng(max+(f|divset(D,j))) by RFUNCT_3:44;
then ex x being Element of A st x in dom(max+(f|divset(D,j
))) & r=(max+(f|divset(D,j))).x by PARTFUN1:3;
hence thesis by RFUNCT_3:37;
end;
then
A70: m1=0 by A27,A28,A58,SEQ_4:def 2;
for r st r in rng (max+(f)|divset(D,j)) holds r <= M
proof
let r;
assume r in rng(max+(f)|divset(D,j));
then consider x being Element of A such that
A71: x in dom(max+(f)|divset(D,j)) and
A72: r=(max+(f)|divset(D,j)).x by PARTFUN1:3;
A73: r=(max+(f|divset(D,j))).x by A72,RFUNCT_3:44;
A74: x in dom(max+(f|divset(D,j))) by A71,RFUNCT_3:44;
then
A75: x in dom(f|divset(D,j)) by RFUNCT_3:def 10;
now
per cases by A73,RFUNCT_3:37;
suppose
r=0;
hence thesis by A57;
end;
suppose
A76: r>0;
r=max+((f|divset(D,j)).x) by A73,A74,RFUNCT_3:def 10;
then r=max((f|divset(D,j)).x,0) by RFUNCT_3:def 1;
then r=(f|divset(D,j)).x by A76,XXREAL_0:def 10;
then r in rng(f|divset(D,j)) by A75,FUNCT_1:def 3;
hence thesis by A25,SEQ_4:def 1;
end;
end;
hence thesis;
end;
then
A77: for r be Real st r in rng (max+(f)|divset(D,j))
holds r<=M;
for s be Real st 0<s ex r be Real st r in
rng (max+(f)|divset(D,j)) & M-s<r
proof
assume not(for s be Real st 0<s ex r be Real
st r in rng (max+(f)|divset(D,j)) & M-s<r );
then consider s be Real such that
A78: s >0 and
A79: for r be Real st r in rng (max+(f)|divset(D
,j)) holds M-s>= r;
consider r1 being Real such that
A80: r1 in rng (f|divset(D,j)) and
A81: M-s < r1 by A26,A25,A78,SEQ_4:def 1;
consider x being Element of A such that
A82: x in dom(f|divset(D,j)) and
A83: r1=(f|divset(D,j)).x by A80,PARTFUN1:3;
A84: x in dom(max+(f|divset(D,j))) by A82,RFUNCT_3:def 10;
then x in dom(max+(f)|divset(D,j)) by RFUNCT_3:44;
then
A85: (max+(f)|divset(D,j)).x in rng (max+(f)|divset(D,j))
by FUNCT_1:def 3;
(max+(f|divset(D,j))).x >= 0 by RFUNCT_3:37;
then (max+(f)|divset(D,j)).x >= 0 by RFUNCT_3:44;
then
A86: M-s >= 0 by A79,A85;
(max+(f)|divset(D,j)).x = (max+(f|divset(D,j))).x by
RFUNCT_3:44
.=max+((f|divset(D,j)).x) by A84,RFUNCT_3:def 10
.=max(r1,0) by A83,RFUNCT_3:def 1
.=r1 by A81,A86,XXREAL_0:def 10;
hence contradiction by A79,A81,A85;
end;
then M1=M by A27,A30,A77,SEQ_4:def 1;
hence thesis by A57,A70,XREAL_1:13;
end;
suppose
A87: M <= 0 & m <= 0;
A88: for s be Real st 0<s ex r be Real st r in
rng(max+(f)|divset(D,j)) & r<0+s
proof
let s be Real;
assume
A89: s>0;
consider r being Element of REAL such that
A90: r in rng (max+(f)|divset(D,j)) by A27,SUBSET_1:4;
consider x being Element of A such that
A91: x in dom (max+(f)|divset(D,j)) and
A92: r=(max+(f)|divset(D,j)).x by A90,PARTFUN1:3;
A93: x in dom (max+(f|divset(D,j))) by A91,RFUNCT_3:44;
then x in dom (f|divset(D,j)) by RFUNCT_3:def 10;
then (f|divset(D,j)).x in rng (f|divset(D,j)) by
FUNCT_1:def 3;
then
A94: (f|divset(D,j)).x <= M by A25,SEQ_4:def 1;
r=(max+(f|divset(D,j))).x by A92,RFUNCT_3:44;
then r=max+((f|divset(D,j)).x) by A93,RFUNCT_3:def 10
.=max((f|divset(D,j)).x,0) by RFUNCT_3:def 1;
then r=0 by A87,A94,XXREAL_0:def 10;
hence thesis by A89,A90;
end;
for r be Real st r in rng (max+(f)|divset(D,j))
holds 0<=r
proof
let r be Real;
assume r in rng (max+(f)|divset(D,j));
then consider x being Element of A such that
x in dom (max+(f)|divset(D,j)) and
A95: r = (max+(f)|divset(D,j)).x by PARTFUN1:3;
r=(max+(f|divset(D,j))).x by A95,RFUNCT_3:44;
hence thesis by RFUNCT_3:37;
end;
then
A96: m1=0 by A27,A28,A88,SEQ_4:def 2;
A97: for r be Real st r in rng (max+(f)|divset(D,j))
holds r<=0
proof
let r be Real;
assume r in rng (max+(f)|divset(D,j));
then consider x being Element of A such that
A98: x in dom (max+(f)|divset(D,j)) and
A99: r = (max+(f)|divset(D,j)).x by PARTFUN1:3;
A100: x in dom (max+(f|divset(D,j))) by A98,RFUNCT_3:44;
then x in dom (f|divset(D,j)) by RFUNCT_3:def 10;
then (f|divset(D,j)).x in rng (f|divset(D,j)) by
FUNCT_1:def 3;
then
A101: (f|divset(D,j)).x <= M by A25,SEQ_4:def 1;
r=(max+(f|divset(D,j))).x by A99,RFUNCT_3:44;
then r=max+((f|divset(D,j)).x) by A100,RFUNCT_3:def 10
.=max((f|divset(D,j)).x,0) by RFUNCT_3:def 1
.=0 by A87,A101,XXREAL_0:def 10;
hence thesis;
end;
for s be Real st 0<s ex r be Real st r in
rng (max+(f)|divset(D,j)) & 0-s<r
proof
let s be Real;
assume
A102: s>0;
consider r being Element of REAL such that
A103: r in rng (max+(f)|divset(D,j)) by A27,SUBSET_1:4;
consider x being Element of A such that
x in dom (max+(f)|divset(D,j)) and
A104: r=(max+(f)|divset(D,j)).x by A103,PARTFUN1:3;
r=(max+(f|divset(D,j))).x by A104,RFUNCT_3:44;
then r >= 0 by RFUNCT_3:37;
hence thesis by A102,A103;
end;
then M1=0 by A27,A30,A97,SEQ_4:def 1;
hence thesis by A19,A96,SEQ_4:11,XREAL_1:48;
end;
end;
hence thesis;
end;
A105: LV.j=(lower_bound rng (f|divset(D,j)))*vol(divset(D,j)) by A17,
INTEGRA1:def 7;
UV .j=(upper_bound rng (f|divset(D,j)))*vol(divset(D,j)) by A17,
INTEGRA1:def 6;
then
A106: y=(upper_bound rng (f|divset(D,j)))*vol(divset(D,j)) -(
lower_bound rng (f|divset(D,j)))*vol(divset(D,j)) by A105,RVSUM_1:27
.=(upper_bound rng (f|divset(D,j))-lower_bound rng (f|divset(D,j
)))* vol(divset(D,j));
UV1.j=(upper_bound (rng (max+(f)|divset(D,j))))*vol(divset(D,j)
) by A17,INTEGRA1:def 6;
then
A107: x=(upper_bound rng (max+(f)|divset(D,j)))*vol(divset(D,j)) -(
lower_bound rng (max+(f)|divset(D,j)))*vol(divset(D,j)) by A18,RVSUM_1:27
.=(upper_bound rng (max+(f)|divset(D,j))- lower_bound rng (max+(
f)|divset(D,j))) *vol(divset(D,j));
vol(divset(D,j)) >= 0 by INTEGRA1:9;
hence thesis by A107,A106,A22,XREAL_1:64;
end;
assume n <= m;
then
A108: |. osc.m - 0 .|<a by A13;
for j be Nat st j in dom F holds 0 <= F.j
proof
let j be Nat;
set r = F.j;
(max+f)|A is bounded_below by Th15;
then
A109: rng max+(f) is bounded_below by INTEGRA1:11;
assume that
A110: j in dom F;
j in Seg len F by A110,FINSEQ_1:def 3;
then
A111: j in Seg len D by CARD_1:def 7;
then
A112: j in dom D by FINSEQ_1:def 3;
then
A113: LV1.j=(lower_bound (rng (max+(f)|divset(D,j))))*vol(divset(D,j
)) by INTEGRA1:def 7;
A114: ex r st r in rng (max+(f)|divset(D,j))
proof
consider r being Element of REAL such that
A115: r in divset(D,j) by SUBSET_1:4;
j in dom D by A111,FINSEQ_1:def 3;
then divset(D,j) c= A by INTEGRA1:8;
then r in A by A115;
then r in dom f by FUNCT_2:def 1;
then r in dom f /\ divset(D,j) by A115,XBOOLE_0:def 4;
then r in dom (f|divset(D,j)) by RELAT_1:61;
then r in dom max+(f|divset(D,j)) by RFUNCT_3:def 10;
then r in dom (max+(f)|divset(D,j)) by RFUNCT_3:44;
then
(max+(f)|divset(D,j)).r in rng(max+(f)| divset(D,j)) by FUNCT_1:def 3;
hence thesis;
end;
(max+f)|A is bounded_above by A1,Th14;
then rng max+(f) is bounded_above by INTEGRA1:13;
then rng (max+(f)|divset(D,j)) is real-bounded by A109,RELAT_1:70
,XXREAL_2:45;
then
A116: upper_bound(rng(max+(f)|divset(D,j)))- lower_bound(rng(max+(f)
|divset(D,j )))>=0 by A114,SEQ_4:11,XREAL_1:48;
UV1.j=(upper_bound (rng (max+(f)|divset(D,j))))* vol(divset(D,
j)) by A112,INTEGRA1:def 6;
then
A117: r = (upper_bound(rng(max+(f)|divset(D,j))))*vol(divset(D,j ))
-(lower_bound(rng(max+(f)|divset(D,j))))*vol(divset(D,j)) by A110,A113,
VALUED_1:13
.=(upper_bound(rng(max+(f)|divset(D,j))) - lower_bound(rng(max+(
f)|divset(D,j))))* vol(divset(D,j));
vol(divset(D,j))>=0 by INTEGRA1:9;
hence thesis by A117,A116;
end;
then
A118: osc1.m >= 0 by A14,RVSUM_1:84;
then
A119: |. osc1.m-0 .|=osc1.m by ABSVALUE:def 1;
osc.m=(upper_sum(f,T)).m+(-lower_sum(f,T)).m by SEQ_1:7
.=(upper_sum(f,T)).m+-(lower_sum(f,T)).m by SEQ_1:10
.=(upper_sum(f,T)).m-(lower_sum(f,T)).m
.=upper_sum(f,T.mm)-(lower_sum(f,T)).m by INTEGRA2:def 2
.=upper_sum(f,T.mm)-lower_sum(f,T.mm) by INTEGRA2:def 3
.=Sum(upper_volume(f,D))-lower_sum(f,T.mm) by INTEGRA1:def 8
.=Sum(upper_volume(f,D))-Sum(lower_volume(f,D)) by INTEGRA1:def 9;
then osc.m=Sum(UV-LV) by RVSUM_1:90;
then
A120: osc1.m <= osc.m by A14,A15,RVSUM_1:82;
then |. osc.m .|=osc.m by A118,ABSVALUE:def 1;
hence thesis by A108,A120,A119,XXREAL_0:2;
end;
then osc1 is convergent by SEQ_2:def 6;
then
A121: lim(upper_sum(max+(f),T)-lower_sum(max+(f),T))=0 by A12,SEQ_2:def 7;
A122: lower_sum(max+(f),T) is convergent by A3,A5,A4,A6,A7,Th8;
upper_sum(max+(f),T) is convergent by A3,A5,A4,A6,A7,Th9;
hence thesis by A122,A121,SEQ_2:12;
end;
hence thesis by A3,A5,A4,Th12;
end;
theorem Th21:
for f being PartFunc of C,REAL holds max-(f)=max+(-f)
proof
let f be PartFunc of C,REAL;
dom max+(-f)= dom -f by RFUNCT_3:def 10;
then
A1: dom max+(-f)= dom f by VALUED_1:8;
A2: dom max-(f) = dom f by RFUNCT_3:def 11;
for x1 being Element of C st x1 in dom f holds max-(f).x1=max+(-f).x1
proof
let x1 be Element of C;
assume
A3: x1 in dom f;
then
A4: max+(-f).x1 = max+((-f).x1) by A1,RFUNCT_3:def 10
.= max((-f).x1,0 ) by RFUNCT_3:def 1
.= max(-(f.x1),0) by VALUED_1:8;
max-(f).x1 = max-(f.x1) by A2,A3,RFUNCT_3:def 11
.= max(-(f.x1),0) by RFUNCT_3:def 2;
hence thesis by A4;
end;
hence thesis by A2,A1,PARTFUN1:5;
end;
theorem Th22:
for f being Function of A,REAL st f|A is bounded & f is
integrable holds max-(f) is integrable
proof
let f be Function of A,REAL;
assume that
A1: f|A is bounded and
A2: f is integrable;
A3: (-f)|A is bounded by A1,RFUNCT_1:82;
(-1)(#)f is integrable by A1,A2,INTEGRA2:31;
then max+(-f) is integrable by A3,Th20;
hence thesis by Th21;
end;
theorem
for f being Function of A,REAL st f|A is bounded & f is integrable
holds abs(f) is integrable & |.integral(f).|<=integral(abs(f))
proof
let f be Function of A,REAL;
assume that
A1: f|A is bounded and
A2: f is integrable;
A3: max-(f) is integrable by A1,A2,Th22;
A4: (max+f)|A is bounded_above by A1,Th14;
A5: (max-f)|A is bounded_above by A1,Th16;
A6: max+(f) is total by Th13;
A7: (max-f)|A is bounded_below by Th17;
A8: (max+f)|A is bounded_below by Th15;
A9: max-(f) is total by Th13;
A10: max+(f) is integrable by A1,A2,Th20;
then max+(f) + max-(f) is integrable by A6,A9,A4,A8,A5,A7,A3,INTEGRA1:57;
hence abs(f) is integrable by RFUNCT_3:34;
A11: integral(max+(f))-integral(max-(f)) = integral(max+(f)-max-(f)) by A6,A9
,A4,A8,A5,A7,A10,A3,INTEGRA2:33
.= integral(f) by RFUNCT_3:34;
A12: integral(max+(f))+integral(max-(f)) = integral(max+(f)+max-(f)) by A6,A9
,A4,A8,A5,A7,A10,A3,INTEGRA1:57
.= integral(abs(f)) by RFUNCT_3:34;
then
A13: integral(abs(f))-integral(f) =2*integral(max-(f)) by A11;
for x st x in A holds (max-(f)).x >= 0 by RFUNCT_3:40;
then integral(max-(f))>=0 by A9,A5,A7,INTEGRA2:32;
then
A14: integral(abs(f))>=integral(f) by A13,XREAL_1:49;
A15: integral(abs(f))+integral(f) =2*integral(max+(f)) by A12,A11;
for x st x in A holds (max+(f)).x >= 0 by RFUNCT_3:37;
then integral(max+(f))>=0 by A6,A4,A8,INTEGRA2:32;
then -integral(abs(f))<=integral(f) by A15,XREAL_1:61;
hence thesis by A14,ABSVALUE:5;
end;
theorem Th24:
for f being Function of A,REAL st (for x,y st x in A & y in A
holds |.f.x-f.y.|<=a) holds upper_bound rng f - lower_bound rng f <= a
proof
let f be Function of A,REAL;
assume
A1: for x,y st x in A & y in A holds |.f.x-f.y.|<=a;
A2: for y be Real st y in A holds upper_bound rng f - a <= f.y
proof
let y be Real;
assume
A3: y in A;
for b be Real st b in rng f holds b <= a+f.y
proof
let b be Real;
assume b in rng f;
then consider x being Element of A such that
x in dom f and
A4: b=f.x by PARTFUN1:3;
|.f.x-f.y.|<=a by A1,A3;
then f.x-f.y <= a by ABSVALUE:5;
hence thesis by A4,XREAL_1:20;
end;
then upper_bound rng f <= a + f.y by SEQ_4:45;
hence thesis by XREAL_1:20;
end;
for b be Real st b in rng f holds upper_bound rng f - a <= b
proof
let b be Real;
assume b in rng f;
then ex x being Element of A st x in dom f & b=f.x by PARTFUN1:3;
hence thesis by A2;
end;
then upper_bound rng f - a <= lower_bound rng f by SEQ_4:43;
then upper_bound rng f <= a + lower_bound rng f by XREAL_1:20;
hence thesis by XREAL_1:20;
end;
theorem Th25:
for f,g being Function of A,REAL st f|A is bounded & a>=0 & (for
x,y st x in A & y in A holds |.g.x-g.y.|<=a*|.f.x-f.y.|) holds upper_bound
rng g - lower_bound rng g <= a*(upper_bound rng f - lower_bound rng f)
proof
let f,g be Function of A,REAL;
assume that
A1: f|A is bounded and
A2: a>=0 and
A3: for x,y st x in A & y in A holds |.g.x-g.y.|<=a*|.f.x-f.y.|;
A4: rng f is bounded_above by A1,INTEGRA1:13;
A5: dom f = A by FUNCT_2:def 1;
A6: rng f is bounded_below by A1,INTEGRA1:11;
A7: for x,y st x in A & y in A holds |.f.x-f.y.|<= upper_bound rng f -
lower_bound rng f
proof
let x,y;
assume that
A8: x in A and
A9: y in A;
now
per cases;
suppose
f.x >= f.y;
then f.x - f.y >= 0 by XREAL_1:48;
then |.f.x-f.y.| = f.x - f.y by ABSVALUE:def 1;
then
A10: |.f.x-f.y.| + f.y = f.x;
f.y in rng f by A5,A9,FUNCT_1:def 3;
then
A11: lower_bound rng f <= f.y by A6,SEQ_4:def 2;
f.x in rng f by A5,A8,FUNCT_1:def 3;
then f.x <= upper_bound rng f by A4,SEQ_4:def 1;
then f.y <= upper_bound rng f - |.f.x-f.y.| by A10,XREAL_1:19;
then lower_bound rng f <= upper_bound rng f - |.f.x-f.y.| by A11,
XXREAL_0:2;
then lower_bound rng f + |.f.x-f.y.| <= upper_bound rng f by
XREAL_1:19;
hence thesis by XREAL_1:19;
end;
suppose
f.x < f.y;
then f.x - f.y < 0 by XREAL_1:49;
then |.f.x-f.y.| = -(f.x-f.y) by ABSVALUE:def 1
.= f.y - f.x;
then
A12: |.f.x-f.y.| + f.x = f.y;
f.x in rng f by A5,A8,FUNCT_1:def 3;
then
A13: lower_bound rng f <= f.x by A6,SEQ_4:def 2;
f.y in rng f by A5,A9,FUNCT_1:def 3;
then f.y <= upper_bound rng f by A4,SEQ_4:def 1;
then f.x <= upper_bound rng f - |.f.x-f.y.| by A12,XREAL_1:19;
then lower_bound rng f <= upper_bound rng f - |.f.x-f.y.| by A13,
XXREAL_0:2;
then lower_bound rng f + |.f.x-f.y.| <= upper_bound rng f by
XREAL_1:19;
hence thesis by XREAL_1:19;
end;
end;
hence thesis;
end;
for x,y st x in A & y in A holds |.g.x-g.y.|<= a*(upper_bound rng f -
lower_bound rng f )
proof
let x,y;
assume that
A14: x in A and
A15: y in A;
A16: |.g.x-g.y.|<=a*|.f.x-f.y.| by A3,A14,A15;
a*|.f.x-f.y.|<=a*(upper_bound rng f - lower_bound rng f) by A2,A7,A14,A15,
XREAL_1:64;
hence thesis by A16,XXREAL_0:2;
end;
hence thesis by Th24;
end;
theorem Th26:
for f,g,h being Function of A,REAL st f|A is bounded & g|A is
bounded & a>=0 & (for x,y st x in A & y in A holds |.h.x-h.y.|<=a*(|.f.x-f.y
.|+|.g.x-g.y.|))
holds upper_bound rng h - lower_bound rng h <= a*((upper_bound
rng f - lower_bound rng f)+(upper_bound rng g - lower_bound rng g))
proof
let f,g,h be Function of A,REAL;
assume that
A1: f|A is bounded and
A2: g|A is bounded and
A3: a>=0 and
A4: for x,y st x in A & y in A holds |.h.x-h.y.|<=a*(|.f.x-f.y.|+|.g
.x-g.y.|);
A5: rng g is bounded_above by A2,INTEGRA1:13;
A6: rng f is bounded_above by A1,INTEGRA1:13;
A7: dom g = A by FUNCT_2:def 1;
A8: rng g is bounded_below by A2,INTEGRA1:11;
A9: for x,y st x in A & y in A holds |.g.x-g.y.|<=upper_bound rng g -
lower_bound rng g
proof
let x,y;
assume that
A10: x in A and
A11: y in A;
now
per cases;
suppose
g.x >= g.y;
then g.x - g.y >= 0 by XREAL_1:48;
then |.g.x-g.y.| = g.x - g.y by ABSVALUE:def 1;
then
A12: |.g.x-g.y.| + g.y = g.x;
g.y in rng g by A7,A11,FUNCT_1:def 3;
then
A13: lower_bound rng g <= g.y by A8,SEQ_4:def 2;
g.x in rng g by A7,A10,FUNCT_1:def 3;
then g.x <= upper_bound rng g by A5,SEQ_4:def 1;
then g.y <= upper_bound rng g - |.g.x-g.y.| by A12,XREAL_1:19;
then lower_bound rng g <= upper_bound rng g - |.g.x-g.y.| by A13,
XXREAL_0:2;
then lower_bound rng g + |.g.x-g.y.| <= upper_bound rng g by
XREAL_1:19;
hence thesis by XREAL_1:19;
end;
suppose
g.x < g.y;
then g.x - g.y < 0 by XREAL_1:49;
then |.g.x-g.y.| = -(g.x-g.y) by ABSVALUE:def 1
.= g.y - g.x;
then
A14: |.g.x-g.y.| + g.x = g.y;
g.x in rng g by A7,A10,FUNCT_1:def 3;
then
A15: lower_bound rng g <= g.x by A8,SEQ_4:def 2;
g.y in rng g by A7,A11,FUNCT_1:def 3;
then g.y <= upper_bound rng g by A5,SEQ_4:def 1;
then g.x <= upper_bound rng g - |.g.x-g.y.| by A14,XREAL_1:19;
then lower_bound rng g <= upper_bound rng g - |.g.x-g.y.| by A15,
XXREAL_0:2;
then lower_bound rng g + |.g.x-g.y.| <= upper_bound rng g by
XREAL_1:19;
hence thesis by XREAL_1:19;
end;
end;
hence thesis;
end;
A16: dom f = A by FUNCT_2:def 1;
A17: rng f is bounded_below by A1,INTEGRA1:11;
A18: for x,y st x in A & y in A holds |.f.x-f.y.|<= upper_bound rng f -
lower_bound rng f
proof
let x,y;
assume that
A19: x in A and
A20: y in A;
now
per cases;
suppose
f.x >= f.y;
then f.x - f.y >= 0 by XREAL_1:48;
then |.f.x-f.y.| = f.x - f.y by ABSVALUE:def 1;
then
A21: |.f.x-f.y.| + f.y = f.x;
f.y in rng f by A16,A20,FUNCT_1:def 3;
then
A22: lower_bound rng f <= f.y by A17,SEQ_4:def 2;
f.x in rng f by A16,A19,FUNCT_1:def 3;
then f.x <= upper_bound rng f by A6,SEQ_4:def 1;
then f.y <= upper_bound rng f - |.f.x-f.y.| by A21,XREAL_1:19;
then lower_bound rng f <= upper_bound rng f - |.f.x-f.y.| by A22,
XXREAL_0:2;
then lower_bound rng f + |.f.x-f.y.| <= upper_bound rng f by
XREAL_1:19;
hence thesis by XREAL_1:19;
end;
suppose
f.x < f.y;
then f.x - f.y < 0 by XREAL_1:49;
then |.f.x-f.y.| = -(f.x-f.y) by ABSVALUE:def 1
.= f.y - f.x;
then
A23: |.f.x-f.y.| + f.x = f.y;
f.x in rng f by A16,A19,FUNCT_1:def 3;
then
A24: lower_bound rng f <= f.x by A17,SEQ_4:def 2;
f.y in rng f by A16,A20,FUNCT_1:def 3;
then f.y <= upper_bound rng f by A6,SEQ_4:def 1;
then f.x <= upper_bound rng f - |.f.x-f.y.| by A23,XREAL_1:19;
then lower_bound rng f <= upper_bound rng f - |.f.x-f.y.| by A24,
XXREAL_0:2;
then lower_bound rng f + |.f.x-f.y.| <= upper_bound rng f by
XREAL_1:19;
hence thesis by XREAL_1:19;
end;
end;
hence thesis;
end;
for x,y st x in A & y in A holds |.h.x-h.y.|<=a*((upper_bound rng f -
lower_bound rng f)+ (upper_bound rng g - lower_bound rng g))
proof
let x,y;
assume that
A25: x in A and
A26: y in A;
A27: a*|.g.x-g.y.|<=a*(upper_bound rng g - lower_bound rng g) by A3,A9,A25,A26
,XREAL_1:64;
a*|.f.x-f.y.|<=a*(upper_bound rng f - lower_bound rng f) by A3,A18,A25,A26
,XREAL_1:64;
then
A28: a*|.f.x-f.y.|+a*|.g.x-g.y.|<= a*(upper_bound rng f - lower_bound
rng f)+ a*(upper_bound rng g - lower_bound rng g) by A27,XREAL_1:7;
|.h.x-h.y.|<=a*(|.f.x-f.y.|+|.g.x-g.y.|) by A4,A25,A26;
hence thesis by A28,XXREAL_0:2;
end;
hence thesis by Th24;
end;
theorem Th27:
for f,g being Function of A,REAL st f|A is bounded & f is
integrable & g|A is bounded & a>0 & (for x,y st x in A & y in A holds |.g.x-g
.y.|<=a*|.f.x-f.y.|) holds g is integrable
proof
let f,g be Function of A,REAL;
assume that
A1: f|A is bounded and
A2: f is integrable and
A3: g|A is bounded and
A4: a>0 and
A5: for x,y st x in A & y in A holds |.g.x-g.y.|<=a*|.f.x-f.y.|;
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;
assume that
A6: delta(T) is convergent and
A7: lim delta(T)=0;
A8: lower_sum(f,T) is convergent by A1,A6,A7,Th8;
A9: upper_sum(f,T) is convergent by A1,A6,A7,Th9;
then
A10: upper_sum(f,T)-lower_sum(f,T) is convergent by A8;
reconsider osc1=upper_sum(g,T)-lower_sum(g,T) as Real_Sequence;
reconsider osc=upper_sum(f,T)-lower_sum(f,T) as Real_Sequence;
lim upper_sum(f,T)-lim lower_sum(f,T)=0 by A1,A2,A6,A7,Th12;
then
A11: lim(upper_sum(f,T)-lower_sum(f,T))=0 by A9,A8,SEQ_2:12;
A12: for b be Real st 0<b
ex n being Nat st for m being Nat st n <= m holds |.osc1.m-
0.|<b
proof
let b be Real;
assume b>0;
then b/a > 0 by A4,XREAL_1:139;
then consider n being Nat such that
A13: for m being Nat st n <= m
holds |. osc.m - 0.|<b/a by A10,A11,SEQ_2:def 7;
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;
len upper_volume(f,D)=len D by INTEGRA1:def 6;
then reconsider
UV=upper_volume(f,D) as Element of (len D)-tuples_on REAL
by FINSEQ_2:133;
len lower_volume(f,D)=len D by INTEGRA1:def 7;
then reconsider
LV=lower_volume(f,D) as Element of (len D)-tuples_on REAL
by FINSEQ_2:133;
osc.m=(upper_sum(f,T)).m+(-lower_sum(f,T)).m by SEQ_1:7
.=(upper_sum(f,T)).m+-(lower_sum(f,T)).m by SEQ_1:10
.=(upper_sum(f,T)).m-(lower_sum(f,T)).m
.=upper_sum(f,T.mm)-(lower_sum(f,T)).m by INTEGRA2:def 2
.=upper_sum(f,T.mm)-lower_sum(f,T.mm) by INTEGRA2:def 3
.=Sum(upper_volume(f,D))-lower_sum(f,T.mm) by INTEGRA1:def 8
.=Sum(upper_volume(f,D))-Sum(lower_volume(f,D)) by INTEGRA1:def 9;
then
A14: osc.m=Sum(UV-LV) by RVSUM_1:90;
assume n <= m;
then
A15: |. osc.m - 0 .|<b/a by A13;
len lower_volume(g,D) = len D by INTEGRA1:def 7;
then reconsider
LV1=lower_volume(g,D) as Element of (len D)-tuples_on REAL
by FINSEQ_2:133;
len upper_volume(g,D) = len D by INTEGRA1:def 6;
then reconsider
UV1=upper_volume(g,D) as Element of (len D)-tuples_on REAL
by FINSEQ_2:133;
reconsider F = UV1-LV1 as FinSequence of REAL;
osc1.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
.=upper_sum(g,T.mm)-(lower_sum(g,T)).m by INTEGRA2:def 2
.=upper_sum(g,T.mm)-lower_sum(g,T.mm) by INTEGRA2:def 3
.=Sum(upper_volume(g,D))-lower_sum(g,T.mm) by INTEGRA1:def 8
.=Sum(upper_volume(g,D))-Sum(lower_volume(g,D)) by INTEGRA1:def 9;
then
A16: osc1.m=Sum(UV1-LV1) by RVSUM_1:90;
for j be Nat st j in dom F holds 0 <= F.j
proof
let j be Nat;
set r = F.j;
A17: rng g is bounded_below by A3,INTEGRA1:11;
assume that
A18: j in dom F;
j in Seg len F by A18,FINSEQ_1:def 3;
then
A19: j in Seg len D by CARD_1:def 7;
then
A20: j in dom D by FINSEQ_1:def 3;
then
A21: LV1.j=(lower_bound (rng (g|divset(D,j))))*vol(divset(D,j)) by
INTEGRA1:def 7;
A22: ex r st r in rng (g|divset(D,j))
proof
consider r being Element of REAL such that
A23: r in divset(D,j) by SUBSET_1:4;
j in dom D by A19,FINSEQ_1:def 3;
then divset(D,j) c= A by INTEGRA1:8;
then r in A by A23;
then r in dom g by FUNCT_2:def 1;
then r in dom g /\ divset(D,j) by A23,XBOOLE_0:def 4;
then r in dom (g|divset(D,j)) by RELAT_1:61;
then (g|divset(D,j)).r in rng(g|divset(D,j)) by FUNCT_1:def 3;
hence thesis;
end;
rng g is bounded_above by A3,INTEGRA1:13;
then rng (g|divset(D,j)) is real-bounded
by A17,RELAT_1:70,XXREAL_2:45;
then
A24: upper_bound(rng(g|divset(D,j)))-lower_bound(rng(g|divset(D,j)))
>=0 by A22,SEQ_4:11,XREAL_1:48;
UV1.j=(upper_bound (rng (g|divset(D,j))))*vol(divset(D,j)) by A20,
INTEGRA1:def 6;
then
A25: r = (upper_bound(rng(g|divset(D,j))))*vol(divset(D,j)) -(
lower_bound(rng(g|divset(D,j))))*vol(divset(D,j)) by A18,A21,VALUED_1:13
.=(upper_bound(rng(g|divset(D,j))) - lower_bound(rng(g|divset(D,
j))))* vol(divset(D,j));
vol(divset(D,j))>=0 by INTEGRA1:9;
hence thesis by A25,A24;
end;
then
A26: osc1.m >= 0 by A16,RVSUM_1:84;
then
A27: |. osc1.m .|=osc1.m by ABSVALUE:def 1;
for j be Nat st j in Seg (len D) holds (UV1-LV1).j <= (a*(UV-LV))
.j
proof
let j be Nat;
set x=(UV1-LV1).j, y=(a*(UV-LV)).j;
A28: y=a*((UV-LV).j) by RVSUM_1:45;
assume
A29: j in Seg (len D);
then
A30: j in dom D by FINSEQ_1:def 3;
then
A31: LV1.j=(lower_bound (rng (g|divset(D,j))))*vol(divset(D,j)) by
INTEGRA1:def 7;
A32: a*(upper_bound rng (f|divset(D,j))-lower_bound rng (f|divset(D,
j))) >= upper_bound rng (g|divset(D,j))-lower_bound rng (g|divset(D,j))
proof
A33: j in dom D by A29,FINSEQ_1:def 3;
then
A34: f|divset(D,j)|divset(D,j) is bounded_below by A1,INTEGRA1:8
,INTEGRA2:6;
A35: dom(g|divset(D,j)) = dom g /\ divset(D,j) by RELAT_1:61
.= A /\ divset(D,j) by FUNCT_2:def 1
.= divset(D,j) by A33,INTEGRA1:8,XBOOLE_1:28;
then reconsider
g1=g|divset(D,j) as PartFunc of divset(D,j),REAL by RELSET_1:5;
A36: dom(f|divset(D,j)) = dom f /\ divset(D,j) by RELAT_1:61
.= A /\ divset(D,j) by FUNCT_2:def 1
.= divset(D,j) by A33,INTEGRA1:8,XBOOLE_1:28;
then reconsider
f1=f|divset(D,j) as PartFunc of divset(D,j),REAL by RELSET_1:5;
reconsider g1 as Function of divset(D,j),REAL by A35,FUNCT_2:def 1;
reconsider f1 as Function of divset(D,j),REAL by A36,FUNCT_2:def 1;
A37: divset(D,j) c= A by A33,INTEGRA1:8;
A38: for x,y st x in divset(D,j) & y in divset(D,j) holds |.g1.x
-g1.y.| <= a*|.f1.x-f1.y.|
proof
let x,y;
assume that
A39: x in divset(D,j) and
A40: y in divset(D,j);
A41: g.y=g1.y by A35,A40,FUNCT_1:47;
A42: f.y=f1.y by A36,A40,FUNCT_1:47;
A43: f.x=f1.x by A36,A39,FUNCT_1:47;
g.x=g1.x by A35,A39,FUNCT_1:47;
hence thesis by A5,A37,A39,A40,A41,A43,A42;
end;
f|divset(D,j)|divset(D,j) is bounded_above by A1,A33,INTEGRA1:8
,INTEGRA2:5;
then f1|divset(D,j) is bounded by A34;
hence thesis by A4,A38,Th25;
end;
vol(divset(D,j)) >= 0 by INTEGRA1:9;
then
A44: a*(upper_bound rng (f|divset(D,j))-lower_bound rng (f|divset(D,
j)))*vol(divset(D,j )) >= (upper_bound rng (g|divset(D,j))-lower_bound rng (g|
divset(D,j)))*vol(divset(D,j)) by A32,XREAL_1:64;
UV1.j=(upper_bound (rng (g|divset(D,j))))*vol(divset(D,j)) by A30,
INTEGRA1:def 6;
then
A45: x=(upper_bound rng (g|divset(D,j)))*vol(divset(D,j)) -(
lower_bound rng (g|divset(D,j)))*vol(divset(D,j)) by A31,RVSUM_1:27
.=(upper_bound rng (g|divset(D,j))-lower_bound rng (g|divset(D,j
))) *vol(divset(D,j));
A46: LV.j=(lower_bound rng (f|divset(D,j)))*vol(divset(D,j)) by A30,
INTEGRA1:def 7;
UV .j=(upper_bound rng (f|divset(D,j)))*vol(divset(D,j)) by A30,
INTEGRA1:def 6;
then y=a*((upper_bound rng (f|divset(D,j)))*vol(divset(D,j)) -(
lower_bound rng (f|divset(D,j)))*vol(divset(D,j))) by A46,A28,RVSUM_1:27
.=a*((upper_bound rng (f|divset(D,j))-lower_bound rng (f|divset(
D,j)))*vol(divset(D,j)));
hence thesis by A45,A44;
end;
then osc1.m <= Sum(a*(UV-LV)) by A16,RVSUM_1:82;
then
A47: osc1.m <= a*osc.m by A14,RVSUM_1:87;
then osc.m >= 0/a by A4,A26,XREAL_1:79;
then |. osc.m .|=osc.m by ABSVALUE:def 1;
then a*osc.m < a*(b/a) by A4,A15,XREAL_1:68;
then a*osc.m < b by A4,XCMPLX_1:87;
hence thesis by A47,A27,XXREAL_0:2;
end;
then osc1 is convergent by SEQ_2:def 6;
then
A48: lim(upper_sum(g,T)-lower_sum(g,T))=0 by A12,SEQ_2:def 7;
A49: lower_sum(g,T) is convergent by A3,A6,A7,Th8;
upper_sum(g,T) is convergent by A3,A6,A7,Th9;
hence thesis by A49,A48,SEQ_2:12;
end;
hence thesis by A3,Th12;
end;
theorem Th28:
for f,g,h being Function of A,REAL st f|A is bounded & f is
integrable & g|A is bounded & g is integrable & h|A is bounded & a > 0 & (for x
,y st x in A & y in A holds |.h.x-h.y.|<=a*(|.f.x-f.y.|+|.g.x-g.y.|)) holds
h is integrable
proof
let f,g,h be Function of A,REAL;
assume that
A1: f|A is bounded and
A2: f is integrable and
A3: g|A is bounded and
A4: g is integrable and
A5: h|A is bounded and
A6: a>0 and
A7: for x,y st x in A & y in A holds |.h.x-h.y.|<=a*(|.f.x-f.y.|+|.g
.x-g.y.|);
for T being DivSequence of A st delta(T) is convergent & lim delta(T)= 0
holds lim upper_sum(h,T)-lim lower_sum(h,T)=0
proof
let T be DivSequence of A;
assume that
A8: delta(T) is convergent and
A9: lim delta(T)=0;
A10: lower_sum(g,T) is convergent by A3,A8,A9,Th8;
A11: upper_sum(g,T) is convergent by A3,A8,A9,Th9;
then
A12: upper_sum(g,T)-lower_sum(g,T) is convergent by A10;
lim upper_sum(g,T)-lim lower_sum(g,T)=0 by A3,A4,A8,A9,Th12;
then
A13: lim(upper_sum(g,T)-lower_sum(g,T))=0 by A11,A10,SEQ_2:12;
A14: lower_sum(f,T) is convergent by A1,A8,A9,Th8;
reconsider osc2=upper_sum(h,T)-lower_sum(h,T) as Real_Sequence;
reconsider osc1=upper_sum(g,T)-lower_sum(g,T) as Real_Sequence;
reconsider osc=upper_sum(f,T)-lower_sum(f,T) as Real_Sequence;
A15: upper_sum(f,T) is convergent by A1,A8,A9,Th9;
lim upper_sum(f,T)-lim lower_sum(f,T)=0 by A1,A2,A8,A9,Th12;
then
A16: lim(upper_sum(f,T)-lower_sum(f,T))=0 by A15,A14,SEQ_2:12;
A17: upper_sum(f,T)-lower_sum(f,T) is convergent by A15,A14;
A18: for b be Real st 0<b
ex n being Nat st for m being Nat st n <= m holds |.osc2.m-
0.|<b
proof
let b be Real;
assume b>0;
then b/a > 0 by A6,XREAL_1:139;
then
A19: (b/a)/2 > 0 by XREAL_1:139;
then consider n1 being Nat such that
A20: for m being Nat st n1 <= m
holds |. osc.m - 0 .|<(b/a)/2 by A17,A16,SEQ_2:def 7;
consider n2 being Nat such that
A21: for m being Nat st n2 <= m
holds |. osc1.m-0 .|<(b/a)/2 by A12,A13,A19,SEQ_2:def 7;
ex n st n1 <= n & n2 <= n
proof
take n=max(n1,n2);
n is Element of NAT by ORDINAL1:def 12;
hence thesis by XXREAL_0:25;
end;
then consider n such that
A22: n1 <= n and
A23: n2 <= n;
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;
len upper_volume(f,D)=len D by INTEGRA1:def 6;
then reconsider
UV=upper_volume(f,D) as Element of (len D)-tuples_on REAL
by FINSEQ_2:133;
len lower_volume(f,D)=len D by INTEGRA1:def 7;
then reconsider
LV=lower_volume(f,D) as Element of (len D)-tuples_on REAL
by FINSEQ_2:133;
osc.m=(upper_sum(f,T)).m+(-lower_sum(f,T)).m by SEQ_1:7
.=(upper_sum(f,T)).m+-(lower_sum(f,T)).m by SEQ_1:10
.=(upper_sum(f,T)).m-(lower_sum(f,T)).m
.=upper_sum(f,T.mm)-(lower_sum(f,T)).m by INTEGRA2:def 2
.=upper_sum(f,T.mm)-lower_sum(f,T.mm) by INTEGRA2:def 3
.=Sum(upper_volume(f,D))-lower_sum(f,T.mm) by INTEGRA1:def 8
.=Sum(upper_volume(f,D))-Sum(lower_volume(f,D)) by INTEGRA1:def 9;
then
A24: osc.m=Sum(UV-LV) by RVSUM_1:90;
len lower_volume(h,D) = len D by INTEGRA1:def 7;
then reconsider
LV2=lower_volume(h,D) as Element of (len D)-tuples_on REAL
by FINSEQ_2:133;
len upper_volume(h,D) = len D by INTEGRA1:def 6;
then reconsider
UV2=upper_volume(h,D) as Element of (len D)-tuples_on REAL
by FINSEQ_2:133;
len lower_volume(g,D)=len D by INTEGRA1:def 7;
then reconsider
LV1=lower_volume(g,D) as Element of (len D)-tuples_on REAL
by FINSEQ_2:133;
len upper_volume(g,D)=len D by INTEGRA1:def 6;
then reconsider
UV1=upper_volume(g,D) as Element of (len D)-tuples_on REAL
by FINSEQ_2:133;
reconsider H = UV-LV as FinSequence of REAL;
reconsider G = UV1-LV1 as FinSequence of REAL;
reconsider F = UV2-LV2 as FinSequence of REAL;
osc1.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
.=upper_sum(g,T.mm)-(lower_sum(g,T)).m by INTEGRA2:def 2
.=upper_sum(g,T.mm)-lower_sum(g,T.mm) by INTEGRA2:def 3
.=Sum(upper_volume(g,D))-lower_sum(g,T.mm) by INTEGRA1:def 8
.=Sum(upper_volume(g,D))-Sum(lower_volume(g,D)) by INTEGRA1:def 9;
then
A25: osc1.m=Sum(UV1-LV1) by RVSUM_1:90;
for j be Nat st j in dom G holds 0 <= G.j
proof
let j be Nat;
set r = G.j;
A26: rng g is bounded_below by A3,INTEGRA1:11;
assume that
A27: j in dom G;
j in Seg len G by A27,FINSEQ_1:def 3;
then
A28: j in Seg len D by CARD_1:def 7;
then
A29: j in dom D by FINSEQ_1:def 3;
then
A30: LV1.j=(lower_bound (rng (g|divset(D,j))))*vol(divset(D,j)) by
INTEGRA1:def 7;
A31: ex r st r in rng (g|divset(D,j))
proof
consider r being Element of REAL such that
A32: r in divset(D,j) by SUBSET_1:4;
j in dom D by A28,FINSEQ_1:def 3;
then divset(D,j) c= A by INTEGRA1:8;
then r in A by A32;
then r in dom g by FUNCT_2:def 1;
then r in dom g /\ divset(D,j) by A32,XBOOLE_0:def 4;
then r in dom (g|divset(D,j)) by RELAT_1:61;
then (g|divset(D,j)).r in rng(g|divset(D,j)) by FUNCT_1:def 3;
hence thesis;
end;
rng g is bounded_above by A3,INTEGRA1:13;
then rng (g|divset(D,j)) is real-bounded
by A26,RELAT_1:70,XXREAL_2:45;
then
A33: upper_bound(rng(g|divset(D,j)))-lower_bound(rng(g|divset(D,j))
)>=0 by A31,SEQ_4:11,XREAL_1:48;
UV1.j=(upper_bound (rng (g|divset(D,j))))*vol(divset(D,j)) by A29,
INTEGRA1:def 6;
then
A34: r = (upper_bound(rng(g|divset(D,j))))*vol(divset(D,j)) -(
lower_bound(rng(g|divset(D,j))))*vol(divset(D,j)) by A27,A30,VALUED_1:13
.=(upper_bound(rng(g|divset(D,j))) - lower_bound(rng(g|divset(D,
j))))* vol(divset(D,j));
vol(divset(D,j))>=0 by INTEGRA1:9;
hence thesis by A34,A33;
end;
then
A35: osc1.m >=0 by A25,RVSUM_1:84;
assume
A36: n <= m;
then n1<=m by A22,XXREAL_0:2;
then
A37: |. osc.m - 0 .|<(b/a)/2 by A20;
n2<=m by A23,A36,XXREAL_0:2;
then
A38: |. osc1.m - 0 .|<(b/a)/2 by A21;
for j be Nat st j in dom H holds 0 <= H.j
proof
let j be Nat;
set r = H.j;
A39: rng f is bounded_below by A1,INTEGRA1:11;
assume that
A40: j in dom H;
j in Seg len H by A40,FINSEQ_1:def 3;
then
A41: j in Seg len D by CARD_1:def 7;
then
A42: j in dom D by FINSEQ_1:def 3;
then
A43: LV.j=(lower_bound (rng (f|divset(D,j))))*vol(divset(D,j)) by
INTEGRA1:def 7;
A44: ex r st r in rng (f|divset(D,j))
proof
consider r being Element of REAL such that
A45: r in divset(D,j) by SUBSET_1:4;
j in dom D by A41,FINSEQ_1:def 3;
then divset(D,j) c= A by INTEGRA1:8;
then r in A by A45;
then r in dom f by FUNCT_2:def 1;
then r in dom f /\ divset(D,j) by A45,XBOOLE_0:def 4;
then r in dom (f|divset(D,j)) by RELAT_1:61;
then (f|divset(D,j)).r in rng(f|divset(D,j)) by FUNCT_1:def 3;
hence thesis;
end;
rng f is bounded_above by A1,INTEGRA1:13;
then rng (f|divset(D,j)) is real-bounded
by A39,RELAT_1:70,XXREAL_2:45;
then
A46: upper_bound(rng(f|divset(D,j)))-lower_bound(rng(f|divset(D,j))
)>=0 by A44,SEQ_4:11,XREAL_1:48;
UV.j=(upper_bound (rng (f|divset(D,j))))*vol(divset(D,j)) by A42,
INTEGRA1:def 6;
then
A47: r = (upper_bound(rng(f|divset(D,j))))*vol(divset(D,j)) -(
lower_bound(rng(f|divset(D,j))))*vol(divset(D,j)) by A40,A43,VALUED_1:13
.=(upper_bound(rng(f|divset(D,j))) - lower_bound(rng(f|divset(D,
j))))* vol(divset(D,j));
vol(divset(D,j))>=0 by INTEGRA1:9;
hence thesis by A47,A46;
end;
then
A48: osc.m >= 0 by A24,RVSUM_1:84;
then osc.m*osc1.m >=0 by A35;
then |.osc.m.|+|.osc1.m.|=|.osc.m+osc1.m.| by ABSVALUE:11;
then |.osc.m-0.|+|.osc1.m.|=osc.m+osc1.m by A48,A35,ABSVALUE:def 1;
then osc.m+osc1.m < (b/a)/2+(b/a)/2 by A37,A38,XREAL_1:8;
then a*(osc.m+osc1.m) < a*(b/a) by A6,XREAL_1:68;
then
A49: a*(osc.m+osc1.m) < b by A6,XCMPLX_1:87;
osc2.m=(upper_sum(h,T)).m+(-lower_sum(h,T)).m by SEQ_1:7
.=(upper_sum(h,T)).m+-(lower_sum(h,T)).m by SEQ_1:10
.=(upper_sum(h,T)).m-(lower_sum(h,T)).m
.=upper_sum(h,T.mm)-(lower_sum(h,T)).m by INTEGRA2:def 2
.=upper_sum(h,T.mm)-lower_sum(h,T.mm) by INTEGRA2:def 3
.=Sum(upper_volume(h,D))-lower_sum(h,T.mm) by INTEGRA1:def 8
.=Sum(upper_volume(h,D))-Sum(lower_volume(h,D)) by INTEGRA1:def 9;
then
A50: osc2.m=Sum(UV2-LV2) by RVSUM_1:90;
for j be Nat st j in dom F holds 0 <= F.j
proof
let j be Nat;
set r = F.j;
A51: rng h is bounded_below by A5,INTEGRA1:11;
assume that
A52: j in dom F;
j in Seg len F by A52,FINSEQ_1:def 3;
then
A53: j in Seg len D by CARD_1:def 7;
then
A54: j in dom D by FINSEQ_1:def 3;
then
A55: LV2.j=(lower_bound (rng (h|divset(D,j))))*vol(divset(D,j)) by
INTEGRA1:def 7;
A56: ex r st r in rng (h|divset(D,j))
proof
consider r being Element of REAL such that
A57: r in divset(D,j) by SUBSET_1:4;
j in dom D by A53,FINSEQ_1:def 3;
then divset(D,j) c= A by INTEGRA1:8;
then r in A by A57;
then r in dom h by FUNCT_2:def 1;
then r in dom h /\ divset(D,j) by A57,XBOOLE_0:def 4;
then r in dom (h|divset(D,j)) by RELAT_1:61;
then (h|divset(D,j)).r in rng(h|divset(D,j)) by FUNCT_1:def 3;
hence thesis;
end;
rng h is bounded_above by A5,INTEGRA1:13;
then rng (h|divset(D,j)) is real-bounded
by A51,RELAT_1:70,XXREAL_2:45;
then
A58: upper_bound(rng(h|divset(D,j)))-lower_bound(rng(h|divset(D,j))
)>=0 by A56,SEQ_4:11,XREAL_1:48;
UV2.j=(upper_bound (rng (h|divset(D,j))))*vol(divset(D,j)) by A54,
INTEGRA1:def 6;
then
A59: r = (upper_bound(rng(h|divset(D,j))))*vol(divset(D,j)) -(
lower_bound(rng(h|divset(D,j))))*vol(divset(D,j)) by A52,A55,VALUED_1:13
.=(upper_bound(rng(h|divset(D,j))) - lower_bound(rng(h|divset(D,
j))))* vol(divset(D,j));
vol(divset(D,j))>=0 by INTEGRA1:9;
hence thesis by A59,A58;
end;
then osc2.m >= 0 by A50,RVSUM_1:84;
then
A60: |. osc2.m .|=osc2.m by ABSVALUE:def 1;
for j be Nat st j in Seg(len D) holds (UV2-LV2).j <= (a*((UV-LV)+
(UV1-LV1))).j
proof
let j be Nat;
set x=(UV2-LV2).j, y=(a*((UV-LV)+(UV1-LV1))).j;
A61: y=a*(((UV-LV)+(UV1-LV1)).j) by RVSUM_1:45
.=a*((UV-LV).j+(UV1-LV1).j) by RVSUM_1:11
.=a*(UV.j-LV.j+(UV1-LV1).j) by RVSUM_1:27
.=a*(UV.j-LV.j+(UV1.j-LV1.j)) by RVSUM_1:27;
A62: vol(divset(D,j)) >= 0 by INTEGRA1:9;
assume
A63: j in Seg (len D);
then
A64: j in dom D by FINSEQ_1:def 3;
then
A65: LV2.j=(lower_bound (rng (h|divset(D,j))))*vol(divset(D,j)) by
INTEGRA1:def 7;
UV2.j=(upper_bound (rng (h|divset(D,j))))*vol(divset(D,j)) by A64,
INTEGRA1:def 6;
then
A66: x=(upper_bound rng (h|divset(D,j)))*vol(divset(D,j)) -(
lower_bound rng (h|divset(D,j)))*vol(divset(D,j)) by A65,RVSUM_1:27
.=(upper_bound rng (h|divset(D,j))-lower_bound rng (h|divset(D,j
))) *vol(divset(D,j));
A67: LV1 .j=(lower_bound rng (g|divset(D,j)))*vol(divset(D,j)) by A64,
INTEGRA1:def 7;
A68: UV1 .j=(upper_bound rng (g|divset(D,j)))*vol(divset(D,j)) by A64,
INTEGRA1:def 6;
A69: a*(((upper_bound rng(f|divset(D,j))-lower_bound rng(f|divset(D,
j))) +(upper_bound rng (g|divset(D,j))-lower_bound rng (g|divset(D,j))))) >=
upper_bound rng (h|divset(D,j))-lower_bound rng (h|divset(D,j))
proof
A70: j in dom D by A63,FINSEQ_1:def 3;
A71: dom(g|divset(D,j)) = dom g /\ divset(D,j) by RELAT_1:61
.= A /\ divset(D,j) by FUNCT_2:def 1
.= divset(D,j) by A70,INTEGRA1:8,XBOOLE_1:28;
then reconsider
g1=g|divset(D,j) as PartFunc of divset(D,j),REAL by RELSET_1:5;
reconsider g1 as Function of divset(D,j),REAL by A71,FUNCT_2:def 1;
A72: g|divset(D,j)|divset(D,j) is bounded_below by A3,A71,INTEGRA2:6;
A73: dom(h|divset(D,j)) = dom h /\ divset(D,j) by RELAT_1:61
.= A /\ divset(D,j) by FUNCT_2:def 1
.= divset(D,j) by A70,INTEGRA1:8,XBOOLE_1:28;
then reconsider
h1=h|divset(D,j) as PartFunc of divset(D,j),REAL by RELSET_1:5;
reconsider h1 as Function of divset(D,j),REAL by A73,FUNCT_2:def 1;
A74: dom(f|divset(D,j)) = dom f /\ divset(D,j) by RELAT_1:61
.= A /\ divset(D,j) by FUNCT_2:def 1
.= divset(D,j) by A70,INTEGRA1:8,XBOOLE_1:28;
then reconsider
f1=f|divset(D,j) as PartFunc of divset(D,j),REAL by RELSET_1:5;
A75: f|divset(D,j)|divset(D,j) is bounded_below by A1,A74,INTEGRA2:6;
A76: for x,y st x in divset(D,j) & y in divset(D,j) holds |.h1.x
-h1.y.| <= a*(|.f1.x-f1.y.|+|.g1.x-g1.y.|)
proof
let x,y;
assume that
A77: x in divset(D,j) and
A78: y in divset(D,j);
A79: g.y=g1.y by A71,A78,FUNCT_1:47;
A80: h.y=h1.y by A73,A78,FUNCT_1:47;
A81: h.x=h1.x by A73,A77,FUNCT_1:47;
A82: f.y=f1.y by A74,A78,FUNCT_1:47;
A83: f.x=f1.x by A74,A77,FUNCT_1:47;
g.x=g1.x by A71,A77,FUNCT_1:47;
hence thesis by A7,A74,A77,A78,A79,A83,A82,A81,A80;
end;
g|divset(D,j)|divset(D,j) is bounded_above by A3,A71,INTEGRA2:5;
then
A84: g1|divset(D,j) is bounded by A72;
f|divset(D,j)|divset(D,j) is bounded_above by A1,A74,INTEGRA2:5;
then
A85: f1|divset(D,j) is bounded by A75;
f1 is total by A74,PARTFUN1:def 2;
hence thesis by A6,A85,A84,A76,Th26;
end;
LV .j=(lower_bound rng (f|divset(D,j)))*vol(divset(D,j)) by A64,
INTEGRA1:def 7;
then y=a*(((upper_bound rng (f|divset(D,j)))*vol(divset(D,j)) -(
lower_bound rng (f|divset(D,j)))*vol(divset(D,j))) +((upper_bound rng (g|divset
(D,j)))*vol(divset(D,j)) -(lower_bound rng (g|divset(D,j)))*vol(divset(D,j))))
by A64,A68,A67,A61,INTEGRA1:def 6
.=a*(((upper_bound rng(f|divset(D,j))- lower_bound rng(f|divset(
D,j))) +(upper_bound rng (g|divset(D,j))-lower_bound rng (g|divset(D,j)))))*
vol(divset(D,j));
hence thesis by A66,A69,A62,XREAL_1:64;
end;
then osc2.m <= Sum(a*((UV-LV)+(UV1-LV1))) by A50,RVSUM_1:82;
then osc2.m <= a*Sum((UV-LV)+(UV1-LV1)) by RVSUM_1:87;
then osc2.m <= a*(osc.m+osc1.m) by A24,A25,RVSUM_1:89;
hence thesis by A60,A49,XXREAL_0:2;
end;
then osc2 is convergent by SEQ_2:def 6;
then
A86: lim(upper_sum(h,T)-lower_sum(h,T))=0 by A18,SEQ_2:def 7;
A87: lower_sum(h,T) is convergent by A5,A8,A9,Th8;
upper_sum(h,T) is convergent by A5,A8,A9,Th9;
hence thesis by A87,A86,SEQ_2:12;
end;
hence thesis by A5,Th12;
end;
theorem
for f,g being Function of A,REAL st f|A is bounded & f is integrable &
g|A is bounded & g is integrable holds f(#)g is integrable
proof
let f,g be Function of A,REAL;
assume that
A1: f|A is bounded and
A2: f is integrable and
A3: g|A is bounded and
A4: g is integrable;
A5: (f(#)g)|(A /\ A) is bounded by A1,A3,RFUNCT_1:84;
consider r2 be Real such that
A6: for x being object st x in A /\ dom g holds |.g.x.|<=r2 by A3,RFUNCT_1:73;
A7: A /\ dom g = A /\ A by FUNCT_2:def 1
.= A;
A8: A /\ dom f = A /\ A by FUNCT_2:def 1
.= A;
then consider a being Element of REAL such that
A9: a in A /\ dom f by SUBSET_1:4;
reconsider a as Element of A by A9;
A10: |.f.a.|>=0 by COMPLEX1:46;
consider r1 be Real such that
A11: for x being object st x in A /\ dom f holds |.f.x.|<=r1
by A1,RFUNCT_1:73;
reconsider r=max(r1,r2) as Real;
A12: r2<=r by XXREAL_0:25;
A13: r1<=r by XXREAL_0:25;
A14: for x,y st x in A & y in A holds |.(f(#)g).x-(f(#)g).y.|<=r*(|.g.x-g
.y.|+|.f.x-f.y.|)
proof
let x,y;
assume that
A15: x in A and
A16: y in A;
A17: (f(#)g).y=f.y*g.y by VALUED_1:5;
|.g.y.|<=r2 by A6,A7,A16;
then
A18: |.g.y.|<=r by A12,XXREAL_0:2;
A19: |.f.x-f.y.|>=0 by COMPLEX1:46;
|.(f.x-f.y)*g.y.|=|.f.x-f.y.|*|.g.y.| by COMPLEX1:65;
then
A20: |.(f.x-f.y)*g.y.|<=r*|.f.x-f.y.| by A19,A18,XREAL_1:64;
(f(#)g).x=f.x*g.x by VALUED_1:5;
then |.(f(#)g).x-(f(#) g).y.|=|.f.x*(g.x-g.y)+(f.x-f.y)*g.y.| by A17;
then
A21: |.(f(#)g).x-(f(#) g).y.|<=|.f.x*(g.x-g.y).|+|.(f.x-f.y)*g.y.| by
COMPLEX1:56;
|.f.x.|<=r1 by A11,A8,A15;
then
A22: |.f.x.|<=r by A13,XXREAL_0:2;
A23: |.g.x-g.y.|>=0 by COMPLEX1:46;
|.f.x*(g.x-g.y).|=|.f.x.|*|.g.x-g.y.| by COMPLEX1:65;
then |.f.x*(g.x-g.y).|<=r*|.g.x-g.y.| by A23,A22,XREAL_1:64;
then |.f.x*(g.x-g.y).|+|.(f.x-f.y)*g.y.|<=r*|.g.x-g.y.|+r*|.f.x-f.y.|
by A20,XREAL_1:7;
hence thesis by A21,XXREAL_0:2;
end;
A24: |.f.a.|<=r1 by A11,A9;
now
per cases by A24,A10,XXREAL_0:25;
suppose
A25: r=0;
for x,y st x in A & y in A holds |.(f(#)g).x-(f(#)g).y.|<=1*|.f.
x-f.y.|
proof
let x,y;
assume that
A26: x in A and
A27: y in A;
|.(f(#)g).x-(f(#)g).y.|<=r*(|.g.x-g.y.|+|.f.x-f.y.|) by A14,A26,A27;
hence thesis by A25,COMPLEX1:46;
end;
hence thesis by A1,A2,A5,Th27;
end;
suppose
r>0;
hence thesis by A1,A2,A3,A4,A5,A14,Th28;
end;
end;
hence thesis;
end;
theorem
for f being Function of A,REAL st f|A is bounded & f is integrable &
not 0 in rng f & f^|A is bounded holds f^ is integrable
proof
let f be Function of A,REAL;
assume that
A1: f|A is bounded and
A2: f is integrable and
A3: not 0 in rng f and
A4: f^|A is bounded;
consider r be Real such that
A5: for x being object st x in A /\ dom(f^) holds |.(f^).x.|<=r
by A4,RFUNCT_1:73;
reconsider r as Real;
f"{0} = {} by A3,FUNCT_1:72;
then
A6: f^ is total by RFUNCT_1:54;
A7: for x,y st x in A & y in A holds |.(f^).x-(f^).y.|<=(r^2)*|.f.x-f.y.|
proof
let x,y;
assume that
A8: x in A and
A9: y in A;
A10: x in dom(f^) by A6,A8,PARTFUN1:def 2;
then
A11: f.x<>0 by RFUNCT_1:3;
A12: y in dom(f^) by A6,A9,PARTFUN1:def 2;
then
A13: f.y<>0 by RFUNCT_1:3;
0<=1/|.f.x.| &0<=1/|.f.y.| & 1/|.f.x.|<=r & 1/|.f.y.|<=r
proof
A14: |.f.y.|>0 by A13,COMPLEX1:47;
|.f.x.|>0 by A11,COMPLEX1:47;
hence 0<=1/|.f.x.| &0<=1/|.f.y.| by A14;
reconsider x,y as Element of A by A8,A9;
y in A /\ dom(f^) by A12,XBOOLE_0:def 4;
then |.(f^).y.|<=r by A5;
then |.1*(f.y)".|<=r by A12,RFUNCT_1:def 2;
then
A15: |.1/(f.y).|<=r by XCMPLX_0:def 9;
x in A /\ dom(f^) by A10,XBOOLE_0:def 4;
then |.(f^).x.|<=r by A5;
then |.1*(f.x)".|<=r by A10,RFUNCT_1:def 2;
then |.1/(f.x).|<=r by XCMPLX_0:def 9;
hence thesis by A15,ABSVALUE:7;
end;
then
A16: (1/|.f.x.|)*(1/|.f.y.|)<=r*r by XREAL_1:66;
|.f.x-f.y.|>=0 by COMPLEX1:46;
then
A17: |.f.x-f.y.|*((1/|.f.x.|)*(1/|.f.y.|))<=|.f.x-f.y.|*r^2 by A16,
XREAL_1:64;
(f^).x-(f^).y = (f.x)"-(f^).y by A10,RFUNCT_1:def 2
.=(f.x)"-(f.y)" by A12,RFUNCT_1:def 2;
then |.(f^).x-(f^).y.|=|.f.x-f.y.|/(|.f.x.|*|.f.y.|) by A13,A11,SEQ_2:2
.=|.f.x-f.y.|/|.f.x.|*(1/|.f.y.|) by XCMPLX_1:103
.=|.f.x-f.y.|*(1/|.f.x.|)*(1/|.f.y.|) by XCMPLX_1:99;
hence thesis by A17;
end;
per cases by XREAL_1:63;
suppose
A18: r^2=0;
for x,y st x in A & y in A holds |.(f^).x-(f^).y.|<=1*|.f.x-f.y.|
proof
let x,y;
assume that
A19: x in A and
A20: y in A;
|.(f^).x-(f^).y.|<=0*|.f.x-f.y.| by A7,A18,A19,A20;
hence thesis by COMPLEX1:46;
end;
hence thesis by A1,A2,A4,A6,Th27;
end;
suppose
r^2>0;
hence thesis by A1,A2,A4,A6,A7,Th27;
end;
end;