let A be non empty closed_interval Subset of REAL; for rho being Function of A,REAL
for f being Point of (DualSp (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A))) st rho is bounded_variation & ( for u being continuous PartFunc of REAL,REAL st dom u = A holds
f . u = integral (u,rho) ) holds
||.f.|| <= total_vd rho
let rho be Function of A,REAL; for f being Point of (DualSp (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A))) st rho is bounded_variation & ( for u being continuous PartFunc of REAL,REAL st dom u = A holds
f . u = integral (u,rho) ) holds
||.f.|| <= total_vd rho
let f be Point of (DualSp (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A))); ( rho is bounded_variation & ( for u being continuous PartFunc of REAL,REAL st dom u = A holds
f . u = integral (u,rho) ) implies ||.f.|| <= total_vd rho )
assume that
A1:
rho is bounded_variation
and
A2:
for u being continuous PartFunc of REAL,REAL st dom u = A holds
f . u = integral (u,rho)
; ||.f.|| <= total_vd rho
set X = R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A);
A3:
for u being continuous PartFunc of REAL,REAL st u in the carrier of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) holds
f . u = integral (u,rho)
A4:
for u being continuous PartFunc of REAL,REAL
for v being Point of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) st dom u = A & u = v holds
|.(integral (u,rho)).| <= ||.v.|| * (total_vd rho)
proof
let u be
continuous PartFunc of
REAL,
REAL;
for v being Point of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) st dom u = A & u = v holds
|.(integral (u,rho)).| <= ||.v.|| * (total_vd rho)let v be
Point of
(R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A));
( dom u = A & u = v implies |.(integral (u,rho)).| <= ||.v.|| * (total_vd rho) )
assume A5:
(
dom u = A &
u = v )
;
|.(integral (u,rho)).| <= ||.v.|| * (total_vd rho)
then B6:
u is_RiemannStieltjes_integrable_with rho
by A1, INTEGR23:21;
consider T being
DivSequence of
A such that A7:
(
delta T is
convergent &
lim (delta T) = 0 )
by INTEGRA4:11;
set S = the
middle_volume_Sequence of
rho,
u,
T;
A9:
|.(middle_sum the middle_volume_Sequence of rho,u,T).| is
convergent
by SEQ_4:13, B6, A7;
A10:
for
n being
Nat holds
|.((middle_sum the middle_volume_Sequence of rho,u,T) . n).| <= ||.v.|| * (total_vd rho)
proof
let n be
Nat;
|.((middle_sum the middle_volume_Sequence of rho,u,T) . n).| <= ||.v.|| * (total_vd rho)
set F = the
var_volume of
rho,
T . n;
reconsider v0 =
||.v.|| as
Real ;
reconsider vF =
v0 * the
var_volume of
rho,
T . n as
FinSequence of
REAL ;
dom the
var_volume of
rho,
T . n = Seg (len the var_volume of rho,T . n)
by FINSEQ_1:def 3;
then B14:
dom vF = Seg (len the var_volume of rho,T . n)
by VALUED_1:def 5;
A15:
len ( the middle_volume_Sequence of rho,u,T . n) =
len (T . n)
by A1, A5, INTEGR22:def 5
.=
len the
var_volume of
rho,
T . n
by INTEGR22:def 2
.=
len vF
by B14, FINSEQ_1:def 3
;
for
j being
Nat st
j in dom ( the middle_volume_Sequence of rho,u,T . n) holds
|.(( the middle_volume_Sequence of rho,u,T . n) . j).| <= vF . j
proof
let j be
Nat;
( j in dom ( the middle_volume_Sequence of rho,u,T . n) implies |.(( the middle_volume_Sequence of rho,u,T . n) . j).| <= vF . j )
assume
j in dom ( the middle_volume_Sequence of rho,u,T . n)
;
|.(( the middle_volume_Sequence of rho,u,T . n) . j).| <= vF . j
then B17:
j in Seg (len ( the middle_volume_Sequence of rho,u,T . n))
by FINSEQ_1:def 3;
then
j in Seg (len (T . n))
by A1, A5, INTEGR22:def 5;
then A16:
j in dom (T . n)
by FINSEQ_1:def 3;
consider r being
Real such that A18:
r in rng (u | (divset ((T . n),j)))
and A19:
( the middle_volume_Sequence of rho,u,T . n) . j = r * (vol ((divset ((T . n),j)),rho))
by A1, A5, INTEGR22:def 5, A16;
A20:
|.(( the middle_volume_Sequence of rho,u,T . n) . j).| =
|.r.| * |.(vol ((divset ((T . n),j)),rho)).|
by COMPLEX1:65, A19
.=
|.r.| * ( the var_volume of rho,T . n . j)
by A16, INTEGR22:def 2
;
consider x being
object such that A21:
(
x in dom (u | (divset ((T . n),j))) &
r = (u | (divset ((T . n),j))) . x )
by A18, FUNCT_1:def 3;
set AV = the
carrier of
(ClstoCmp A);
u in BoundedFunctions the
carrier of
(ClstoCmp A)
by A5, Lm2;
then consider u1 being
Function of the
carrier of
(ClstoCmp A),
REAL such that A23:
(
u = u1 &
u1 | the
carrier of
(ClstoCmp A) is
bounded )
;
x in A
by A5, A21, RELAT_1:57;
then reconsider x1 =
x as
Element of the
carrier of
(ClstoCmp A) by Lm1;
reconsider v1 =
v as
Point of
(R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) by Lm2;
|.(u1 . x1).| <= ||.v1.||
by A5, A23, C0SP1:26;
then
|.(u . x).| <= ||.v.||
by A23, FUNCT_1:49;
then A24:
|.r.| <= ||.v.||
by A21, FUNCT_1:47;
j in Seg (len (T . n))
by B17, A1, A5, INTEGR22:def 5;
then
j in Seg (len the var_volume of rho,T . n)
by INTEGR22:def 2;
then
j in dom the
var_volume of
rho,
T . n
by FINSEQ_1:def 3;
then
0 <= the
var_volume of
rho,
T . n . j
by INTEGR22:3;
then
|.r.| * ( the var_volume of rho,T . n . j) <= v0 * ( the var_volume of rho,T . n . j)
by A24, XREAL_1:64;
hence
|.(( the middle_volume_Sequence of rho,u,T . n) . j).| <= vF . j
by A20, VALUED_1:6;
verum
end;
then
|.(Sum ( the middle_volume_Sequence of rho,u,T . n)).| <= Sum vF
by A15, INTEGR23:3;
then A25:
|.(Sum ( the middle_volume_Sequence of rho,u,T . n)).| <= ||.v.|| * (Sum the var_volume of rho,T . n)
by RVSUM_1:87;
||.v.|| * (Sum the var_volume of rho,T . n) <= ||.v.|| * (total_vd rho)
by A1, INTEGR22:5, XREAL_1:64;
then
|.(Sum ( the middle_volume_Sequence of rho,u,T . n)).| <= ||.v.|| * (total_vd rho)
by A25, XXREAL_0:2;
hence
|.((middle_sum the middle_volume_Sequence of rho,u,T) . n).| <= ||.v.|| * (total_vd rho)
by INTEGR22:def 7;
verum
end;
reconsider a =
||.v.|| * (total_vd rho) as
Real ;
then
lim |.(middle_sum the middle_volume_Sequence of rho,u,T).| <= lim (seq_const a)
by A9, SEQ_2:18;
then A27:
|.(lim (middle_sum the middle_volume_Sequence of rho,u,T)).| <= lim (seq_const a)
by B6, A7, SEQ_4:14;
lim (seq_const a) =
(seq_const a) . 0
by SEQ_4:26
.=
a
by SEQ_1:57
;
hence
|.(integral (u,rho)).| <= ||.v.|| * (total_vd rho)
by B6, A1, A5, INTEGR22:def 9, A7, A27;
verum
end;
reconsider g = f as Lipschitzian linear-Functional of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) by DUALSP01:def 10;
then
upper_bound (PreNorms g) <= total_vd rho
by SEQ_4:45;
hence
||.f.|| <= total_vd rho
by DUALSP01:24; verum