let a be Real; for A being non empty 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
|.((g . x) - (g . y)).| <= a * |.((f . x) - (f . y)).| ) holds
g is integrable
let A be non empty 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
|.((g . x) - (g . y)).| <= a * |.((f . x) - (f . y)).| ) holds
g is integrable
let f, g be Function of A,REAL; ( 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
|.((g . x) - (g . y)).| <= a * |.((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
|.((g . x) - (g . y)).| <= a * |.((f . x) - (f . y)).|
; 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;
( 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
;
(lim (upper_sum (g,T))) - (lim (lower_sum (g,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 being
Real st
0 < b holds
ex
n being
Nat st
for
m being
Nat st
n <= m holds
|.((osc1 . m) - 0).| < b
proof
let b be
Real;
( 0 < b implies ex n being Nat st
for m being Nat st n <= m holds
|.((osc1 . m) - 0).| < b )
assume
b > 0
;
ex n being Nat st
for m being Nat st n <= m holds
|.((osc1 . m) - 0).| < b
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
;
for m being Nat st n <= m holds
|.((osc1 . m) - 0).| < b
let m be
Nat;
( n <= m implies |.((osc1 . m) - 0).| < b )
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
;
|.((osc1 . m) - 0).| < b
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 being
Nat st
j in dom F holds
0 <= F . j
proof
let j be
Nat;
( j in dom F implies 0 <= F . j )
set r =
F . j;
A17:
rng g is
bounded_below
by A3, INTEGRA1:11;
assume A18:
j in dom F
;
0 <= F . j
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 being
Real st
r in rng (g | (divset (D,j)))
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:
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 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
0 <= F . j
by A25, A24;
verum
end;
then A26:
osc1 . m >= 0
by A16, RVSUM_1:84;
then A27:
|.(osc1 . m).| = osc1 . m
by ABSVALUE:def 1;
for
j being
Nat st
j in Seg (len D) holds
(UV1 - LV1) . j <= (a * (UV - LV)) . j
proof
let j be
Nat;
( j in Seg (len D) implies (UV1 - LV1) . j <= (a * (UV - LV)) . j )
set x =
(UV1 - LV1) . j;
set y =
(a * (UV - LV)) . j;
A28:
(a * (UV - LV)) . j = a * ((UV - LV) . j)
by RVSUM_1:45;
assume A29:
j in Seg (len D)
;
(UV1 - LV1) . j <= (a * (UV - LV)) . j
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 =
g1 as
Function of
(divset (D,j)),
REAL by A35, FUNCT_2:def 1;
reconsider f1 =
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 being
Real 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 be
Real;
( x in divset (D,j) & y in divset (D,j) implies |.((g1 . x) - (g1 . y)).| <= a * |.((f1 . x) - (f1 . y)).| )
assume that A39:
x in divset (
D,
j)
and A40:
y in divset (
D,
j)
;
|.((g1 . x) - (g1 . y)).| <= a * |.((f1 . x) - (f1 . y)).|
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
|.((g1 . x) - (g1 . y)).| <= a * |.((f1 . x) - (f1 . y)).|
by A5, A37, A39, A40, A41, A43, A42;
verum
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
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, A38, Th25;
verum
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:
(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 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 (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 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
(UV1 - LV1) . j <= (a * (UV - LV)) . j
by A45, A44;
verum
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
|.((osc1 . m) - 0).| < b
by A47, A27, XXREAL_0:2;
verum
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
(lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0
by A49, A48, SEQ_2:12;
verum
end;
hence
g is integrable
by A3, Th12; verum