let X be RealBanachSpace; for A being non empty closed_interval Subset of REAL
for h being Function of A, the carrier of X st ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom h & x2 in dom h & |.(x1 - x2).| < s holds
||.((h /. x1) - (h /. x2)).|| < r ) ) ) holds
for T being DivSequence of A
for S being middle_volume_Sequence of h,T st delta T is convergent & lim (delta T) = 0 holds
middle_sum (h,S) is convergent
let A be non empty closed_interval Subset of REAL; for h being Function of A, the carrier of X st ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom h & x2 in dom h & |.(x1 - x2).| < s holds
||.((h /. x1) - (h /. x2)).|| < r ) ) ) holds
for T being DivSequence of A
for S being middle_volume_Sequence of h,T st delta T is convergent & lim (delta T) = 0 holds
middle_sum (h,S) is convergent
let h be Function of A, the carrier of X; ( ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom h & x2 in dom h & |.(x1 - x2).| < s holds
||.((h /. x1) - (h /. x2)).|| < r ) ) ) implies for T being DivSequence of A
for S being middle_volume_Sequence of h,T st delta T is convergent & lim (delta T) = 0 holds
middle_sum (h,S) is convergent )
assume A1:
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom h & x2 in dom h & |.(x1 - x2).| < s holds
||.((h /. x1) - (h /. x2)).|| < r ) )
; for T being DivSequence of A
for S being middle_volume_Sequence of h,T st delta T is convergent & lim (delta T) = 0 holds
middle_sum (h,S) is convergent
thus
for T being DivSequence of A
for S being middle_volume_Sequence of h,T st delta T is convergent & lim (delta T) = 0 holds
middle_sum (h,S) is convergent
verumproof
let T be
DivSequence of
A;
for S being middle_volume_Sequence of h,T st delta T is convergent & lim (delta T) = 0 holds
middle_sum (h,S) is convergent let S be
middle_volume_Sequence of
h,
T;
( delta T is convergent & lim (delta T) = 0 implies middle_sum (h,S) is convergent )
assume A2:
(
delta T is
convergent &
lim (delta T) = 0 )
;
middle_sum (h,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 (h | (divset ((T . $1),i))) & ex
z being
Point of
X st
(
z = (h | (divset ((T . $1),i))) . (p . i) &
(S . $1) . i = (vol (divset ((T . $1),i))) * z ) ) ) );
A3:
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 (h | (divset ((T . k),$1))) & ex
c being
Point of
X st
(
c = (h | (divset ((T . k),$1))) . $2 &
(S . k) . $1
= (vol (divset ((T . k),$1))) * c ) );
A4:
Seg (len (T . k)) = dom (T . k)
by FINSEQ_1:def 3;
A5:
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
Point of
X such that A6:
(
c in rng (h | (divset ((T . k),i))) &
(S . k) . i = (vol (divset ((T . k),i))) * c )
by INTEGR18:def 1;
consider x being
object such that A7:
(
x in dom (h | (divset ((T . k),i))) &
c = (h | (divset ((T . k),i))) . x )
by A6, FUNCT_1:def 3;
(
x in dom h &
x in divset (
(T . k),
i) )
by A7, RELAT_1:57;
then reconsider x =
x as
Element of
REAL ;
take
x
;
S2[i,x]
thus
S2[
i,
x]
by A6, A7;
verum
end;
consider p being
FinSequence of
REAL such that A8:
(
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(A5);
take
p
;
( p is Element of REAL * & S1[k,p] )
len p = len (T . k)
by A8, FINSEQ_1:def 3;
hence
(
p is
Element of
REAL * &
S1[
k,
p] )
by A8, A4, FINSEQ_1:def 11;
verum
end;
consider Fn being
sequence of
(REAL *) such that A9:
for
x being
Element of
NAT holds
S1[
x,
Fn . x]
from FUNCT_2:sch 3(A3);
consider Fm being
sequence of
(REAL *) such that A10:
for
x being
Element of
NAT holds
S1[
x,
Fm . x]
from FUNCT_2:sch 3(A3);
A11:
0 <= vol A
by INTEGRA1:9;
now for p being Real st p > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.(((middle_sum (h,S)) . n) - ((middle_sum (h,S)) . m)).|| < plet p be
Real;
( p > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.(((middle_sum (h,S)) . n) - ((middle_sum (h,S)) . m)).|| < p )set pp2 =
p / 2;
set pv =
(p / 2) / ((vol A) + 1);
assume
p > 0
;
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.(((middle_sum (h,S)) . n) - ((middle_sum (h,S)) . m)).|| < pthen A12:
(
0 < p / 2 &
p / 2
< p )
by XREAL_1:215, XREAL_1:216;
then A13:
0 < (p / 2) / ((vol A) + 1)
by A11, XREAL_1:139;
then
((p / 2) / ((vol A) + 1)) * (vol A) < ((p / 2) / ((vol A) + 1)) * ((vol A) + 1)
by XREAL_1:29, XREAL_1:68;
then
((p / 2) / ((vol A) + 1)) * (vol A) < p / 2
by A11, XCMPLX_1:87;
then A14:
((p / 2) / ((vol A) + 1)) * (vol A) < p
by A12, XXREAL_0:2;
set p2v =
((p / 2) / ((vol A) + 1)) / 2;
consider sk being
Real such that A15:
(
0 < sk & ( for
x1,
x2 being
Real st
x1 in dom h &
x2 in dom h &
|.(x1 - x2).| < sk holds
||.((h /. x1) - (h /. x2)).|| < ((p / 2) / ((vol A) + 1)) / 2 ) )
by A1, A13, XREAL_1:215;
consider k being
Nat such that A16:
for
i being
Nat st
k <= i holds
|.(((delta T) . i) - 0).| < sk
by A15, A2, SEQ_2:def 7;
take k =
k;
for n, m being Nat st n >= k & m >= k holds
||.(((middle_sum (h,S)) . n) - ((middle_sum (h,S)) . m)).|| < plet n,
m be
Nat;
( n >= k & m >= k implies ||.(((middle_sum (h,S)) . n) - ((middle_sum (h,S)) . m)).|| < p )A17:
(
n in NAT &
m in NAT )
by ORDINAL1:def 12;
assume
(
n >= k &
m >= k )
;
||.(((middle_sum (h,S)) . n) - ((middle_sum (h,S)) . m)).|| < pthen
(
|.(((delta T) . n) - 0).| < sk &
|.(((delta T) . m) - 0).| < sk )
by A16;
then
(
|.(delta (T . n)).| < sk &
|.(delta (T . m)).| < sk )
by INTEGRA3:def 2, A17;
then A18:
(
delta (T . n) < sk &
delta (T . m) < sk )
by INTEGRA3:9, ABSVALUE:def 1;
A19:
(
(middle_sum (h,S)) . n = middle_sum (
h,
(S . n)) &
(middle_sum (h,S)) . m = middle_sum (
h,
(S . m)) )
by INTEGR18:def 4;
consider p1 being
FinSequence of
REAL such that A20:
(
p1 = Fn . n &
len p1 = len (T . n) & ( for
i being
Nat st
i in dom (T . n) holds
(
p1 . i in dom (h | (divset ((T . n),i))) & ex
z being
Point of
X st
(
z = (h | (divset ((T . n),i))) . (p1 . i) &
(S . n) . i = (vol (divset ((T . n),i))) * z ) ) ) )
by A9, A17;
consider p2 being
FinSequence of
REAL such that A21:
(
p2 = Fm . m &
len p2 = len (T . m) & ( for
i being
Nat st
i in dom (T . m) holds
(
p2 . i in dom (h | (divset ((T . m),i))) & ex
z being
Point of
X st
(
z = (h | (divset ((T . m),i))) . (p2 . i) &
(S . m) . i = (vol (divset ((T . m),i))) * z ) ) ) )
by A10, A17;
defpred S2[
object ,
object ,
object ]
means ex
i,
j being
Nat ex
z being
Point of
X st
( $1
= i & $2
= j &
z = (h | (divset ((T . n),i))) . (p1 . i) & $3
= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z );
A22:
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 the
carrier of
X &
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 the carrier of X & S2[x,y,w] ) )
assume A23:
(
x in Seg (len (T . n)) &
y in Seg (len (T . m)) )
;
ex w being object st
( w in the carrier of X & S2[x,y,w] )
then reconsider i =
x,
j =
y as
Nat ;
i in dom (T . n)
by FINSEQ_1:def 3, A23;
then consider z being
Point of
X such that A24:
(
z = (h | (divset ((T . n),i))) . (p1 . i) &
(S . n) . i = (vol (divset ((T . n),i))) * z )
by A20;
(xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z in the
carrier of
X
;
hence
ex
w being
object st
(
w in the
carrier of
X &
S2[
x,
y,
w] )
by A24;
verum
end; consider Snm being
Function of
[:(Seg (len (T . n))),(Seg (len (T . m))):], the
carrier of
X such that A25:
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(A22);
A26:
for
i,
j being
Nat st
i in Seg (len (T . n)) &
j in Seg (len (T . m)) holds
ex
z being
Point of
X st
(
z = (h | (divset ((T . n),i))) . (p1 . i) &
Snm . (
i,
j)
= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z )
proof
let i,
j be
Nat;
( i in Seg (len (T . n)) & j in Seg (len (T . m)) implies ex z being Point of X st
( z = (h | (divset ((T . n),i))) . (p1 . i) & Snm . (i,j) = (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z ) )
assume
(
i in Seg (len (T . n)) &
j in Seg (len (T . m)) )
;
ex z being Point of X st
( z = (h | (divset ((T . n),i))) . (p1 . i) & Snm . (i,j) = (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z )
then
ex
i1,
j1 being
Nat ex
z being
Point of
X st
(
i = i1 &
j = j1 &
z = (h | (divset ((T . n),i1))) . (p1 . i1) &
Snm . (
i,
j)
= (xvol ((divset ((T . n),i1)) /\ (divset ((T . m),j1)))) * z )
by A25;
hence
ex
z being
Point of
X st
(
z = (h | (divset ((T . n),i))) . (p1 . i) &
Snm . (
i,
j)
= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z )
;
verum
end; defpred S3[
Nat,
object ]
means ex
r being
FinSequence of
X 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) ) );
A27:
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 A33:
(
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(A27);
for
i being
Nat st
i in dom Xp holds
Xp . i in the
carrier of
X
then reconsider Xp =
Xp as
FinSequence of
X by FINSEQ_2:12;
A34:
len Xp = len (T . n)
by FINSEQ_1:def 3, A33;
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 A35:
(
k in Seg (len Xp) &
k in Seg (len (T . n)) )
by A34;
then A36:
(
k in dom Xp &
k in dom (T . n) )
by FINSEQ_1:def 3;
then consider z being
Point of
X such that A37:
(
z = (h | (divset ((T . n),k))) . (p1 . k) &
(S . n) . k = (vol (divset ((T . n),k))) * z )
by A20;
consider r being
FinSequence of
X such that A38:
(
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, A33;
defpred S4[
Nat,
set ]
means $2
= xvol ((divset ((T . n),k)) /\ (divset ((T . m),$1)));
A39:
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 A40:
(
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(A39);
A41:
(
dom vtntm = dom r & ( for
j being
Nat st
j in dom vtntm holds
vtntm . j = xvol ((divset ((T . n),k)) /\ (divset ((T . m),j))) ) )
by A40, FINSEQ_1:def 3;
A42:
(
len vtntm = len r &
len (T . m) = len r )
by A38, A40, FINSEQ_1:def 3;
then A43:
Sum vtntm = vol (divset ((T . n),k))
by Th8, A40, A36, 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 A44:
j in dom r
;
ex x being Real st
( x = vtntm . j & r . j = x * z )
then A45:
ex
w being
Point of
X st
(
w = (h | (divset ((T . n),k))) . (p1 . k) &
Snm . (
k,
j)
= (xvol ((divset ((T . n),k)) /\ (divset ((T . m),j)))) * w )
by A26, A35, A38;
take
vtntm . j
;
( vtntm . j = vtntm . j & r . j = (vtntm . j) * z )
r . j = (xvol ((divset ((T . n),k)) /\ (divset ((T . m),j)))) * z
by A37, A45, A44, A38;
hence
(
vtntm . j = vtntm . j &
r . j = (vtntm . j) * z )
by A41, A44;
verum
end;
hence
Xp . k = (S . n) . k
by A37, A38, A43, Th7, A42;
verum
end; then A46:
Xp = S . n
by INTEGR18:def 1, A34;
defpred S4[
Nat,
object ]
means ex
s being
FinSequence of
X 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) ) );
A47:
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 A53:
(
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(A47);
for
j being
Nat st
j in dom Xq holds
Xq . j in the
carrier of
X
then reconsider Xq =
Xq as
FinSequence of
X by FINSEQ_2:12;
defpred S5[
object ,
object ,
object ]
means ex
i,
j being
Nat ex
z being
Point of
X st
( $1
= i & $2
= j &
z = (h | (divset ((T . m),j))) . (p2 . j) & $3
= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z );
A54:
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 the
carrier of
X &
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 the carrier of X & S5[x,y,w] ) )
assume A55:
(
x in Seg (len (T . n)) &
y in Seg (len (T . m)) )
;
ex w being object st
( w in the carrier of X & S5[x,y,w] )
then reconsider i =
x,
j =
y as
Nat ;
j in dom (T . m)
by FINSEQ_1:def 3, A55;
then consider z being
Point of
X such that A56:
(
z = (h | (divset ((T . m),j))) . (p2 . j) &
(S . m) . j = (vol (divset ((T . m),j))) * z )
by A21;
(xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z in the
carrier of
X
;
hence
ex
w being
object st
(
w in the
carrier of
X &
S5[
x,
y,
w] )
by A56;
verum
end; consider Smn being
Function of
[:(Seg (len (T . n))),(Seg (len (T . m))):], the
carrier of
X such that A57:
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(A54);
A58:
for
i,
j being
Nat st
i in Seg (len (T . n)) &
j in Seg (len (T . m)) holds
ex
z being
Point of
X st
(
z = (h | (divset ((T . m),j))) . (p2 . j) &
Smn . (
i,
j)
= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z )
proof
let i,
j be
Nat;
( i in Seg (len (T . n)) & j in Seg (len (T . m)) implies ex z being Point of X st
( z = (h | (divset ((T . m),j))) . (p2 . j) & Smn . (i,j) = (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z ) )
assume
(
i in Seg (len (T . n)) &
j in Seg (len (T . m)) )
;
ex z being Point of X st
( z = (h | (divset ((T . m),j))) . (p2 . j) & Smn . (i,j) = (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z )
then
ex
i1,
j1 being
Nat ex
z being
Point of
X st
(
i = i1 &
j = j1 &
z = (h | (divset ((T . m),j1))) . (p2 . j1) &
Smn . (
i,
j)
= (xvol ((divset ((T . n),i1)) /\ (divset ((T . m),j1)))) * z )
by A57;
hence
ex
z being
Point of
X st
(
z = (h | (divset ((T . m),j))) . (p2 . j) &
Smn . (
i,
j)
= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z )
;
verum
end; defpred S6[
Nat,
object ]
means ex
s being
FinSequence of
X 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) ) );
A59:
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 A65:
(
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(A59);
for
j being
Nat st
j in dom Zq holds
Zq . j in the
carrier of
X
then reconsider Zq =
Zq as
FinSequence of
X by FINSEQ_2:12;
A66:
len Zq = len (T . m)
by FINSEQ_1:def 3, A65;
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 A67:
( 1
<= k &
k <= len Zq )
;
Zq . k = (S . m) . k
then consider s being
FinSequence of
X such that A68:
(
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 A65, FINSEQ_3:25;
A69:
k in Seg (len (T . m))
by A67, A66;
A70:
k in dom (T . m)
by A67, A66, FINSEQ_3:25;
then consider z being
Point of
X such that A71:
(
z = (h | (divset ((T . m),k))) . (p2 . k) &
(S . m) . k = (vol (divset ((T . m),k))) * z )
by A21;
defpred S7[
Nat,
set ]
means $2
= xvol ((divset ((T . n),$1)) /\ (divset ((T . m),k)));
A72:
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 A73:
(
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(A72);
A74:
(
dom vtntm = dom s &
len vtntm = len s )
by A73, FINSEQ_1:def 3;
A75:
for
j being
Nat st
j in dom vtntm holds
vtntm . j = xvol ((divset ((T . m),k)) /\ (divset ((T . n),j)))
by A73;
len s = len (T . n)
by A68, FINSEQ_1:def 3;
then A76:
Sum vtntm = vol (divset ((T . m),k))
by Th8, A75, A74, A70, 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 A77:
j in dom s
;
ex x being Real st
( x = vtntm . j & s . j = x * z )
then A78:
ex
w being
Point of
X st
(
w = (h | (divset ((T . m),k))) . (p2 . k) &
Smn . (
j,
k)
= (xvol ((divset ((T . n),j)) /\ (divset ((T . m),k)))) * w )
by A58, A69, A68;
take
vtntm . j
;
( vtntm . j = vtntm . j & s . j = (vtntm . j) * z )
s . j = (xvol ((divset ((T . n),j)) /\ (divset ((T . m),k)))) * z
by A71, A78, A77, A68;
hence
(
vtntm . j = vtntm . j &
s . j = (vtntm . j) * z )
by A77, A73, A74;
verum
end;
hence
Zq . k = (S . m) . k
by A71, A68, A76, Th7, A74;
verum
end; then
Zq = S . m
by INTEGR18:def 1, A66;
then A79:
(Sum (S . n)) - (Sum (S . m)) = (Sum Xq) - (Sum Zq)
by Th4, A33, A53, A46;
set XZq =
Xq - Zq;
A80:
dom (Xq - Zq) = (dom Xq) /\ (dom Zq)
by VFUNCT_1:def 2;
then reconsider XZq =
Xq - Zq as
FinSequence by A53, A65, FINSEQ_1:def 2;
then reconsider XZq =
Xq - Zq as
FinSequence of
X by FINSEQ_2:12;
len Xq = len Zq
by FINSEQ_3:29, A53, A65;
then A81:
(Sum (S . n)) - (Sum (S . m)) = Sum XZq
by A79, INTEGR18:2;
A82:
for
i,
j being
Nat for
Snmij,
Smnij being
Point of
X st
i in Seg (len (T . n)) &
j in Seg (len (T . m)) &
Snmij = Snm . (
i,
j) &
Smnij = Smn . (
i,
j) holds
||.(Snmij - Smnij).|| <= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * ((p / 2) / ((vol A) + 1))
proof
let i,
j be
Nat;
for Snmij, Smnij being Point of X st i in Seg (len (T . n)) & j in Seg (len (T . m)) & Snmij = Snm . (i,j) & Smnij = Smn . (i,j) holds
||.(Snmij - Smnij).|| <= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * ((p / 2) / ((vol A) + 1))let Snmij,
Smnij be
Point of
X;
( i in Seg (len (T . n)) & j in Seg (len (T . m)) & Snmij = Snm . (i,j) & Smnij = Smn . (i,j) implies ||.(Snmij - Smnij).|| <= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * ((p / 2) / ((vol A) + 1)) )
assume A83:
(
i in Seg (len (T . n)) &
j in Seg (len (T . m)) &
Snmij = Snm . (
i,
j) &
Smnij = Smn . (
i,
j) )
;
||.(Snmij - Smnij).|| <= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * ((p / 2) / ((vol A) + 1))
then consider z1 being
Point of
X such that A84:
(
z1 = (h | (divset ((T . n),i))) . (p1 . i) &
Snm . (
i,
j)
= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z1 )
by A26;
consider z2 being
Point of
X such that A85:
(
z2 = (h | (divset ((T . m),j))) . (p2 . j) &
Smn . (
i,
j)
= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z2 )
by A58, A83;
A86:
(
i in dom (T . n) &
j in dom (T . m) )
by A83, FINSEQ_1:def 3;
then A87:
(
p1 . i in dom (h | (divset ((T . n),i))) &
p2 . j in dom (h | (divset ((T . m),j))) )
by A20, A21;
then
(
p1 . i in (dom h) /\ (divset ((T . n),i)) &
p2 . j in (dom h) /\ (divset ((T . m),j)) )
by RELAT_1:61;
then A88:
(
p1 . i in dom h &
p1 . i in divset (
(T . n),
i) &
p2 . j in dom h &
p2 . j in divset (
(T . m),
j) )
by XBOOLE_0:def 4;
(
z1 = h . (p1 . i) &
z2 = h . (p2 . j) )
by A84, A85, A87, FUNCT_1:47;
then A89:
(
z1 = h /. (p1 . i) &
z2 = h /. (p2 . j) )
by A88, PARTFUN1:def 6;
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).|| <= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * ((p / 2) / ((vol A) + 1))then consider t being
object such that A92:
t in (divset ((T . n),i)) /\ (divset ((T . m),j))
by XBOOLE_0:def 1;
reconsider t =
t as
Real by A92;
A93:
dom h = A
by FUNCT_2:def 1;
A94:
divset (
(T . m),
j)
c= A
by A86, INTEGRA1:8;
A95:
(
t in divset (
(T . n),
i) &
t in divset (
(T . m),
j) )
by A92, XBOOLE_0:def 4;
then
(
|.((p1 . i) - t).| < sk &
|.(t - (p2 . j)).| < sk )
by A86, A88, Th12, A18;
then A96:
(
||.((h /. (p1 . i)) - (h /. t)).|| < ((p / 2) / ((vol A) + 1)) / 2 &
||.((h /. t) - (h /. (p2 . j))).|| < ((p / 2) / ((vol A) + 1)) / 2 )
by A94, A95, A93, A88, A15;
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 = (xvol DMN) * (((h /. (p1 . i)) - (0. X)) - (h /. (p2 . j)))
by A83, A84, A89, A85, RLVECT_1:34;
then
Snmij - Smnij = (xvol DMN) * (((h /. (p1 . i)) - ((h /. t) - (h /. t))) - (h /. (p2 . j)))
by RLVECT_1:15;
then
Snmij - Smnij = (xvol DMN) * ((((h /. (p1 . i)) - (h /. t)) + (h /. t)) - (h /. (p2 . j)))
by RLVECT_1:29;
then
Snmij - Smnij = (xvol DMN) * (((h /. (p1 . i)) - (h /. t)) + ((h /. t) - (h /. (p2 . j))))
by RLVECT_1:28;
then
Snmij - Smnij = ((xvol DMN) * ((h /. (p1 . i)) - (h /. t))) + ((xvol DMN) * ((h /. t) - (h /. (p2 . j))))
by RLVECT_1:def 5;
then A97:
||.(Snmij - Smnij).|| <= ||.((xvol DMN) * ((h /. (p1 . i)) - (h /. t))).|| + ||.((xvol DMN) * ((h /. t) - (h /. (p2 . j)))).||
by NORMSP_1:def 1;
(
||.((xvol DMN) * ((h /. (p1 . i)) - (h /. t))).|| = |.(xvol DMN).| * ||.((h /. (p1 . i)) - (h /. t)).|| &
||.((xvol DMN) * ((h /. t) - (h /. (p2 . j)))).|| = |.(xvol DMN).| * ||.((h /. t) - (h /. (p2 . j))).|| )
by NORMSP_1:def 1;
then A98:
(
||.((xvol DMN) * ((h /. (p1 . i)) - (h /. t))).|| = (xvol DMN) * ||.((h /. (p1 . i)) - (h /. t)).|| &
||.((xvol DMN) * ((h /. t) - (h /. (p2 . j)))).|| = (xvol DMN) * ||.((h /. t) - (h /. (p2 . j))).|| )
by Th5, ABSVALUE:def 1;
0 <= xvol DMN
by Th5;
then
(
||.((xvol DMN) * ((h /. (p1 . i)) - (h /. t))).|| <= (xvol DMN) * (((p / 2) / ((vol A) + 1)) / 2) &
||.((xvol DMN) * ((h /. t) - (h /. (p2 . j)))).|| <= (xvol DMN) * (((p / 2) / ((vol A) + 1)) / 2) )
by A98, A96, XREAL_1:64;
then
||.((xvol DMN) * ((h /. (p1 . i)) - (h /. t))).|| + ||.((xvol DMN) * ((h /. t) - (h /. (p2 . j)))).|| <= ((xvol DMN) * (((p / 2) / ((vol A) + 1)) / 2)) + ((xvol DMN) * (((p / 2) / ((vol A) + 1)) / 2))
by XREAL_1:7;
hence
||.(Snmij - Smnij).|| <= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * ((p / 2) / ((vol A) + 1))
by A97, XXREAL_0:2;
verum end; end;
end; A99:
for
j being
Nat st
j in dom XZq holds
||.(XZq /. j).|| <= (vol (divset ((T . m),j))) * ((p / 2) / ((vol A) + 1))
proof
let j be
Nat;
( j in dom XZq implies ||.(XZq /. j).|| <= (vol (divset ((T . m),j))) * ((p / 2) / ((vol A) + 1)) )
assume A100:
j in dom XZq
;
||.(XZq /. j).|| <= (vol (divset ((T . m),j))) * ((p / 2) / ((vol A) + 1))
then A101:
XZq /. j = (Xq /. j) - (Zq /. j)
by VFUNCT_1:def 2;
A102:
(
Xq /. j = Xq . j &
Zq /. j = Zq . j )
by A100, A65, A53, A80, PARTFUN1:def 6;
A103:
dom XZq = (dom Xq) /\ (dom Zq)
by VFUNCT_1:def 2;
consider Xsq being
FinSequence of
X such that A104:
(
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 A100, A53, A65, A80;
consider Zsq being
FinSequence of
X such that A105:
(
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 A100, A65, A53, A80;
set XZsq =
Xsq - Zsq;
A106:
dom (Xsq - Zsq) = (dom Xsq) /\ (dom Zsq)
by VFUNCT_1:def 2;
then reconsider XZsq =
Xsq - Zsq as
FinSequence by A104, A105, FINSEQ_1:def 2;
then reconsider XZsq =
XZsq as
FinSequence of
X by FINSEQ_2:12;
defpred S7[
Nat,
set ]
means $2
= xvol ((divset ((T . n),$1)) /\ (divset ((T . m),j)));
A107:
for
i being
Nat st
i in Seg (len XZsq) holds
ex
x being
Element of
REAL st
S7[
i,
x]
consider vtntm being
FinSequence of
REAL such that A108:
(
dom vtntm = Seg (len XZsq) & ( for
i being
Nat st
i in Seg (len XZsq) holds
S7[
i,
vtntm . i] ) )
from FINSEQ_1:sch 5(A107);
A109:
for
i being
Nat st
i in dom vtntm holds
vtntm . i = xvol ((divset ((T . m),j)) /\ (divset ((T . n),i)))
by A108;
A110:
len vtntm = len XZsq
by A108, FINSEQ_1:def 3;
A111:
len XZsq = len (T . n)
by A104, A105, A106, FINSEQ_1:def 3;
reconsider pvtntm =
((p / 2) / ((vol A) + 1)) * vtntm as
FinSequence of
REAL ;
j in dom (T . m)
by A100, A103, A53, A65, FINSEQ_1:def 3;
then
divset (
(T . m),
j)
c= A
by INTEGRA1:8;
then
Sum vtntm = vol (divset ((T . m),j))
by Th8, A109, A110, A104, A105, A106, FINSEQ_1:def 3;
then A112:
Sum pvtntm = ((p / 2) / ((vol A) + 1)) * (vol (divset ((T . m),j)))
by RVSUM_1:87;
dom pvtntm = dom vtntm
by VALUED_1:def 5;
then
dom pvtntm = Seg (len (T . n))
by A104, A105, A106, A108, FINSEQ_1:def 3;
then A113:
len pvtntm = len (T . n)
by FINSEQ_1:def 3;
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 A114:
i in dom XZsq
;
||.(XZsq /. i).|| <= pvtntm . i
then A115:
XZsq /. i = (Xsq /. i) - (Zsq /. i)
by VFUNCT_1:def 2;
(
Xsq /. i = Xsq . i &
Zsq /. i = Zsq . i )
by PARTFUN1:def 6, A114, A105, A106, A104;
then A116:
(
Xsq /. i = Snm . (
i,
j) &
Zsq /. i = Smn . (
i,
j) )
by A114, A104, A106, A105;
dom vtntm = dom XZsq
by A108, FINSEQ_1:def 3;
then
((p / 2) / ((vol A) + 1)) * (vtntm . i) = ((p / 2) / ((vol A) + 1)) * (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j))))
by A108, A114;
then
(((p / 2) / ((vol A) + 1)) (#) vtntm) . i = ((p / 2) / ((vol A) + 1)) * (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j))))
by VALUED_1:6;
hence
||.(XZsq /. i).|| <= pvtntm . i
by A115, A116, A82, A114, A104, A105, A106, A100, A103, A53, A65;
verum
end;
then A117:
||.(Sum XZsq).|| <= (vol (divset ((T . m),j))) * ((p / 2) / ((vol A) + 1))
by A112, Th10, A111, A113;
len Xsq = len Zsq
by FINSEQ_3:29, A104, A105;
hence
||.(XZq /. j).|| <= (vol (divset ((T . m),j))) * ((p / 2) / ((vol A) + 1))
by A101, A102, A104, A105, A117, INTEGR18:2;
verum
end; defpred S7[
Nat,
set ]
means $2
= vol (divset ((T . m),$1));
A118:
for
i being
Nat st
i in Seg (len XZq) holds
ex
x being
Element of
REAL st
S7[
i,
x]
consider vtm being
FinSequence of
REAL such that A119:
(
dom vtm = Seg (len XZq) & ( for
i being
Nat st
i in Seg (len XZq) holds
S7[
i,
vtm . i] ) )
from FINSEQ_1:sch 5(A118);
A120:
len XZq = len (T . m)
by A53, A65, A80, FINSEQ_1:def 3;
A121:
Seg (len XZq) = dom XZq
by FINSEQ_1:def 3;
A122:
Sum vtm = vol A
by A119, Th6, A120;
reconsider pvtm =
((p / 2) / ((vol A) + 1)) * vtm as
FinSequence of
REAL ;
dom pvtm = dom vtm
by VALUED_1:def 5;
then
dom pvtm = Seg (len (T . m))
by A53, A65, A80, A119, FINSEQ_1:def 3;
then A123:
len pvtm = len (T . m)
by FINSEQ_1:def 3;
A124:
Sum pvtm = ((p / 2) / ((vol A) + 1)) * (vol A)
by RVSUM_1:87, A122;
for
j being
Nat st
j in dom XZq holds
||.(XZq /. j).|| <= pvtm . j
then
||.(Sum XZq).|| <= (vol A) * ((p / 2) / ((vol A) + 1))
by A124, A120, A123, Th10;
hence
||.(((middle_sum (h,S)) . n) - ((middle_sum (h,S)) . m)).|| < p
by A19, A81, XXREAL_0:2, A14;
verum end;
hence
middle_sum (
h,
S) is
convergent
by RSSPACE3:8, LOPBAN_1:def 15;
verum
end;