let A be non empty closed_interval Subset of REAL; for x being Point of (DualSp (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A))) st 0 < vol A holds
ex rho being Function of A,REAL st
( rho is bounded_variation & ( for u being continuous PartFunc of REAL,REAL st dom u = A holds
x . u = integral (u,rho) ) & ||.x.|| = total_vd rho )
let x be Point of (DualSp (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A))); ( 0 < vol A implies ex rho being Function of A,REAL st
( rho is bounded_variation & ( for u being continuous PartFunc of REAL,REAL st dom u = A holds
x . u = integral (u,rho) ) & ||.x.|| = total_vd rho ) )
assume A1:
0 < vol A
; ex rho being Function of A,REAL st
( rho is bounded_variation & ( for u being continuous PartFunc of REAL,REAL st dom u = A holds
x . u = integral (u,rho) ) & ||.x.|| = total_vd rho )
set X = R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A);
set V = R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A);
set AV = the carrier of (ClstoCmp A);
A2:
the carrier of (ClstoCmp A) = A
by Lm1;
R_Algebra_of_ContinuousFunctions (ClstoCmp A) is Subalgebra of R_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)
by C0SP2:9;
then A3:
( the carrier of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) c= the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) & the addF of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) = the addF of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) || the carrier of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) & the Mult of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) = the Mult of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) | [:REAL, the carrier of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)):] )
by C0SP1:def 9;
A4: 0. (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) =
(ClstoCmp A) --> 0
by C0SP2:12
.=
0. (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))
by C0SP1:25
;
B5:
R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A) is SubRealNormSpace of R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)
by A3, A4, DUALSP01:def 16;
reconsider h = x as Lipschitzian linear-Functional of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) by DUALSP01:def 10;
consider f being Lipschitzian linear-Functional of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)), F being Point of (DualSp (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))) such that
A6:
( f = F & f | the carrier of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) = h & ||.F.|| = ||.x.|| )
by B5, DUALSP01:36;
consider a, b being Real such that
A7:
( a <= b & [.a,b.] = A & ClstoCmp A = Closed-Interval-TSpace (a,b) )
by Def7ClstoCmp;
consider m being Function of A,(BoundedFunctions A) such that
A8:
for s being Real st s in [.a,b.] holds
( ( s = a implies m . s = [.a,b.] --> 0 ) & ( s <> a implies m . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) )
by A7, LM83;
the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) = BoundedFunctions A
by Lm1;
then reconsider rho = f * m as Function of A,REAL ;
A9:
for D being Division of A
for K being var_volume of rho,D st a < D . 1 holds
Sum K <= ||.x.||
proof
let D be
Division of
A;
for K being var_volume of rho,D st a < D . 1 holds
Sum K <= ||.x.||let K be
var_volume of
rho,
D;
( a < D . 1 implies Sum K <= ||.x.|| )
assume A10:
a < D . 1
;
Sum K <= ||.x.||
consider s being
FinSequence of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) such that A11:
len s = len D
and A12:
for
i being
Nat st
i in dom s holds
s . i = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i)))
by LM84;
set yD =
Sum s;
Sum s in the
carrier of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))
;
then
Sum s in BoundedFunctions A
by Lm1;
then consider g being
Function of
A,
REAL such that A13:
(
g = Sum s &
g | A is
bounded )
;
A14:
f . (Sum s) = Sum (f * s)
by LM87;
A15:
for
t being
Element of
A holds
|.(g . t).| <= 1
proof
let t be
Element of
A;
|.(g . t).| <= 1
defpred S1[
Nat,
set ]
means ex
sk being
Function of
A,
REAL st
(
sk = s . $1 & $2
= sk . t );
A16:
for
k being
Nat st
k in Seg (len D) holds
ex
x being
Element of
REAL st
S1[
k,
x]
proof
let k be
Nat;
( k in Seg (len D) implies ex x being Element of REAL st S1[k,x] )
assume
k in Seg (len D)
;
ex x being Element of REAL st S1[k,x]
then
k in dom s
by FINSEQ_1:def 3, A11;
then
s . k = (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * ((Dp1 (m,D,(k + 1))) - (Dp1 (m,D,k)))
by A12;
then
s . k in the
carrier of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))
;
then
s . k in BoundedFunctions A
by Lm1;
then consider sk being
Function of
A,
REAL such that A17:
(
sk = s . k &
sk | A is
bounded )
;
take x =
sk . t;
S1[k,x]
thus
S1[
k,
x]
by A17;
verum
end;
consider z being
FinSequence of
REAL such that A18:
(
dom z = Seg (len D) & ( for
k being
Nat st
k in Seg (len D) holds
S1[
k,
z . k] ) )
from FINSEQ_1:sch 5(A16);
A20:
len s = len z
by A11, A18, FINSEQ_1:def 3;
A22:
dom z = dom D
by FINSEQ_1:def 3, A18;
A = [.(lower_bound A),(upper_bound A).]
by INTEGRA1:4;
then
lower_bound A = a
by A7, INTEGRA1:5;
then consider i being
Element of
NAT such that A50:
i in dom D
and A51:
t in divset (
D,
i)
and A52:
(
i = 1 or (
lower_bound (divset (D,i)) < t &
t <= upper_bound (divset (D,i)) ) )
by A10, LM94;
t in [.(lower_bound (divset (D,i))),(upper_bound (divset (D,i))).]
by A51, INTEGRA1:4;
then A53:
(
lower_bound (divset (D,i)) <= t &
t <= upper_bound (divset (D,i)) )
by XXREAL_1:1;
reconsider i =
i as
Nat ;
A54:
i in Seg (len D)
by A50, FINSEQ_1:def 3;
then consider si being
Function of
A,
REAL such that A55:
(
si = s . i &
z . i = si . t )
by A18;
i in Seg (len s)
by A11, A50, FINSEQ_1:def 3;
then B56:
i in dom s
by FINSEQ_1:def 3;
set r =
sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)));
A57:
( 1
<= i &
i <= len D )
by A50, FINSEQ_3:25;
then
i + 0 <= (len D) + 1
by XREAL_1:7;
then A58:
i in Seg ((len D) + 1)
by A57;
b:
( 1
+ 0 <= i + 1 &
i <= len D )
by A54, FINSEQ_1:1, XREAL_1:7;
then
i + 1
<= (len D) + 1
by XREAL_1:7;
then A59:
i + 1
in Seg ((len D) + 1)
by b;
z . i = sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))
proof
set f0 =
[.a,b.] --> 0;
set f1 =
([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0);
set g1 =
[.a,(D . i).] --> 1;
set g2 =
].(D . i),b.] --> 0;
set f2 =
([.a,(D . (i - 1)).] --> 1) +* (].(D . (i - 1)),b.] --> 0);
set h1 =
[.a,(D . (i - 1)).] --> 1;
set h2 =
].(D . (i - 1)),b.] --> 0;
B0:
(
dom ([.a,b.] --> 0) = [.a,b.] &
dom ([.a,(D . i).] --> 1) = [.a,(D . i).] &
dom (].(D . i),b.] --> 0) = ].(D . i),b.] &
dom ([.a,(D . (i - 1)).] --> 1) = [.a,(D . (i - 1)).] &
dom (].(D . (i - 1)),b.] --> 0) = ].(D . (i - 1)),b.] )
by FUNCOP_1:13;
per cases
( i = 1 or i <> 1 )
;
suppose A62:
i = 1
;
z . i = sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))
A = [.(lower_bound A),(upper_bound A).]
by INTEGRA1:4;
then A63:
lower_bound A = a
by A7, INTEGRA1:5;
A64:
a in [.a,b.]
by A7;
A65:
D . i in [.a,b.]
by A7, A50, INTEGRA1:6;
A66:
(
lower_bound (divset (D,i)) = lower_bound A &
upper_bound (divset (D,i)) = D . i )
by A50, A62, INTEGRA1:def 4;
A69:
Dp1 (
m,
D,
(i + 1)) =
m . (D . ((i + 1) - 1))
by A59, defDp1, A62
.=
([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0)
by A8, A65, A10, A62
;
A70:
Dp1 (
m,
D,
i) =
m . (lower_bound A)
by A58, A62, defDp1
.=
[.a,b.] --> 0
by A8, A63, A64
;
A72:
dom ([.a,b.] --> 0) = A
by A7, FUNCOP_1:13;
A73:
(
a <= D . i &
D . i <= b )
by A65, XXREAL_1:1;
A74:
dom (([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0)) =
(dom ([.a,(D . i).] --> 1)) \/ (dom (].(D . i),b.] --> 0))
by FUNCT_4:def 1
.=
A
by A7, B0, A73, XXREAL_1:167
;
rng ([.a,b.] --> 0) c= REAL
;
then reconsider f0 =
[.a,b.] --> 0 as
Function of
A,
REAL by A72, FUNCT_2:2;
rng (([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0)) c= REAL
;
then reconsider f1 =
([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0) as
Function of
A,
REAL by A74, FUNCT_2:2;
A76:
si . t = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f1 . t) - (f0 . t))
proof
reconsider H =
(Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i)) as
Element of
(R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider h =
H as
Function of
A,
REAL by LM88;
si = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i)))
by A55, B56, A12;
then
si = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * H
by Lm1;
then si . t =
(sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * (h . t)
by C0SP1:30
.=
(sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f1 . t) - (f0 . t))
by A2, A69, A70, C0SP1:34
;
hence
si . t = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f1 . t) - (f0 . t))
;
verum
end; A77:
t in [.a,(D . i).]
by A63, A66, INTEGRA1:4, A51;
then A79:
f1 . t =
([.a,(D . i).] --> 1) . t
by FUNCT_4:16, B0, XXREAL_1:90
.=
1
by A77, FUNCOP_1:7
;
f0 . t = 0
by A7, FUNCOP_1:7;
hence
z . i = sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))
by A55, A76, A79;
verum end; suppose A80:
i <> 1
;
z . i = sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))then A82:
D . (i - 1) in [.a,b.]
by A7, A50, INTEGRA1:7;
A81:
D . i in [.a,b.]
by A7, A50, INTEGRA1:6;
A83:
(
lower_bound (divset (D,i)) = D . (i - 1) &
upper_bound (divset (D,i)) = D . i )
by A50, A80, INTEGRA1:def 4;
i - 1
in dom D
by A50, A80, INTEGRA1:7;
then A86:
D . (i - 1) < D . i
by A50, XREAL_1:146, VALUED_0:def 13;
(
D . (i - 1) = a or
D . (i - 1) in ].a,b.] )
by A80, A7, A50, INTEGRA1:7, XXREAL_1:6;
per cases then
( a = D . (i - 1) or a < D . (i - 1) )
by XXREAL_1:2;
suppose A88:
a = D . (i - 1)
;
z . i = sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))
1
+ 0 < i + 1
by XREAL_1:8, A57;
then A90:
Dp1 (
m,
D,
(i + 1)) =
m . (D . ((i + 1) - 1))
by A59, defDp1
.=
([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0)
by A8, A81, A88, A86
;
A91:
Dp1 (
m,
D,
i) =
m . (D . (i - 1))
by A58, A80, defDp1
.=
[.a,b.] --> 0
by A8, A82, A88
;
A93:
dom ([.a,b.] --> 0) = A
by A7, FUNCOP_1:13;
A94:
(
a <= D . i &
D . i <= b )
by A81, XXREAL_1:1;
A96:
dom (([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0)) =
(dom ([.a,(D . i).] --> 1)) \/ (dom (].(D . i),b.] --> 0))
by FUNCT_4:def 1
.=
A
by A7, B0, A94, XXREAL_1:167
;
rng ([.a,b.] --> 0) c= REAL
;
then reconsider f0 =
[.a,b.] --> 0 as
Function of
A,
REAL by A93, FUNCT_2:2;
rng (([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0)) c= REAL
;
then reconsider f1 =
([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0) as
Function of
A,
REAL by A96, FUNCT_2:2;
A98:
si . t = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f1 . t) - (f0 . t))
proof
reconsider H =
(Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i)) as
Element of
(R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider h =
H as
Function of
A,
REAL by LM88;
si = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i)))
by A55, B56, A12;
then
si = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * H
by Lm1;
then si . t =
(sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * (h . t)
by C0SP1:30
.=
(sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f1 . t) - (f0 . t))
by A2, A90, A91, C0SP1:34
;
hence
si . t = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f1 . t) - (f0 . t))
;
verum
end; A99:
t in [.(D . (i - 1)),(D . i).]
by A83, INTEGRA1:4, A51;
(
a <= D . (i - 1) &
D . (i - 1) <= b )
by A82, XXREAL_1:1;
then B100:
[.(D . (i - 1)),(D . i).] c= [.a,(D . i).]
by XXREAL_1:34;
then A102:
f1 . t =
([.a,(D . i).] --> 1) . t
by A99, FUNCT_4:16, B0, XXREAL_1:90
.=
1
by B100, A99, FUNCOP_1:7
;
f0 . t = 0
by A7, FUNCOP_1:7;
hence
z . i = sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))
by A55, A98, A102;
verum end; suppose A103:
a < D . (i - 1)
;
z . i = sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))
1
+ 0 < i + 1
by XREAL_1:8, A57;
then A105:
Dp1 (
m,
D,
(i + 1)) =
m . (D . ((i + 1) - 1))
by A59, defDp1
.=
([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0)
by A8, A81, A103, A86
;
A106:
Dp1 (
m,
D,
i) =
m . (D . (i - 1))
by A58, A80, defDp1
.=
([.a,(D . (i - 1)).] --> 1) +* (].(D . (i - 1)),b.] --> 0)
by A8, A82, A103
;
A108:
(
a <= D . i &
D . i <= b )
by A81, XXREAL_1:1;
A109:
(
a <= D . (i - 1) &
D . (i - 1) <= b )
by A82, XXREAL_1:1;
A110:
dom (([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0)) =
(dom ([.a,(D . i).] --> 1)) \/ (dom (].(D . i),b.] --> 0))
by FUNCT_4:def 1
.=
A
by A7, B0, A108, XXREAL_1:167
;
A111:
dom (([.a,(D . (i - 1)).] --> 1) +* (].(D . (i - 1)),b.] --> 0)) =
(dom ([.a,(D . (i - 1)).] --> 1)) \/ (dom (].(D . (i - 1)),b.] --> 0))
by FUNCT_4:def 1
.=
A
by A7, B0, A109, XXREAL_1:167
;
rng (([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0)) c= REAL
;
then reconsider f1 =
([.a,(D . i).] --> 1) +* (].(D . i),b.] --> 0) as
Function of
A,
REAL by A110, FUNCT_2:2;
rng (([.a,(D . (i - 1)).] --> 1) +* (].(D . (i - 1)),b.] --> 0)) c= REAL
;
then reconsider f2 =
([.a,(D . (i - 1)).] --> 1) +* (].(D . (i - 1)),b.] --> 0) as
Function of
A,
REAL by A111, FUNCT_2:2;
A112:
(
a <= t &
t <= b )
by XXREAL_1:1, A7;
A113:
si . t = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f1 . t) - (f2 . t))
proof
reconsider H =
(Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i)) as
Element of
(R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider h =
H as
Function of
A,
REAL by LM88;
si = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i)))
by A55, B56, A12;
then
si = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * H
by Lm1;
then si . t =
(sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * (h . t)
by C0SP1:30
.=
(sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f1 . t) - (f2 . t))
by A2, A105, A106, C0SP1:34
;
hence
si . t = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f1 . t) - (f2 . t))
;
verum
end; A114:
t in [.(D . (i - 1)),(D . i).]
by A83, INTEGRA1:4, A51;
B115:
[.(D . (i - 1)),(D . i).] c= [.a,(D . i).]
by A109, XXREAL_1:34;
then A117:
f1 . t =
([.a,(D . i).] --> 1) . t
by A114, FUNCT_4:16, B0, XXREAL_1:90
.=
1
by B115, A114, FUNCOP_1:7
;
(
D . (i - 1) < t &
t <= D . i )
by A50, A80, INTEGRA1:def 4, A52;
then A118:
t in ].(D . (i - 1)),b.]
by A112;
then f2 . t =
(].(D . (i - 1)),b.] --> 0) . t
by B0, FUNCT_4:13
.=
0
by A118, FUNCOP_1:7
;
hence
z . i = sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))
by A55, A113, A117;
verum end; end; end; end;
end;
then A119:
|.(z . i).| <= 1
by LM91;
for
k being
Nat st
k in dom z &
k <> i holds
z . k = 0
proof
let k be
Nat;
( k in dom z & k <> i implies z . k = 0 )
assume that A120:
k in dom z
and A121:
k <> i
;
z . k = 0
consider sk being
Function of
A,
REAL such that A124:
(
sk = s . k &
z . k = sk . t )
by A18, A120;
B125:
k in dom s
by FINSEQ_1:def 3, A11, A18, A120;
then A125:
s . k = (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * ((Dp1 (m,D,(k + 1))) - (Dp1 (m,D,k)))
by A12;
set r =
sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)));
A126:
k in dom D
by A18, A120, FINSEQ_1:def 3;
then A127:
( 1
<= k &
k <= len D )
by FINSEQ_3:25;
then
k + 0 <= (len D) + 1
by XREAL_1:7;
then A128:
k in Seg ((len D) + 1)
by A127;
a:
1
+ 0 <= k + 1
by XREAL_1:7;
k + 1
<= (len D) + 1
by A127, XREAL_1:7;
then A129:
k + 1
in Seg ((len D) + 1)
by a;
set f0 =
[.a,b.] --> 0;
set f1 =
([.a,(D . k).] --> 1) +* (].(D . k),b.] --> 0);
set g1 =
[.a,(D . k).] --> 1;
set g2 =
].(D . k),b.] --> 0;
set f2 =
([.a,(D . (k - 1)).] --> 1) +* (].(D . (k - 1)),b.] --> 0);
set h1 =
[.a,(D . (k - 1)).] --> 1;
set h2 =
].(D . (k - 1)),b.] --> 0;
B10:
(
dom ([.a,b.] --> 0) = [.a,b.] &
dom ([.a,(D . k).] --> 1) = [.a,(D . k).] &
dom (].(D . k),b.] --> 0) = ].(D . k),b.] &
dom ([.a,(D . (k - 1)).] --> 1) = [.a,(D . (k - 1)).] &
dom (].(D . (k - 1)),b.] --> 0) = ].(D . (k - 1)),b.] )
by FUNCOP_1:13;
per cases
( k = 1 or k <> 1 )
;
suppose A130:
k = 1
;
z . k = 0 then A134:
(
lower_bound (divset (D,i)) = D . (i - 1) &
upper_bound (divset (D,i)) = D . i )
by A50, INTEGRA1:def 4, A121;
A136:
i - 1
in dom D
by A50, INTEGRA1:7, A130, A121;
A141:
D . k in [.a,b.]
by A7, A126, INTEGRA1:6;
then A147:
(
a <= D . k &
D . k <= b )
by XXREAL_1:1;
A146:
dom ([.a,b.] --> 0) = A
by A7, FUNCOP_1:13;
A148:
dom (([.a,(D . k).] --> 1) +* (].(D . k),b.] --> 0)) =
(dom ([.a,(D . k).] --> 1)) \/ (dom (].(D . k),b.] --> 0))
by FUNCT_4:def 1
.=
A
by A7, B10, A147, XXREAL_1:167
;
rng ([.a,b.] --> 0) c= REAL
;
then reconsider f0 =
[.a,b.] --> 0 as
Function of
A,
REAL by A146, FUNCT_2:2;
rng (([.a,(D . k).] --> 1) +* (].(D . k),b.] --> 0)) c= REAL
;
then reconsider f1 =
([.a,(D . k).] --> 1) +* (].(D . k),b.] --> 0) as
Function of
A,
REAL by A148, FUNCT_2:2;
A153:
Dp1 (
m,
D,
(k + 1)) =
m . (D . ((k + 1) - 1))
by A129, defDp1, A130
.=
([.a,(D . k).] --> 1) +* (].(D . k),b.] --> 0)
by A8, A141, A10, A130
;
A = [.(lower_bound A),(upper_bound A).]
by INTEGRA1:4;
then A139:
lower_bound A = a
by A7, INTEGRA1:5;
A140:
a in [.a,b.]
by A7;
A144:
Dp1 (
m,
D,
k) =
m . (lower_bound A)
by A128, A130, defDp1
.=
[.a,b.] --> 0
by A8, A139, A140
;
A154:
sk . t = (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * ((f1 . t) - (f0 . t))
proof
reconsider H =
(Dp1 (m,D,(k + 1))) - (Dp1 (m,D,k)) as
Element of
(R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider h =
H as
Function of
A,
REAL by LM88;
sk = (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * ((Dp1 (m,D,(k + 1))) - (Dp1 (m,D,k)))
by A124, B125, A12;
then
sk = (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * H
by Lm1;
then sk . t =
(sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * (h . t)
by C0SP1:30
.=
(sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * ((f1 . t) - (f0 . t))
by A2, A144, A153, C0SP1:34
;
hence
sk . t = (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * ((f1 . t) - (f0 . t))
;
verum
end;
k < i
by A130, A121, A57, XXREAL_0:1;
then
k + 1
<= i
by NAT_1:13;
then A157:
(k + 1) - 1
<= i - 1
by XREAL_1:13;
D . k <= D . (i - 1)
then A158:
D . k < t
by A52, A130, A121, XXREAL_0:2, A134;
(
a <= t &
t <= b )
by XXREAL_1:1, A7;
then A160:
t in ].(D . k),b.]
by A158;
then A162:
f1 . t =
(].(D . k),b.] --> 0) . t
by B10, FUNCT_4:13
.=
0
by A160, FUNCOP_1:7
;
f0 . t = 0
by A7, FUNCOP_1:7;
hence
z . k = 0
by A124, A154, A162;
verum end; suppose A163:
k <> 1
;
z . k = 0 then A165:
D . (k - 1) in [.a,b.]
by A7, A126, INTEGRA1:7;
A164:
D . k in [.a,b.]
by A7, A126, INTEGRA1:6;
A168:
k - 1
in dom D
by A126, A163, INTEGRA1:7;
then A169:
D . (k - 1) < D . k
by A126, XREAL_1:146, VALUED_0:def 13;
1
< k
by A127, A163, XXREAL_0:1;
then
1
+ 1
<= k
by NAT_1:13;
then A171:
2
- 1
<= k - 1
by XREAL_1:13;
1
<= len D
by A127, XXREAL_0:2;
then A172:
1
in dom D
by FINSEQ_3:25;
B173:
D . 1
<= D . (k - 1)
then A173:
a < D . (k - 1)
by A10, XXREAL_0:2;
1
+ 0 < k + 1
by XREAL_1:8, A127;
then A175:
Dp1 (
m,
D,
(k + 1)) =
m . (D . ((k + 1) - 1))
by A129, defDp1
.=
([.a,(D . k).] --> 1) +* (].(D . k),b.] --> 0)
by A8, A164, A173, A169
;
A176:
Dp1 (
m,
D,
k) =
m . (D . (k - 1))
by A128, A163, defDp1
.=
([.a,(D . (k - 1)).] --> 1) +* (].(D . (k - 1)),b.] --> 0)
by A8, A165, B173, A10
;
A178:
(
a <= D . k &
D . k <= b )
by A164, XXREAL_1:1;
A179:
(
a <= D . (k - 1) &
D . (k - 1) <= b )
by A165, XXREAL_1:1;
A180:
dom (([.a,(D . k).] --> 1) +* (].(D . k),b.] --> 0)) =
(dom ([.a,(D . k).] --> 1)) \/ (dom (].(D . k),b.] --> 0))
by FUNCT_4:def 1
.=
A
by A7, B10, A178, XXREAL_1:167
;
A181:
dom (([.a,(D . (k - 1)).] --> 1) +* (].(D . (k - 1)),b.] --> 0)) =
(dom ([.a,(D . (k - 1)).] --> 1)) \/ (dom (].(D . (k - 1)),b.] --> 0))
by FUNCT_4:def 1
.=
A
by A7, B10, A179, XXREAL_1:167
;
rng (([.a,(D . k).] --> 1) +* (].(D . k),b.] --> 0)) c= REAL
;
then reconsider f1 =
([.a,(D . k).] --> 1) +* (].(D . k),b.] --> 0) as
Function of
A,
REAL by A180, FUNCT_2:2;
rng (([.a,(D . (k - 1)).] --> 1) +* (].(D . (k - 1)),b.] --> 0)) c= REAL
;
then reconsider f2 =
([.a,(D . (k - 1)).] --> 1) +* (].(D . (k - 1)),b.] --> 0) as
Function of
A,
REAL by A181, FUNCT_2:2;
A183:
sk . t = (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * ((f1 . t) - (f2 . t))
proof
reconsider H =
(Dp1 (m,D,(k + 1))) - (Dp1 (m,D,k)) as
Element of
(R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider h =
H as
Function of
A,
REAL by LM88;
sk = (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * H
by Lm1, A124, A125;
then sk . t =
(sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * (h . t)
by C0SP1:30
.=
(sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * ((f1 . t) - (f2 . t))
by A2, A175, A176, C0SP1:34
;
hence
sk . t = (sgn ((Dp2 (rho,D,(k + 1))) - (Dp2 (rho,D,k)))) * ((f1 . t) - (f2 . t))
;
verum
end; per cases
( i < k or k < i )
by A121, XXREAL_0:1;
suppose
i < k
;
z . k = 0 then
i + 1
<= k
by NAT_1:13;
then A186:
(i + 1) - 1
<= k - 1
by XREAL_1:13;
A187:
D . i <= D . (k - 1)
A189:
upper_bound (divset (D,i)) <= D . (k - 1)
A191:
(
a <= t &
t <= D . (k - 1) )
by A189, XXREAL_0:2, A53, XXREAL_1:1, A7;
then A192:
t in [.a,(D . (k - 1)).]
;
(
a <= t &
t <= D . k )
by A169, A191, XXREAL_0:2;
then A193:
t in [.a,(D . k).]
;
then A196:
f1 . t =
([.a,(D . k).] --> 1) . t
by FUNCT_4:16, B10, XXREAL_1:90
.=
1
by A193, FUNCOP_1:7
;
f2 . t =
([.a,(D . (k - 1)).] --> 1) . t
by B10, A192, FUNCT_4:16, XXREAL_1:90
.=
1
by A192, FUNCOP_1:7
;
hence
z . k = 0
by A124, A183, A196;
verum end; suppose A198:
k < i
;
z . k = 0 then
k + 1
<= i
by NAT_1:13;
then A201:
(k + 1) - 1
<= i - 1
by XREAL_1:13;
A202:
i - 1
in dom D
by A50, A198, A127, INTEGRA1:7;
A203:
(
lower_bound (divset (D,i)) = D . (i - 1) &
upper_bound (divset (D,i)) = D . i )
by A50, A198, A127, INTEGRA1:def 4;
D . k <= D . (i - 1)
then A206:
D . k < t
by A198, A52, A18, A120, FINSEQ_1:1, XXREAL_0:2, A203;
then A207:
D . (k - 1) < t
by A169, XXREAL_0:2;
A208:
(
a <= t &
t <= b )
by XXREAL_1:1, A7;
then A209:
t in ].(D . k),b.]
by A206;
then A211:
f1 . t =
(].(D . k),b.] --> 0) . t
by B10, FUNCT_4:13
.=
0
by A209, FUNCOP_1:7
;
A210:
t in ].(D . (k - 1)),b.]
by A207, A208;
then f2 . t =
(].(D . (k - 1)),b.] --> 0) . t
by B10, FUNCT_4:13
.=
0
by A210, FUNCOP_1:7
;
hence
z . k = 0
by A124, A183, A211;
verum end; end; end; end;
end;
then
|.(Sum z).| <= 1
by A22, A50, A119, INTEGR23:6;
hence
|.(g . t).| <= 1
by A13, A20, LM89, A18;
verum
end;
then
upper_bound (PreNorms g) <= 1
by SEQ_4:45;
then
(BoundedFunctionsNorm A) . g <= 1
by A13, C0SP1:20;
then A214:
||.(Sum s).|| <= 1
by A13, Lm1;
A215:
(
len K = len D & ( for
i being
Nat st
i in dom D holds
K . i = |.(vol ((divset (D,i)),rho)).| ) )
by INTEGR22:def 2;
dom f = the
carrier of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))
by FUNCT_2:def 1;
then
rng s c= dom f
;
then A216:
dom (f * s) =
dom s
by RELAT_1:27
.=
Seg (len s)
by FINSEQ_1:def 3
.=
dom K
by A11, A215, FINSEQ_1:def 3
;
A217:
for
i being
Nat st
i in dom D holds
(f * s) . i = |.(vol ((divset (D,i)),rho)).|
proof
let i be
Nat;
( i in dom D implies (f * s) . i = |.(vol ((divset (D,i)),rho)).| )
assume A218:
i in dom D
;
(f * s) . i = |.(vol ((divset (D,i)),rho)).|
then A220:
( 1
<= i &
i <= len D )
by FINSEQ_3:25;
then
i + 0 <= (len D) + 1
by XREAL_1:7;
then A221:
i in Seg ((len D) + 1)
by A220;
b:
1
+ 0 <= i + 1
by XREAL_1:7;
i + 1
<= (len D) + 1
by A220, XREAL_1:7;
then A222:
i + 1
in Seg ((len D) + 1)
by b;
i in Seg (len s)
by A11, A218, FINSEQ_1:def 3;
then A223:
i in dom s
by FINSEQ_1:def 3;
set r =
sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)));
A = [.(lower_bound A),(upper_bound A).]
by INTEGRA1:4;
then A224:
lower_bound A = a
by A7, INTEGRA1:5;
D . i in A
by A218, INTEGRA1:6;
then A225:
D . i in dom m
by FUNCT_2:def 1;
lower_bound A in A
by A7, A224;
then A226:
lower_bound A in dom m
by FUNCT_2:def 1;
per cases
( i = 1 or i <> 1 )
;
suppose A227:
i = 1
;
(f * s) . i = |.(vol ((divset (D,i)),rho)).|then A228:
(
lower_bound (divset (D,i)) = lower_bound A &
upper_bound (divset (D,i)) = D . i )
by A218, INTEGRA1:def 4;
A229:
Dp1 (
m,
D,
(i + 1)) =
m . (D . ((i + 1) - 1))
by A222, defDp1, A227
.=
m . (D . i)
;
A231:
(f * s) . i =
f . (s . i)
by A223, FUNCT_1:13
.=
f . ((sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i))))
by A12, A223
.=
(sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * (f . ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i))))
by HAHNBAN:def 3
.=
(sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f . (Dp1 (m,D,(i + 1)))) - (f . (Dp1 (m,D,i))))
by HAHNBAN:19
.=
(sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f . (m . (D . i))) - (f . (m . (lower_bound A))))
by A229, A221, A227, defDp1
.=
(sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * (((f * m) . (D . i)) - (f . (m . (lower_bound A))))
by A225, FUNCT_1:13
.=
(sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((rho . (upper_bound (divset (D,i)))) - (rho . (lower_bound (divset (D,i)))))
by A228, A226, FUNCT_1:13
.=
(sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * (vol ((divset (D,i)),rho))
by INTEGR22:def 1
;
A232:
Dp2 (
rho,
D,
(i + 1)) =
rho . (D . ((i + 1) - 1))
by defDp2, A227
.=
rho . (D . i)
;
sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i))) =
sgn ((rho . (upper_bound (divset (D,i)))) - (rho . (lower_bound (divset (D,i)))))
by A228, A232, A227, defDp2
.=
sgn (vol ((divset (D,i)),rho))
by INTEGR22:def 1
;
hence
(f * s) . i = |.(vol ((divset (D,i)),rho)).|
by A231, LM86;
verum end; suppose A234:
i <> 1
;
(f * s) . i = |.(vol ((divset (D,i)),rho)).|
D . i in A
by A218, INTEGRA1:6;
then A235:
D . i in dom m
by FUNCT_2:def 1;
D . (i - 1) in A
by A218, A234, INTEGRA1:7;
then A236:
D . (i - 1) in dom m
by FUNCT_2:def 1;
A237:
(
lower_bound (divset (D,i)) = D . (i - 1) &
upper_bound (divset (D,i)) = D . i )
by A218, A234, INTEGRA1:def 4;
A238:
1
+ 0 < i + 1
by XREAL_1:8, A220;
then A239:
Dp1 (
m,
D,
(i + 1)) =
m . (D . ((i + 1) - 1))
by A222, defDp1
.=
m . (D . i)
;
A241:
(f * s) . i =
f . (s . i)
by A223, FUNCT_1:13
.=
f . ((sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i))))
by A12, A223
.=
(sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * (f . ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i))))
by HAHNBAN:def 3
.=
(sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f . (Dp1 (m,D,(i + 1)))) - (f . (Dp1 (m,D,i))))
by HAHNBAN:19
.=
(sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((f . (m . (D . i))) - (f . (m . (D . (i - 1)))))
by A239, A221, A234, defDp1
.=
(sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * (((f * m) . (D . i)) - (f . (m . (D . (i - 1)))))
by A235, FUNCT_1:13
.=
(sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((rho . (upper_bound (divset (D,i)))) - (rho . (lower_bound (divset (D,i)))))
by A237, A236, FUNCT_1:13
.=
(sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * (vol ((divset (D,i)),rho))
by INTEGR22:def 1
;
A242:
Dp2 (
rho,
D,
(i + 1)) =
rho . (D . ((i + 1) - 1))
by A238, defDp2
.=
rho . (D . i)
;
sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i))) =
sgn ((rho . (upper_bound (divset (D,i)))) - (rho . (lower_bound (divset (D,i)))))
by A237, A242, A234, defDp2
.=
sgn (vol ((divset (D,i)),rho))
by INTEGR22:def 1
;
hence
(f * s) . i = |.(vol ((divset (D,i)),rho)).|
by A241, LM86;
verum end; end;
end;
for
i being
Nat st
i in dom K holds
(f * s) . i = K . i
then A245:
f . (Sum s) = Sum K
by A14, A216, FINSEQ_1:13;
A246:
f . (Sum s) <= |.(f . (Sum s)).|
by ABSVALUE:4;
A247:
|.(f . (Sum s)).| <= ||.F.|| * ||.(Sum s).||
by A6, DUALSP01:26;
||.F.|| * ||.(Sum s).|| <= ||.F.|| * 1
by A214, XREAL_1:64;
then
|.(f . (Sum s)).| <= ||.F.||
by A247, XXREAL_0:2;
hence
Sum K <= ||.x.||
by A6, A245, A246, XXREAL_0:2;
verum
end;
reconsider d = ||.x.|| + 1 as Real ;
A = [.(lower_bound A),(upper_bound A).]
by INTEGRA1:4;
then A249:
lower_bound A = a
by A7, INTEGRA1:5;
then
for D being Division of A
for K being var_volume of rho,D holds Sum K <= ||.x.||
by A1, A9, LM95;
then B250:
for t being Division of A
for F0 being var_volume of rho,t holds Sum F0 <= d
by XREAL_1:39;
then A251:
rho is bounded_variation
;
then consider VD being non empty Subset of REAL such that
VD is bounded_above
and
A253:
VD = { r where r is Real : ex t being Division of A ex F0 being var_volume of rho,t st r = Sum F0 }
and
A254:
total_vd rho = upper_bound VD
by INTEGR22:def 4;
then A258:
total_vd rho <= ||.x.||
by A254, SEQ_4:45;
A259:
for u being continuous PartFunc of REAL,REAL st dom u = A holds
x . u = integral (u,rho)
proof
let u be
continuous PartFunc of
REAL,
REAL;
( dom u = A implies x . u = integral (u,rho) )
assume A260:
dom u = A
;
x . u = integral (u,rho)
then A261:
for
r being
Real st
0 < r holds
ex
s being
Real st
(
0 < s & ( for
x1,
x2 being
Real st
x1 in dom (u | A) &
x2 in dom (u | A) &
|.(x1 - x2).| < s holds
|.(((u | A) . x1) - ((u | A) . x2)).| < r ) )
by FCONT_2:def 1, FCONT_2:11;
B262:
u is_RiemannStieltjes_integrable_with rho
by A251, A260, INTEGR23:21;
consider T being
DivSequence of
A such that A263:
(
delta T is
convergent &
lim (delta T) = 0 & ( for
n being
Element of
NAT ex
Tn being
Division of
A st
(
Tn divide_into_equal n + 1 &
T . n = Tn ) ) )
by A1, INTEGRA6:16;
A264:
for
n being
Nat holds
a < (T . n) . 1
set S = the
middle_volume_Sequence of
rho,
u,
T;
A269:
u is
Point of
(R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A))
by A260, Th80;
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) &
( the middle_volume_Sequence of rho,u,T . $1) . i = z * (vol ((divset ((T . $1),i)),rho)) ) ) ) );
A270:
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 &
( the middle_volume_Sequence of rho,u,T . k) . $1
= c * (vol ((divset ((T . k),$1)),rho)) ) );
A271:
Seg (len (T . k)) = dom (T . k)
by FINSEQ_1:def 3;
A272:
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 A273:
(
c in rng (u | (divset ((T . k),i))) &
( the middle_volume_Sequence of rho,u,T . k) . i = c * (vol ((divset ((T . k),i)),rho)) )
by A251, A260, INTEGR22:def 5;
consider x being
object such that A274:
(
x in dom (u | (divset ((T . k),i))) &
c = (u | (divset ((T . k),i))) . x )
by A273, FUNCT_1:def 3;
reconsider x =
x as
Element of
REAL by A274;
take
x
;
S2[i,x]
thus
S2[
i,
x]
by A273, A274;
verum
end;
consider p being
FinSequence of
REAL such that A275:
(
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(A272);
take
p
;
( p is Element of REAL * & S1[k,p] )
len p = len (T . k)
by A275, FINSEQ_1:def 3;
hence
(
p is
Element of
REAL * &
S1[
k,
p] )
by A271, A275, FINSEQ_1:def 11;
verum
end;
consider F being
sequence of
(REAL *) such that A276:
for
x being
Element of
NAT holds
S1[
x,
F . x]
from FUNCT_2:sch 3(A270);
defpred S2[
Element of
NAT ,
object ]
means ex
q being
FinSequence of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st
(
len q = len (T . $1) & $2
= Sum q & ( for
i being
Nat st
i in dom (T . $1) holds
ex
r being
Real st
(
(F . $1) . i in dom (u | (divset ((T . $1),i))) &
r = (u | (divset ((T . $1),i))) . ((F . $1) . i) &
q . i = r * ((Dp1 (m,(T . $1),(i + 1))) - (Dp1 (m,(T . $1),i))) ) ) );
A277:
for
k being
Element of
NAT ex
x being
Element of the
carrier of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st
S2[
k,
x]
proof
let k be
Element of
NAT ;
ex x being Element of the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st S2[k,x]
defpred S3[
Nat,
object ]
means ex
r being
Real st
(
(F . k) . $1
in dom (u | (divset ((T . k),$1))) &
r = (u | (divset ((T . k),$1))) . ((F . k) . $1) & $2
= r * ((Dp1 (m,(T . k),($1 + 1))) - (Dp1 (m,(T . k),$1))) );
A278:
for
i being
Nat st
i in Seg (len (T . k)) holds
ex
y being
Element of the
carrier of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st
S3[
i,
y]
proof
let i be
Nat;
( i in Seg (len (T . k)) implies ex y being Element of the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st S3[i,y] )
assume
i in Seg (len (T . k))
;
ex y being Element of the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st S3[i,y]
then A279:
i in dom (T . k)
by FINSEQ_1:def 3;
consider p being
FinSequence of
REAL such that A280:
(
p = F . k &
len p = len (T . k) & ( for
i being
Nat st
i in dom (T . k) holds
(
p . i in dom (u | (divset ((T . k),i))) & ex
z being
Real st
(
z = (u | (divset ((T . k),i))) . (p . i) &
( the middle_volume_Sequence of rho,u,T . k) . i = z * (vol ((divset ((T . k),i)),rho)) ) ) ) )
by A276;
p . i in dom (u | (divset ((T . k),i)))
by A279, A280;
then
(u | (divset ((T . k),i))) . (p . i) in rng (u | (divset ((T . k),i)))
by FUNCT_1:3;
then reconsider r =
(u | (divset ((T . k),i))) . (p . i) as
Element of
REAL ;
r * ((Dp1 (m,(T . k),(i + 1))) - (Dp1 (m,(T . k),i))) is
Element of the
carrier of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))
;
hence
ex
y being
Element of the
carrier of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st
S3[
i,
y]
by A280, A279;
verum
end;
consider q being
FinSequence of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) such that A282:
(
dom q = Seg (len (T . k)) & ( for
i being
Nat st
i in Seg (len (T . k)) holds
S3[
i,
q . i] ) )
from FINSEQ_1:sch 5(A278);
take x =
Sum q;
S2[k,x]
A283:
dom (T . k) = Seg (len (T . k))
by FINSEQ_1:def 3;
len q = len (T . k)
by A282, FINSEQ_1:def 3;
hence
S2[
k,
x]
by A282, A283;
verum
end;
consider xD being
sequence of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) such that A284:
for
z being
Element of
NAT holds
S2[
z,
xD . z]
from FUNCT_2:sch 3(A277);
B314:
for
n being
Element of
NAT holds
(f * xD) . n = (middle_sum the middle_volume_Sequence of rho,u,T) . n
proof
let n be
Element of
NAT ;
(f * xD) . n = (middle_sum the middle_volume_Sequence of rho,u,T) . n
consider p1 being
FinSequence of
REAL such that A285:
(
p1 = F . 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) &
( the middle_volume_Sequence of rho,u,T . n) . i = z * (vol ((divset ((T . n),i)),rho)) ) ) ) )
by A276;
consider q1 being
FinSequence of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) such that A286:
(
len q1 = len (T . n) &
xD . n = Sum q1 & ( for
i being
Nat st
i in dom (T . n) holds
ex
r being
Real st
(
(F . n) . i in dom (u | (divset ((T . n),i))) &
r = (u | (divset ((T . n),i))) . ((F . n) . i) &
q1 . i = r * ((Dp1 (m,(T . n),(i + 1))) - (Dp1 (m,(T . n),i))) ) ) )
by A284;
A287:
(middle_sum the middle_volume_Sequence of rho,u,T) . n = Sum ( the middle_volume_Sequence of rho,u,T . n)
by INTEGR22:def 7;
dom xD = NAT
by FUNCT_2:def 1;
then A288:
(f * xD) . n =
f . (Sum q1)
by A286, FUNCT_1:13
.=
Sum (f * q1)
by LM87
;
dom f = the
carrier of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))
by FUNCT_2:def 1;
then
rng q1 c= dom f
;
then dom (f * q1) =
dom q1
by RELAT_1:27
.=
Seg (len q1)
by FINSEQ_1:def 3
.=
Seg (len ( the middle_volume_Sequence of rho,u,T . n))
by A251, A260, A286, INTEGR22:def 5
;
then A289:
len (f * q1) = len ( the middle_volume_Sequence of rho,u,T . n)
by FINSEQ_1:def 3;
for
k being
Nat st 1
<= k &
k <= len ( the middle_volume_Sequence of rho,u,T . n) holds
(f * q1) . k = ( the middle_volume_Sequence of rho,u,T . n) . k
proof
let k be
Nat;
( 1 <= k & k <= len ( the middle_volume_Sequence of rho,u,T . n) implies (f * q1) . k = ( the middle_volume_Sequence of rho,u,T . n) . k )
assume A290:
( 1
<= k &
k <= len ( the middle_volume_Sequence of rho,u,T . n) )
;
(f * q1) . k = ( the middle_volume_Sequence of rho,u,T . n) . k
then B291:
k in Seg (len ( the middle_volume_Sequence of rho,u,T . n))
;
then
k in Seg (len (T . n))
by A251, A260, INTEGR22:def 5;
then A292:
k in dom (T . n)
by FINSEQ_1:def 3;
then consider z being
Real such that A293:
(
z = (u | (divset ((T . n),k))) . ((F . n) . k) &
( the middle_volume_Sequence of rho,u,T . n) . k = z * (vol ((divset ((T . n),k)),rho)) )
by A285;
consider r being
Real such that A294:
(
(F . n) . k in dom (u | (divset ((T . n),k))) &
r = (u | (divset ((T . n),k))) . ((F . n) . k) &
q1 . k = r * ((Dp1 (m,(T . n),(k + 1))) - (Dp1 (m,(T . n),k))) )
by A286, A292;
( 1
<= k &
k <= len (T . n) )
by A251, A260, A290, INTEGR22:def 5;
then
k + 0 <= (len (T . n)) + 1
by XREAL_1:7;
then A296:
k in Seg ((len (T . n)) + 1)
by A290;
d:
( 1
+ 0 <= k + 1 &
k <= len (T . n) )
by A251, A260, A290, INTEGR22:def 5, XREAL_1:7;
then
k + 1
<= (len (T . n)) + 1
by XREAL_1:7;
then A297:
k + 1
in Seg ((len (T . n)) + 1)
by d;
k in Seg (len q1)
by A286, B291, A251, A260, INTEGR22:def 5;
then A298:
k in dom q1
by FINSEQ_1:def 3;
per cases
( k = 1 or k <> 1 )
;
suppose A299:
k = 1
;
(f * q1) . k = ( the middle_volume_Sequence of rho,u,T . n) . k
A = [.(lower_bound A),(upper_bound A).]
by INTEGRA1:4;
then
lower_bound A = a
by A7, INTEGRA1:5;
then
lower_bound A in A
by A7;
then A301:
lower_bound A in dom m
by FUNCT_2:def 1;
(T . n) . k in A
by A292, INTEGRA1:6;
then A302:
(T . n) . k in dom m
by FUNCT_2:def 1;
A303:
(
lower_bound (divset ((T . n),k)) = lower_bound A &
upper_bound (divset ((T . n),k)) = (T . n) . k )
by A292, A299, INTEGRA1:def 4;
A304:
Dp1 (
m,
(T . n),
(k + 1)) =
m . ((T . n) . ((k + 1) - 1))
by A297, defDp1, A299
.=
m . ((T . n) . k)
;
A306:
f . ((Dp1 (m,(T . n),(k + 1))) - (Dp1 (m,(T . n),k))) =
(f . (Dp1 (m,(T . n),(k + 1)))) - (f . (Dp1 (m,(T . n),k)))
by HAHNBAN:19
.=
(f . (m . ((T . n) . k))) - (f . (m . (lower_bound A)))
by A304, A296, A299, defDp1
.=
((f * m) . ((T . n) . k)) - (f . (m . (lower_bound A)))
by A302, FUNCT_1:13
.=
(rho . (upper_bound (divset ((T . n),k)))) - (rho . (lower_bound (divset ((T . n),k))))
by A303, A301, FUNCT_1:13
.=
vol (
(divset ((T . n),k)),
rho)
by INTEGR22:def 1
;
thus (f * q1) . k =
f . (r * ((Dp1 (m,(T . n),(k + 1))) - (Dp1 (m,(T . n),k))))
by A294, A298, FUNCT_1:13
.=
( the middle_volume_Sequence of rho,u,T . n) . k
by A293, A294, A306, HAHNBAN:def 3
;
verum end; suppose A307:
k <> 1
;
(f * q1) . k = ( the middle_volume_Sequence of rho,u,T . n) . k
(T . n) . k in A
by A292, INTEGRA1:6;
then A308:
(T . n) . k in dom m
by FUNCT_2:def 1;
(T . n) . (k - 1) in A
by A292, A307, INTEGRA1:7;
then A309:
(T . n) . (k - 1) in dom m
by FUNCT_2:def 1;
A310:
(
lower_bound (divset ((T . n),k)) = (T . n) . (k - 1) &
upper_bound (divset ((T . n),k)) = (T . n) . k )
by A292, A307, INTEGRA1:def 4;
1
+ 0 < k + 1
by XREAL_1:8, A290;
then A311:
Dp1 (
m,
(T . n),
(k + 1)) =
m . ((T . n) . ((k + 1) - 1))
by A297, defDp1
.=
m . ((T . n) . k)
;
A313:
f . ((Dp1 (m,(T . n),(k + 1))) - (Dp1 (m,(T . n),k))) =
(f . (Dp1 (m,(T . n),(k + 1)))) - (f . (Dp1 (m,(T . n),k)))
by HAHNBAN:19
.=
(f . (m . ((T . n) . k))) - (f . (m . ((T . n) . (k - 1))))
by A311, A296, A307, defDp1
.=
((f * m) . ((T . n) . k)) - (f . (m . ((T . n) . (k - 1))))
by A308, FUNCT_1:13
.=
(rho . (upper_bound (divset ((T . n),k)))) - (rho . (lower_bound (divset ((T . n),k))))
by A310, A309, FUNCT_1:13
.=
vol (
(divset ((T . n),k)),
rho)
by INTEGR22:def 1
;
thus (f * q1) . k =
f . (r * ((Dp1 (m,(T . n),(k + 1))) - (Dp1 (m,(T . n),k))))
by A294, A298, FUNCT_1:13
.=
( the middle_volume_Sequence of rho,u,T . n) . k
by A293, A294, A313, HAHNBAN:def 3
;
verum end; end;
end;
hence
(f * xD) . n = (middle_sum the middle_volume_Sequence of rho,u,T) . n
by A287, A288, A289, FINSEQ_1:14;
verum
end;
A315:
(
middle_sum the
middle_volume_Sequence of
rho,
u,
T is
convergent &
lim (middle_sum the middle_volume_Sequence of rho,u,T) = integral (
u,
rho) )
by B262, A251, A260, INTEGR22:def 9, A263;
A316:
u in BoundedFunctions the
carrier of
(ClstoCmp A)
by A269, Lm2;
reconsider v =
u as
Point of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) by A269, Lm2;
v in BoundedFunctions A
by A316, Lm1;
then consider g being
Function of
A,
REAL such that A317:
(
g = v &
g | A is
bounded )
;
reconsider v0 =
v as
Point of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) ;
A318:
for
r being
Real st
0 < r holds
ex
m0 being
Nat st
for
n being
Nat st
m0 <= n holds
||.((xD . n) - v0).|| < r
proof
let r be
Real;
( 0 < r implies ex m0 being Nat st
for n being Nat st m0 <= n holds
||.((xD . n) - v0).|| < r )
assume A319:
0 < r
;
ex m0 being Nat st
for n being Nat st m0 <= n holds
||.((xD . n) - v0).|| < r
then A321:
r / 2
< r
by XREAL_1:216;
consider s being
Real such that A322:
0 < s
and A323:
for
x1,
x2 being
Real st
x1 in dom (u | A) &
x2 in dom (u | A) &
|.(x1 - x2).| < s holds
|.(((u | A) . x1) - ((u | A) . x2)).| < r / 2
by A261, A319, XREAL_1:215;
consider m0 being
Nat such that A324:
for
i being
Nat st
m0 <= i holds
|.(((delta T) . i) - 0).| < s
by A263, A322, SEQ_2:def 7;
A325:
for
n being
Nat st
m0 <= n holds
||.((xD . n) - v0).|| < r
proof
let n be
Nat;
( m0 <= n implies ||.((xD . n) - v0).|| < r )
A326:
n in NAT
by ORDINAL1:def 12;
consider p2 being
FinSequence of
REAL such that A327:
(
p2 = F . n &
len p2 = len (T . n) & ( for
i being
Nat st
i in dom (T . n) holds
(
p2 . i in dom (u | (divset ((T . n),i))) & ex
z being
Real st
(
z = (u | (divset ((T . n),i))) . (p2 . i) &
( the middle_volume_Sequence of rho,u,T . n) . i = z * (vol ((divset ((T . n),i)),rho)) ) ) ) )
by A276, A326;
consider q2 being
FinSequence of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) such that A328:
(
len q2 = len (T . n) &
xD . n = Sum q2 & ( for
i being
Nat st
i in dom (T . n) holds
ex
r being
Real st
(
(F . n) . i in dom (u | (divset ((T . n),i))) &
r = (u | (divset ((T . n),i))) . ((F . n) . i) &
q2 . i = r * ((Dp1 (m,(T . n),(i + 1))) - (Dp1 (m,(T . n),i))) ) ) )
by A284, A326;
assume
m0 <= n
;
||.((xD . n) - v0).|| < r
then
|.(((delta T) . n) - 0).| < s
by A324;
then
|.(delta (T . n)).| < s
by A326, INTEGRA3:def 2;
then A329:
delta (T . n) < s
by ABSVALUE:def 1, INTEGRA3:9;
xD . n in the
carrier of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))
;
then
xD . n in BoundedFunctions A
by Lm1;
then consider g1 being
Function of
A,
REAL such that A330:
(
g1 = xD . n &
g1 | A is
bounded )
;
A331:
for
t being
Element of
A for
i being
Nat st
i in dom (T . n) &
t in divset (
(T . n),
i) & (
i = 1 or (
lower_bound (divset ((T . n),i)) < t &
t <= upper_bound (divset ((T . n),i)) ) ) holds
g1 . t = g . (p2 . i)
proof
let t be
Element of
A;
for i being Nat st i in dom (T . n) & t in divset ((T . n),i) & ( i = 1 or ( lower_bound (divset ((T . n),i)) < t & t <= upper_bound (divset ((T . n),i)) ) ) holds
g1 . t = g . (p2 . i)let i be
Nat;
( i in dom (T . n) & t in divset ((T . n),i) & ( i = 1 or ( lower_bound (divset ((T . n),i)) < t & t <= upper_bound (divset ((T . n),i)) ) ) implies g1 . t = g . (p2 . i) )
assume that A332:
i in dom (T . n)
and A333:
t in divset (
(T . n),
i)
and A334:
(
i = 1 or (
lower_bound (divset ((T . n),i)) < t &
t <= upper_bound (divset ((T . n),i)) ) )
;
g1 . t = g . (p2 . i)
consider r being
Real such that A336:
p2 . i in dom (u | (divset ((T . n),i)))
and A337:
r = (u | (divset ((T . n),i))) . (p2 . i)
and A338:
q2 . i = r * ((Dp1 (m,(T . n),(i + 1))) - (Dp1 (m,(T . n),i)))
by A327, A328, A332;
defpred S3[
Nat,
set ]
means ex
qi being
Function of
A,
REAL st
(
qi = q2 . $1 & $2
= qi . t );
A340:
for
i being
Nat st
i in Seg (len (T . n)) holds
ex
x being
Element of
REAL st
S3[
i,
x]
proof
let i be
Nat;
( i in Seg (len (T . n)) implies ex x being Element of REAL st S3[i,x] )
assume
i in Seg (len (T . n))
;
ex x being Element of REAL st S3[i,x]
then
i in dom (T . n)
by FINSEQ_1:def 3;
then consider r being
Real such that A342:
(
p2 . i in dom (u | (divset ((T . n),i))) &
r = (u | (divset ((T . n),i))) . (p2 . i) &
q2 . i = r * ((Dp1 (m,(T . n),(i + 1))) - (Dp1 (m,(T . n),i))) )
by A327, A328;
q2 . i in the
carrier of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))
by A342;
then
q2 . i in BoundedFunctions A
by Lm1;
then consider qi being
Function of
A,
REAL such that A343:
(
qi = q2 . i &
qi | A is
bounded )
;
take x =
qi . t;
S3[i,x]
thus
S3[
i,
x]
by A343;
verum
end;
consider z being
FinSequence of
REAL such that A344:
(
dom z = Seg (len (T . n)) & ( for
i being
Nat st
i in Seg (len (T . n)) holds
S3[
i,
z . i] ) )
from FINSEQ_1:sch 5(A340);
A346:
len q2 = len z
by A328, A344, FINSEQ_1:def 3;
A347:
i in dom z
by A344, A332, FINSEQ_1:def 3;
A348:
g1 . t = Sum z
by A328, A330, A346, LM89, A344;
A349:
dom z = dom (T . n)
by FINSEQ_1:def 3, A344;
A350:
i in Seg (len (T . n))
by A332, FINSEQ_1:def 3;
then consider qi being
Function of
A,
REAL such that A351:
(
qi = q2 . i &
z . i = qi . t )
by A344;
set D =
T . n;
B352:
t in [.(lower_bound (divset ((T . n),i))),(upper_bound (divset ((T . n),i))).]
by A333, INTEGRA1:4;
A354:
( 1
<= i &
i <= len (T . n) )
by A350, FINSEQ_1:1;
then
( 1
<= i &
i + 0 <= (len (T . n)) + 1 )
by XREAL_1:7;
then A355:
i in Seg ((len (T . n)) + 1)
;
( 1
+ 0 <= i + 1 &
i <= len (T . n) )
by A350, FINSEQ_1:1, XREAL_1:7;
then
( 1
+ 0 <= i + 1 &
i + 1
<= (len (T . n)) + 1 )
by XREAL_1:7;
then A356:
i + 1
in Seg ((len (T . n)) + 1)
;
A357:
z . i = r
proof
set f0 =
[.a,b.] --> 0;
set f1 =
([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0);
set g1 =
[.a,((T . n) . i).] --> 1;
set g2 =
].((T . n) . i),b.] --> 0;
set f2 =
([.a,((T . n) . (i - 1)).] --> 1) +* (].((T . n) . (i - 1)),b.] --> 0);
set h1 =
[.a,((T . n) . (i - 1)).] --> 1;
set h2 =
].((T . n) . (i - 1)),b.] --> 0;
B20:
(
dom ([.a,b.] --> 0) = [.a,b.] &
dom ([.a,((T . n) . i).] --> 1) = [.a,((T . n) . i).] &
dom (].((T . n) . i),b.] --> 0) = ].((T . n) . i),b.] &
dom ([.a,((T . n) . (i - 1)).] --> 1) = [.a,((T . n) . (i - 1)).] &
dom (].((T . n) . (i - 1)),b.] --> 0) = ].((T . n) . (i - 1)),b.] )
by FUNCOP_1:13;
per cases
( i = 1 or i <> 1 )
;
suppose A358:
i = 1
;
z . i = r
A = [.(lower_bound A),(upper_bound A).]
by INTEGRA1:4;
then A359:
lower_bound A = a
by A7, INTEGRA1:5;
A360:
a in [.a,b.]
by A7;
A361:
(T . n) . i in [.a,b.]
by A7, A332, INTEGRA1:6;
A362:
(
lower_bound (divset ((T . n),i)) = lower_bound A &
upper_bound (divset ((T . n),i)) = (T . n) . i )
by A332, A358, INTEGRA1:def 4;
A364:
a < (T . n) . i
by A264, A358;
A365:
Dp1 (
m,
(T . n),
(i + 1)) =
m . ((T . n) . ((i + 1) - 1))
by A356, defDp1, A358
.=
([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0)
by A8, A361, A364
;
A366:
Dp1 (
m,
(T . n),
i) =
m . (lower_bound A)
by A355, A358, defDp1
.=
[.a,b.] --> 0
by A8, A359, A360
;
A368:
dom ([.a,b.] --> 0) = A
by A7, FUNCOP_1:13;
A369:
(
a <= (T . n) . i &
(T . n) . i <= b )
by A361, XXREAL_1:1;
A370:
dom (([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0)) =
(dom ([.a,((T . n) . i).] --> 1)) \/ (dom (].((T . n) . i),b.] --> 0))
by FUNCT_4:def 1
.=
A
by A7, B20, A369, XXREAL_1:167
;
rng ([.a,b.] --> 0) c= REAL
;
then reconsider f0 =
[.a,b.] --> 0 as
Function of
A,
REAL by A368, FUNCT_2:2;
rng (([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0)) c= REAL
;
then reconsider f1 =
([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0) as
Function of
A,
REAL by A370, FUNCT_2:2;
A372:
qi . t = r * ((f1 . t) - (f0 . t))
proof
reconsider H =
(Dp1 (m,(T . n),(i + 1))) - (Dp1 (m,(T . n),i)) as
Element of
(R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider h =
H as
Function of
A,
REAL by LM88;
qi = r * H
by Lm1, A351, A338;
then qi . t =
r * (h . t)
by C0SP1:30
.=
r * ((f1 . t) - (f0 . t))
by A2, A365, A366, C0SP1:34
;
hence
qi . t = r * ((f1 . t) - (f0 . t))
;
verum
end; A373:
t in [.a,((T . n) . i).]
by A359, A362, INTEGRA1:4, A333;
then A375:
f1 . t =
([.a,((T . n) . i).] --> 1) . t
by FUNCT_4:16, B20, XXREAL_1:90
.=
1
by A373, FUNCOP_1:7
;
f0 . t = 0
by A7, FUNCOP_1:7;
hence
z . i = r
by A351, A372, A375;
verum end; suppose A376:
i <> 1
;
z . i = rthen A378:
(T . n) . (i - 1) in [.a,b.]
by A7, A332, INTEGRA1:7;
A377:
(T . n) . i in [.a,b.]
by A7, A332, INTEGRA1:6;
A379:
(
lower_bound (divset ((T . n),i)) = (T . n) . (i - 1) &
upper_bound (divset ((T . n),i)) = (T . n) . i )
by A332, A376, INTEGRA1:def 4;
i - 1
in dom (T . n)
by A332, A376, INTEGRA1:7;
then A382:
(T . n) . (i - 1) < (T . n) . i
by A332, XREAL_1:146, VALUED_0:def 13;
(
(T . n) . (i - 1) = a or
(T . n) . (i - 1) in ].a,b.] )
by A376, A7, A332, INTEGRA1:7, XXREAL_1:6;
per cases then
( a = (T . n) . (i - 1) or a < (T . n) . (i - 1) )
by XXREAL_1:2;
suppose A384:
a = (T . n) . (i - 1)
;
z . i = r
1
+ 0 < i + 1
by XREAL_1:8, A354;
then A386:
Dp1 (
m,
(T . n),
(i + 1)) =
m . ((T . n) . ((i + 1) - 1))
by A356, defDp1
.=
([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0)
by A8, A377, A384, A382
;
A387:
Dp1 (
m,
(T . n),
i) =
m . ((T . n) . (i - 1))
by A355, A376, defDp1
.=
[.a,b.] --> 0
by A8, A378, A384
;
A389:
dom ([.a,b.] --> 0) = A
by A7, FUNCOP_1:13;
A390:
(
a <= (T . n) . i &
(T . n) . i <= b )
by A377, XXREAL_1:1;
A392:
dom (([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0)) =
(dom ([.a,((T . n) . i).] --> 1)) \/ (dom (].((T . n) . i),b.] --> 0))
by FUNCT_4:def 1
.=
A
by A7, B20, A390, XXREAL_1:167
;
rng ([.a,b.] --> 0) c= REAL
;
then reconsider f0 =
[.a,b.] --> 0 as
Function of
A,
REAL by A389, FUNCT_2:2;
rng (([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0)) c= REAL
;
then reconsider f1 =
([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0) as
Function of
A,
REAL by A392, FUNCT_2:2;
A394:
qi . t = r * ((f1 . t) - (f0 . t))
proof
reconsider H =
(Dp1 (m,(T . n),(i + 1))) - (Dp1 (m,(T . n),i)) as
Element of
(R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider h =
H as
Function of
A,
REAL by LM88;
qi = r * H
by Lm1, A351, A338;
then qi . t =
r * (h . t)
by C0SP1:30
.=
r * ((f1 . t) - (f0 . t))
by A2, A386, A387, C0SP1:34
;
hence
qi . t = r * ((f1 . t) - (f0 . t))
;
verum
end; A395:
t in [.((T . n) . (i - 1)),((T . n) . i).]
by A379, INTEGRA1:4, A333;
(
a <= (T . n) . (i - 1) &
(T . n) . (i - 1) <= b )
by A378, XXREAL_1:1;
then B396:
[.((T . n) . (i - 1)),((T . n) . i).] c= [.a,((T . n) . i).]
by XXREAL_1:34;
then A398:
f1 . t =
([.a,((T . n) . i).] --> 1) . t
by A395, FUNCT_4:16, B20, XXREAL_1:90
.=
1
by B396, A395, FUNCOP_1:7
;
f0 . t = 0
by A7, FUNCOP_1:7;
hence
z . i = r
by A351, A394, A398;
verum end; suppose A399:
a < (T . n) . (i - 1)
;
z . i = r
1
+ 0 < i + 1
by XREAL_1:8, A354;
then A401:
Dp1 (
m,
(T . n),
(i + 1)) =
m . ((T . n) . ((i + 1) - 1))
by A356, defDp1
.=
([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0)
by A8, A377, A399, A382
;
A402:
Dp1 (
m,
(T . n),
i) =
m . ((T . n) . (i - 1))
by A355, A376, defDp1
.=
([.a,((T . n) . (i - 1)).] --> 1) +* (].((T . n) . (i - 1)),b.] --> 0)
by A8, A378, A399
;
A404:
(
a <= (T . n) . i &
(T . n) . i <= b )
by A377, XXREAL_1:1;
A405:
(
a <= (T . n) . (i - 1) &
(T . n) . (i - 1) <= b )
by A378, XXREAL_1:1;
A406:
dom (([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0)) =
(dom ([.a,((T . n) . i).] --> 1)) \/ (dom (].((T . n) . i),b.] --> 0))
by FUNCT_4:def 1
.=
A
by A7, B20, A404, XXREAL_1:167
;
A407:
dom (([.a,((T . n) . (i - 1)).] --> 1) +* (].((T . n) . (i - 1)),b.] --> 0)) =
(dom ([.a,((T . n) . (i - 1)).] --> 1)) \/ (dom (].((T . n) . (i - 1)),b.] --> 0))
by FUNCT_4:def 1
.=
A
by A7, B20, A405, XXREAL_1:167
;
rng (([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0)) c= REAL
;
then reconsider f1 =
([.a,((T . n) . i).] --> 1) +* (].((T . n) . i),b.] --> 0) as
Function of
A,
REAL by A406, FUNCT_2:2;
rng (([.a,((T . n) . (i - 1)).] --> 1) +* (].((T . n) . (i - 1)),b.] --> 0)) c= REAL
;
then reconsider f2 =
([.a,((T . n) . (i - 1)).] --> 1) +* (].((T . n) . (i - 1)),b.] --> 0) as
Function of
A,
REAL by A407, FUNCT_2:2;
A408:
(
a <= t &
t <= b )
by XXREAL_1:1, A7;
A409:
qi . t = r * ((f1 . t) - (f2 . t))
proof
reconsider H =
(Dp1 (m,(T . n),(i + 1))) - (Dp1 (m,(T . n),i)) as
Element of
(R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider h =
H as
Function of
A,
REAL by LM88;
qi = r * H
by Lm1, A351, A338;
then qi . t =
r * (h . t)
by C0SP1:30
.=
r * ((f1 . t) - (f2 . t))
by A2, A401, A402, C0SP1:34
;
hence
qi . t = r * ((f1 . t) - (f2 . t))
;
verum
end; A410:
t in [.((T . n) . (i - 1)),((T . n) . i).]
by A379, INTEGRA1:4, A333;
B411:
[.((T . n) . (i - 1)),((T . n) . i).] c= [.a,((T . n) . i).]
by A405, XXREAL_1:34;
then A413:
f1 . t =
([.a,((T . n) . i).] --> 1) . t
by A410, FUNCT_4:16, B20, XXREAL_1:90
.=
1
by B411, A410, FUNCOP_1:7
;
(
(T . n) . (i - 1) < t &
t <= (T . n) . i )
by A332, INTEGRA1:def 4, A334, A376;
then A414:
t in ].((T . n) . (i - 1)),b.]
by A408;
then f2 . t =
(].((T . n) . (i - 1)),b.] --> 0) . t
by B20, FUNCT_4:13
.=
0
by A414, FUNCOP_1:7
;
hence
z . i = r
by A351, A409, A413;
verum end; end; end; end;
end;
for
k being
Nat st
k in dom z &
k <> i holds
z . k = 0
proof
let k be
Nat;
( k in dom z & k <> i implies z . k = 0 )
assume that A415:
k in dom z
and A416:
k <> i
;
z . k = 0
consider r being
Real such that
p2 . k in dom (u | (divset ((T . n),k)))
and
r = (u | (divset ((T . n),k))) . (p2 . k)
and A420:
q2 . k = r * ((Dp1 (m,(T . n),(k + 1))) - (Dp1 (m,(T . n),k)))
by A327, A328, A349, A415;
consider qk being
Function of
A,
REAL such that A423:
(
qk = q2 . k &
z . k = qk . t )
by A344, A415;
A425:
k in dom (T . n)
by A344, A415, FINSEQ_1:def 3;
A426:
( 1
<= k &
k <= len (T . n) )
by A344, A415, FINSEQ_1:1;
then
k + 0 <= (len (T . n)) + 1
by XREAL_1:7;
then A427:
k in Seg ((len (T . n)) + 1)
by A426;
e:
1
+ 0 <= k + 1
by XREAL_1:7;
k + 1
<= (len (T . n)) + 1
by XREAL_1:7, A426;
then A428:
k + 1
in Seg ((len (T . n)) + 1)
by e;
set f0 =
[.a,b.] --> 0;
set f1 =
([.a,((T . n) . k).] --> 1) +* (].((T . n) . k),b.] --> 0);
set g1 =
[.a,((T . n) . k).] --> 1;
set g2 =
].((T . n) . k),b.] --> 0;
set f2 =
([.a,((T . n) . (k - 1)).] --> 1) +* (].((T . n) . (k - 1)),b.] --> 0);
set h1 =
[.a,((T . n) . (k - 1)).] --> 1;
set h2 =
].((T . n) . (k - 1)),b.] --> 0;
B30:
(
dom ([.a,b.] --> 0) = [.a,b.] &
dom ([.a,((T . n) . k).] --> 1) = [.a,((T . n) . k).] &
dom (].((T . n) . k),b.] --> 0) = ].((T . n) . k),b.] &
dom ([.a,((T . n) . (k - 1)).] --> 1) = [.a,((T . n) . (k - 1)).] &
dom (].((T . n) . (k - 1)),b.] --> 0) = ].((T . n) . (k - 1)),b.] )
by FUNCOP_1:13;
per cases
( k = 1 or k <> 1 )
;
suppose A429:
k = 1
;
z . k = 0 then A433:
(
lower_bound (divset ((T . n),i)) = (T . n) . (i - 1) &
upper_bound (divset ((T . n),i)) = (T . n) . i )
by A332, INTEGRA1:def 4, A416;
A435:
i - 1
in dom (T . n)
by A332, A429, A416, INTEGRA1:7;
A440:
(T . n) . k in [.a,b.]
by A7, A425, INTEGRA1:6;
then A446:
(
a <= (T . n) . k &
(T . n) . k <= b )
by XXREAL_1:1;
A445:
dom ([.a,b.] --> 0) = A
by A7, FUNCOP_1:13;
A447:
dom (([.a,((T . n) . k).] --> 1) +* (].((T . n) . k),b.] --> 0)) =
(dom ([.a,((T . n) . k).] --> 1)) \/ (dom (].((T . n) . k),b.] --> 0))
by FUNCT_4:def 1
.=
A
by A7, B30, A446, XXREAL_1:167
;
rng ([.a,b.] --> 0) c= REAL
;
then reconsider f0 =
[.a,b.] --> 0 as
Function of
A,
REAL by A445, FUNCT_2:2;
rng (([.a,((T . n) . k).] --> 1) +* (].((T . n) . k),b.] --> 0)) c= REAL
;
then reconsider f1 =
([.a,((T . n) . k).] --> 1) +* (].((T . n) . k),b.] --> 0) as
Function of
A,
REAL by A447, FUNCT_2:2;
A451:
a < (T . n) . k
by A264, A429;
A452:
Dp1 (
m,
(T . n),
(k + 1)) =
m . ((T . n) . ((k + 1) - 1))
by A428, defDp1, A429
.=
([.a,((T . n) . k).] --> 1) +* (].((T . n) . k),b.] --> 0)
by A8, A440, A451
;
A = [.(lower_bound A),(upper_bound A).]
by INTEGRA1:4;
then A438:
lower_bound A = a
by A7, INTEGRA1:5;
A439:
a in [.a,b.]
by A7;
A443:
Dp1 (
m,
(T . n),
k) =
m . (lower_bound A)
by A427, A429, defDp1
.=
[.a,b.] --> 0
by A8, A438, A439
;
A453:
qk . t = r * ((f1 . t) - (f0 . t))
proof
reconsider H =
(Dp1 (m,(T . n),(k + 1))) - (Dp1 (m,(T . n),k)) as
Element of
(R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider h =
H as
Function of
A,
REAL by LM88;
qk = r * H
by Lm1, A423, A420;
then qk . t =
r * (h . t)
by C0SP1:30
.=
r * ((f1 . t) - (f0 . t))
by A2, A443, A452, C0SP1:34
;
hence
qk . t = r * ((f1 . t) - (f0 . t))
;
verum
end;
k < i
by A429, A416, A354, XXREAL_0:1;
then
k + 1
<= i
by NAT_1:13;
then A456:
(k + 1) - 1
<= i - 1
by XREAL_1:13;
(T . n) . k <= (T . n) . (i - 1)
then A457:
(T . n) . k < t
by A334, A429, A416, XXREAL_0:2, A433;
(
a <= t &
t <= b )
by XXREAL_1:1, A7;
then A459:
t in ].((T . n) . k),b.]
by A457;
then A461:
f1 . t =
(].((T . n) . k),b.] --> 0) . t
by B30, FUNCT_4:13
.=
0
by A459, FUNCOP_1:7
;
f0 . t = 0
by A7, FUNCOP_1:7;
hence
z . k = 0
by A423, A453, A461;
verum end; suppose A462:
k <> 1
;
z . k = 0 then A464:
(T . n) . (k - 1) in [.a,b.]
by A7, A425, INTEGRA1:7;
A463:
(T . n) . k in [.a,b.]
by A7, A425, INTEGRA1:6;
A467:
k - 1
in dom (T . n)
by A425, A462, INTEGRA1:7;
then A468:
(T . n) . (k - 1) < (T . n) . k
by A425, XREAL_1:146, VALUED_0:def 13;
1
< k
by A426, A462, XXREAL_0:1;
then
1
+ 1
<= k
by NAT_1:13;
then A470:
2
- 1
<= k - 1
by XREAL_1:13;
1
<= len (T . n)
by A426, XXREAL_0:2;
then A471:
1
in dom (T . n)
by FINSEQ_3:25;
(T . n) . 1
<= (T . n) . (k - 1)
then A472:
a < (T . n) . (k - 1)
by A264, XXREAL_0:2;
1
+ 0 < k + 1
by XREAL_1:8, A426;
then A474:
Dp1 (
m,
(T . n),
(k + 1)) =
m . ((T . n) . ((k + 1) - 1))
by A428, defDp1
.=
([.a,((T . n) . k).] --> 1) +* (].((T . n) . k),b.] --> 0)
by A8, A463, A472, A468
;
A475:
Dp1 (
m,
(T . n),
k) =
m . ((T . n) . (k - 1))
by A427, A462, defDp1
.=
([.a,((T . n) . (k - 1)).] --> 1) +* (].((T . n) . (k - 1)),b.] --> 0)
by A8, A464, A472
;
A477:
(
a <= (T . n) . k &
(T . n) . k <= b )
by A463, XXREAL_1:1;
A478:
(
a <= (T . n) . (k - 1) &
(T . n) . (k - 1) <= b )
by A464, XXREAL_1:1;
A479:
dom (([.a,((T . n) . k).] --> 1) +* (].((T . n) . k),b.] --> 0)) =
(dom ([.a,((T . n) . k).] --> 1)) \/ (dom (].((T . n) . k),b.] --> 0))
by FUNCT_4:def 1
.=
A
by A7, B30, A477, XXREAL_1:167
;
A480:
dom (([.a,((T . n) . (k - 1)).] --> 1) +* (].((T . n) . (k - 1)),b.] --> 0)) =
(dom ([.a,((T . n) . (k - 1)).] --> 1)) \/ (dom (].((T . n) . (k - 1)),b.] --> 0))
by FUNCT_4:def 1
.=
A
by A7, B30, A478, XXREAL_1:167
;
rng (([.a,((T . n) . k).] --> 1) +* (].((T . n) . k),b.] --> 0)) c= REAL
;
then reconsider f1 =
([.a,((T . n) . k).] --> 1) +* (].((T . n) . k),b.] --> 0) as
Function of
A,
REAL by A479, FUNCT_2:2;
rng (([.a,((T . n) . (k - 1)).] --> 1) +* (].((T . n) . (k - 1)),b.] --> 0)) c= REAL
;
then reconsider f2 =
([.a,((T . n) . (k - 1)).] --> 1) +* (].((T . n) . (k - 1)),b.] --> 0) as
Function of
A,
REAL by A480, FUNCT_2:2;
A482:
qk . t = r * ((f1 . t) - (f2 . t))
proof
reconsider H =
(Dp1 (m,(T . n),(k + 1))) - (Dp1 (m,(T . n),k)) as
Element of
(R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider h =
H as
Function of
A,
REAL by LM88;
qk = r * H
by Lm1, A423, A420;
then qk . t =
r * (h . t)
by C0SP1:30
.=
r * ((f1 . t) - (f2 . t))
by A2, A474, A475, C0SP1:34
;
hence
qk . t = r * ((f1 . t) - (f2 . t))
;
verum
end; per cases
( i < k or k < i )
by A416, XXREAL_0:1;
suppose
i < k
;
z . k = 0 then
i + 1
<= k
by NAT_1:13;
then A485:
(i + 1) - 1
<= k - 1
by XREAL_1:13;
A486:
(T . n) . i <= (T . n) . (k - 1)
A488:
upper_bound (divset ((T . n),i)) <= (T . n) . (k - 1)
(
a <= t &
t <= upper_bound (divset ((T . n),i)) )
by B352, XXREAL_1:1, A7;
then A489:
(
a <= t &
t <= (T . n) . (k - 1) )
by A488, XXREAL_0:2;
then A490:
t in [.a,((T . n) . (k - 1)).]
;
(
a <= t &
t <= (T . n) . k )
by A468, A489, XXREAL_0:2;
then A491:
t in [.a,((T . n) . k).]
;
then A494:
f1 . t =
([.a,((T . n) . k).] --> 1) . t
by FUNCT_4:16, B30, XXREAL_1:90
.=
1
by A491, FUNCOP_1:7
;
f2 . t =
([.a,((T . n) . (k - 1)).] --> 1) . t
by A490, FUNCT_4:16, B30, XXREAL_1:90
.=
1
by A490, FUNCOP_1:7
;
hence
z . k = 0
by A423, A482, A494;
verum end; suppose A496:
k < i
;
z . k = 0 then
k + 1
<= i
by NAT_1:13;
then A499:
(k + 1) - 1
<= i - 1
by XREAL_1:13;
A500:
i - 1
in dom (T . n)
by A332, A496, A426, INTEGRA1:7;
A502:
(T . n) . k <= (T . n) . (i - 1)
(T . n) . (i - 1) < t
by A496, A426, A334, A332, INTEGRA1:def 4;
then A504:
(T . n) . k < t
by A502, XXREAL_0:2;
then A505:
(T . n) . (k - 1) < t
by A468, XXREAL_0:2;
A506:
(
a <= t &
t <= b )
by XXREAL_1:1, A7;
then A507:
t in ].((T . n) . k),b.]
by A504;
then A509:
f1 . t =
(].((T . n) . k),b.] --> 0) . t
by B30, FUNCT_4:13
.=
0
by A507, FUNCOP_1:7
;
A508:
t in ].((T . n) . (k - 1)),b.]
by A505, A506;
then f2 . t =
(].((T . n) . (k - 1)),b.] --> 0) . t
by B30, FUNCT_4:13
.=
0
by A508, FUNCOP_1:7
;
hence
z . k = 0
by A423, A482, A509;
verum end; end; end; end;
end;
hence
g1 . t = g . (p2 . i)
by A317, A336, FUNCT_1:47, A348, A337, A347, A357, INTEGR23:6;
verum
end;
A511:
for
t being
Element of
A holds
|.((g1 . t) - (g . t)).| < r / 2
proof
let t be
Element of
A;
|.((g1 . t) - (g . t)).| < r / 2
A = [.(lower_bound A),(upper_bound A).]
by INTEGRA1:4;
then A512:
lower_bound A = a
by A7, INTEGRA1:5;
a < (T . n) . 1
by A264;
then consider j being
Element of
NAT such that A540:
j in dom (T . n)
and A541:
t in divset (
(T . n),
j)
and A542:
(
j = 1 or (
lower_bound (divset ((T . n),j)) < t &
t <= upper_bound (divset ((T . n),j)) ) )
by A512, LM94;
reconsider i =
j as
Nat ;
set tD =
p2 . i;
A543:
for
tD,
t being
Real st
tD in dom g &
t in dom g &
|.(tD - t).| < s holds
|.((g . tD) - (g . t)).| < r / 2
p2 . i in dom (u | (divset ((T . n),i)))
by A327, A540;
then
p2 . i in (dom u) /\ (divset ((T . n),i))
by RELAT_1:61;
then A549:
(
p2 . i in dom u &
p2 . i in divset (
(T . n),
i) )
by XBOOLE_0:def 4;
then B551:
|.((p2 . i) - t).| < s
by A329, A540, A541, INTEGR20:12;
g1 . t = g . (p2 . i)
by A331, A540, A541, A542;
hence
|.((g1 . t) - (g . t)).| < r / 2
by B551, A543, A549, A260, A317;
verum
end;
reconsider z =
(xD . n) - v0 as
Element of
(R_Normed_Algebra_of_BoundedFunctions A) by Lm1;
reconsider g0 =
z as
Function of
A,
REAL by LM88;
g0 in BoundedFunctions A
;
then consider g2 being
Function of
A,
REAL such that A552:
(
g2 = g0 &
g2 | A is
bounded )
;
then
upper_bound (PreNorms g0) <= r / 2
by SEQ_4:45;
then
||.z.|| <= r / 2
by A552, C0SP1:20;
then
||.((xD . n) - v0).|| <= r / 2
by Lm1;
hence
||.((xD . n) - v0).|| < r
by A321, XXREAL_0:2;
verum
end;
take
m0
;
for n being Nat st m0 <= n holds
||.((xD . n) - v0).|| < r
thus
for
n being
Nat st
m0 <= n holds
||.((xD . n) - v0).|| < r
by A325;
verum
end;
then A555:
xD is
convergent
by NORMSP_1:def 6;
then A556:
lim xD = v
by A318, NORMSP_1:def 7;
dom f = the
carrier of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))
by FUNCT_2:def 1;
then A557:
rng xD c= dom f
;
v in the
carrier of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))
;
then A558:
v in dom f
by FUNCT_2:def 1;
consider K being
Real such that A559:
(
0 <= K & ( for
x being
Point of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) holds
|.(f . x).| <= K * ||.x.|| ) )
by DUALSP01:def 9;
for
r being
Real st
0 < r holds
ex
s being
Real st
(
0 < s & ( for
x1 being
Point of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st
x1 in dom f &
||.(x1 - v).|| < s holds
|.((f /. x1) - (f /. v)).| < r ) )
then
f is_continuous_in v
by A558, NFCONT_1:8;
then
f /. v = lim (f /* xD)
by A555, A556, A557, NFCONT_1:def 6;
then
lim (f * xD) = f . v
by A557, FUNCT_2:def 11;
then
f . u = integral (
u,
rho)
by B314, FUNCT_2:def 8, A315;
hence
x . u = integral (
u,
rho)
by A6, FUNCT_1:49, A269;
verum
end;
then B573:
||.x.|| <= total_vd rho
by A251, Lm83;
take
rho
; ( rho is bounded_variation & ( for u being continuous PartFunc of REAL,REAL st dom u = A holds
x . u = integral (u,rho) ) & ||.x.|| = total_vd rho )
thus
( rho is bounded_variation & ( for u being continuous PartFunc of REAL,REAL st dom u = A holds
x . u = integral (u,rho) ) & ||.x.|| = total_vd rho )
by B250, A259, B573, A258, XXREAL_0:1; verum