let a be Real; for A being non empty closed_interval Subset of REAL
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 being Real 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
let A be non empty closed_interval Subset of REAL; 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 being Real 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
let f, g, h be Function of A,REAL; ( f | A is bounded & f is integrable & g | A is bounded & g is integrable & h | A is bounded & a > 0 & ( for x, y being Real st x in A & y in A holds
|.((h . x) - (h . y)).| <= a * (|.((f . x) - (f . y)).| + |.((g . x) - (g . y)).|) ) implies h is integrable )
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 being Real st x in A & y in A holds
|.((h . x) - (h . y)).| <= a * (|.((f . x) - (f . y)).| + |.((g . x) - (g . y)).|)
; h is integrable
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;
( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum (h,T))) - (lim (lower_sum (h,T))) = 0 )
assume that A8:
delta T is
convergent
and A9:
lim (delta T) = 0
;
(lim (upper_sum (h,T))) - (lim (lower_sum (h,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 being
Real st
0 < b holds
ex
n being
Nat st
for
m being
Nat st
n <= m holds
|.((osc2 . m) - 0).| < b
proof
let b be
Real;
( 0 < b implies ex n being Nat st
for m being Nat st n <= m holds
|.((osc2 . m) - 0).| < b )
assume
b > 0
;
ex n being Nat st
for m being Nat st n <= m holds
|.((osc2 . m) - 0).| < b
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 being
Nat st
(
n1 <= n &
n2 <= n )
then consider n being
Nat such that A22:
n1 <= n
and A23:
n2 <= n
;
take
n
;
for m being Nat st n <= m holds
|.((osc2 . m) - 0).| < b
let m be
Nat;
( n <= m implies |.((osc2 . 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 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 being
Nat st
j in dom G holds
0 <= G . j
proof
let j be
Nat;
( j in dom G implies 0 <= G . j )
set r =
G . j;
A26:
rng g is
bounded_below
by A3, INTEGRA1:11;
assume A27:
j in dom G
;
0 <= G . j
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 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 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:
G . j =
((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
0 <= G . j
by A34, A33;
verum
end;
then A35:
osc1 . m >= 0
by A25, RVSUM_1:84;
assume A36:
n <= m
;
|.((osc2 . m) - 0).| < b
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 being
Nat st
j in dom H holds
0 <= H . j
proof
let j be
Nat;
( j in dom H implies 0 <= H . j )
set r =
H . j;
A39:
rng f is
bounded_below
by A1, INTEGRA1:11;
assume A40:
j in dom H
;
0 <= H . j
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 being
Real st
r in rng (f | (divset (D,j)))
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:
H . j =
((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
0 <= H . j
by A47, A46;
verum
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 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;
A51:
rng h is
bounded_below
by A5, INTEGRA1:11;
assume A52:
j in dom F
;
0 <= F . j
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 being
Real st
r in rng (h | (divset (D,j)))
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:
F . j =
((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
0 <= F . j
by A59, A58;
verum
end;
then
osc2 . m >= 0
by A50, RVSUM_1:84;
then A60:
|.(osc2 . m).| = osc2 . m
by ABSVALUE:def 1;
for
j being
Nat st
j in Seg (len D) holds
(UV2 - LV2) . j <= (a * ((UV - LV) + (UV1 - LV1))) . j
proof
let j be
Nat;
( j in Seg (len D) implies (UV2 - LV2) . j <= (a * ((UV - LV) + (UV1 - LV1))) . j )
set x =
(UV2 - LV2) . j;
set y =
(a * ((UV - LV) + (UV1 - LV1))) . j;
A61:
(a * ((UV - LV) + (UV1 - LV1))) . j =
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)
;
(UV2 - LV2) . j <= (a * ((UV - LV) + (UV1 - LV1))) . j
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:
(UV2 - LV2) . j =
((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 =
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 =
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 being
Real 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 be
Real;
( x in divset (D,j) & y in divset (D,j) implies |.((h1 . x) - (h1 . y)).| <= a * (|.((f1 . x) - (f1 . y)).| + |.((g1 . x) - (g1 . y)).|) )
assume that A77:
x in divset (
D,
j)
and A78:
y in divset (
D,
j)
;
|.((h1 . x) - (h1 . y)).| <= a * (|.((f1 . x) - (f1 . y)).| + |.((g1 . x) - (g1 . y)).|)
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
|.((h1 . x) - (h1 . y)).| <= a * (|.((f1 . x) - (f1 . y)).| + |.((g1 . x) - (g1 . y)).|)
by A7, A74, A77, A78, A79, A83, A82, A81, A80;
verum
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
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)))))
by A6, A85, A84, A76, Th26;
verum
end;
LV . j = (lower_bound (rng (f | (divset (D,j))))) * (vol (divset (D,j)))
by A64, INTEGRA1:def 7;
then (a * ((UV - LV) + (UV1 - LV1))) . j =
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
(UV2 - LV2) . j <= (a * ((UV - LV) + (UV1 - LV1))) . j
by A66, A69, A62, XREAL_1:64;
verum
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
|.((osc2 . m) - 0).| < b
by A60, A49, XXREAL_0:2;
verum
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
(lim (upper_sum (h,T))) - (lim (lower_sum (h,T))) = 0
by A87, A86, SEQ_2:12;
verum
end;
hence
h is integrable
by A5, Th12; verum