let a, b be real number ; :: thesis: for H being Functional_Sequence of REAL ,REAL
for rseq being Real_Sequence st a < b & ( for n being Element of NAT holds
( H . n is_integrable_on ['a,b'] & (H . n) | ['a,b'] is bounded & rseq . n = integral (H . n),a,b ) ) & H is_unif_conv_on ['a,b'] holds
( (lim H,['a,b']) | ['a,b'] is bounded & lim H,['a,b'] is_integrable_on ['a,b'] & rseq is convergent & lim rseq = integral (lim H,['a,b']),a,b )
let H be Functional_Sequence of REAL ,REAL ; :: thesis: for rseq being Real_Sequence st a < b & ( for n being Element of NAT holds
( H . n is_integrable_on ['a,b'] & (H . n) | ['a,b'] is bounded & rseq . n = integral (H . n),a,b ) ) & H is_unif_conv_on ['a,b'] holds
( (lim H,['a,b']) | ['a,b'] is bounded & lim H,['a,b'] is_integrable_on ['a,b'] & rseq is convergent & lim rseq = integral (lim H,['a,b']),a,b )
let rseq be Real_Sequence; :: thesis: ( a < b & ( for n being Element of NAT holds
( H . n is_integrable_on ['a,b'] & (H . n) | ['a,b'] is bounded & rseq . n = integral (H . n),a,b ) ) & H is_unif_conv_on ['a,b'] implies ( (lim H,['a,b']) | ['a,b'] is bounded & lim H,['a,b'] is_integrable_on ['a,b'] & rseq is convergent & lim rseq = integral (lim H,['a,b']),a,b ) )
set AB = ['a,b'];
assume that
A1:
a < b
and
A2:
for n being Element of NAT holds
( H . n is_integrable_on ['a,b'] & (H . n) | ['a,b'] is bounded & rseq . n = integral (H . n),a,b )
and
A3:
H is_unif_conv_on ['a,b']
; :: thesis: ( (lim H,['a,b']) | ['a,b'] is bounded & lim H,['a,b'] is_integrable_on ['a,b'] & rseq is convergent & lim rseq = integral (lim H,['a,b']),a,b )
A4:
['a,b'] common_on_dom H
by A3, SEQFUNC:44;
H is_point_conv_on ['a,b']
by A3, SEQFUNC:23;
then A5:
dom (lim H,['a,b']) = ['a,b']
by SEQFUNC:22;
consider K being Element of NAT such that
A6:
for n being Element of NAT
for x being Element of REAL st n >= K & x in ['a,b'] holds
abs (((H . n) . x) - ((lim H,['a,b']) . x)) < 1
by A3, SEQFUNC:44;
(H . K) | ['a,b'] is bounded
by A2;
then consider r being real number such that
A7:
for c being set st c in ['a,b'] /\ (dom (H . K)) holds
abs ((H . K) . c) <= r
by RFUNCT_1:90;
dom (lim H,['a,b']) c= dom (H . K)
by A4, A5, SEQFUNC:def 10;
then A8:
['a,b'] /\ (dom (lim H,['a,b'])) c= ['a,b'] /\ (dom (H . K))
by XBOOLE_1:26;
now let c be
set ;
:: thesis: ( c in ['a,b'] /\ (dom (lim H,['a,b'])) implies abs ((lim H,['a,b']) . c) <= r + 1 )assume A9:
c in ['a,b'] /\ (dom (lim H,['a,b']))
;
:: thesis: abs ((lim H,['a,b']) . c) <= r + 1then A10:
abs ((H . K) . c) <= r
by A7, A8;
c in ['a,b']
by A9, XBOOLE_0:def 4;
then
abs (((H . K) . c) - ((lim H,['a,b']) . c)) < 1
by A6;
then A11:
(abs ((H . K) . c)) + (abs (((H . K) . c) - ((lim H,['a,b']) . c))) <= r + 1
by A10, XREAL_1:9;
(lim H,['a,b']) . c = ((H . K) . c) - (((H . K) . c) - ((lim H,['a,b']) . c))
;
then
abs ((lim H,['a,b']) . c) <= (abs ((H . K) . c)) + (abs (((H . K) . c) - ((lim H,['a,b']) . c)))
by COMPLEX1:143;
hence
abs ((lim H,['a,b']) . c) <= r + 1
by A11, XXREAL_0:2;
:: thesis: verum end;
hence A12:
(lim H,['a,b']) | ['a,b'] is bounded
by RFUNCT_1:90; :: thesis: ( lim H,['a,b'] is_integrable_on ['a,b'] & rseq is convergent & lim rseq = integral (lim H,['a,b']),a,b )
consider T being DivSequence of ['a,b'] such that
A13:
( delta T is convergent & lim (delta T) = 0 )
by INTEGRA4:11;
A14:
for n being Element of NAT holds
( (H . n) || ['a,b'] is Function of ['a,b'], REAL & ((H . n) || ['a,b']) | ['a,b'] is bounded & lower_sum ((H . n) || ['a,b']),T is convergent & lim (lower_sum ((H . n) || ['a,b']),T) = lower_integral ((H . n) || ['a,b']) & upper_sum ((H . n) || ['a,b']),T is convergent & lim (upper_sum ((H . n) || ['a,b']),T) = upper_integral ((H . n) || ['a,b']) & lower_integral ((H . n) || ['a,b']) = upper_integral ((H . n) || ['a,b']) & rseq . n = integral ((H . n) || ['a,b']) )
proof
let n be
Element of
NAT ;
:: thesis: ( (H . n) || ['a,b'] is Function of ['a,b'], REAL & ((H . n) || ['a,b']) | ['a,b'] is bounded & lower_sum ((H . n) || ['a,b']),T is convergent & lim (lower_sum ((H . n) || ['a,b']),T) = lower_integral ((H . n) || ['a,b']) & upper_sum ((H . n) || ['a,b']),T is convergent & lim (upper_sum ((H . n) || ['a,b']),T) = upper_integral ((H . n) || ['a,b']) & lower_integral ((H . n) || ['a,b']) = upper_integral ((H . n) || ['a,b']) & rseq . n = integral ((H . n) || ['a,b']) )
['a,b'] c= dom (H . n)
by A4, SEQFUNC:def 10;
hence A15:
(H . n) || ['a,b'] is
Function of
['a,b'],
REAL
by FUNCT_2:131, INTEGRA5:6;
:: thesis: ( ((H . n) || ['a,b']) | ['a,b'] is bounded & lower_sum ((H . n) || ['a,b']),T is convergent & lim (lower_sum ((H . n) || ['a,b']),T) = lower_integral ((H . n) || ['a,b']) & upper_sum ((H . n) || ['a,b']),T is convergent & lim (upper_sum ((H . n) || ['a,b']),T) = upper_integral ((H . n) || ['a,b']) & lower_integral ((H . n) || ['a,b']) = upper_integral ((H . n) || ['a,b']) & rseq . n = integral ((H . n) || ['a,b']) )
(H . n) | ['a,b'] is
bounded
by A2;
hence
((H . n) || ['a,b']) | ['a,b'] is
bounded
by INTEGRA5:9;
:: thesis: ( lower_sum ((H . n) || ['a,b']),T is convergent & lim (lower_sum ((H . n) || ['a,b']),T) = lower_integral ((H . n) || ['a,b']) & upper_sum ((H . n) || ['a,b']),T is convergent & lim (upper_sum ((H . n) || ['a,b']),T) = upper_integral ((H . n) || ['a,b']) & lower_integral ((H . n) || ['a,b']) = upper_integral ((H . n) || ['a,b']) & rseq . n = integral ((H . n) || ['a,b']) )
hence
(
lower_sum ((H . n) || ['a,b']),
T is
convergent &
lim (lower_sum ((H . n) || ['a,b']),T) = lower_integral ((H . n) || ['a,b']) &
upper_sum ((H . n) || ['a,b']),
T is
convergent &
lim (upper_sum ((H . n) || ['a,b']),T) = upper_integral ((H . n) || ['a,b']) )
by A13, A15, INTEGRA4:8, INTEGRA4:9;
:: thesis: ( lower_integral ((H . n) || ['a,b']) = upper_integral ((H . n) || ['a,b']) & rseq . n = integral ((H . n) || ['a,b']) )
H . n is_integrable_on ['a,b']
by A2;
then
(H . n) || ['a,b'] is
integrable
by INTEGRA5:def 2;
hence
lower_integral ((H . n) || ['a,b']) = upper_integral ((H . n) || ['a,b'])
by INTEGRA1:def 17;
:: thesis: rseq . n = integral ((H . n) || ['a,b'])
rseq . n = integral (H . n),
a,
b
by A2;
then
rseq . n = integral (H . n),
['a,b']
by A1, INTEGRA5:def 5;
hence
rseq . n = integral ((H . n) || ['a,b'])
;
:: thesis: verum
end;
set H0 = (lim H,['a,b']) || ['a,b'];
( (lim H,['a,b']) | ['a,b'] is bounded_above & (lim H,['a,b']) | ['a,b'] is bounded_below )
by A12;
then A16:
( ((lim H,['a,b']) || ['a,b']) | ['a,b'] is bounded_above & ((lim H,['a,b']) || ['a,b']) | ['a,b'] is bounded_below )
by INTEGRA5:7, INTEGRA5:8;
then A17:
((lim H,['a,b']) || ['a,b']) | ['a,b'] is bounded
;
A18:
(lim H,['a,b']) || ['a,b'] is Function of ['a,b'], REAL
by A5, FUNCT_2:131, INTEGRA5:6;
then A19:
( (lim H,['a,b']) || ['a,b'] is upper_integrable & (lim H,['a,b']) || ['a,b'] is lower_integrable )
by A17, INTEGRA4:10;
A20:
for e being Element of REAL st 0 < e holds
ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a)
proof
let e be
Element of
REAL ;
:: thesis: ( 0 < e implies ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a) )
assume
0 < e
;
:: thesis: ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a)
then consider N being
Element of
NAT such that A21:
for
n being
Element of
NAT for
x being
Element of
REAL st
n >= N &
x in ['a,b'] holds
abs (((H . n) . x) - ((lim H,['a,b']) . x)) < e
by A3, SEQFUNC:44;
take
N
;
:: thesis: for n, k being Element of NAT st N <= n holds
abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a)
now let n,
k be
Element of
NAT ;
:: thesis: ( N <= n implies abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a) )reconsider Tk =
T . k as
DivisionPoint of
['a,b'] by INTEGRA1:def 4;
set l0 =
len Tk;
X:
dom Tk = Seg (len Tk)
by FINSEQ_1:def 3;
assume A22:
N <= n
;
:: thesis: abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a)set Hn =
(H . n) || ['a,b'];
len (upper_volume ((H . n) || ['a,b']),(T . k)) = len Tk
by INTEGRA1:def 7;
then reconsider R1 =
upper_volume ((H . n) || ['a,b']),
(T . k) as
Element of
(len Tk) -tuples_on REAL by FINSEQ_2:110;
len (upper_volume ((lim H,['a,b']) || ['a,b']),(T . k)) = len Tk
by INTEGRA1:def 7;
then reconsider R2 =
upper_volume ((lim H,['a,b']) || ['a,b']),
(T . k) as
Element of
(len Tk) -tuples_on REAL by FINSEQ_2:110;
consider H1 being
Function of
['a,b'],
REAL such that A23:
(
rng H1 = {e} &
H1 | ['a,b'] is
bounded )
by INTEGRA4:5;
len (upper_volume H1,(T . k)) = len Tk
by INTEGRA1:def 7;
then reconsider R3 =
upper_volume H1,
(T . k) as
Element of
(len Tk) -tuples_on REAL by FINSEQ_2:110;
((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) = (upper_sum ((H . n) || ['a,b']),(T . k)) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)
by INTEGRA2:def 4;
then
((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) = (upper_sum ((H . n) || ['a,b']),(T . k)) - (upper_sum ((lim H,['a,b']) || ['a,b']),(T . k))
by INTEGRA2:def 4;
then A24:
((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) = Sum (R1 - R2)
by RVSUM_1:120;
((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((upper_sum ((H . n) || ['a,b']),T) . k) = (upper_sum ((lim H,['a,b']) || ['a,b']),(T . k)) - ((upper_sum ((H . n) || ['a,b']),T) . k)
by INTEGRA2:def 4;
then
((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((upper_sum ((H . n) || ['a,b']),T) . k) = (upper_sum ((lim H,['a,b']) || ['a,b']),(T . k)) - (upper_sum ((H . n) || ['a,b']),(T . k))
by INTEGRA2:def 4;
then A25:
((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((upper_sum ((H . n) || ['a,b']),T) . k) = Sum (R2 - R1)
by RVSUM_1:120;
A26:
for
i being
Element of
NAT st
i in dom Tk holds
(
(R1 - R2) . i <= R3 . i &
(R2 - R1) . i <= R3 . i )
proof
let i be
Element of
NAT ;
:: thesis: ( i in dom Tk implies ( (R1 - R2) . i <= R3 . i & (R2 - R1) . i <= R3 . i ) )
assume A27:
i in dom Tk
;
:: thesis: ( (R1 - R2) . i <= R3 . i & (R2 - R1) . i <= R3 . i )
(R1 - R2) . i = (R1 . i) - (R2 . i)
by RVSUM_1:48;
then
(R1 - R2) . i = ((upper_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i))) - ((upper_volume ((lim H,['a,b']) || ['a,b']),(T . k)) . i)
by A27, INTEGRA1:def 7;
then
(R1 - R2) . i = ((upper_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i))) - ((upper_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i)))
by A27, INTEGRA1:def 7;
then A28:
(R1 - R2) . i = ((upper_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) - (upper_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i))))) * (vol (divset (T . k),i))
;
(R2 - R1) . i = (R2 . i) - (R1 . i)
by RVSUM_1:48;
then
(R2 - R1) . i = ((upper_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i))) - ((upper_volume ((H . n) || ['a,b']),(T . k)) . i)
by A27, INTEGRA1:def 7;
then
(R2 - R1) . i = ((upper_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i))) - ((upper_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i)))
by A27, INTEGRA1:def 7;
then A29:
(R2 - R1) . i = ((upper_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) - (upper_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i))))) * (vol (divset (T . k),i))
;
A30:
(
(upper_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) - (upper_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) <= upper_bound (rng (H1 | (divset (T . k),i))) &
(upper_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) - (upper_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) <= upper_bound (rng (H1 | (divset (T . k),i))) )
proof
A32:
divset (T . k),
i c= ['a,b']
by A27, INTEGRA1:10;
((H . n) || ['a,b']) | ['a,b'] is
bounded
by A14;
then
((H . n) || ['a,b']) | ['a,b'] is
bounded_above
;
then A33:
(((H . n) || ['a,b']) | (divset (T . k),i)) | (divset (T . k),i) is
bounded_above
by A27, INTEGRA1:10, INTEGRA2:5;
(H . n) || ['a,b'] is
Function of
['a,b'],
REAL
by A14;
then reconsider f =
((H . n) || ['a,b']) | (divset (T . k),i) as
Function of
divset (T . k),
i,
REAL by A32, FUNCT_2:38;
B33:
f | (divset (T . k),i) is
bounded_above
by A33;
reconsider g =
((lim H,['a,b']) || ['a,b']) | (divset (T . k),i) as
Function of
divset (T . k),
i,
REAL by A18, A32, FUNCT_2:38;
g | (divset (T . k),i) is
bounded_above
by A16, A32, INTEGRA2:5;
then A34:
(
rng f is
bounded_above &
rng g is
bounded_above )
by B33, INTEGRA1:15;
A35:
rng (H1 | (divset (T . k),i)) c= {e}
by A23, RELAT_1:99;
consider x0 being
set such that A36:
x0 in divset (T . k),
i
by XBOOLE_0:def 1;
H1 . x0 in {e}
by A23, A32, A36, FUNCT_2:6;
then
H1 . x0 = e
by TARSKI:def 1;
then A37:
(H1 | (divset (T . k),i)) . x0 = e
by A36, FUNCT_1:72;
H1 | (divset (T . k),i) is
Function of
divset (T . k),
i,
REAL
by A32, FUNCT_2:38;
then
e in rng (H1 | (divset (T . k),i))
by A36, A37, FUNCT_2:6;
then
{e} c= rng (H1 | (divset (T . k),i))
by ZFMISC_1:37;
then
rng (H1 | (divset (T . k),i)) = {e}
by A35, XBOOLE_0:def 10;
then A38:
e = upper_bound (rng (H1 | (divset (T . k),i)))
by SEQ_4:22;
A39:
for
x being
set st
x in divset (T . k),
i holds
abs ((f . x) - (g . x)) <= e
proof
let x be
set ;
:: thesis: ( x in divset (T . k),i implies abs ((f . x) - (g . x)) <= e )
assume A40:
x in divset (T . k),
i
;
:: thesis: abs ((f . x) - (g . x)) <= e
then
abs ((f . x) - (g . x)) = abs ((((H . n) || ['a,b']) . x) - (g . x))
by FUNCT_1:72;
then
abs ((f . x) - (g . x)) = abs ((((H . n) || ['a,b']) . x) - (((lim H,['a,b']) || ['a,b']) . x))
by A40, FUNCT_1:72;
then
abs ((f . x) - (g . x)) = abs (((H . n) . x) - (((lim H,['a,b']) || ['a,b']) . x))
by A32, A40, FUNCT_1:72;
then
abs ((f . x) - (g . x)) = abs (((H . n) . x) - ((lim H,['a,b']) . x))
by A32, A40, FUNCT_1:72;
hence
abs ((f . x) - (g . x)) <= e
by A21, A22, A32, A40;
:: thesis: verum
end;
hence
(upper_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) - (upper_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) <= upper_bound (rng (H1 | (divset (T . k),i)))
by A34, A38, Th1;
:: thesis: (upper_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) - (upper_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) <= upper_bound (rng (H1 | (divset (T . k),i)))
for
x being
set st
x in divset (T . k),
i holds
abs ((g . x) - (f . x)) <= upper_bound (rng (H1 | (divset (T . k),i)))
hence
(upper_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) - (upper_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) <= upper_bound (rng (H1 | (divset (T . k),i)))
by A34, Th1;
:: thesis: verum
end;
A41:
0 <= vol (divset (T . k),i)
by INTEGRA1:11;
then
(R1 - R2) . i <= (upper_bound (rng (H1 | (divset (T . k),i)))) * (vol (divset (T . k),i))
by A28, A30, XREAL_1:66;
hence
(R1 - R2) . i <= R3 . i
by A27, INTEGRA1:def 7;
:: thesis: (R2 - R1) . i <= R3 . i
(R2 - R1) . i <= (upper_bound (rng (H1 | (divset (T . k),i)))) * (vol (divset (T . k),i))
by A29, A30, A41, XREAL_1:66;
hence
(R2 - R1) . i <= R3 . i
by A27, INTEGRA1:def 7;
:: thesis: verum
end; then
for
i being
Nat st
i in Seg (len Tk) holds
(R1 - R2) . i <= R3 . i
by X;
then A42:
((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) <= Sum R3
by A24, RVSUM_1:112;
A43:
upper_bound (rng H1) = e
by A23, SEQ_4:22;
A44:
vol ['a,b'] = b - a
by A1, INTEGRA6:5;
H1 | ['a,b'] is
bounded_above
by A23;
then A45:
upper_sum H1,
(T . k) <= e * (b - a)
by A43, A44, INTEGRA1:29;
then A46:
((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) <= e * (b - a)
by A42, XXREAL_0:2;
for
i being
Nat st
i in dom Tk holds
(R2 - R1) . i <= R3 . i
by A26;
then
((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((upper_sum ((H . n) || ['a,b']),T) . k) <= Sum R3
by A25, X, RVSUM_1:112;
then
((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((upper_sum ((H . n) || ['a,b']),T) . k) <= e * (b - a)
by A45, XXREAL_0:2;
then
- (e * (b - a)) <= - (((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((upper_sum ((H . n) || ['a,b']),T) . k))
by XREAL_1:26;
hence
abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a)
by A46, ABSVALUE:12;
:: thesis: verum end;
hence
for
n,
k being
Element of
NAT st
N <= n holds
abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a)
;
:: thesis: verum
end;
A47:
for e being Element of REAL st 0 < e holds
ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a)
proof
let e be
Element of
REAL ;
:: thesis: ( 0 < e implies ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a) )
assume
0 < e
;
:: thesis: ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a)
then consider N being
Element of
NAT such that A48:
for
n being
Element of
NAT for
x being
Element of
REAL st
n >= N &
x in ['a,b'] holds
abs (((H . n) . x) - ((lim H,['a,b']) . x)) < e
by A3, SEQFUNC:44;
take
N
;
:: thesis: for n, k being Element of NAT st N <= n holds
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a)
hereby :: thesis: verum
let n,
k be
Element of
NAT ;
:: thesis: ( N <= n implies abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a) )assume A49:
N <= n
;
:: thesis: abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a)set Hn =
(H . n) || ['a,b'];
reconsider Tk =
T . k as
DivisionPoint of
['a,b'] by INTEGRA1:def 4;
set l0 =
len Tk;
X:
Seg (len Tk) = dom Tk
by FINSEQ_1:def 3;
len (lower_volume ((H . n) || ['a,b']),(T . k)) = len Tk
by INTEGRA1:def 8;
then reconsider R1 =
lower_volume ((H . n) || ['a,b']),
(T . k) as
Element of
(len Tk) -tuples_on REAL by FINSEQ_2:110;
len (lower_volume ((lim H,['a,b']) || ['a,b']),(T . k)) = len Tk
by INTEGRA1:def 8;
then reconsider R2 =
lower_volume ((lim H,['a,b']) || ['a,b']),
(T . k) as
Element of
(len Tk) -tuples_on REAL by FINSEQ_2:110;
consider H1 being
Function of
['a,b'],
REAL such that A50:
(
rng H1 = {e} &
H1 | ['a,b'] is
bounded )
by INTEGRA4:5;
len (lower_volume H1,(T . k)) = len Tk
by INTEGRA1:def 8;
then reconsider R3 =
lower_volume H1,
(T . k) as
Element of
(len Tk) -tuples_on REAL by FINSEQ_2:110;
((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) = (lower_sum ((H . n) || ['a,b']),(T . k)) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)
by INTEGRA2:def 5;
then
((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) = (lower_sum ((H . n) || ['a,b']),(T . k)) - (lower_sum ((lim H,['a,b']) || ['a,b']),(T . k))
by INTEGRA2:def 5;
then A51:
((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) = Sum (R1 - R2)
by RVSUM_1:120;
((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((lower_sum ((H . n) || ['a,b']),T) . k) = (lower_sum ((lim H,['a,b']) || ['a,b']),(T . k)) - ((lower_sum ((H . n) || ['a,b']),T) . k)
by INTEGRA2:def 5;
then
((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((lower_sum ((H . n) || ['a,b']),T) . k) = (lower_sum ((lim H,['a,b']) || ['a,b']),(T . k)) - (lower_sum ((H . n) || ['a,b']),(T . k))
by INTEGRA2:def 5;
then A52:
((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((lower_sum ((H . n) || ['a,b']),T) . k) = Sum (R2 - R1)
by RVSUM_1:120;
A53:
for
i being
Element of
NAT st
i in dom Tk holds
(
(R1 - R2) . i <= R3 . i &
(R2 - R1) . i <= R3 . i )
proof
let i be
Element of
NAT ;
:: thesis: ( i in dom Tk implies ( (R1 - R2) . i <= R3 . i & (R2 - R1) . i <= R3 . i ) )
assume A54:
i in dom Tk
;
:: thesis: ( (R1 - R2) . i <= R3 . i & (R2 - R1) . i <= R3 . i )
(R1 - R2) . i = (R1 . i) - (R2 . i)
by RVSUM_1:48;
then
(R1 - R2) . i = ((lower_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i))) - ((lower_volume ((lim H,['a,b']) || ['a,b']),(T . k)) . i)
by A54, INTEGRA1:def 8;
then
(R1 - R2) . i = ((lower_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i))) - ((lower_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i)))
by A54, INTEGRA1:def 8;
then A55:
(R1 - R2) . i = ((lower_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) - (lower_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i))))) * (vol (divset (T . k),i))
;
(R2 - R1) . i = (R2 . i) - (R1 . i)
by RVSUM_1:48;
then
(R2 - R1) . i = ((lower_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i))) - ((lower_volume ((H . n) || ['a,b']),(T . k)) . i)
by A54, INTEGRA1:def 8;
then
(R2 - R1) . i = ((lower_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i))) - ((lower_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i)))
by A54, INTEGRA1:def 8;
then A56:
(R2 - R1) . i = ((lower_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) - (lower_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i))))) * (vol (divset (T . k),i))
;
A58:
divset (T . k),
i c= ['a,b']
by A54, INTEGRA1:10;
A59:
(((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)) | (divset (T . k),i) is
bounded_below
by A16, A54, INTEGRA1:10, INTEGRA2:6;
reconsider g =
((lim H,['a,b']) || ['a,b']) | (divset (T . k),i) as
Function of
divset (T . k),
i,
REAL by A18, A58, FUNCT_2:38;
X:
g | (divset (T . k),i) is
bounded_below
by A59;
(H . n) || ['a,b'] is
Function of
['a,b'],
REAL
by A14;
then reconsider f =
((H . n) || ['a,b']) | (divset (T . k),i) as
Function of
divset (T . k),
i,
REAL by A58, FUNCT_2:38;
((H . n) || ['a,b']) | ['a,b'] is
bounded
by A14;
then
((H . n) || ['a,b']) | ['a,b'] is
bounded_below
;
then
f | (divset (T . k),i) is
bounded_below
by A58, INTEGRA2:6;
then A60:
(
rng f is
bounded_below &
rng g is
bounded_below )
by X, INTEGRA1:13;
A61:
rng (H1 | (divset (T . k),i)) c= {e}
by A50, RELAT_1:99;
consider x0 being
set such that A62:
x0 in divset (T . k),
i
by XBOOLE_0:def 1;
H1 . x0 in {e}
by A50, A58, A62, FUNCT_2:6;
then
H1 . x0 = e
by TARSKI:def 1;
then A63:
(H1 | (divset (T . k),i)) . x0 = e
by A62, FUNCT_1:72;
H1 | (divset (T . k),i) is
Function of
divset (T . k),
i,
REAL
by A58, FUNCT_2:38;
then
e in rng (H1 | (divset (T . k),i))
by A62, A63, FUNCT_2:6;
then
{e} c= rng (H1 | (divset (T . k),i))
by ZFMISC_1:37;
then
rng (H1 | (divset (T . k),i)) = {e}
by A61, XBOOLE_0:def 10;
then A64:
e = lower_bound (rng (H1 | (divset (T . k),i)))
by SEQ_4:22;
A65:
0 <= vol (divset (T . k),i)
by INTEGRA1:11;
A66:
now let x be
set ;
:: thesis: ( x in divset (T . k),i implies abs ((f . x) - (g . x)) <= e )assume A67:
x in divset (T . k),
i
;
:: thesis: abs ((f . x) - (g . x)) <= ethen
abs ((f . x) - (g . x)) = abs ((((H . n) || ['a,b']) . x) - (g . x))
by FUNCT_1:72;
then
abs ((f . x) - (g . x)) = abs ((((H . n) || ['a,b']) . x) - (((lim H,['a,b']) || ['a,b']) . x))
by A67, FUNCT_1:72;
then
abs ((f . x) - (g . x)) = abs (((H . n) . x) - (((lim H,['a,b']) || ['a,b']) . x))
by A58, A67, FUNCT_1:72;
then
abs ((f . x) - (g . x)) = abs (((H . n) . x) - ((lim H,['a,b']) . x))
by A58, A67, FUNCT_1:72;
hence
abs ((f . x) - (g . x)) <= e
by A48, A49, A58, A67;
:: thesis: verum end;
then
(lower_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) - (lower_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) <= lower_bound (rng (H1 | (divset (T . k),i)))
by A60, A64, Th2;
then
(R1 - R2) . i <= (lower_bound (rng (H1 | (divset (T . k),i)))) * (vol (divset (T . k),i))
by A55, A65, XREAL_1:66;
hence
(R1 - R2) . i <= R3 . i
by A54, INTEGRA1:def 8;
:: thesis: (R2 - R1) . i <= R3 . i
then
(lower_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) - (lower_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) <= lower_bound (rng (H1 | (divset (T . k),i)))
by A60, Th2;
then
(R2 - R1) . i <= (lower_bound (rng (H1 | (divset (T . k),i)))) * (vol (divset (T . k),i))
by A56, A65, XREAL_1:66;
hence
(R2 - R1) . i <= R3 . i
by A54, INTEGRA1:def 8;
:: thesis: verum
end; then
for
i being
Nat st
i in Seg (len Tk) holds
(R1 - R2) . i <= R3 . i
by X;
then A68:
((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) <= lower_sum H1,
(T . k)
by A51, RVSUM_1:112;
A69:
upper_bound (rng H1) = e
by A50, SEQ_4:22;
A70:
vol ['a,b'] = b - a
by A1, INTEGRA6:5;
H1 | ['a,b'] is
bounded_above
by A50;
then A71:
upper_sum H1,
(T . k) <= e * (b - a)
by A69, A70, INTEGRA1:29;
lower_sum H1,
(T . k) <= upper_sum H1,
(T . k)
by A50, INTEGRA1:30;
then A72:
lower_sum H1,
(T . k) <= e * (b - a)
by A71, XXREAL_0:2;
then A73:
((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) <= e * (b - a)
by A68, XXREAL_0:2;
for
i being
Nat st
i in Seg (len Tk) holds
(R2 - R1) . i <= R3 . i
by A53, X;
then
((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((lower_sum ((H . n) || ['a,b']),T) . k) <= Sum R3
by A52, RVSUM_1:112;
then
((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((lower_sum ((H . n) || ['a,b']),T) . k) <= e * (b - a)
by A72, XXREAL_0:2;
then
- (e * (b - a)) <= - (((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((lower_sum ((H . n) || ['a,b']),T) . k))
by XREAL_1:26;
hence
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a)
by A73, ABSVALUE:12;
:: thesis: verum
end;
end;
A74:
0 < b - a
by A1, XREAL_1:52;
A75:
for e being Element of REAL st 0 < e holds
ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e
proof
let e be
Element of
REAL ;
:: thesis: ( 0 < e implies ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e )
assume
0 < e
;
:: thesis: ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e
then
0 < e / (b - a)
by A74, XREAL_1:141;
then consider N being
Element of
NAT such that A76:
for
n,
k being
Element of
NAT st
N <= n holds
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= (e / (b - a)) * (b - a)
by A47;
take
N
;
:: thesis: for n, k being Element of NAT st N <= n holds
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e
hereby :: thesis: verum
let n,
k be
Element of
NAT ;
:: thesis: ( N <= n implies abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e )assume
N <= n
;
:: thesis: abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= ethen
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= (e / (b - a)) * (b - a)
by A76;
hence
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e
by A74, XCMPLX_1:88;
:: thesis: verum
end;
end;
A77:
( lower_sum ((lim H,['a,b']) || ['a,b']),T is convergent & lim (lower_sum ((lim H,['a,b']) || ['a,b']),T) = lower_integral ((lim H,['a,b']) || ['a,b']) & upper_sum ((lim H,['a,b']) || ['a,b']),T is convergent & lim (upper_sum ((lim H,['a,b']) || ['a,b']),T) = upper_integral ((lim H,['a,b']) || ['a,b']) )
by A13, A17, A18, INTEGRA4:8, INTEGRA4:9;
A78:
for e being Element of REAL st 0 < e holds
ex N being Element of NAT st
for n being Element of NAT st N <= n holds
abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= e
proof
let e be
Element of
REAL ;
:: thesis: ( 0 < e implies ex N being Element of NAT st
for n being Element of NAT st N <= n holds
abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= e )
assume
0 < e
;
:: thesis: ex N being Element of NAT st
for n being Element of NAT st N <= n holds
abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= e
then
0 < e / (b - a)
by A74, XREAL_1:141;
then consider N being
Element of
NAT such that A79:
for
n,
k being
Element of
NAT st
N <= n holds
abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= (e / (b - a)) * (b - a)
by A20;
A80:
now let n,
k be
Element of
NAT ;
:: thesis: ( N <= n implies abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e )assume
N <= n
;
:: thesis: abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= ethen
abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= (e / (b - a)) * (b - a)
by A79;
hence
abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e
by A74, XCMPLX_1:88;
:: thesis: verum end;
take
N
;
:: thesis: for n being Element of NAT st N <= n holds
abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= e
hereby :: thesis: verum
let n be
Element of
NAT ;
:: thesis: ( N <= n implies abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= e )assume A81:
N <= n
;
:: thesis: abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= eA82:
now let k be
Element of
NAT ;
:: thesis: (abs ((upper_sum ((H . n) || ['a,b']),T) - (upper_sum ((lim H,['a,b']) || ['a,b']),T))) . k <= e
abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e
by A80, A81;
then
abs (((upper_sum ((H . n) || ['a,b']),T) . k) + ((- (upper_sum ((lim H,['a,b']) || ['a,b']),T)) . k)) <= e
by SEQ_1:14;
then
abs (((upper_sum ((H . n) || ['a,b']),T) + (- (upper_sum ((lim H,['a,b']) || ['a,b']),T))) . k) <= e
by SEQ_1:11;
hence
(abs ((upper_sum ((H . n) || ['a,b']),T) - (upper_sum ((lim H,['a,b']) || ['a,b']),T))) . k <= e
by SEQ_1:16;
:: thesis: verum end; A83:
upper_sum ((H . n) || ['a,b']),
T is
convergent
by A14;
then A84:
(upper_sum ((H . n) || ['a,b']),T) - (upper_sum ((lim H,['a,b']) || ['a,b']),T) is
convergent
by A77, SEQ_2:25;
lim ((upper_sum ((H . n) || ['a,b']),T) - (upper_sum ((lim H,['a,b']) || ['a,b']),T)) = (lim (upper_sum ((H . n) || ['a,b']),T)) - (lim (upper_sum ((lim H,['a,b']) || ['a,b']),T))
by A77, A83, SEQ_2:26;
then
lim ((upper_sum ((H . n) || ['a,b']),T) - (upper_sum ((lim H,['a,b']) || ['a,b']),T)) = (upper_integral ((H . n) || ['a,b'])) - (lim (upper_sum ((lim H,['a,b']) || ['a,b']),T))
by A14;
then A85:
lim ((upper_sum ((H . n) || ['a,b']),T) - (upper_sum ((lim H,['a,b']) || ['a,b']),T)) = (upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))
by A13, A17, A18, INTEGRA4:9;
abs ((upper_sum ((H . n) || ['a,b']),T) - (upper_sum ((lim H,['a,b']) || ['a,b']),T)) is
convergent
by A84, SEQ_4:26;
then
lim (abs ((upper_sum ((H . n) || ['a,b']),T) - (upper_sum ((lim H,['a,b']) || ['a,b']),T))) <= e
by A82, PREPOWER:3;
hence
abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= e
by A84, A85, SEQ_4:27;
:: thesis: verum
end;
end;
A86:
for e being Element of REAL st 0 < e holds
ex N being Element of NAT st
for n being Element of NAT st N <= n holds
abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) <= e
proof
let e be
Element of
REAL ;
:: thesis: ( 0 < e implies ex N being Element of NAT st
for n being Element of NAT st N <= n holds
abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) <= e )
assume
0 < e
;
:: thesis: ex N being Element of NAT st
for n being Element of NAT st N <= n holds
abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) <= e
then consider N being
Element of
NAT such that A87:
for
n,
k being
Element of
NAT st
N <= n holds
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e
by A75;
take
N
;
:: thesis: for n being Element of NAT st N <= n holds
abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) <= e
hereby :: thesis: verum
let n be
Element of
NAT ;
:: thesis: ( N <= n implies abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) <= e )set LHT =
lower_sum ((H . n) || ['a,b']),
T;
assume A88:
N <= n
;
:: thesis: abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) <= eA89:
now let k be
Element of
NAT ;
:: thesis: (abs ((lower_sum ((H . n) || ['a,b']),T) - (lower_sum ((lim H,['a,b']) || ['a,b']),T))) . k <= e
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e
by A87, A88;
then
abs (((lower_sum ((H . n) || ['a,b']),T) . k) + ((- (lower_sum ((lim H,['a,b']) || ['a,b']),T)) . k)) <= e
by SEQ_1:14;
then
abs (((lower_sum ((H . n) || ['a,b']),T) + (- (lower_sum ((lim H,['a,b']) || ['a,b']),T))) . k) <= e
by SEQ_1:11;
hence
(abs ((lower_sum ((H . n) || ['a,b']),T) - (lower_sum ((lim H,['a,b']) || ['a,b']),T))) . k <= e
by SEQ_1:16;
:: thesis: verum end; A90:
lower_sum ((H . n) || ['a,b']),
T is
convergent
by A14;
then
lim ((lower_sum ((H . n) || ['a,b']),T) - (lower_sum ((lim H,['a,b']) || ['a,b']),T)) = (lim (lower_sum ((H . n) || ['a,b']),T)) - (lim (lower_sum ((lim H,['a,b']) || ['a,b']),T))
by A77, SEQ_2:26;
then
lim ((lower_sum ((H . n) || ['a,b']),T) - (lower_sum ((lim H,['a,b']) || ['a,b']),T)) = (lower_integral ((H . n) || ['a,b'])) - (lim (lower_sum ((lim H,['a,b']) || ['a,b']),T))
by A14;
then A91:
lim ((lower_sum ((H . n) || ['a,b']),T) - (lower_sum ((lim H,['a,b']) || ['a,b']),T)) = (lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))
by A13, A17, A18, INTEGRA4:8;
A92:
(lower_sum ((H . n) || ['a,b']),T) - (lower_sum ((lim H,['a,b']) || ['a,b']),T) is
convergent
by A77, A90, SEQ_2:25;
then
abs ((lower_sum ((H . n) || ['a,b']),T) - (lower_sum ((lim H,['a,b']) || ['a,b']),T)) is
convergent
by SEQ_4:26;
then
lim (abs ((lower_sum ((H . n) || ['a,b']),T) - (lower_sum ((lim H,['a,b']) || ['a,b']),T))) <= e
by A89, PREPOWER:3;
hence
abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) <= e
by A91, A92, SEQ_4:27;
:: thesis: verum
end;
end;
set K1 = upper_integral ((lim H,['a,b']) || ['a,b']);
set L1 = lower_integral ((lim H,['a,b']) || ['a,b']);
A93:
now let e1 be
Element of
REAL ;
:: thesis: ( 0 < e1 implies abs ((lower_integral ((lim H,['a,b']) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) < e1 )set e =
e1 / 2;
assume
0 < e1
;
:: thesis: abs ((lower_integral ((lim H,['a,b']) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) < e1then A94:
(
0 < e1 / 2 &
e1 / 2
< e1 )
by XREAL_1:217, XREAL_1:218;
then A95:
0 < (e1 / 2) / 2
by XREAL_1:217;
then consider N1 being
Element of
NAT such that A96:
for
n being
Element of
NAT st
N1 <= n holds
abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= (e1 / 2) / 2
by A78;
consider N2 being
Element of
NAT such that A97:
for
n being
Element of
NAT st
N2 <= n holds
abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) <= (e1 / 2) / 2
by A86, A95;
reconsider n =
max N1,
N2 as
Element of
NAT by XXREAL_0:16;
set K =
upper_integral ((H . n) || ['a,b']);
set L =
lower_integral ((H . n) || ['a,b']);
A98:
abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= (e1 / 2) / 2
by A96, XXREAL_0:25;
abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) <= (e1 / 2) / 2
by A97, XXREAL_0:25;
then A99:
abs ((upper_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) <= (e1 / 2) / 2
by A14;
((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) - ((upper_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) = (lower_integral ((lim H,['a,b']) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))
;
then A100:
abs ((lower_integral ((lim H,['a,b']) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= (abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b'])))) + (abs ((upper_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))))
by COMPLEX1:143;
(abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b'])))) + (abs ((upper_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b'])))) <= ((e1 / 2) / 2) + ((e1 / 2) / 2)
by A98, A99, XREAL_1:9;
then
abs ((lower_integral ((lim H,['a,b']) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= e1 / 2
by A100, XXREAL_0:2;
hence
abs ((lower_integral ((lim H,['a,b']) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) < e1
by A94, XXREAL_0:2;
:: thesis: verum end;
now assume
upper_integral ((lim H,['a,b']) || ['a,b']) <> lower_integral ((lim H,['a,b']) || ['a,b'])
;
:: thesis: contradictionthen
0 < abs ((lower_integral ((lim H,['a,b']) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b'])))
by COMPLEX1:148;
hence
contradiction
by A93;
:: thesis: verum end;
then
(lim H,['a,b']) || ['a,b'] is integrable
by A19, INTEGRA1:def 17;
hence
lim H,['a,b'] is_integrable_on ['a,b']
by INTEGRA5:def 2; :: thesis: ( rseq is convergent & lim rseq = integral (lim H,['a,b']),a,b )
A101:
for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((rseq . m) - (integral (lim H,['a,b']),a,b)) < p
proof
let p be
real number ;
:: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((rseq . m) - (integral (lim H,['a,b']),a,b)) < p )
assume
0 < p
;
:: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((rseq . m) - (integral (lim H,['a,b']),a,b)) < p
then A102:
(
0 < p / 2 &
p / 2
< p )
by XREAL_1:217, XREAL_1:218;
set e =
p / 2;
consider N being
Element of
NAT such that A103:
for
n being
Element of
NAT st
N <= n holds
abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= p / 2
by A78, A102;
take
N
;
:: thesis: for m being Element of NAT st N <= m holds
abs ((rseq . m) - (integral (lim H,['a,b']),a,b)) < p
hereby :: thesis: verum
let n be
Element of
NAT ;
:: thesis: ( N <= n implies abs ((rseq . n) - (integral (lim H,['a,b']),a,b)) < p )assume
N <= n
;
:: thesis: abs ((rseq . n) - (integral (lim H,['a,b']),a,b)) < pthen A104:
abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= p / 2
by A103;
upper_integral ((H . n) || ['a,b']) = integral ((H . n) || ['a,b'])
;
then A105:
upper_integral ((H . n) || ['a,b']) = rseq . n
by A14;
upper_integral ((lim H,['a,b']) || ['a,b']) = integral (lim H,['a,b']),
['a,b']
;
then
upper_integral ((lim H,['a,b']) || ['a,b']) = integral (lim H,['a,b']),
a,
b
by A1, INTEGRA5:def 5;
hence
abs ((rseq . n) - (integral (lim H,['a,b']),a,b)) < p
by A102, A104, A105, XXREAL_0:2;
:: thesis: verum
end;
end;
hence
rseq is convergent
by SEQ_2:def 6; :: thesis: lim rseq = integral (lim H,['a,b']),a,b
hence
lim rseq = integral (lim H,['a,b']),a,b
by A101, SEQ_2:def 7; :: thesis: verum