let A be non empty closed_interval Subset of REAL; for rho being Function of A,REAL
for u being PartFunc of REAL,REAL st rho is bounded_variation & dom u = A & u | A is uniformly_continuous holds
for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds
middle_sum S is convergent
let rho be Function of A,REAL; for u being PartFunc of REAL,REAL st rho is bounded_variation & dom u = A & u | A is uniformly_continuous holds
for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds
middle_sum S is convergent
let u be PartFunc of REAL,REAL; ( rho is bounded_variation & dom u = A & u | A is uniformly_continuous implies for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds
middle_sum S is convergent )
assume that
A1:
( rho is bounded_variation & dom u = A )
and
A2:
u | A is uniformly_continuous
; for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds
middle_sum S is convergent
thus
for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds
middle_sum S is convergent
verumproof
let T be
DivSequence of
A;
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds
middle_sum S is convergent let S be
middle_volume_Sequence of
rho,
u,
T;
( delta T is convergent & lim (delta T) = 0 implies middle_sum S is convergent )
assume A4:
(
delta T is
convergent &
lim (delta T) = 0 )
;
middle_sum S is convergent
defpred S1[
Element of
NAT ,
set ]
means ex
p being
FinSequence of
REAL st
(
p = $2 &
len p = len (T . $1) & ( for
i being
Nat st
i in dom (T . $1) holds
(
p . i in dom (u | (divset ((T . $1),i))) & ex
z being
Real st
(
z = (u | (divset ((T . $1),i))) . (p . i) &
(S . $1) . i = z * (vol ((divset ((T . $1),i)),rho)) ) ) ) );
A5:
for
k being
Element of
NAT ex
p being
Element of
REAL * st
S1[
k,
p]
proof
let k be
Element of
NAT ;
ex p being Element of REAL * st S1[k,p]
defpred S2[
Nat,
set ]
means ( $2
in dom (u | (divset ((T . k),$1))) & ex
c being
Real st
(
c = (u | (divset ((T . k),$1))) . $2 &
(S . k) . $1
= c * (vol ((divset ((T . k),$1)),rho)) ) );
A6:
Seg (len (T . k)) = dom (T . k)
by FINSEQ_1:def 3;
A7:
for
i being
Nat st
i in Seg (len (T . k)) holds
ex
x being
Element of
REAL st
S2[
i,
x]
proof
let i be
Nat;
( i in Seg (len (T . k)) implies ex x being Element of REAL st S2[i,x] )
assume
i in Seg (len (T . k))
;
ex x being Element of REAL st S2[i,x]
then
i in dom (T . k)
by FINSEQ_1:def 3;
then consider c being
Real such that A8:
(
c in rng (u | (divset ((T . k),i))) &
(S . k) . i = c * (vol ((divset ((T . k),i)),rho)) )
by A1, INTEGR22:def 5;
consider x being
object such that A9:
(
x in dom (u | (divset ((T . k),i))) &
c = (u | (divset ((T . k),i))) . x )
by A8, FUNCT_1:def 3;
reconsider x =
x as
Element of
REAL by A9;
take
x
;
S2[i,x]
thus
S2[
i,
x]
by A8, A9;
verum
end;
consider p being
FinSequence of
REAL such that A10:
(
dom p = Seg (len (T . k)) & ( for
i being
Nat st
i in Seg (len (T . k)) holds
S2[
i,
p . i] ) )
from FINSEQ_1:sch 5(A7);
take
p
;
( p is Element of REAL * & S1[k,p] )
len p = len (T . k)
by A10, FINSEQ_1:def 3;
hence
(
p is
Element of
REAL * &
S1[
k,
p] )
by A6, A10, FINSEQ_1:def 11;
verum
end;
consider Fn being
sequence of
(REAL *) such that A11:
for
x being
Element of
NAT holds
S1[
x,
Fn . x]
from FUNCT_2:sch 3(A5);
consider Fm being
sequence of
(REAL *) such that A12:
for
x being
Element of
NAT holds
S1[
x,
Fm . x]
from FUNCT_2:sch 3(A5);
set TVD =
total_vd rho;
A13:
0 <= total_vd rho
by A1, INTEGR22:6;
now for p being Real st p > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
|.(((middle_sum S) . n) - ((middle_sum S) . m)).| < plet p be
Real;
( p > 0 implies ex m being Nat st
for n being Nat st n >= m holds
|.(((middle_sum S) . n) - ((middle_sum S) . m)).| < p )set pp2 =
p / 2;
set pv =
(p / 2) / ((total_vd rho) + 1);
assume B13:
p > 0
;
ex m being Nat st
for n being Nat st n >= m holds
|.(((middle_sum S) . n) - ((middle_sum S) . m)).| < pthen A14:
(
0 < p / 2 &
p / 2
< p )
by XREAL_1:215, XREAL_1:216;
then A15:
0 < (p / 2) / ((total_vd rho) + 1)
by A13, XREAL_1:139;
then
((p / 2) / ((total_vd rho) + 1)) * (total_vd rho) < ((p / 2) / ((total_vd rho) + 1)) * ((total_vd rho) + 1)
by XREAL_1:29, XREAL_1:68;
then
((p / 2) / ((total_vd rho) + 1)) * (total_vd rho) < p / 2
by A13, XCMPLX_1:87;
then A16:
((p / 2) / ((total_vd rho) + 1)) * (total_vd rho) < p
by A14, XXREAL_0:2;
set p2v =
((p / 2) / ((total_vd rho) + 1)) / 2;
consider sk being
Real such that A17:
(
0 < sk & ( for
x1,
x2 being
Real st
x1 in dom (u | A) &
x2 in dom (u | A) &
|.(x1 - x2).| < sk holds
|.(((u | A) . x1) - ((u | A) . x2)).| < ((p / 2) / ((total_vd rho) + 1)) / 2 ) )
by A2, A15, FCONT_2:def 1, XREAL_1:215;
consider m being
Nat such that A18:
for
i being
Nat st
m <= i holds
|.(((delta T) . i) - 0).| < sk
by A4, A17, SEQ_2:def 7;
take m =
m;
for n being Nat st n >= m holds
|.(((middle_sum S) . n) - ((middle_sum S) . m)).| < plet n be
Nat;
( n >= m implies |.(((middle_sum S) . n) - ((middle_sum S) . m)).| < p )A19:
(
n in NAT &
m in NAT )
by ORDINAL1:def 12;
assume
n >= m
;
|.(((middle_sum S) . n) - ((middle_sum S) . m)).| < pthen
(
|.(((delta T) . n) - 0).| < sk &
|.(((delta T) . m) - 0).| < sk )
by A18;
then
(
|.(delta (T . n)).| < sk &
|.(delta (T . m)).| < sk )
by A19, INTEGRA3:def 2;
then A20:
(
delta (T . n) < sk &
delta (T . m) < sk )
by ABSVALUE:def 1, INTEGRA3:9;
A21:
(
(middle_sum S) . n = Sum (S . n) &
(middle_sum S) . m = Sum (S . m) )
by INTEGR22:def 7;
consider p1 being
FinSequence of
REAL such that A22:
(
p1 = Fn . n &
len p1 = len (T . n) & ( for
i being
Nat st
i in dom (T . n) holds
(
p1 . i in dom (u | (divset ((T . n),i))) & ex
z being
Real st
(
z = (u | (divset ((T . n),i))) . (p1 . i) &
(S . n) . i = z * (vol ((divset ((T . n),i)),rho)) ) ) ) )
by A11, A19;
consider p2 being
FinSequence of
REAL such that A23:
(
p2 = Fm . m &
len p2 = len (T . m) & ( for
i being
Nat st
i in dom (T . m) holds
(
p2 . i in dom (u | (divset ((T . m),i))) & ex
z being
Real st
(
z = (u | (divset ((T . m),i))) . (p2 . i) &
(S . m) . i = z * (vol ((divset ((T . m),i)),rho)) ) ) ) )
by A12, A19;
defpred S2[
object ,
object ,
object ]
means ex
i,
j being
Nat ex
z being
Real st
( $1
= i & $2
= j &
z = (u | (divset ((T . n),i))) . (p1 . i) & $3
= (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z );
A24:
for
x,
y being
object st
x in Seg (len (T . n)) &
y in Seg (len (T . m)) holds
ex
w being
object st
(
w in REAL &
S2[
x,
y,
w] )
proof
let x,
y be
object ;
( x in Seg (len (T . n)) & y in Seg (len (T . m)) implies ex w being object st
( w in REAL & S2[x,y,w] ) )
assume A25:
(
x in Seg (len (T . n)) &
y in Seg (len (T . m)) )
;
ex w being object st
( w in REAL & S2[x,y,w] )
then reconsider i =
x,
j =
y as
Nat ;
i in dom (T . n)
by A25, FINSEQ_1:def 3;
then consider z being
Real such that A26:
(
z = (u | (divset ((T . n),i))) . (p1 . i) &
(S . n) . i = z * (vol ((divset ((T . n),i)),rho)) )
by A22;
(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z in REAL
by XREAL_0:def 1;
hence
ex
w being
object st
(
w in REAL &
S2[
x,
y,
w] )
by A26;
verum
end; consider Snm being
Function of
[:(Seg (len (T . n))),(Seg (len (T . m))):],
REAL such that A27:
for
x,
y being
object st
x in Seg (len (T . n)) &
y in Seg (len (T . m)) holds
S2[
x,
y,
Snm . (
x,
y)]
from BINOP_1:sch 1(A24);
A28:
for
i,
j being
Nat st
i in Seg (len (T . n)) &
j in Seg (len (T . m)) holds
ex
z being
Real st
(
z = (u | (divset ((T . n),i))) . (p1 . i) &
Snm . (
i,
j)
= (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z )
proof
let i,
j be
Nat;
( i in Seg (len (T . n)) & j in Seg (len (T . m)) implies ex z being Real st
( z = (u | (divset ((T . n),i))) . (p1 . i) & Snm . (i,j) = (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z ) )
assume
(
i in Seg (len (T . n)) &
j in Seg (len (T . m)) )
;
ex z being Real st
( z = (u | (divset ((T . n),i))) . (p1 . i) & Snm . (i,j) = (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z )
then
ex
i1,
j1 being
Nat ex
z being
Real st
(
i = i1 &
j = j1 &
z = (u | (divset ((T . n),i1))) . (p1 . i1) &
Snm . (
i,
j)
= (vol (((divset ((T . n),i1)) /\ (divset ((T . m),j1))),rho)) * z )
by A27;
hence
ex
z being
Real st
(
z = (u | (divset ((T . n),i))) . (p1 . i) &
Snm . (
i,
j)
= (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z )
;
verum
end; defpred S3[
Nat,
object ]
means ex
r being
FinSequence of
REAL st
(
dom r = Seg (len (T . m)) & $2
= Sum r & ( for
j being
Nat st
j in dom r holds
r . j = Snm . ($1,
j) ) );
A29:
for
k being
Nat st
k in Seg (len (T . n)) holds
ex
x being
object st
S3[
k,
x]
consider Xp being
FinSequence such that A35:
(
dom Xp = Seg (len (T . n)) & ( for
k being
Nat st
k in Seg (len (T . n)) holds
S3[
k,
Xp . k] ) )
from FINSEQ_1:sch 1(A29);
for
i being
Nat st
i in dom Xp holds
Xp . i in REAL
then reconsider Xp =
Xp as
FinSequence of
REAL by FINSEQ_2:12;
A36:
len Xp = len (T . n)
by A35, FINSEQ_1:def 3;
for
k being
Nat st 1
<= k &
k <= len Xp holds
Xp . k = (S . n) . k
proof
let k be
Nat;
( 1 <= k & k <= len Xp implies Xp . k = (S . n) . k )
assume
( 1
<= k &
k <= len Xp )
;
Xp . k = (S . n) . k
then A38:
(
k in Seg (len Xp) &
k in Seg (len (T . n)) )
by A36;
then A39:
(
k in dom Xp &
k in dom (T . n) )
by FINSEQ_1:def 3;
then consider z being
Real such that A40:
(
z = (u | (divset ((T . n),k))) . (p1 . k) &
(S . n) . k = z * (vol ((divset ((T . n),k)),rho)) )
by A22;
consider r being
FinSequence of
REAL such that A41:
(
dom r = Seg (len (T . m)) &
Xp . k = Sum r & ( for
j being
Nat st
j in dom r holds
r . j = Snm . (
k,
j) ) )
by A35, A38;
defpred S4[
Nat,
set ]
means $2
= vol (
((divset ((T . n),k)) /\ (divset ((T . m),$1))),
rho);
A42:
for
i being
Nat st
i in Seg (len r) holds
ex
x being
Element of
REAL st
S4[
i,
x]
consider vtntm being
FinSequence of
REAL such that A43:
(
dom vtntm = Seg (len r) & ( for
i being
Nat st
i in Seg (len r) holds
S4[
i,
vtntm . i] ) )
from FINSEQ_1:sch 5(A42);
A44:
(
dom vtntm = dom r & ( for
j being
Nat st
j in dom vtntm holds
vtntm . j = vol (
((divset ((T . n),k)) /\ (divset ((T . m),j))),
rho) ) )
by A43, FINSEQ_1:def 3;
A45:
(
len vtntm = len r &
len (T . m) = len r )
by A41, A43, FINSEQ_1:def 3;
then A46:
Sum vtntm = vol (
(divset ((T . n),k)),
rho)
by A39, A43, INTEGR22:1, INTEGRA1:8;
for
j being
Nat st
j in dom r holds
ex
x being
Real st
(
x = vtntm . j &
r . j = x * z )
proof
let j be
Nat;
( j in dom r implies ex x being Real st
( x = vtntm . j & r . j = x * z ) )
assume A47:
j in dom r
;
ex x being Real st
( x = vtntm . j & r . j = x * z )
then A48:
ex
w being
Real st
(
w = (u | (divset ((T . n),k))) . (p1 . k) &
Snm . (
k,
j)
= (vol (((divset ((T . n),k)) /\ (divset ((T . m),j))),rho)) * w )
by A28, A38, A41;
take
vtntm . j
;
( vtntm . j = vtntm . j & r . j = (vtntm . j) * z )
r . j = (vol (((divset ((T . n),k)) /\ (divset ((T . m),j))),rho)) * z
by A40, A41, A47, A48;
hence
(
vtntm . j = vtntm . j &
r . j = (vtntm . j) * z )
by A44, A47;
verum
end;
hence
Xp . k = (S . n) . k
by A40, A41, A45, A46, Th1;
verum
end; then A49:
Xp = S . n
by A1, A36, INTEGR22:def 5;
defpred S4[
Nat,
object ]
means ex
s being
FinSequence of
REAL st
(
dom s = Seg (len (T . n)) & $2
= Sum s & ( for
i being
Nat st
i in dom s holds
s . i = Snm . (
i,$1) ) );
A50:
for
k being
Nat st
k in Seg (len (T . m)) holds
ex
x being
object st
S4[
k,
x]
consider Xq being
FinSequence such that A56:
(
dom Xq = Seg (len (T . m)) & ( for
k being
Nat st
k in Seg (len (T . m)) holds
S4[
k,
Xq . k] ) )
from FINSEQ_1:sch 1(A50);
for
j being
Nat st
j in dom Xq holds
Xq . j in REAL
then reconsider Xq =
Xq as
FinSequence of
REAL by FINSEQ_2:12;
defpred S5[
object ,
object ,
object ]
means ex
i,
j being
Nat ex
z being
Real st
( $1
= i & $2
= j &
z = (u | (divset ((T . m),j))) . (p2 . j) & $3
= (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z );
A57:
for
x,
y being
object st
x in Seg (len (T . n)) &
y in Seg (len (T . m)) holds
ex
w being
object st
(
w in REAL &
S5[
x,
y,
w] )
proof
let x,
y be
object ;
( x in Seg (len (T . n)) & y in Seg (len (T . m)) implies ex w being object st
( w in REAL & S5[x,y,w] ) )
assume A58:
(
x in Seg (len (T . n)) &
y in Seg (len (T . m)) )
;
ex w being object st
( w in REAL & S5[x,y,w] )
then reconsider i =
x,
j =
y as
Nat ;
j in dom (T . m)
by A58, FINSEQ_1:def 3;
then consider z being
Real such that A59:
(
z = (u | (divset ((T . m),j))) . (p2 . j) &
(S . m) . j = z * (vol ((divset ((T . m),j)),rho)) )
by A23;
(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z in REAL
by XREAL_0:def 1;
hence
ex
w being
object st
(
w in REAL &
S5[
x,
y,
w] )
by A59;
verum
end; consider Smn being
Function of
[:(Seg (len (T . n))),(Seg (len (T . m))):],
REAL such that A60:
for
x,
y being
object st
x in Seg (len (T . n)) &
y in Seg (len (T . m)) holds
S5[
x,
y,
Smn . (
x,
y)]
from BINOP_1:sch 1(A57);
A61:
for
i,
j being
Nat st
i in Seg (len (T . n)) &
j in Seg (len (T . m)) holds
ex
z being
Real st
(
z = (u | (divset ((T . m),j))) . (p2 . j) &
Smn . (
i,
j)
= (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z )
proof
let i,
j be
Nat;
( i in Seg (len (T . n)) & j in Seg (len (T . m)) implies ex z being Real st
( z = (u | (divset ((T . m),j))) . (p2 . j) & Smn . (i,j) = (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z ) )
assume
(
i in Seg (len (T . n)) &
j in Seg (len (T . m)) )
;
ex z being Real st
( z = (u | (divset ((T . m),j))) . (p2 . j) & Smn . (i,j) = (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z )
then
ex
i1,
j1 being
Nat ex
z being
Real st
(
i = i1 &
j = j1 &
z = (u | (divset ((T . m),j1))) . (p2 . j1) &
Smn . (
i,
j)
= (vol (((divset ((T . n),i1)) /\ (divset ((T . m),j1))),rho)) * z )
by A60;
hence
ex
z being
Real st
(
z = (u | (divset ((T . m),j))) . (p2 . j) &
Smn . (
i,
j)
= (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z )
;
verum
end; defpred S6[
Nat,
object ]
means ex
s being
FinSequence of
REAL st
(
dom s = Seg (len (T . n)) & $2
= Sum s & ( for
i being
Nat st
i in dom s holds
s . i = Smn . (
i,$1) ) );
A62:
for
k being
Nat st
k in Seg (len (T . m)) holds
ex
x being
object st
S6[
k,
x]
consider Zq being
FinSequence such that A68:
(
dom Zq = Seg (len (T . m)) & ( for
k being
Nat st
k in Seg (len (T . m)) holds
S6[
k,
Zq . k] ) )
from FINSEQ_1:sch 1(A62);
for
j being
Nat st
j in dom Zq holds
Zq . j in REAL
then reconsider Zq =
Zq as
FinSequence of
REAL by FINSEQ_2:12;
A69:
len Zq = len (T . m)
by A68, FINSEQ_1:def 3;
for
k being
Nat st 1
<= k &
k <= len Zq holds
Zq . k = (S . m) . k
proof
let k be
Nat;
( 1 <= k & k <= len Zq implies Zq . k = (S . m) . k )
assume A71:
( 1
<= k &
k <= len Zq )
;
Zq . k = (S . m) . k
then consider s being
FinSequence of
REAL such that A72:
(
dom s = Seg (len (T . n)) &
Zq . k = Sum s & ( for
i being
Nat st
i in dom s holds
s . i = Smn . (
i,
k) ) )
by A68, FINSEQ_3:25;
A73:
k in Seg (len (T . m))
by A69, A71;
A74:
k in dom (T . m)
by A69, A71, FINSEQ_3:25;
then consider z being
Real such that A75:
(
z = (u | (divset ((T . m),k))) . (p2 . k) &
(S . m) . k = z * (vol ((divset ((T . m),k)),rho)) )
by A23;
defpred S7[
Nat,
set ]
means $2
= vol (
((divset ((T . n),$1)) /\ (divset ((T . m),k))),
rho);
A76:
for
i being
Nat st
i in Seg (len s) holds
ex
x being
Element of
REAL st
S7[
i,
x]
consider vtntm being
FinSequence of
REAL such that A77:
(
dom vtntm = Seg (len s) & ( for
i being
Nat st
i in Seg (len s) holds
S7[
i,
vtntm . i] ) )
from FINSEQ_1:sch 5(A76);
A78:
(
dom vtntm = dom s &
len vtntm = len s )
by A77, FINSEQ_1:def 3;
A79:
for
j being
Nat st
j in dom vtntm holds
vtntm . j = vol (
((divset ((T . m),k)) /\ (divset ((T . n),j))),
rho)
by A77;
len s = len (T . n)
by A72, FINSEQ_1:def 3;
then A80:
Sum vtntm = vol (
(divset ((T . m),k)),
rho)
by A74, A78, A79, INTEGR22:1, INTEGRA1:8;
for
j being
Nat st
j in dom s holds
ex
x being
Real st
(
x = vtntm . j &
s . j = x * z )
proof
let j be
Nat;
( j in dom s implies ex x being Real st
( x = vtntm . j & s . j = x * z ) )
assume A81:
j in dom s
;
ex x being Real st
( x = vtntm . j & s . j = x * z )
then A82:
ex
w being
Real st
(
w = (u | (divset ((T . m),k))) . (p2 . k) &
Smn . (
j,
k)
= (vol (((divset ((T . n),j)) /\ (divset ((T . m),k))),rho)) * w )
by A61, A72, A73;
take
vtntm . j
;
( vtntm . j = vtntm . j & s . j = (vtntm . j) * z )
s . j = (vol (((divset ((T . n),j)) /\ (divset ((T . m),k))),rho)) * z
by A72, A75, A81, A82;
hence
(
vtntm . j = vtntm . j &
s . j = (vtntm . j) * z )
by A77, A78, A81;
verum
end;
hence
Zq . k = (S . m) . k
by A72, A75, A78, A80, Th1;
verum
end; then
Zq = S . m
by A1, A69, INTEGR22:def 5;
then A83:
(Sum (S . n)) - (Sum (S . m)) = (Sum Xq) - (Sum Zq)
by A35, A49, A56, INTEGR22:2;
set XZq =
Xq - Zq;
A84:
dom (Xq - Zq) = (dom Xq) /\ (dom Zq)
by VALUED_1:12;
reconsider XZq =
Xq - Zq as
FinSequence of
REAL ;
len Xq = len Zq
by A56, A68, FINSEQ_3:29;
then A86:
(
Xq is
Element of
(len Xq) -tuples_on REAL &
Zq is
Element of
(len Xq) -tuples_on REAL )
by FINSEQ_2:92;
A87:
for
i,
j being
Nat for
Snmij,
Smnij being
Real st
i in Seg (len (T . n)) &
j in Seg (len (T . m)) &
Snmij = Snm . (
i,
j) &
Smnij = Smn . (
i,
j) holds
|.(Snmij - Smnij).| <= |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| * ((p / 2) / ((total_vd rho) + 1))
proof
let i,
j be
Nat;
for Snmij, Smnij being Real st i in Seg (len (T . n)) & j in Seg (len (T . m)) & Snmij = Snm . (i,j) & Smnij = Smn . (i,j) holds
|.(Snmij - Smnij).| <= |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| * ((p / 2) / ((total_vd rho) + 1))let Snmij,
Smnij be
Real;
( i in Seg (len (T . n)) & j in Seg (len (T . m)) & Snmij = Snm . (i,j) & Smnij = Smn . (i,j) implies |.(Snmij - Smnij).| <= |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| * ((p / 2) / ((total_vd rho) + 1)) )
assume A88:
(
i in Seg (len (T . n)) &
j in Seg (len (T . m)) &
Snmij = Snm . (
i,
j) &
Smnij = Smn . (
i,
j) )
;
|.(Snmij - Smnij).| <= |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| * ((p / 2) / ((total_vd rho) + 1))
then consider z1 being
Real such that A89:
(
z1 = (u | (divset ((T . n),i))) . (p1 . i) &
Snm . (
i,
j)
= (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z1 )
by A28;
consider z2 being
Real such that A90:
(
z2 = (u | (divset ((T . m),j))) . (p2 . j) &
Smn . (
i,
j)
= (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z2 )
by A61, A88;
A91:
(
i in dom (T . n) &
j in dom (T . m) )
by A88, FINSEQ_1:def 3;
then A92:
(
p1 . i in dom (u | (divset ((T . n),i))) &
p2 . j in dom (u | (divset ((T . m),j))) )
by A22, A23;
then
(
p1 . i in (dom u) /\ (divset ((T . n),i)) &
p2 . j in (dom u) /\ (divset ((T . m),j)) )
by RELAT_1:61;
then A93:
(
p1 . i in dom u &
p1 . i in divset (
(T . n),
i) &
p2 . j in dom u &
p2 . j in divset (
(T . m),
j) )
by XBOOLE_0:def 4;
A94:
(
z1 = u . (p1 . i) &
z2 = u . (p2 . j) )
by A89, A90, A92, FUNCT_1:47;
per cases
( (divset ((T . n),i)) /\ (divset ((T . m),j)) = {} or (divset ((T . n),i)) /\ (divset ((T . m),j)) <> {} )
;
suppose
(divset ((T . n),i)) /\ (divset ((T . m),j)) <> {}
;
|.(Snmij - Smnij).| <= |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| * ((p / 2) / ((total_vd rho) + 1))then consider t being
object such that A97:
t in (divset ((T . n),i)) /\ (divset ((T . m),j))
by XBOOLE_0:def 1;
reconsider t =
t as
Real by A97;
A98:
divset (
(T . m),
j)
c= A
by A91, INTEGRA1:8;
A99:
(
t in divset (
(T . n),
i) &
t in divset (
(T . m),
j) )
by A97, XBOOLE_0:def 4;
then
(
|.((p1 . i) - t).| < sk &
|.(t - (p2 . j)).| < sk )
by A20, A91, A93, INTEGR20:12;
then A100:
(
|.((u . (p1 . i)) - (u . t)).| < ((p / 2) / ((total_vd rho) + 1)) / 2 &
|.((u . t) - (u . (p2 . j))).| < ((p / 2) / ((total_vd rho) + 1)) / 2 )
by A1, A17, A93, A98, A99;
reconsider DMN =
(divset ((T . n),i)) /\ (divset ((T . m),j)) as
real-bounded Subset of
REAL by XBOOLE_1:17, XXREAL_2:45;
Snmij - Smnij = ((vol (DMN,rho)) * ((u . (p1 . i)) - (u . t))) + ((vol (DMN,rho)) * ((u . t) - (u . (p2 . j))))
by A88, A89, A90, A94;
then A101:
|.(Snmij - Smnij).| <= |.((vol (DMN,rho)) * ((u . (p1 . i)) - (u . t))).| + |.((vol (DMN,rho)) * ((u . t) - (u . (p2 . j)))).|
by COMPLEX1:56;
A102:
(
|.((vol (DMN,rho)) * ((u . (p1 . i)) - (u . t))).| = |.(vol (DMN,rho)).| * |.((u . (p1 . i)) - (u . t)).| &
|.((vol (DMN,rho)) * ((u . t) - (u . (p2 . j)))).| = |.(vol (DMN,rho)).| * |.((u . t) - (u . (p2 . j))).| )
by COMPLEX1:65;
0 <= |.(vol (DMN,rho)).|
by COMPLEX1:46;
then
(
|.((vol (DMN,rho)) * ((u . (p1 . i)) - (u . t))).| <= |.(vol (DMN,rho)).| * (((p / 2) / ((total_vd rho) + 1)) / 2) &
|.((vol (DMN,rho)) * ((u . t) - (u . (p2 . j)))).| <= |.(vol (DMN,rho)).| * (((p / 2) / ((total_vd rho) + 1)) / 2) )
by A100, A102, XREAL_1:64;
then
|.((vol (DMN,rho)) * ((u . (p1 . i)) - (u . t))).| + |.((vol (DMN,rho)) * ((u . t) - (u . (p2 . j)))).| <= (|.(vol (DMN,rho)).| * (((p / 2) / ((total_vd rho) + 1)) / 2)) + (|.(vol (DMN,rho)).| * (((p / 2) / ((total_vd rho) + 1)) / 2))
by XREAL_1:7;
hence
|.(Snmij - Smnij).| <= |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| * ((p / 2) / ((total_vd rho) + 1))
by A101, XXREAL_0:2;
verum end; end;
end; consider vtntm being
FinSequence of
REAL such that A103:
(
len vtntm = len (T . m) &
Sum vtntm <= total_vd rho & ( for
j being
Nat st
j in dom (T . m) holds
ex
p being
FinSequence of
REAL st
(
vtntm . j = Sum p &
len p = len (T . n) & ( for
i being
Nat st
i in dom (T . n) holds
p . i = |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| ) ) ) )
by A1, Th19;
reconsider PVD =
((p / 2) / ((total_vd rho) + 1)) * vtntm as
FinSequence of
REAL ;
dom PVD = dom vtntm
by VALUED_1:def 5;
then
dom PVD = Seg (len (T . m))
by A103, FINSEQ_1:def 3;
then A104:
len PVD = len (T . m)
by FINSEQ_1:def 3;
A105:
for
j being
Nat st
j in Seg (len (T . m)) holds
ex
pvtntm being
FinSequence of
REAL st
(
PVD . j = Sum pvtntm &
len pvtntm = len (T . n) & ( for
i being
Nat st
i in Seg (len (T . n)) holds
pvtntm . i = ((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| ) )
proof
let j be
Nat;
( j in Seg (len (T . m)) implies ex pvtntm being FinSequence of REAL st
( PVD . j = Sum pvtntm & len pvtntm = len (T . n) & ( for i being Nat st i in Seg (len (T . n)) holds
pvtntm . i = ((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| ) ) )
assume
j in Seg (len (T . m))
;
ex pvtntm being FinSequence of REAL st
( PVD . j = Sum pvtntm & len pvtntm = len (T . n) & ( for i being Nat st i in Seg (len (T . n)) holds
pvtntm . i = ((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| ) )
then
j in dom (T . m)
by FINSEQ_1:def 3;
then consider v being
FinSequence of
REAL such that A107:
(
vtntm . j = Sum v &
len v = len (T . n) & ( for
i being
Nat st
i in dom (T . n) holds
v . i = |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| ) )
by A103;
reconsider pvtntm =
((p / 2) / ((total_vd rho) + 1)) * v as
FinSequence of
REAL ;
take
pvtntm
;
( PVD . j = Sum pvtntm & len pvtntm = len (T . n) & ( for i being Nat st i in Seg (len (T . n)) holds
pvtntm . i = ((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| ) )
thus PVD . j =
((p / 2) / ((total_vd rho) + 1)) * (vtntm . j)
by VALUED_1:6
.=
Sum pvtntm
by A107, RVSUM_1:87
;
( len pvtntm = len (T . n) & ( for i being Nat st i in Seg (len (T . n)) holds
pvtntm . i = ((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| ) )
dom pvtntm = dom v
by VALUED_1:def 5;
then
dom pvtntm = Seg (len (T . n))
by A107, FINSEQ_1:def 3;
hence
len pvtntm = len (T . n)
by FINSEQ_1:def 3;
for i being Nat st i in Seg (len (T . n)) holds
pvtntm . i = ((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).|
let i be
Nat;
( i in Seg (len (T . n)) implies pvtntm . i = ((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| )
assume
i in Seg (len (T . n))
;
pvtntm . i = ((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).|
then a108:
i in dom (T . n)
by FINSEQ_1:def 3;
thus pvtntm . i =
((p / 2) / ((total_vd rho) + 1)) * (v . i)
by VALUED_1:6
.=
((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).|
by A107, a108
;
verum
end; A109:
Sum PVD = ((p / 2) / ((total_vd rho) + 1)) * (Sum vtntm)
by RVSUM_1:87;
A110:
((p / 2) / ((total_vd rho) + 1)) * (Sum vtntm) <= ((p / 2) / ((total_vd rho) + 1)) * (total_vd rho)
by A13, B13, A103, XREAL_1:64;
A111:
len XZq = len (T . m)
by A56, A68, A84, FINSEQ_1:def 3;
for
j being
Nat st
j in dom XZq holds
|.(XZq . j).| <= PVD . j
proof
let j be
Nat;
( j in dom XZq implies |.(XZq . j).| <= PVD . j )
assume A112:
j in dom XZq
;
|.(XZq . j).| <= PVD . j
then A113:
XZq . j = (Xq . j) - (Zq . j)
by VALUED_1:13;
consider Xsq being
FinSequence of
REAL such that A114:
(
dom Xsq = Seg (len (T . n)) &
Xq . j = Sum Xsq & ( for
i being
Nat st
i in dom Xsq holds
Xsq . i = Snm . (
i,
j) ) )
by A56, A68, A84, A112;
consider Zsq being
FinSequence of
REAL such that A115:
(
dom Zsq = Seg (len (T . n)) &
Zq . j = Sum Zsq & ( for
i being
Nat st
i in dom Zsq holds
Zsq . i = Smn . (
i,
j) ) )
by A56, A68, A84, A112;
set XZsq =
Xsq - Zsq;
A116:
dom (Xsq - Zsq) = (dom Xsq) /\ (dom Zsq)
by VALUED_1:12;
reconsider XZsq =
Xsq - Zsq as
FinSequence of
REAL ;
A117:
len XZsq = len (T . n)
by A114, A115, A116, FINSEQ_1:def 3;
consider pvtntm being
FinSequence of
REAL such that A118:
(
PVD . j = Sum pvtntm &
len pvtntm = len (T . n) & ( for
i being
Nat st
i in Seg (len (T . n)) holds
pvtntm . i = ((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| ) )
by A105, A56, A68, A84, A112;
for
i being
Nat st
i in dom XZsq holds
|.(XZsq . i).| <= pvtntm . i
proof
let i be
Nat;
( i in dom XZsq implies |.(XZsq . i).| <= pvtntm . i )
assume A119:
i in dom XZsq
;
|.(XZsq . i).| <= pvtntm . i
then A120:
XZsq . i = (Xsq . i) - (Zsq . i)
by VALUED_1:13;
A121:
pvtntm . i = ((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).|
by A118, A114, A115, A116, A119;
(
Xsq . i = Snm . (
i,
j) &
Zsq . i = Smn . (
i,
j) )
by A114, A115, A116, A119;
hence
|.(XZsq . i).| <= pvtntm . i
by A56, A68, A84, A87, A112, A114, A115, A116, A119, A120, A121;
verum
end;
then A122:
|.(Sum XZsq).| <= PVD . j
by A117, A118, Th3;
len Xsq = len Zsq
by A114, A115, FINSEQ_3:29;
then
(
Xsq is
Element of
(len Xsq) -tuples_on REAL &
Zsq is
Element of
(len Xsq) -tuples_on REAL )
by FINSEQ_2:92;
hence
|.(XZq . j).| <= PVD . j
by A113, A114, A115, A122, RVSUM_1:90;
verum
end; then
|.(Sum XZq).| <= Sum PVD
by A104, A111, Th3;
then A124:
|.(Sum XZq).| <= (total_vd rho) * ((p / 2) / ((total_vd rho) + 1))
by A109, A110, XXREAL_0:2;
Sum XZq = ((middle_sum S) . n) - ((middle_sum S) . m)
by A21, A83, A86, RVSUM_1:90;
hence
|.(((middle_sum S) . n) - ((middle_sum S) . m)).| < p
by A16, A124, XXREAL_0:2;
verum end;
hence
middle_sum S is
convergent
by SEQ_4:41;
verum
end;