let a be Real; :: thesis: for A being closed-interval Subset of REAL
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 being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) holds
g is integrable
let A be closed-interval Subset of REAL ; :: thesis: 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 being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) holds
g is integrable
let f, g be Function of A,REAL ; :: thesis: ( f | A is bounded & f is integrable & g | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) implies g is integrable )
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 being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y)))
; :: thesis: g is integrable
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;
:: thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum g,T)) - (lim (lower_sum g,T)) = 0 )
assume that A6:
delta T is
convergent
and A7:
lim (delta T) = 0
;
:: thesis: (lim (upper_sum g,T)) - (lim (lower_sum g,T)) = 0
A8:
(
upper_sum g,
T is
convergent &
lower_sum g,
T is
convergent )
by A3, A6, A7, Th8, Th9;
A9:
(
upper_sum f,
T is
convergent &
lower_sum f,
T is
convergent )
by A1, A6, A7, Th8, Th9;
A10:
(lim (upper_sum f,T)) - (lim (lower_sum f,T)) = 0
by A1, A2, A6, A7, Th12;
A11:
(upper_sum f,T) - (lower_sum f,T) is
convergent
by A9, SEQ_2:25;
reconsider osc =
(upper_sum f,T) - (lower_sum f,T) as
Real_Sequence ;
reconsider osc1 =
(upper_sum g,T) - (lower_sum g,T) as
Real_Sequence ;
A12:
lim ((upper_sum f,T) - (lower_sum f,T)) = 0
by A9, A10, SEQ_2:26;
A13:
for
b being
real number st
0 < b holds
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
n <= m holds
abs ((osc1 . m) - 0 ) < b
proof
let b be
real number ;
:: thesis: ( 0 < b implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0 ) < b )
assume
b > 0
;
:: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc1 . m) - 0 ) < b
then
b / a > 0
by A4, XREAL_1:141;
then consider n being
Element of
NAT such that A14:
for
m being
Element of
NAT st
n <= m holds
abs ((osc . m) - 0 ) < b / a
by A11, A12, SEQ_2:def 7;
for
m being
Element of
NAT st
n <= m holds
abs ((osc1 . m) - 0 ) < b
proof
let m be
Element of
NAT ;
:: thesis: ( n <= m implies abs ((osc1 . m) - 0 ) < b )
assume
n <= m
;
:: thesis: abs ((osc1 . m) - 0 ) < b
then A15:
abs ((osc . m) - 0 ) < b / a
by A14;
reconsider D =
T . m as
Division of
A ;
A16:
osc . m =
((upper_sum f,T) . m) + ((- (lower_sum f,T)) . m)
by SEQ_1:11
.=
((upper_sum f,T) . m) + (- ((lower_sum f,T) . m))
by SEQ_1:14
.=
((upper_sum f,T) . m) - ((lower_sum f,T) . m)
.=
(upper_sum f,(T . m)) - ((lower_sum f,T) . m)
by INTEGRA2:def 4
.=
(upper_sum f,(T . m)) - (lower_sum f,(T . m))
by INTEGRA2:def 5
.=
(Sum (upper_volume f,D)) - (lower_sum f,(T . m))
by INTEGRA1:def 9
.=
(Sum (upper_volume f,D)) - (Sum (lower_volume f,D))
by INTEGRA1:def 10
;
len (upper_volume f,D) = len D
by INTEGRA1:def 7;
then reconsider UV =
upper_volume f,
D as
Element of
(len D) -tuples_on REAL by CATALG_1:5;
len (lower_volume f,D) = len D
by INTEGRA1:def 8;
then reconsider LV =
lower_volume f,
D as
Element of
(len D) -tuples_on REAL by CATALG_1:5;
A17:
osc . m = Sum (UV - LV)
by A16, RVSUM_1:120;
A18:
osc1 . m =
((upper_sum g,T) . m) + ((- (lower_sum g,T)) . m)
by SEQ_1:11
.=
((upper_sum g,T) . m) + (- ((lower_sum g,T) . m))
by SEQ_1:14
.=
((upper_sum g,T) . m) - ((lower_sum g,T) . m)
.=
(upper_sum g,(T . m)) - ((lower_sum g,T) . m)
by INTEGRA2:def 4
.=
(upper_sum g,(T . m)) - (lower_sum g,(T . m))
by INTEGRA2:def 5
.=
(Sum (upper_volume g,D)) - (lower_sum g,(T . m))
by INTEGRA1:def 9
.=
(Sum (upper_volume g,D)) - (Sum (lower_volume g,D))
by INTEGRA1:def 10
;
len (upper_volume g,D) = len D
by INTEGRA1:def 7;
then reconsider UV1 =
upper_volume g,
D as
Element of
(len D) -tuples_on REAL by CATALG_1:5;
len (lower_volume g,D) = len D
by INTEGRA1:def 8;
then reconsider LV1 =
lower_volume g,
D as
Element of
(len D) -tuples_on REAL by CATALG_1:5;
A19:
osc1 . m = Sum (UV1 - LV1)
by A18, RVSUM_1:120;
for
j being
Nat st
j in Seg (len D) holds
(UV1 - LV1) . j <= (a * (UV - LV)) . j
proof
let j be
Nat;
:: thesis: ( j in Seg (len D) implies (UV1 - LV1) . j <= (a * (UV - LV)) . j )
assume A20:
j in Seg (len D)
;
:: thesis: (UV1 - LV1) . j <= (a * (UV - LV)) . j
then B20:
j in dom D
by FINSEQ_1:def 3;
set x =
(UV1 - LV1) . j;
set y =
(a * (UV - LV)) . j;
A21:
UV1 . j = (upper_bound (rng (g | (divset D,j)))) * (vol (divset D,j))
by B20, INTEGRA1:def 7;
LV1 . j = (lower_bound (rng (g | (divset D,j)))) * (vol (divset D,j))
by B20, INTEGRA1:def 8;
then A22:
(UV1 - LV1) . j =
((upper_bound (rng (g | (divset D,j)))) * (vol (divset D,j))) - ((lower_bound (rng (g | (divset D,j)))) * (vol (divset D,j)))
by A21, RVSUM_1:48
.=
((upper_bound (rng (g | (divset D,j)))) - (lower_bound (rng (g | (divset D,j))))) * (vol (divset D,j))
;
A23:
UV . j = (upper_bound (rng (f | (divset D,j)))) * (vol (divset D,j))
by B20, INTEGRA1:def 7;
A24:
LV . j = (lower_bound (rng (f | (divset D,j)))) * (vol (divset D,j))
by B20, INTEGRA1:def 8;
(a * (UV - LV)) . j = a * ((UV - LV) . j)
by RVSUM_1:67;
then A25:
(a * (UV - LV)) . j =
a * (((upper_bound (rng (f | (divset D,j)))) * (vol (divset D,j))) - ((lower_bound (rng (f | (divset D,j)))) * (vol (divset D,j))))
by A23, A24, RVSUM_1:48
.=
a * (((upper_bound (rng (f | (divset D,j)))) - (lower_bound (rng (f | (divset D,j))))) * (vol (divset D,j)))
;
A26:
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
A27:
j in dom D
by A20, FINSEQ_1:def 3;
then A28:
divset D,
j c= A
by INTEGRA1:10;
A29:
dom (f | (divset D,j)) =
(dom f) /\ (divset D,j)
by RELAT_1:90
.=
A /\ (divset D,j)
by FUNCT_2:def 1
.=
divset D,
j
by A27, INTEGRA1:10, XBOOLE_1:28
;
then reconsider f1 =
f | (divset D,j) as
PartFunc of
(divset D,j),
REAL by RELSET_1:13;
reconsider f1 =
f1 as
Function of
(divset D,j),
REAL by A29, FUNCT_2:def 1;
A30:
dom (g | (divset D,j)) =
(dom g) /\ (divset D,j)
by RELAT_1:90
.=
A /\ (divset D,j)
by FUNCT_2:def 1
.=
divset D,
j
by A27, INTEGRA1:10, XBOOLE_1:28
;
then reconsider g1 =
g | (divset D,j) as
PartFunc of
(divset D,j),
REAL by RELSET_1:13;
reconsider g1 =
g1 as
Function of
(divset D,j),
REAL by A30, FUNCT_2:def 1;
(
f | A is
bounded_above &
f | A is
bounded_below )
by A1;
then
(
(f | (divset D,j)) | (divset D,j) is
bounded_above &
(f | (divset D,j)) | (divset D,j) is
bounded_below )
by A28, INTEGRA2:5, INTEGRA2:6;
then
(f | (divset D,j)) | (divset D,j) is
bounded
;
then consider r being
real number such that A31:
for
x being
set st
x in (divset D,j) /\ (dom (f | (divset D,j))) holds
abs ((f | (divset D,j)) . x) <= r
by RFUNCT_1:90;
A32:
f1 | (divset D,j) is
bounded
by A31, RFUNCT_1:90;
for
x,
y being
Real st
x in divset D,
j &
y in divset D,
j holds
abs ((g1 . x) - (g1 . y)) <= a * (abs ((f1 . x) - (f1 . y)))
hence
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))))
by A4, A32, Th25;
:: thesis: verum
end;
vol (divset D,j) >= 0
by INTEGRA1:11;
then
(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 A26, XREAL_1:66;
hence
(UV1 - LV1) . j <= (a * (UV - LV)) . j
by A22, A25;
:: thesis: verum
end;
then
osc1 . m <= Sum (a * (UV - LV))
by A19, RVSUM_1:112;
then A34:
osc1 . m <= a * (osc . m)
by A17, RVSUM_1:117;
reconsider F =
UV1 - LV1 as
FinSequence of
REAL ;
A35:
osc1 . m >= 0
proof
for
j being
Nat st
j in dom F holds
0 <= F . j
proof
let j be
Nat;
:: thesis: ( j in dom F implies 0 <= F . j )
assume A36:
j in dom F
;
:: thesis: 0 <= F . j
set r =
F . j;
j in Seg (len F)
by A36, FINSEQ_1:def 3;
then A37:
j in Seg (len D)
by FINSEQ_1:def 18;
then
j in dom D
by FINSEQ_1:def 3;
then
(
UV1 . j = (upper_bound (rng (g | (divset D,j)))) * (vol (divset D,j)) &
LV1 . j = (lower_bound (rng (g | (divset D,j)))) * (vol (divset D,j)) )
by INTEGRA1:def 7, INTEGRA1:def 8;
then A38:
F . j =
((upper_bound (rng (g | (divset D,j)))) * (vol (divset D,j))) - ((lower_bound (rng (g | (divset D,j)))) * (vol (divset D,j)))
by A36, VALUED_1:13
.=
((upper_bound (rng (g | (divset D,j)))) - (lower_bound (rng (g | (divset D,j))))) * (vol (divset D,j))
;
A39:
(upper_bound (rng (g | (divset D,j)))) - (lower_bound (rng (g | (divset D,j)))) >= 0
proof
(
rng (g | (divset D,j)) is
bounded & ex
r being
Real st
r in rng (g | (divset D,j)) )
proof
consider r being
Real such that A40:
r in divset D,
j
by SUBSET_1:10;
j in dom D
by A37, FINSEQ_1:def 3;
then
divset D,
j c= A
by INTEGRA1:10;
then
r in A
by A40;
then
r in dom g
by FUNCT_2:def 1;
then
r in (dom g) /\ (divset D,j)
by A40, XBOOLE_0:def 4;
then
r in dom (g | (divset D,j))
by RELAT_1:90;
then A41:
(g | (divset D,j)) . r in rng (g | (divset D,j))
by FUNCT_1:def 5;
(
g | A is
bounded_above &
g | A is
bounded_below )
by A3;
then
(
rng g is
bounded_above &
rng g is
bounded_below )
by INTEGRA1:13, INTEGRA1:15;
then
rng g is
bounded
;
hence
rng (g | (divset D,j)) is
bounded
by RELAT_1:99, XXREAL_2:45;
:: thesis: ex r being Real st r in rng (g | (divset D,j))
thus
ex
r being
Real st
r in rng (g | (divset D,j))
by A41;
:: thesis: verum
end;
hence
(upper_bound (rng (g | (divset D,j)))) - (lower_bound (rng (g | (divset D,j)))) >= 0
by SEQ_4:24, XREAL_1:50;
:: thesis: verum
end;
vol (divset D,j) >= 0
by INTEGRA1:11;
hence
0 <= F . j
by A38, A39;
:: thesis: verum
end;
hence
osc1 . m >= 0
by A19, RVSUM_1:114;
:: thesis: verum
end;
then A42:
abs (osc1 . m) = osc1 . m
by ABSVALUE:def 1;
osc . m >= 0 / a
by A4, A34, A35, XREAL_1:81;
then
abs (osc . m) = osc . m
by ABSVALUE:def 1;
then
a * (osc . m) < a * (b / a)
by A4, A15, XREAL_1:70;
then
a * (osc . m) < b
by A4, XCMPLX_1:88;
hence
abs ((osc1 . m) - 0 ) < b
by A34, A42, XXREAL_0:2;
:: thesis: verum
end;
hence
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
n <= m holds
abs ((osc1 . m) - 0 ) < b
;
:: thesis: verum
end;
then
osc1 is
convergent
by SEQ_2:def 6;
then
lim ((upper_sum g,T) - (lower_sum g,T)) = 0
by A13, SEQ_2:def 7;
hence
(lim (upper_sum g,T)) - (lim (lower_sum g,T)) = 0
by A8, SEQ_2:26;
:: thesis: verum
end;
hence
g is integrable
by A3, Th12; :: thesis: verum