:: F. Riesz Theorem
:: by Keiko Narita , Kazuhisa Nakasho and Yasunari Shidama
::
:: Received August 30, 2017
:: Copyright (c) 2017-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies DUALSP05, ABSVALUE, NUMBERS, INTEGRA1, SUBSET_1, FUNCT_1,
FINSEQ_1, NAT_1, RELAT_1, MEASURE7, XBOOLE_0, XXREAL_2, XXREAL_0, SEQ_4,
CARD_1, REAL_1, ARYTM_3, ARYTM_1, CARD_3, INTEGRA2, SEQ_2, ORDINAL2,
HAHNBAN, FUNCT_4, COMPLEX1, XXREAL_1, FUNCT_3, STRUCT_0, PARTFUN1,
TARSKI, DUALSP01, TOPMETR, PRE_TOPC, REALSET1, INTEGR15, MEASURE5,
FUNCT_7, INTEGR22, C0SP2, RCOMP_1, NORMSP_1, FCONT_1, PSCOMP_1, C0SP1,
ZFMISC_1, INTEGRA4, RFINSEQ, ORDINAL4, FUNCOP_1, RLVECT_1, RSSPACE4,
POLYALG1, MSSUBFAM, LOPBAN_1, ALGSTR_0, FUNCT_2, SUPINF_2, ASYMPT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1,
PARTFUN1, FUNCT_2, FUNCOP_1, FUNCT_4, REALSET1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, NAT_1, VALUED_0, ABSVALUE, XXREAL_2, FINSEQ_1,
FINSEQ_2, FINSEQOP, VALUED_1, SEQ_1, SEQ_2, RVSUM_1, SEQ_4, RCOMP_1,
FCONT_1, HAHNBAN, RFINSEQ, MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3,
INTEGRA4, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, COMPTS_1, NORMSP_0,
NORMSP_1, TOPMETR, PSCOMP_1, NFCONT_1, C0SP1, C0SP2, DUALSP01, INTEGR22;
constructors REAL_1, FINSEQOP, MONOID_0, SEQ_4, PSCOMP_1, NAT_D, FCONT_1,
FCONT_2, INTEGRA4, SEQ_2, INTEGRA3, RFINSEQ, REALSET1, FUNCT_4, RSSPACE,
ABSVALUE, TOPMETR, COMSEQ_2, C0SP1, C0SP2, DUALSP01, PCOMPS_1, INTEGR22,
SEQ_1, NFCONT_1;
registrations NUMBERS, XREAL_0, SEQ_1, SEQ_2, INTEGRA1, FUNCT_2, NAT_1,
MEMBERED, ORDINAL1, FCONT_1, VALUED_0, VALUED_1, RELSET_1, PSCOMP_1,
TOPMETR, COMPTS_1, CARD_1, MEASURE5, PRE_TOPC, FINSEQ_1, C0SP1, STRUCT_0,
ABSVALUE, NORMSP_1, C0SP2, DUALSP01, INT_1, XXREAL_2, FUNCSDOM;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, RCOMP_1, NORMSP_0, TOPMETR, C0SP2, PCOMPS_1, STRUCT_0,
C0SP1, FINSEQ_1, DUALSP01, METRIC_1, FUNCSDOM, INTEGRA1;
expansions MEMBERED, INTEGR22, VALUED_0;
theorems XBOOLE_0, XBOOLE_1, INTEGRA1, INTEGRA4, XXREAL_2, XXREAL_0, RELAT_1,
XCMPLX_1, ORDINAL1, XREAL_1, RCOMP_1, SEQ_4, SEQ_2, FINSEQ_1, FINSEQ_2,
RVSUM_1, FUNCT_1, FUNCT_2, INTEGRA6, VALUED_1, RELSET_1, RFINSEQ,
PRE_TOPC, TOPMETR, FCONT_1, TARSKI, C0SP2, MEASURE5, COMPLEX1, HAHNBAN,
SEQ_1, NORMSP_1, FINSEQ_3, ABSVALUE, DUALSP01, XXREAL_1, FUNCT_4,
VALUED_0, C0SP1, NAT_1, HEINE, FCONT_2, INTEGR20, FINSEQ_4, FINSEQ_5,
RLVECT_1, INTEGRA3, INT_1, FUNCOP_1, INTEGR22, INTEGR23, RFUNCT_1,
NFCONT_1, BORSUK_5;
schemes FUNCT_2, FINSEQ_1, NAT_1;
begin :: The normed spaces of Continuous Functions on closed interval
theorem LM91:
for d be Real holds |. sgn d .| <= 1
proof
let d be Real;
per cases;
suppose d > 0; then
sgn d = 1 by ABSVALUE:def 2;
hence |. sgn d .| <= 1;
end;
suppose d < 0; then
sgn d = -1 by ABSVALUE:def 2; then
|. sgn d .| = -(-1) by ABSVALUE:def 1
.= 1;
hence |. sgn d .| <= 1;
end;
suppose d = 0; then
sgn d = 0 by ABSVALUE:def 2;
hence |. sgn d .| <= 1;
end;
end;
theorem LM86:
for x be Real holds |.x.| = (sgn x) * x
proof
let x be Real;
A1: 0 < x implies |.x.| = (sgn x) * x
proof
assume A2: 0 < x; then
(sgn x) * x = 1 * x by ABSVALUE:def 2
.= x;
hence thesis by A2,ABSVALUE:def 1;
end;
A4: x < 0 implies |.x.| = (sgn x) * x
proof
assume A5: x < 0; then
(sgn x) * x = (-1) * x by ABSVALUE:def 2
.= -x;
hence thesis by A5,ABSVALUE:def 1;
end;
x = 0 implies |.x.| = (sgn x) * x;
hence thesis by A1,A4;
end;
definition
let A be non empty closed_interval Subset of REAL;
func ClstoCmp(A) -> strict compact non empty TopSpace means
:Def7ClstoCmp:
ex a,b be Real st a <= b & [.a,b.] = A
& it = Closed-Interval-TSpace(a,b);
existence
proof
consider a,b be Real such that
A1: [.a,b.] = A by MEASURE5:def 3;
consider p be object such that
A2: p in A by XBOOLE_0:def 1;
consider r be Real such that
A3: r = p & a <= r & r <= b by A1,A2;
Closed-Interval-TSpace (a,b) is compact by A3,HEINE:4,XXREAL_0:2;
hence thesis by A1,A3,XXREAL_0:2;
end;
uniqueness
proof
let A1,A2 be strict compact non empty TopSpace;
assume that
A4: ex a,b be Real st a <= b & [.a,b.] = A
& A1 = Closed-Interval-TSpace (a,b) and
A5: ex a,b be Real st a <= b & [.a,b.] = A
& A2 = Closed-Interval-TSpace (a,b);
consider a1,b1 be Real such that
A6: a1 <= b1 & [.a1,b1.] = A
& A1 = Closed-Interval-TSpace (a1,b1) by A4;
consider a2,b2 be Real such that
A7: a2 <= b2 & [.a2,b2.] = A
& A2 = Closed-Interval-TSpace (a2,b2) by A5;
a1 = a2 & b1 = b2 by A6,A7,XXREAL_1:66;
hence A1 = A2 by A6,A7;
end;
end;
theorem Th80a:
for X be strict non empty SubSpace of R^1,
f be RealMap of X,
g be PartFunc of REAL,REAL,
x be Point of X,
x0 be Real
st g = f & x = x0
holds
( for V be Subset of REAL st f.x in V & V is open holds
ex W be Subset of X st
x in W & W is open & f.:W c= V )
iff
g is_continuous_in x0
proof
let X be strict non empty SubSpace of R^1,
f be RealMap of X,
g be PartFunc of REAL,REAL,
x be Point of X,
x0 be Real;
assume AS:g=f & x=x0;
A1: dom g = the carrier of X by FUNCT_2:def 1,AS;
hereby
assume
A2: for V be Subset of REAL st f.x in V & V is open holds
ex W be Subset of X st
x in W & W is open & f.:W c= V;
for N1 be Neighbourhood of g.x0
ex N be Neighbourhood of x0 st g.:N c= N1
proof
let N1 be Neighbourhood of g.x0;
consider s be Real such that
A3: 0 < s & N1 = ]. g.x0 -s,g.x0+s.[ by RCOMP_1:def 6;
A4: ]. g.x0-s,g.x0+s.[ is open by RCOMP_1:7;
B5: |. g.x0 - g.x0 .| = 0;
consider W be Subset of X such that
A6: x in W & W is open & f.:W c= ]. g.x0-s,g.x0+s.[
by A2,A4,B5,A3,RCOMP_1:1,AS;
W in the topology of X by A6,PRE_TOPC:def 2; then
consider W0 be Subset of R^1 such that
A7: W0 in the topology of R^1 & W = W0 /\ ([#] X) by PRE_TOPC:def 4;
reconsider W1=W0 as Subset of REAL;
W0 is open by A7,PRE_TOPC:def 2; then
A8: W1 is open by BORSUK_5:39;
x0 in W1 by A6,A7,AS,XBOOLE_0:def 4; then
consider N be Neighbourhood of x0 such that
A9: N c= W1 by A8,RCOMP_1:18;
take N;
A10: g.:N c= g.:W1 by A9,RELAT_1:123;
g.:W1 = f.: W by A1,A7,AS,RELAT_1:112;
hence g.:N c= N1 by A3,A6,A10;
end;
hence g is_continuous_in x0 by FCONT_1:5;
end;
assume B11: g is_continuous_in x0;
thus for V be Subset of REAL st f . x in V & V is open holds
ex W be Subset of X st
x in W & W is open & f.:W c= V
proof
let V be Subset of REAL;
assume f.x in V & V is open; then
consider N1 being Neighbourhood of f.x such that
A13: N1 c= V by RCOMP_1:18;
consider N be Neighbourhood of x0 such that
A14: g.:N c= N1 by B11,FCONT_1:5,AS;
consider s be Real such that
A15: 0 < s & N = ]. x0-s,x0+s.[ by RCOMP_1:def 6;
A16: ]. x0-s,x0+s.[ is open by RCOMP_1:7;
B17: |. x0 - x0 .| = 0;
reconsider W0 = ]. x0-s,x0+s.[ as Subset of R^1;
W0 is open by A16,BORSUK_5:39; then
W0 in the topology of R^1 by PRE_TOPC:def 2; then
W0 /\ [#]X in the topology of X by PRE_TOPC:def 4; then
reconsider W= W0 /\ [#]X as open Subset of X by PRE_TOPC:def 2;
take W;
x in W0 & x in [#]X by B17,A15,RCOMP_1:1,AS;
hence x in W by XBOOLE_0:def 4;
thus W is open;
f.:W = g.:W0 by RELAT_1:112,A1,AS;
hence f.:W c= V by A13,A14,A15;
end;
end;
theorem Th80b:
for X be strict non empty SubSpace of R^1,
f be RealMap of X,
g be PartFunc of REAL,REAL
st g = f
holds
f is continuous iff g is continuous
proof
let X be strict non empty SubSpace of R^1,
f be RealMap of X,
g be PartFunc of REAL,REAL;
assume A1: g=f;
A2: dom g = the carrier of X by FUNCT_2:def 1,A1;
hereby
assume B3: f is continuous;
for x0 being Real st x0 in dom g holds g is_continuous_in x0
proof
let x0 be Real;
assume x0 in dom g; then
reconsider x=x0 as Point of X by FUNCT_2:def 1,A1;
for V be Subset of REAL st f.x in V & V is open holds
ex W be Subset of X st
x in W & W is open & f.: W c= V by B3,C0SP2:1;
hence g is_continuous_in x0 by A1,Th80a;
end;
hence g is continuous by FCONT_1:def 2;
end;
assume B5: g is continuous;
for x be Point of X
for V be Subset of REAL st f.x in V & V is open holds
ex W be Subset of X st
x in W & W is open & f.:W c= V
proof
let x be Point of X;
let V be Subset of REAL;
assume A6: f.x in V & V is open;
reconsider x0=x as Real;
g is_continuous_in x0 by B5,FCONT_1:def 2,A2;
hence ex W be Subset of X st
x in W & W is open & f.: W c= V by A1,A6,Th80a;
end;
hence f is continuous by C0SP2:1;
end;
theorem Lm1:
for A be non empty closed_interval Subset of REAL
holds the carrier of ClstoCmp(A) = A
proof
let A be non empty closed_interval Subset of REAL;
consider a,b be Real such that
A1: a <= b & [.a,b.] = A
& ClstoCmp(A) = Closed-Interval-TSpace(a,b) by Def7ClstoCmp;
thus the carrier of ClstoCmp(A) = A by A1,TOPMETR:10;
end;
theorem Th80:
for A be non empty closed_interval Subset of REAL,
u be Function
holds
( u is Point of
R_Normed_Algebra_of_ContinuousFunctions(ClstoCmp(A))
iff
dom u = A & u is continuous PartFunc of REAL,REAL )
proof
let A be non empty closed_interval Subset of REAL,
u be Function;
consider a,b be Real such that
A1: a <= b & [.a,b.] = A
& ClstoCmp(A) = Closed-Interval-TSpace (a,b) by Def7ClstoCmp;
hereby
assume u is Point of
R_Normed_Algebra_of_ContinuousFunctions(ClstoCmp(A)); then
u in ContinuousFunctions ClstoCmp(A); then
consider w be continuous RealMap of ClstoCmp(A) such that
A2: u = w;
B3: dom w = the carrier of ClstoCmp(A) by FUNCT_2:def 1; then
dom w = A by Lm1; then
dom w c= REAL & rng w c= REAL; then
reconsider v=w as PartFunc of REAL,REAL by RELSET_1:4;
v is continuous PartFunc of REAL,REAL by A1,Th80b;
hence dom u = A & u is continuous PartFunc of REAL,REAL by A2,B3,Lm1;
end;
assume
A4: dom u = A & u is continuous PartFunc of REAL,REAL; then
A5: dom u = the carrier of ClstoCmp(A) by Lm1;
rng u c= REAL by A4,RELAT_1:def 19; then
reconsider v=u as RealMap of ClstoCmp(A) by A5,FUNCT_2:2;
v is continuous by A1,A4,Th80b; then
v in the carrier of R_Normed_Algebra_of_ContinuousFunctions(ClstoCmp(A));
hence u is Point of
R_Normed_Algebra_of_ContinuousFunctions(ClstoCmp(A));
end;
theorem Lm2:
for A be non empty closed_interval Subset of REAL,
v be Point of
R_Normed_Algebra_of_ContinuousFunctions ClstoCmp(A)
holds
v in BoundedFunctions the carrier of ClstoCmp(A)
proof
let A be non empty closed_interval Subset of REAL,
v be Point of
R_Normed_Algebra_of_ContinuousFunctions(ClstoCmp(A));
set AV = the carrier of ClstoCmp(A);
R_Algebra_of_ContinuousFunctions ClstoCmp(A) is
Subalgebra of R_Algebra_of_BoundedFunctions(AV) by C0SP2:9; then
A1: the carrier of
R_Algebra_of_ContinuousFunctions ClstoCmp(A) c=
the carrier of
R_Algebra_of_BoundedFunctions(AV) by C0SP1:def 9;
v in the carrier of
R_Algebra_of_ContinuousFunctions ClstoCmp(A);
hence v in BoundedFunctions(AV) by A1;
end;
begin :: Preliminaries
theorem LM83:
for A be non empty closed_interval Subset of REAL,
a,b be Real st A=[.a,b.]
ex x be Function of A, BoundedFunctions(A)
st for s be Real st s in [.a,b.]
holds
(s = a implies x.s = [.a,b.] --> 0)
&
(s <> a implies x.s = ([.a,s.] --> 1) +* (].s,b.] --> 0))
proof
let A be non empty closed_interval Subset of REAL,
a,b be Real;
assume
A2: A = [.a,b.];
defpred C[object] means $1 = a;
deffunc F(object) = [.a,b.] --> 0;
deffunc G(object) = ([.a,In($1,REAL) .] --> 1)
+* (].In($1,REAL),b.] --> 0);
set B = BoundedFunctions(A);
A3: for s being object st s in [.a,b.]
holds (C[s] implies F(s) in B) & (not C[s] implies G(s) in B)
proof
let s be object;
assume A4: s in [.a,b.]; then
reconsider r=s as Real;
thus C[s] implies F(s) in B
proof
assume C[s];
set f1 = [.a,b.] --> 0;
A7: dom f1 = A by A2,FUNCOP_1:13;
rng f1 c= REAL; then
reconsider f = [.a,b.] --> 0 as Function of A,REAL by A7,FUNCT_2:2;
reconsider r0=0 as Real;
for r be ExtReal st r in PreNorms f holds r <= r0
proof
let r be ExtReal;
assume r in PreNorms f; then
consider t be Element of A such that
A8: r = |.f.t.|;
f.t = 0 by A2,FUNCOP_1:7;
hence r <= r0 by A8;
end; then
r0 is UpperBound of PreNorms f by XXREAL_2:def 1; then
PreNorms f is bounded_above by XXREAL_2:def 10; then
f|A is bounded by C0SP1:18;
hence F(s) in B;
end;
G(s) in B
proof
set g1 = [.a,In(s,REAL) .] --> 1;
set g2 = ].In(s,REAL),b.] --> 0;
B9: a <= r & r <= b by A4,XXREAL_1:1;
A10: dom g1 = [.a,In(s,REAL).] & dom g2 = ].In(s,REAL),b.]
by FUNCOP_1:13; then
A11: dom g1 \/ dom g2 = A by A2,B9,XXREAL_1:167; then
A12: dom(g1+*g2) = A by FUNCT_4:def 1;
rng(g1+*g2) c= REAL; then
reconsider f = ([.a,In(s,REAL) .] --> 1) +* (].In(s,REAL),b.] --> 0)
as Function of A,REAL by A12,FUNCT_2:2;
reconsider r0=1 as Real;
for c being object st c in dom g1 /\ dom f holds |.f.c.|<=r0
proof
let c be object;
assume c in dom g1 /\ dom f; then
A16: c in dom g1 by FUNCT_4:10,XBOOLE_1:28; then
|.g1.c.| = 1 by FUNCOP_1:7; then
|. (f|dom g1).c.| = 1 by FUNCT_4:33,A10,XXREAL_1:90;
hence |.f.c.| <= r0 by A16,FUNCT_1:49;
end; then
A17: f|(dom g1) is bounded by RFUNCT_1:73;
reconsider s0=0 as Real;
for c being object st c in dom g2 /\ dom f holds |.f.c.|<=s0
proof
let c be object;
assume c in dom g2 /\ dom f; then
A18: c in dom g2 by FUNCT_4:10,XBOOLE_1:28; then
|.g2.c.| = 0 by FUNCOP_1:7; then
|. (f|dom g2).c.| = 0 by FUNCT_4:23;
hence |.f.c.| <= s0 by A18,FUNCT_1:49;
end; then
f|(dom g2) is bounded by RFUNCT_1:73; then
f|A is bounded by A11,A17,RFUNCT_1:87;
hence G(s) in B;
end;
hence thesis;
end;
consider x being Function of [.a,b.], B such that
A19: for s being object st s in [.a,b.]
holds (C[s] implies x.s = F(s))
& ( not C[s] implies x.s = G(s)) from FUNCT_2:sch 5(A3);
reconsider x as Function of A,B by A2;
take x;
for s be Real st s in [.a,b.] holds
(s = a implies x.s = [.a,b.] --> 0)
&
(s <> a implies x.s = ([.a,s.] --> 1) +* (].s,b.] --> 0 ))
proof
let s be Real;
assume A20: s in [.a,b.];
In(s,REAL) = s;
hence thesis by A19,A20;
end;
hence thesis;
end;
definition
let A be non empty closed_interval Subset of REAL,
D be Division of A,
m be Function of A, BoundedFunctions(A),
i be Nat;
assume
A1: i in Seg(len D + 1);
func Dp1(m,D,i) -> Point of
R_Normed_Algebra_of_BoundedFunctions
the carrier of ClstoCmp(A) equals
:defDp1:
m.(lower_bound A) if i=1
otherwise m.(D.(i-1));
coherence
proof
set V = R_Normed_Algebra_of_BoundedFunctions the carrier of ClstoCmp(A);
hereby assume i=1;
thus m.(lower_bound A) is Point of
R_Normed_Algebra_of_BoundedFunctions
the carrier of ClstoCmp(A)
proof
set f = m.(lower_bound A);
consider a,b be Real such that
A2: a <= b & A = [.a,b.] by MEASURE5:14;
A = [.lower_bound A,upper_bound A.] by INTEGRA1:4; then
A3: lower_bound A = a by A2,INTEGRA1:5;
lower_bound A in A by A2,A3; then
f in BoundedFunctions(A) by FUNCT_2:5;
hence thesis by Lm1;
end;
end;
assume
A5: i<>1;
set f = m.(D.(i-1));
A6: 1 <= i <= len D + 1 by A1,FINSEQ_1:1; then
A7: i - 1 <= len D + 1 - 1 by XREAL_1:9;
reconsider i1 = i - 1 as Nat by A6,INT_1:5,ORDINAL1:def 12;
1 < i by A5,A6,XXREAL_0:1; then
1 - 1 < i1 by XREAL_1:14; then
1 <= i1 by NAT_1:14; then
i - 1 in dom D by FINSEQ_3:25,A7; then
f in BoundedFunctions(A) by FUNCT_2:5,INTEGRA1:6;
hence thesis by Lm1;
end;
correctness;
end;
definition
let A be non empty closed_interval Subset of REAL,
D be Division of A,
rho be Function of A, REAL,
i be Nat;
::: assume i in Seg(len D + 1);
func Dp2(rho,D,i) -> Real equals
:defDp2:
rho.(lower_bound A) if i=1
otherwise rho.(D.(i-1));
correctness;
end;
theorem LM84:
for A be non empty closed_interval Subset of REAL,
D be Division of A,
m be Function of A, BoundedFunctions(A),
rho be Function of A,REAL
ex s be FinSequence of
R_Normed_Algebra_of_BoundedFunctions
the carrier of ClstoCmp(A)
st len s = len D
& for i be 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))
proof
let A be non empty closed_interval Subset of REAL,
D be Division of A,
m be Function of A, BoundedFunctions(A),
rho be Function of A,REAL;
set V = R_Normed_Algebra_of_BoundedFunctions the carrier of ClstoCmp(A);
defpred P[Nat,set] means
$2 = sgn(Dp2(rho,D,$1+1) - Dp2(rho,D,$1) )
* ( Dp1(m,D,$1+1) - Dp1(m,D,$1) );
A0: for i be Nat st i in Seg len D
ex x be Element of the carrier of V st P[i,x];
consider s be FinSequence of V such that
A1: dom s = Seg len D
& for i be Nat st i in Seg len D holds P[i,s.i]
from FINSEQ_1:sch 5(A0);
take s;
thus thesis by A1,FINSEQ_1:def 3;
end;
theorem LM87:
for V be RealLinearSpace,
f be Functional of V,
s be FinSequence of V
st f is additive
holds f.(Sum s) = Sum(f*s)
proof
let V be RealLinearSpace,
f be Functional of V,
s be FinSequence of V;
assume A1: f is additive;
defpred P[Nat] means
for V be RealLinearSpace,
f be Functional of V,
s be FinSequence of V
st len s = $1 & f is additive
holds f.(Sum s) = Sum (f*s);
A2: P[0]
proof
let V be RealLinearSpace,
f be Functional of V,
s be FinSequence of V;
assume that
A3: len s = 0 and
A4: f is additive;
B5: Sum s = 0.V by A3,RLVECT_1:75;
dom f = the carrier of V by FUNCT_2:def 1; then
rng s c= dom f; then
dom(f*s) = dom s by RELAT_1:27
.= Seg len s by FINSEQ_1:def 3; then
len (f*s) = 0 by A3,FINSEQ_1:def 3; then
f*s = <*>REAL;
hence thesis by B5,A4,HAHNBAN:20,RVSUM_1:72;
end;
A6: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A7: P[n];
let V be RealLinearSpace,
f be Functional of V,
s be FinSequence of V;
assume that
A8: len s = n+1 and
A9: f is additive;
set s0=s|n, p=f*s;
B10: dom s = Seg(n+1) by A8,FINSEQ_1:def 3; then
s.(n+1) in rng s by FUNCT_1:3,FINSEQ_1:4; then
reconsider v=s.(n+1) as Point of V;
A11: n = len s0 by A8,FINSEQ_1:59,NAT_1:11; then
B12: s0 = s | dom s0 by FINSEQ_1:def 3;
A13: f.(s.(n+1)) = (f*s).(n+1) by B10,FINSEQ_1:4,FUNCT_1:13;
A15: f.(Sum s) = f.(Sum s0 + v) by B12,A8,A11,RLVECT_1:38
.= f.(Sum s0) + f.(s.(n+1)) by A9,HAHNBAN:def 2
.= Sum(f*s0) + p.(n+1) by A13,A7,A9,A11;
dom f = the carrier of V by FUNCT_2:def 1; then
rng s c= dom f; then
B18: dom(f*s) = dom s by RELAT_1:27
.= Seg len s by FINSEQ_1:def 3; then
A17: len (f*s) = n+1 by A8,FINSEQ_1:def 3;
A18: 1 <= n+1 <= len p by NAT_1:11,B18,A8,FINSEQ_1:def 3;
p = (p|n)^<*p/.(n+1)*> by A17,FINSEQ_5:21; then
p = (p|n)^<*p.(n+1)*> by A18,FINSEQ_4:15; then
Sum p = Sum(p|n) + p.(n+1) by RVSUM_1:74;
hence thesis by A15,RELAT_1:83;
end;
A19: for n be Nat holds P[n] from NAT_1:sch 2(A2,A6);
len s is Nat;
hence thesis by A1,A19;
end;
theorem LM88:
for A be non empty set,
x be Element of R_Normed_Algebra_of_BoundedFunctions(A)
holds x is Function of A,REAL
proof
let A be non empty set,
x be Element of R_Normed_Algebra_of_BoundedFunctions(A);
x is Element of BoundedFunctions(A); then
x is Element of Funcs(A,REAL);
hence thesis;
end;
theorem LM89:
for A be non empty closed_interval Subset of REAL,
s be FinSequence of
R_Normed_Algebra_of_BoundedFunctions
the carrier of ClstoCmp(A),
z be FinSequence of REAL,
g be Function of A,REAL,
t be Element of A
st len s = len z
& g = Sum s
& for k be Nat st k in dom z
holds ex sk be Function of A,REAL st
sk = s.k & z.k = sk.t
holds g.t = Sum z
proof
let A be non empty closed_interval Subset of REAL,
s be FinSequence of
R_Normed_Algebra_of_BoundedFunctions
the carrier of ClstoCmp(A),
z be FinSequence of REAL,
g be Function of A,REAL,
t be Element of A;
assume
A1: len s = len z & g = Sum s &
for k be Nat st k in dom z holds
ex sk be Function of A,REAL st
sk = s.k & z.k = sk.t;
defpred P[Nat] means
for A be non empty closed_interval Subset of REAL,
s be FinSequence of
R_Normed_Algebra_of_BoundedFunctions
the carrier of ClstoCmp(A),
z be FinSequence of REAL,
g be Function of A,REAL,
t be Element of A
st len s = $1 & len s = len z
& g = Sum s
& for k be Nat st k in dom z holds
ex sk be Function of A,REAL st
sk = s.k & z.k = sk.t
holds g.t = Sum z;
A2: P[0]
proof
let A be non empty closed_interval Subset of REAL,
s be FinSequence of
R_Normed_Algebra_of_BoundedFunctions
the carrier of ClstoCmp(A),
z be FinSequence of REAL,
g be Function of A,REAL,
t be Element of A;
assume that
A3: len s = 0 and
A4: len s = len z and
A5: g = Sum s and
for k be Nat st k in dom z holds
ex sk be Function of A,REAL st
sk = s.k & z.k = sk.t;
set V = R_Normed_Algebra_of_BoundedFunctions
the carrier of ClstoCmp(A);
set AV = the carrier of ClstoCmp(A);
B8: Sum s = 0.V by A3,RLVECT_1:75
.= AV -->0 by C0SP1:25
.= A -->0 by Lm1;
z = <*>REAL by A3,A4;
hence thesis by B8,FUNCOP_1:7,A5,RVSUM_1:72;
end;
A9: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A10: P[n];
let A be non empty closed_interval Subset of REAL,
s be FinSequence of
R_Normed_Algebra_of_BoundedFunctions
the carrier of ClstoCmp(A),
z be FinSequence of REAL,
g be Function of A,REAL,
t be Element of A;
assume that
A11: len s = n+1 and
A12: len s = len z and
A13: g = Sum s and
A14: for k be Nat st k in dom z holds
ex sk be Function of A,REAL st
sk = s.k & z.k = sk.t;
set V = R_Normed_Algebra_of_BoundedFunctions
the carrier of ClstoCmp(A);
set AV = the carrier of ClstoCmp(A);
A15: A = AV by Lm1;
set s0=s|n, z0=z|n;
A16: for k be Nat st k in dom z0 holds
ex sk be Function of A,REAL st
sk = s0.k & z0.k = sk.t
proof
let k be Nat;
assume k in dom z0; then
A17: k in Seg n & k in dom z by RELAT_1:57; then
consider sk be Function of A,REAL such that
A18: sk = s.k & z.k = sk.t by A14;
take sk;
thus thesis by A17,A18,FUNCT_1:49;
end;
dom z = Seg(n+1) by A11,A12,FINSEQ_1:def 3; then
consider sk be Function of A,REAL such that
A19: sk = s.(n+1) & z.(n+1) = sk.t by A14,FINSEQ_1:4;
A20: 1 <= n+1 <= len z by A11,A12,NAT_1:11;
z = (z|n)^<*z/.(n+1)*> by A11,A12,FINSEQ_5:21; then
B21: z = (z|n)^<*z.(n+1)*> by A20,FINSEQ_4:15;
Sum s0 is
Point of R_Normed_Algebra_of_BoundedFunctions(A) by Lm1; then
reconsider g1=Sum s0 as Function of A,REAL by LM88;
dom s = Seg(n+1) by A11,FINSEQ_1:def 3; then
s.(n+1) in rng s by FUNCT_1:3,FINSEQ_1:4; then
reconsider v=s.(n+1) as Point of V;
v is Point of R_Normed_Algebra_of_BoundedFunctions(A) by Lm1; then
reconsider v1=v as Function of A,REAL by LM88;
A23: n = len s0 & n = len z0 by A11,A12,FINSEQ_1:59,NAT_1:11; then
s0 = s | dom s0 by FINSEQ_1:def 3; then
A24: Sum s = Sum s0 + v by A11,A23,RLVECT_1:38;
Sum s is Point of R_Normed_Algebra_of_BoundedFunctions(A) by Lm1; then
reconsider g0=Sum s as Function of A,REAL by LM88;
A25: g0.t = g1.t + sk.t by A19,A15,A24,C0SP1:29;
g1.t = Sum z0 by A10,A16,A23;
hence g.t = Sum z by A13,A25,B21,A19,RVSUM_1:74;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A2,A9);
hence thesis by A1;
end;
theorem LM94:
for A be non empty closed_interval Subset of REAL,
D be Division of A,
t be Element of A
st lower_bound A < D.1 holds
ex i be Element of NAT st
i in dom D
& t in divset(D,i)
& ( i = 1 or
(lower_bound divset(D,i) < t
& t <= (upper_bound divset(D,i)) ) )
proof
let A be non empty closed_interval Subset of REAL,
D be Division of A,
t be Element of A;
assume AS: lower_bound A < D.1;
consider i be Element of NAT such that
A24: i in dom D and
A25: t in divset(D,i) by INTEGRA3:3;
per cases;
suppose i = 1;
hence thesis by A24,A25;
end;
suppose A26: i <> 1;
t in [.(lower_bound divset(D,i)),(upper_bound divset(D,i)).]
by A25,INTEGRA1:4; then
A30: (lower_bound divset(D,i)) <= t
& t <= (upper_bound divset(D,i)) by XXREAL_1:1;
thus ex i be Element of NAT st
i in dom D
& t in divset(D,i)
& ( i = 1 or
(lower_bound divset(D,i) < t
& t <= (upper_bound divset(D,i)) ) )
proof
per cases;
suppose not lower_bound divset(D,i) = t; then
lower_bound divset(D,i) < t by A30,XXREAL_0:1;
hence thesis by A24,A25,A30;
end;
suppose A31: lower_bound divset(D,i) = t;
A38: i-1 in dom D by A24,A26,INTEGRA1:7;
reconsider j = i- 1 as Element of NAT by A24,A26,INTEGRA1:7;
A40: t = upper_bound divset(D,j) & t in divset(D,j)
proof
j = 1 or j <> 1; then
upper_bound divset(D,j) = D.(i-1) by A38,INTEGRA1:def 4;
hence
A41: t = upper_bound divset(D,j) by A31,A24,A26,INTEGRA1:def 4;
(lower_bound divset(D,j))
<= (upper_bound divset(D,j)) by SEQ_4:11; then
t in [.(lower_bound divset(D,j)),
(upper_bound divset(D,j)).] by A41;
hence thesis by INTEGRA1:4;
end;
lower_bound divset(D,j) < upper_bound divset(D,j)
proof
per cases;
suppose A42: j = 1; then
lower_bound divset(D,j)= lower_bound A
& upper_bound divset(D,j) = D.j by A38,INTEGRA1:def 4;
hence thesis by AS,A42;
end;
suppose A44: j <> 1; then
A45: ( lower_bound divset(D,j) = D.(j - 1)
& upper_bound divset(D,j) = D.j) by A38,INTEGRA1:def 4;
j-1 in dom D by A38,A44,INTEGRA1:7;
hence thesis by A45,A38,XREAL_1:146,VALUED_0:def 13;
end;
end;
hence thesis by A38,A40;
end;
end;
end;
end;
LM95A:
for A be non empty closed_interval Subset of REAL,
D be Division of A
st 0 < vol A & D.1 = lower_bound A
holds D /^ 1 is Division of A
proof
let A be non empty closed_interval Subset of REAL,
D be Division of A;
assume A1: 0 < vol A & D.1 = lower_bound A;
0 < len D; then
A2: 0 + 1 <= len D by NAT_1:13;
1 <> len D
proof
assume 1=len D; then
D.1 = upper_bound A by INTEGRA1:def 2;
hence contradiction by A1;
end; then
1 < len D by A2,XXREAL_0:1; then
1+1 <= len D by NAT_1:13; then
A5: 1+1 -1 <= len D - 1 by XREAL_1:9;
A6: len D - 1 = len (D /^ 1) by A2,RFINSEQ:def 1;
A8: len (D /^ 1) <> 0 by A5,RFINSEQ:def 1,A2; then
len (D /^ 1) in Seg len (D /^ 1) by FINSEQ_1:3; then
A9: len (D /^ 1) in dom (D /^ 1) by FINSEQ_1:def 3;
for e1, e2 being Nat
st e1 in dom (D /^ 1) & e2 in dom (D /^ 1) & e1 < e2
holds (D /^ 1).e1 < (D /^ 1).e2
proof
let e1,e2 be Nat;
assume A10: e1 in dom (D /^ 1) & e2 in dom (D /^ 1) & e1 < e2; then
A11: (D /^ 1).e1 = D.(e1+1) & (D /^ 1).e2 = D.(e2+1)
by A2,RFINSEQ:def 1;
1 <= e1 & e1 <= len (D /^ 1) by A10,FINSEQ_3:25; then
1 + 0 <= e1 + 1 <= len (D /^ 1) + 1 by XREAL_1:7; then
A14: e1 + 1 in dom D by A6,FINSEQ_3:25;
1 <= e2 <= len (D /^ 1) by A10,FINSEQ_3:25; then
1 + 0 <= e2 + 1 & e2 + 1 <= len(D /^ 1) + 1 by XREAL_1:7; then
A15: e2 + 1 in dom D by FINSEQ_3:25,A6;
e1 + 1 < e2 + 1 by A10,XREAL_1:8;
hence thesis by A11,A14,A15,VALUED_0:def 13;
end; then
A16: (D /^ 1) is increasing;
A17: len (D /^ 1) = (len D) - 1 by A2,RFINSEQ:def 1;
B23: for x be object st x in rng (D /^ 1) holds x in rng D
proof
let x be object;
assume x in rng (D /^ 1); then
consider m being Nat such that
A18: m in dom (D /^ 1) and
A19: (D /^ 1).m = x by FINSEQ_2:10;
B20: m <= len (D /^ 1) by A18,FINSEQ_3:25;
1 <= m + 1 by NAT_1:11; then
A22: m + 1 in dom D by B20,A17,XREAL_1:19,FINSEQ_3:25;
(D /^ 1).m = D.(m + 1) by A2,A18,RFINSEQ:def 1;
hence x in rng D by A19,A22,FUNCT_1:def 3;
end;
rng D c= A by INTEGRA1:def 2; then
A24: rng (D /^ 1) c= A by B23;
A25: (D /^ 1).(len (D /^ 1))
= D.(len (D /^ 1) + 1) by A2,A9,RFINSEQ:def 1
.= D.(len D - 1 +1) by A2,RFINSEQ:def 1
.= upper_bound A by INTEGRA1:def 2;
D /^ 1 <> {} by A8;
hence thesis by A16,A24,A25,INTEGRA1:def 2;
end;
LM95B:
for A be non empty closed_interval Subset of REAL,
D be Division of A
st 0 < vol A & D.1 = lower_bound A
holds lower_bound A < (D /^ 1).1
proof
let A be non empty closed_interval Subset of REAL,
D be Division of A;
assume A1: 0 < vol A & D.1 = lower_bound A;
0 < len D; then
A2: 0 + 1 <= len D by NAT_1:13;
1 <> len D
proof
assume 1=len D; then
D.1 = upper_bound A by INTEGRA1:def 2;
hence contradiction by A1;
end; then
1 < len D by A2,XXREAL_0:1; then
A4: 1+1 <= len D by NAT_1:13; then
A5: 1+1 -1 <= len D - 1 by XREAL_1:9;
1 <= len (D /^ 1) by A5,A2,RFINSEQ:def 1; then
1 in dom (D /^ 1) by FINSEQ_3:25; then
A9: (D /^ 1).1 = D.(1+1) by A2,RFINSEQ:def 1;
A10: 1 in dom D by FINSEQ_3:25,A2;
2 in dom D by A4,FINSEQ_3:25;
hence thesis by A1,A9,A10,VALUED_0:def 13;
end;
LM95C:
for A be non empty closed_interval Subset of REAL,
D,E be Division of A,
rho be Function of A,REAL,
K be var_volume of rho,D,
L be var_volume of rho,E
st 0 < vol A & D.1 = lower_bound A & E = D /^ 1
holds Sum K = Sum L
proof
let A be non empty closed_interval Subset of REAL,
D,E be Division of A,
rho be Function of A,REAL,
K be var_volume of rho,D,
L be var_volume of rho,E;
assume A1: 0 < vol A & D.1 = lower_bound A & E = D /^ 1;
0 < len D; then
A4: 0 + 1 <= len D by NAT_1:13;
A9: len K = len D -1 + 1 by INTEGR22:def 2
.= len E + 1 by A1,A4,RFINSEQ:def 1
.= len <*0*> + len E by FINSEQ_1:40
.= len <*0*> + len L by INTEGR22:def 2;
A10: dom K = Seg (len <*0*> + len L) by A9,FINSEQ_1:def 3;
A11: for i being Nat st i in dom <*0*>
holds K.i = (<*0*>).i
proof
let i be Nat;
assume i in dom <*0*>; then
i in Seg len <*0*> by FINSEQ_1:def 3; then
i in Seg 1 by FINSEQ_1:40; then
A13: i = 1 by FINSEQ_1:2,TARSKI:def 1; then
A14: i in dom D by FINSEQ_3:25,A4;
A16: vol (divset(D,i),rho)
= rho.(upper_bound divset(D,i))
- rho.(lower_bound divset(D,i)) by INTEGR22:def 1;
lower_bound divset(D,i) = lower_bound A
& upper_bound divset(D,i) = lower_bound A
by A1,A13,A14,INTEGRA1:def 4; then
K.i = |. 0 .| by A14,INTEGR22:def 2,A16
.= (<*0*>).i by A13;
hence thesis;
end;
for i being Nat st i in dom L
holds K.((len<*0*>) + i) = L.i
proof
let i be Nat;
assume a20: i in dom L; then
i in Seg len L by FINSEQ_1:def 3; then
i in Seg len E by INTEGR22:def 2; then
A22: i in dom E by FINSEQ_1:def 3;
A26: 1 <= i & i <= len L by a20,FINSEQ_3:25; then
1 + 0 <= i + 1 <= len L + 1 by XREAL_1:7; then
1 <= i+1 <= len K by A9,FINSEQ_1:40; then
i+1 in Seg len K; then
i+1 in Seg len D by INTEGR22:def 2; then
A29: i+1 in dom D by FINSEQ_1:def 3; then
A30: K.(i+1) = |. vol (divset(D,(i+1)),rho) .| by INTEGR22:def 2;
A31: vol (divset(D,(i+1)),rho)
= rho.(upper_bound divset(D,(i+1)))
- rho.(lower_bound divset(D,(i+1))) by INTEGR22:def 1;
upper_bound divset(D,(i+1)) = upper_bound divset(E,i)
& lower_bound divset(D,(i+1)) = lower_bound divset(E,i)
proof
per cases;
suppose A33: i = 1; then
B35: lower_bound divset(E,i) = lower_bound A
& upper_bound divset(E,i) = E.i by A22,INTEGRA1:def 4;
lower_bound divset(D,(i+1)) = D.(i+1 - 1)
& upper_bound divset(D,(i+1)) = D.(i+1)
by A29,INTEGRA1:def 4,A33;
hence
upper_bound divset(D,(i+1)) = upper_bound divset(E,i)
& lower_bound divset(D,(i+1)) = lower_bound divset(E,i)
by A33,B35,A1,A4,A22,RFINSEQ:def 1;
end;
suppose A36: i <> 1; then
A37: lower_bound divset(E,i) = E.(i-1)
& upper_bound divset(E,i) = E .i by A22,INTEGRA1:def 4;
1 < i by A26,A36,XXREAL_0:1; then
1+1 <= i & i <= len E by INTEGR22:def 2,A26,NAT_1:13; then
A39: 1+1 -1 <= i-1 & i-1 <= len E - 0 by XREAL_1:13;
i-1 is Nat by A26,INT_1:5,ORDINAL1:def 12; then
i-1 in dom E by FINSEQ_3:25,A39; then
A42: lower_bound divset(E,i) = D.(i-1+1)
& upper_bound divset(E,i) = D.(i+1)
by A1,A4,A22,A37,RFINSEQ:def 1;
1 + 0 < i + 1 by A26,XREAL_1:8; then
lower_bound divset(D,(i+1)) = D.(i+1-1)
& upper_bound divset(D,(i+1)) = D.(i+1) by A29,INTEGRA1:def 4;
hence
upper_bound divset(D,(i+1)) = upper_bound divset(E,i)
& lower_bound divset(D,(i+1)) = lower_bound divset(E,i) by A42;
end;
end; then
vol(divset(D,(i+1)),rho) = vol(divset(E,i),rho)
by INTEGR22:def 1,A31; then
K.(i+1) = L.i by A22,INTEGR22:def 2,A30;
hence thesis by FINSEQ_1:40;
end; then
K = <*0*>^L by A10,A11,FINSEQ_1:def 7;
hence Sum K = 0 + Sum L by RVSUM_1:76
.= Sum L;
end;
theorem LM95:
for A be non empty closed_interval Subset of REAL,
rho be Function of A,REAL,
B be Real
st 0 < vol A
holds
( for D be Division of A, K be var_volume of rho,D
st lower_bound A < D.1
holds Sum(K) <= B )
implies
( for D be Division of A, K be var_volume of rho,D
holds Sum(K) <= B )
proof
let A be non empty closed_interval Subset of REAL,
rho be Function of A,REAL,
B be Real;
assume A1: 0 < vol A;
assume
A2: for D be Division of A, K be var_volume of rho,D
st lower_bound A < D.1 holds Sum(K) <= B;
let D be Division of A, K be var_volume of rho,D;
1 <= len D by FINSEQ_1:20; then
1 in dom D by FINSEQ_3:25; then
D.1 in A by INTEGRA1:6; then
lower_bound A <= D.1 by SEQ_4:def 2; then
per cases by XXREAL_0:1;
suppose
lower_bound A < D.1;
hence Sum(K) <= B by A2;
end;
suppose A5: lower_bound A = D.1; then
reconsider E = D /^ 1 as Division of A by A1,LM95A;
A6: lower_bound A < E.1 by A1,A5,LM95B;
set L = the var_volume of rho,E;
Sum(L) <= B by A2,A6;
hence Sum(K) <= B by A1,A5,LM95C;
end;
end;
begin :: F. Riesz Theorem
theorem Lm83:
for A be non empty closed_interval Subset of REAL,
rho be Function of A,REAL,
f be Point of
DualSp (R_Normed_Algebra_of_ContinuousFunctions(ClstoCmp(A)))
st
rho is bounded_variation &
( for u be continuous PartFunc of REAL,REAL
st dom u = A holds f.u = integral(u,rho) )
holds ||. f .|| <= total_vd(rho)
proof
let A be non empty closed_interval Subset of REAL,
rho be Function of A,REAL,
f be Point of
DualSp (R_Normed_Algebra_of_ContinuousFunctions(ClstoCmp(A)));
assume that
A1: rho is bounded_variation and
A2: for u be continuous PartFunc of REAL,REAL
st dom u = A holds f.u = integral(u,rho);
set X = R_Normed_Algebra_of_ContinuousFunctions(ClstoCmp(A));
A3: for u be continuous PartFunc of REAL,REAL
st u in the carrier of X holds f.u = integral(u,rho)
proof
let u be continuous PartFunc of REAL,REAL;
assume u in the carrier of X; then
dom u = A & u is continuous PartFunc of REAL,REAL by Th80;
hence f.u = integral(u,rho) by A2;
end;
A4: for u be continuous PartFunc of REAL,REAL,
v be Point of X
st dom u = A & u=v holds
|. integral(u,rho) .| <= ||.v.|| * total_vd(rho)
proof
let u be continuous PartFunc of REAL,REAL,
v be Point of X;
assume A5: dom u = A & u=v; 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(S) .| is convergent by SEQ_4:13,B6,A7;
A10: for n be Nat holds
|. (middle_sum(S)).n .| <= ||.v.|| * total_vd(rho)
proof
let n be Nat;
set F = the var_volume of rho,T.n;
reconsider v0 = ||.v.|| as Real;
reconsider vF = v0*F as FinSequence of REAL;
dom F = Seg len F by FINSEQ_1:def 3; then
B14: dom vF = Seg len F by VALUED_1:def 5;
A15: len(S.n) = len(T.n) by A1,A5,INTEGR22:def 5
.= len F by INTEGR22:def 2
.= len vF by B14,FINSEQ_1:def 3;
for j be Nat st j in dom(S.n) holds |. (S.n).j .| <= (vF).j
proof
let j be Nat;
assume j in dom(S.n); then
B17: j in Seg len(S.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 be Real such that
A18: r in rng (u|divset(T.n,j)) and
A19: (S.n).j = r*(vol (divset(T.n,j),rho))
by A1,A5,INTEGR22:def 5,A16;
A20: |. (S.n).j .| = |.r.| * |. vol (divset(T.n,j),rho) .|
by COMPLEX1:65,A19
.= |.r.| * (F.j) by A16,INTEGR22:def 2;
consider x be 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(AV) by A5,Lm2; then
consider u1 be Function of AV,REAL such that
A23: u=u1 & u1| AV is bounded;
x in A by A5,A21,RELAT_1:57; then
reconsider x1=x as Element of AV by Lm1;
reconsider v1=v as Point of
R_Normed_Algebra_of_BoundedFunctions(AV) 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 F by INTEGR22:def 2; then
j in dom F by FINSEQ_1:def 3; then
0 <= F.j by INTEGR22:3; then
|.r.| * (F.j) <= v0 * (F.j) by A24,XREAL_1:64;
hence |. (S.n).j .| <= (vF).j by A20,VALUED_1:6;
end; then
|. Sum(S.n) .| <= Sum(vF) by A15,INTEGR23:3; then
A25: |. Sum(S.n) .| <= ||.v.|| * Sum(F) by RVSUM_1:87;
||.v.|| * Sum(F) <= ||.v.|| * total_vd(rho)
by A1,INTEGR22:5,XREAL_1:64; then
|. Sum(S.n) .| <= ||.v.|| * total_vd(rho) by A25,XXREAL_0:2;
hence thesis by INTEGR22:def 7;
end;
reconsider a = ||.v.|| * total_vd(rho) as Real;
now
let n be Nat;
|. (middle_sum(S)).n .| <= a by A10; then
|. (middle_sum(S)) .|.n <= a by SEQ_1:12;
hence |. (middle_sum(S)) .|.n <= (seq_const a).n by SEQ_1:57;
end; then
lim |. middle_sum(S) .| <= lim (seq_const a) by A9,SEQ_2:18; then
A27: |. lim (middle_sum(S)) .| <= 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 thesis by B6,A1,A5,INTEGR22:def 9,A7,A27;
end;
reconsider g=f as Lipschitzian linear-Functional of X by DUALSP01:def 10;
now
let k be Real;
assume k in PreNorms g;
then
consider u be Point of X such that
A28: k = |. g.u .| & ||.u.|| <= 1;
u in ContinuousFunctions(ClstoCmp(A)); then
ex v be continuous RealMap of ClstoCmp(A) st u=v; then
reconsider v=u as Function;
A29: dom v = A & v is continuous PartFunc of REAL,REAL by Th80;
reconsider v as continuous PartFunc of REAL,REAL by Th80;
|. integral(v,rho) .| <= ||.u.|| * total_vd(rho) by A4,A29; then
A30: |. g.u .| <= ||.u.|| * total_vd(rho) by A3;
0 <= total_vd(rho) by A1,INTEGR22:6; then
||.u.|| * total_vd(rho) <= 1 * total_vd(rho) by A28,XREAL_1:64;
hence k <= total_vd(rho) by A28,A30,XXREAL_0:2;
end; then
upper_bound PreNorms g <= total_vd(rho) by SEQ_4:45;
hence ||. f .|| <= total_vd(rho) by DUALSP01:24;
end;
theorem
for A be non empty closed_interval Subset of REAL,
x be Point of
DualSp R_Normed_Algebra_of_ContinuousFunctions ClstoCmp A
st 0 < vol A
holds
ex rho be Function of A,REAL st
rho is bounded_variation
&
( for u be continuous PartFunc of REAL,REAL
st dom u = A holds x.u = integral(u,rho) )
&
||.x.|| = total_vd(rho)
proof
let A be non empty closed_interval Subset of REAL,
x be Point of
DualSp R_Normed_Algebra_of_ContinuousFunctions ClstoCmp(A);
assume A1: 0 < vol A;
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: AV = A by Lm1;
R_Algebra_of_ContinuousFunctions ClstoCmp(A)
is Subalgebra of R_Algebra_of_BoundedFunctions AV by C0SP2:9; then
A3: the carrier of X c= the carrier of V
& the addF of X = (the addF of V) || the carrier of X
& the Mult of X = (the Mult of V) | [:REAL, the carrier of X:]
by C0SP1:def 9;
A4: 0.X = ClstoCmp(A) -->0 by C0SP2:12
.= 0.V by C0SP1:25;
B5: X is SubRealNormSpace of V by A3,A4,DUALSP01:def 16;
reconsider h=x as Lipschitzian linear-Functional of X by DUALSP01:def 10;
consider f be Lipschitzian linear-Functional of V, F be Point of DualSp V
such that
A6: f = F & f|(the carrier of X) = h & ||.F.||=||.x.|| by B5,DUALSP01:36;
consider a,b be Real such that
A7: a <= b & [.a,b.] = A
& ClstoCmp(A) = Closed-Interval-TSpace(a,b) by Def7ClstoCmp;
consider m be Function of A, BoundedFunctions(A) such that
A8: for s be 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 V = BoundedFunctions(A) by Lm1; then
reconsider rho = f*m as Function of A,REAL;
A9: for D be Division of A, K be var_volume of rho,D
st a < D.1 holds Sum(K) <= ||.x.||
proof
let D be Division of A, K be var_volume of rho,D;
assume A10: a < D.1;
consider s be FinSequence of V such that
A11: len s = len D and
A12: for i be 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);
yD in the carrier of V; then
yD in BoundedFunctions(A) by Lm1; then
consider g be Function of A,REAL such that
A13: g=yD & g|A is bounded;
A14: f.yD = Sum(f*s) by LM87;
A15: for t be Element of A holds |. g.t .| <= 1
proof
let t be Element of A;
defpred R1[Nat,set] means
ex sk be Function of A,REAL st
sk = s.$1 & $2 = sk.t;
A16: for k be Nat st k in Seg len D
ex x be Element of REAL st R1[k,x]
proof
let k be Nat;
assume k in Seg len D; 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 V; then
s.k in BoundedFunctions(A) by Lm1; then
consider sk be Function of A,REAL such that
A17: sk = s.k & sk|A is bounded;
take x = sk.t;
thus thesis by A17;
end;
consider z be FinSequence of REAL such that
A18: dom z = Seg len D
& for k be Nat st k in Seg len D holds R1[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 be 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 as Nat;
A54: i in Seg len D by A50,FINSEQ_1:def 3; then
consider si be 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 <= 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 = r
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 f0 = [.a,b.] &
dom g1 = [.a,D.i .] & dom g2 = ]. D.i,b.] &
dom h1 = [.a,D.(i-1) .] & dom h2 = ]. D.(i-1),b.] by FUNCOP_1:13;
per cases;
suppose A62: i = 1;
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 f0 = A by A7,FUNCOP_1:13;
A73: a <= D.i & D.i <= b by A65,XXREAL_1:1;
A74: dom f1 = dom g1 \/ dom g2 by FUNCT_4:def 1
.= A by A7,B0,A73,XXREAL_1:167;
rng f0 c= REAL; then
reconsider f0 as Function of A,REAL by A72,FUNCT_2:2;
rng f1 c= REAL; then
reconsider f1 as Function of A,REAL by A74,FUNCT_2:2;
A76: si.t = r * (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 = r * (Dp1(m,D,i+1) - Dp1(m,D,i)) by A55,B56,A12; then
si = r * H by Lm1; then
si.t = r * (h.t) by C0SP1:30
.= r * (f1.t - f0.t) by A2,A69,A70,C0SP1:34;
hence thesis;
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 thesis by A55,A76,A79;
end;
suppose A80: i <> 1; 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; then
per cases by XXREAL_1:2;
suppose A88: a = D.(i-1);
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 f0 = A by A7,FUNCOP_1:13;
A94: a <= D.i & D.i <= b by A81,XXREAL_1:1;
A96: dom f1 = dom g1 \/ dom g2 by FUNCT_4:def 1
.= A by A7,B0,A94,XXREAL_1:167;
rng f0 c= REAL; then
reconsider f0 as Function of A,REAL by A93,FUNCT_2:2;
rng f1 c= REAL; then
reconsider f1 as Function of A,REAL by A96,FUNCT_2:2;
A98: si.t = r * (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 = r * (Dp1(m,D,i+1) - Dp1(m,D,i)) by A55,B56,A12; then
si = r * H by Lm1; then
si.t = r * (h.t) by C0SP1:30
.= r * (f1.t - f0.t) by A2,A90,A91,C0SP1:34;
hence thesis;
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 thesis by A55,A98,A102;
end;
suppose A103: a < D.(i-1);
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 <= b by A81,XXREAL_1:1;
A109: a <= D.(i-1) <= b by A82,XXREAL_1:1;
A110: dom f1 = dom g1 \/ dom g2 by FUNCT_4:def 1
.= A by A7,B0,A108,XXREAL_1:167;
A111: dom f2 = dom h1 \/ dom h2 by FUNCT_4:def 1
.= A by A7,B0,A109,XXREAL_1:167;
rng f1 c= REAL; then
reconsider f1 as Function of A,REAL by A110,FUNCT_2:2;
rng f2 c= REAL; then
reconsider f2 as Function of A,REAL by A111,FUNCT_2:2;
A112: a <= t & t <= b by XXREAL_1:1,A7;
A113: si.t = r * (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 = r * (Dp1(m,D,i+1) - Dp1(m,D,i)) by A55,B56,A12; then
si = r * H by Lm1; then
si.t = r * (h.t) by C0SP1:30
.= r * (f1.t - f2.t) by A2,A105,A106,C0SP1:34;
hence thesis;
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 thesis by A55,A113,A117;
end;
end;
end; then
A119: |.z.i.| <= 1 by LM91;
for k be Nat st k in dom z & k <> i holds z.k = 0
proof
let k be Nat;
assume that
A120: k in dom z and
A121: k <> i;
consider sk be 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 <= 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 f0 = [.a,b.] &
dom g1 = [.a,D.k .] & dom g2 = ]. D.k,b.] &
dom h1 = [.a,D.(k-1) .] & dom h2 = ]. D.(k-1),b.] by FUNCOP_1:13;
per cases;
suppose A130: k = 1; 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 f0 = A by A7,FUNCOP_1:13;
A148: dom f1 = dom g1 \/ dom g2 by FUNCT_4:def 1
.= A by A7,B10,A147,XXREAL_1:167;
rng f0 c= REAL; then
reconsider f0 as Function of A,REAL by A146,FUNCT_2:2;
rng f1 c= REAL; then
reconsider f1 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 = r * (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 = r * (Dp1(m,D,k+1) - Dp1(m,D,k)) by A124,B125,A12; then
sk = r * H by Lm1; then
sk.t = r * (h.t) by C0SP1:30
.= r * (f1.t - f0.t) by A2,A144,A153,C0SP1:34;
hence thesis;
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)
proof
k = i-1 or k < i-1 by A157,XXREAL_0:1;
hence thesis by A126,A136,VALUED_0:def 13;
end; 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 thesis by A124,A154,A162;
end;
suppose A163: k <> 1; 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)
proof
1 = k -1 or 1 < k -1 by A171,XXREAL_0:1;
hence thesis by A168,A172,VALUED_0:def 13;
end; 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 f1 = dom g1 \/ dom g2 by FUNCT_4:def 1
.= A by A7,B10,A178,XXREAL_1:167;
A181: dom f2 = dom h1 \/ dom h2 by FUNCT_4:def 1
.= A by A7,B10,A179,XXREAL_1:167;
rng f1 c= REAL; then
reconsider f1 as Function of A,REAL by A180,FUNCT_2:2;
rng f2 c= REAL; then
reconsider f2 as Function of A,REAL by A181,FUNCT_2:2;
A183: sk.t = r * (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 = r * H by Lm1,A124,A125; then
sk.t = r * (h.t) by C0SP1:30
.= r * (f1.t - f2.t) by A2,A175,A176,C0SP1:34;
hence thesis;
end;
per cases by A121,XXREAL_0:1;
suppose i < k; 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)
proof
i = k -1 or i < k -1 by A186,XXREAL_0:1;
hence thesis by A50,A168,VALUED_0:def 13;
end;
A189: (upper_bound divset(D,i)) <=D.(k-1)
proof
per cases;
suppose i = 1;
hence (upper_bound divset(D,i)) <=D.(k-1)
by A187,A50,INTEGRA1:def 4;
end;
suppose i <> 1;
hence (upper_bound divset(D,i)) <=D.(k-1)
by A187,A50,INTEGRA1:def 4;
end;
end;
A191: a <= t <= D.(k-1)
by A189,XXREAL_0:2,A53,XXREAL_1:1,A7; then
A192: t in [.a,D.(k-1) .];
a <= 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 thesis by A124,A183,A196;
end;
suppose A198: k < i; 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)
proof
k = i-1 or k < i-1 by A201,XXREAL_0:1;
hence thesis by A126,A202,VALUED_0:def 13;
end; 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 thesis by A124,A183,A211;
end;
end;
end; then
|. Sum z .| <= 1 by A22,A50,A119,INTEGR23:6;
hence |. g.t .| <= 1 by A13,A20,LM89,A18;
end;
now
let k be Real;
assume k in PreNorms g; then
consider t be Element of A such that
A213: k = |.g.t.|;
thus k <= 1 by A15,A213;
end; then
upper_bound PreNorms g <= 1 by SEQ_4:45; then
(BoundedFunctionsNorm A).g <= 1 by A13,C0SP1:20; then
A214: ||.yD.|| <= 1 by A13,Lm1;
A215: len K = len D
& for i be Nat st i in dom D holds K.i = |. vol (divset(D,i),rho) .|
by INTEGR22:def 2;
dom f = the carrier of V 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 be Nat st i in dom D
holds (f*s).i = |. vol (divset(D,i),rho) .|
proof
let i be Nat;
assume A218: i in dom D; then
A220: 1 <= 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;
suppose A227: i = 1; 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.( r * ( Dp1(m,D,i+1) - Dp1(m,D,i) ) ) by A12,A223
.= r * f.( Dp1(m,D,i+1) - Dp1(m,D,i) ) by HAHNBAN:def 3
.= r * ( f.( Dp1(m,D,i+1) ) - f.( Dp1(m,D,i) ) )
by HAHNBAN:19
.= r * ( f.( m.(D.i) ) - f.( m.(lower_bound A) ))
by A229,A221,A227,defDp1
.= r * ( (f*m).(D.i) - f.( m.(lower_bound A) ) )
by A225,FUNCT_1:13
.= r * ( rho.(upper_bound divset(D,i))
- rho.(lower_bound divset(D,i)) )
by A228,A226,FUNCT_1:13
.= r * 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);
r = 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;
end;
suppose A234: i <> 1;
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.(r * ( Dp1(m,D,i+1) - Dp1(m,D,i) ) ) by A12,A223
.= r * f.( Dp1(m,D,i+1) - Dp1(m,D,i) ) by HAHNBAN:def 3
.= r * ( f.( Dp1(m,D,i+1) ) - f.( Dp1(m,D,i) ) )
by HAHNBAN:19
.= r * ( f.( m.(D.i)) - f.( m.(D.(i-1) ) ) )
by A239,A221,A234,defDp1
.= r * ( (f*m).(D.i) - f.( m.(D.(i-1)) ) )
by A235,FUNCT_1:13
.= r * ( rho.(upper_bound divset(D,i))
- rho.(lower_bound divset(D,i)) )
by A237,A236,FUNCT_1:13
.= r * 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);
r = 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;
end;
end;
for i be Nat st i in dom K holds (f*s).i = K.i
proof
let i be Nat;
assume i in dom K; then
i in Seg len D by A215,FINSEQ_1:def 3; then
A244: i in dom D by FINSEQ_1:def 3; then
K.i = |. vol (divset(D,i),rho) .| by INTEGR22:def 2;
hence thesis by A217,A244;
end; then
A245: f.yD = Sum(K) by A14,A216,FINSEQ_1:13;
A246: f.yD <= |.f.yD.| by ABSVALUE:4;
A247: |.f.yD.| <= ||.F.|| * ||.yD.|| by A6,DUALSP01:26;
||.F.|| * ||.yD.|| <= ||.F.|| * 1 by A214,XREAL_1:64; then
|.f.yD.| <= ||.F.|| by A247,XXREAL_0:2;
hence Sum(K) <= ||. x .|| by A6,A245,A246,XXREAL_0:2;
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 be Division of A, K be var_volume of rho,D
holds Sum(K) <= ||.x.|| by A1,A9,LM95; then
B250: for t be Division of A, F0 be var_volume of rho,t
holds Sum(F0) <= d by XREAL_1:39; then
A251: rho is bounded_variation; then
consider VD be non empty Subset of REAL such that
VD is bounded_above and
A253: VD = { r where r is Real:
ex t be Division of A, F0 be var_volume of rho,t st
r = Sum(F0) } and
A254: total_vd(rho) = upper_bound VD by INTEGR22:def 4;
now
let k be Real;
assume k in VD; then
consider r be Real such that
A255: k = r and
A256: ex t be Division of A, F0 be var_volume of rho,t st
r = Sum(F0) by A253;
consider t be Division of A, F0 be var_volume of rho,t such that
A257: r = Sum(F0) by A256;
thus k <= ||.x.|| by A249,A1,A9,LM95,A255,A257;
end; then
A258: total_vd(rho) <= ||.x.|| by A254,SEQ_4:45;
A259: for u be continuous PartFunc of REAL,REAL
st dom u = A holds x.u = integral(u,rho)
proof
let u be continuous PartFunc of REAL,REAL;
assume A260: dom u = A; then
A261: for r be Real st 0 < r
ex s be Real st
0 < s &
for x1,x2 be 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 be Nat holds a < (T.n).1
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 12; then
consider Tn being Division of A such that
A265: Tn divide_into_equal n + 1 & T.n = Tn by A263;
A266: len Tn = n+1 by A265,INTEGRA4:def 1;
n+1 in Seg (n+1) by FINSEQ_1:4; then
1 <= n+1 <= len Tn by FINSEQ_1:1,A265,INTEGRA4:def 1; then
1 <= len Tn by XXREAL_0:2; then
B268: 1 in dom Tn by FINSEQ_3:25;
0 < (vol A) / (len Tn) by A1,A266,XREAL_1:139; then
(lower_bound A) + 0 <
(lower_bound A) + (( (vol A) / (len Tn) ) * 1) by XREAL_1:8;
hence thesis by A265,A249,B268,INTEGRA4:def 1;
end;
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 P[Element of NAT, set] means
ex p being FinSequence of REAL st
p = $2 & len p = len (T.$1) & for i be Nat st i in dom (T.$1) holds
p.i in dom (u|divset((T.$1),i)) & ex z be Real st
z = (u|divset((T.$1),i)).(p.i) &
(S.$1).i = z * (vol (divset((T.$1),i),rho));
A270: for k be Element of NAT ex p be Element of (REAL)* st P[k, p]
proof
let k be Element of NAT;
defpred P1[Nat,set] means
$2 in dom (u|divset((T.k),$1)) &
ex c be Real st c = (u|divset((T.k),$1)).$2 &
(S.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 be Nat st i in Seg len (T.k)
ex x be Element of REAL st P1[i,x]
proof
let i be Nat;
assume i in Seg len(T.k); then
i in dom (T.k) by FINSEQ_1:def 3; then
consider c be Real such that
A273: c in rng (u|divset((T.k),i)) &
(S.k).i = c * (vol(divset((T.k),i),rho))
by A251,A260,INTEGR22:def 5;
consider x be 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 as Element of REAL by A274;
take x;
thus thesis by A273,A274;
end;
consider p be FinSequence of REAL such that
A275: dom p = Seg len(T.k)
& for i be Nat st i in Seg len(T.k) holds P1[i,p.i]
from FINSEQ_1:sch 5(A272);
take p;
len p = len (T.k) by A275,FINSEQ_1:def 3;
hence thesis by A271,A275,FINSEQ_1:def 11;
end;
consider F be sequence of (REAL)* such that
A276: for x be Element of NAT holds P[x, F.x] from FUNCT_2:sch 3(A270);
defpred Q[Element of NAT, object] means
ex q be FinSequence of V st
len q = len (T.$1) & $2=Sum q &
for i be Nat st i in dom (T.$1) holds
ex r be 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 be Element of NAT
ex x be Element of the carrier of V st Q[k,x]
proof
let k be Element of NAT;
defpred Q1[Nat,object] means
ex r be 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 be Nat st i in Seg len (T.k) ex y be Element of
the carrier of V st Q1[i,y]
proof
let i be Nat;
assume i in Seg len (T.k); 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 be Nat st i in dom (T.k) holds
p.i in dom (u|divset((T.k),i)) & ex z be Real st
z = (u|divset((T.k),i)).(p.i) &
(S.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 V;
hence thesis by A280,A279;
end;
consider q be FinSequence of V such that
A282: dom q = Seg len(T.k)
& for i be Nat st i in Seg len(T.k) holds Q1[i,q.i]
from FINSEQ_1:sch 5(A278);
take x=Sum q;
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 thesis by A282,A283;
end;
consider xD be sequence of V such that
A284: for z be Element of NAT holds Q[z,xD.z] from FUNCT_2:sch 3(A277);
B314: for n be Element of NAT holds (f*xD).n = (middle_sum(S)).n
proof
let n be Element of NAT;
consider p1 be FinSequence of REAL such that
A285: p1 = F.n & len p1 = len (T.n)
& for i be Nat st i in dom (T.n)
holds p1.i in dom (u|divset(T.n,i))
& ex z be Real st z = (u|divset(T.n,i)).(p1.i)
& (S.n).i = z * (vol (divset(T.n,i),rho)) by A276;
consider q1 be FinSequence of V such that
A286: len q1 = len (T.n) & xD.n = Sum q1 &
for i be Nat st i in dom (T.n) holds
ex r be 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(S)).n = Sum(S.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 V 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 (S.n) by A251,A260,A286,INTEGR22:def 5; then
A289: len (f*q1) = len (S.n) by FINSEQ_1:def 3;
for k be Nat st 1 <= k & k <= len (S.n) holds (f*q1).k = (S.n).k
proof
let k be Nat;
assume A290: 1 <= k & k <= len (S.n); then
B291: k in Seg len (S.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 be Real such that
A293: z = (u|divset(T.n,k)).((F.n).k)
& (S.n).k = z * (vol (divset(T.n,k),rho)) by A285;
consider r be 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 <= 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;
suppose A299: k = 1;
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
.= (S.n).k by A293,A294,A306,HAHNBAN:def 3;
end;
suppose A307: k <> 1;
(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
.= (S.n).k by A293,A294,A313,HAHNBAN:def 3;
end;
end;
hence thesis by A287,A288,A289,FINSEQ_1:14;
end;
A315: middle_sum(S) is convergent &
lim (middle_sum(S)) = 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 V by A269,Lm2;
v in BoundedFunctions(A) by A316,Lm1; then
consider g be Function of A,REAL such that
A317: g=v & g|A is bounded;
reconsider v0=v as Point of V;
A318: for r be Real st 0 < r ex m0 be Nat st
for n be Nat st m0 <= n holds ||. xD.n - v0 .|| < r
proof
let r be Real;
assume A319: 0 < r; then
A321: r/2 < r by XREAL_1:216;
consider s be Real such that
A322: 0 < s and
A323: for x1,x2 be 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 be Nat such that
A324: for i be Nat st m0 <= i holds |. (delta T).i - 0 .| < s
by A263,A322,SEQ_2:def 7;
A325: for n be Nat st m0 <= n holds ||. xD.n - v0 .|| < r
proof
let n be Nat;
A326: n in NAT by ORDINAL1:def 12;
consider p2 be FinSequence of REAL such that
A327: p2 = F.n & len p2 = len (T.n)
& for i be Nat st i in dom (T.n)
holds p2.i in dom (u|divset((T.n),i))
& ex z be Real st z = (u|divset((T.n),i)).(p2.i)
& (S.n).i = z * (vol (divset((T.n),i),rho)) by A276,A326;
consider q2 be FinSequence of V such that
A328: len q2 = len (T.n) & xD.n = Sum q2
& for i be Nat st i in dom (T.n) holds
ex r be 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; 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 V; then
xD.n in BoundedFunctions(A) by Lm1; then
consider g1 be Function of A,REAL such that
A330: g1=xD.n & g1|A is bounded;
A331: for t be Element of A, i be 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, i be Nat;
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)) );
consider r be 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 R2[Nat,set] means
ex qi be Function of A,REAL st
qi = q2.$1 & $2 = qi.t;
A340: for i be Nat st i in Seg len (T.n)
ex x be Element of REAL st R2[i,x]
proof
let i be Nat;
assume i in Seg len (T.n); then
i in dom (T.n) by FINSEQ_1:def 3; then
consider r be 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 V by A342; then
q2.i in BoundedFunctions(A) by Lm1; then
consider qi be Function of A,REAL such that
A343: qi = q2.i & qi|A is bounded;
take x = qi.t;
thus thesis by A343;
end;
consider z be FinSequence of REAL such that
A344: dom z = Seg len (T.n)
& for i be Nat st i in Seg len (T.n) holds R2[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 be 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(D,i)),(upper_bound divset(D,i)).]
by A333,INTEGRA1:4;
A354: 1 <= i & i <= len D by A350,FINSEQ_1:1; then
1 <= i & i + 0 <= len D + 1 by XREAL_1:7; then
A355: i in Seg (len D + 1);
1 + 0 <= i + 1 & i <= len D by A350,FINSEQ_1:1,XREAL_1:7; then
1 + 0 <= i + 1 <= len D + 1 by XREAL_1:7; then
A356: i + 1 in Seg (len D + 1);
A357: z.i = r
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;
B20: dom f0 = [.a,b.] &
dom g1 = [.a,D.i .] & dom g2 = ]. D.i,b.] &
dom h1 = [.a,D.(i-1) .] & dom h2 = ]. D.(i-1),b.]
by FUNCOP_1:13;
per cases;
suppose A358: i = 1;
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: D.i in [.a,b.] by A7,A332,INTEGRA1:6;
A362: lower_bound divset(D,i) = lower_bound A &
upper_bound divset(D,i) = D.i by A332,A358,INTEGRA1:def 4;
A364: a < D.i by A264,A358;
A365: Dp1(m,D,(i+1)) = m.(D.(i+1 -1)) by A356,defDp1,A358
.= ([.a,D.i .] --> 1) +* (]. D.i,b.] --> 0)
by A8,A361,A364;
A366: Dp1(m,D,i) = m.(lower_bound A) by A355,A358,defDp1
.= [.a,b.] -->0 by A8,A359,A360;
A368: dom f0 = A by A7,FUNCOP_1:13;
A369: a <= D.i & D.i <= b by A361,XXREAL_1:1;
A370: dom f1 = dom g1 \/ dom g2 by FUNCT_4:def 1
.= A by A7,B20,A369,XXREAL_1:167;
rng f0 c= REAL; then
reconsider f0 as Function of A,REAL by A368,FUNCT_2:2;
rng f1 c= REAL; then
reconsider f1 as Function of A,REAL by A370,FUNCT_2:2;
A372: qi.t = r * (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;
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 thesis;
end;
A373: t in [.a,D.i .] by A359,A362,INTEGRA1:4,A333; then
A375: f1.t = ([.a,D.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 thesis by A351,A372,A375;
end;
suppose A376: i <> 1; then
A378: D.(i-1) in [.a,b.] by A7,A332,INTEGRA1:7;
A377: D.i in [.a,b.] by A7,A332,INTEGRA1:6;
A379: lower_bound divset(D,i) = D.(i-1) &
upper_bound divset(D,i) = D.i by A332,A376,INTEGRA1:def 4;
i-1 in dom D by A332,A376,INTEGRA1:7; then
A382: D.(i-1) < D.i by A332,XREAL_1:146,VALUED_0:def 13;
D.(i-1) = a or D.(i-1) in ].a,b.]
by A376,A7,A332,INTEGRA1:7,XXREAL_1:6; then
per cases by XXREAL_1:2;
suppose A384: a = D.(i-1);
1 + 0 < i + 1 by XREAL_1:8,A354; then
A386: Dp1(m,D,(i+1)) = m.(D.(i+1 -1)) by A356,defDp1
.= ([.a,D.i .] --> 1) +* (]. D.i,b.] --> 0)
by A8,A377,A384,A382;
A387: Dp1(m,D,i) = m.(D.(i-1)) by A355,A376,defDp1
.= [.a,b.] -->0 by A8,A378,A384;
A389: dom f0 = A by A7,FUNCOP_1:13;
A390: a <= D.i & D.i <= b by A377,XXREAL_1:1;
A392: dom f1 = dom g1 \/ dom g2 by FUNCT_4:def 1
.= A by A7,B20,A390,XXREAL_1:167;
rng f0 c= REAL; then
reconsider f0 as Function of A,REAL by A389,FUNCT_2:2;
rng f1 c= REAL; then
reconsider f1 as Function of A,REAL by A392,FUNCT_2:2;
A394: qi.t = r * (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;
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 thesis;
end;
A395: t in [. D.(i-1),D.i .] by A379,INTEGRA1:4,A333;
a <= D.(i-1) & D.(i-1) <= b by A378,XXREAL_1:1; then
B396: [. D.(i-1),D.i .] c= [.a,D.i .] by XXREAL_1:34; then
A398: f1.t = ([.a,D.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 thesis by A351,A394,A398;
end;
suppose A399: a < D.(i-1);
1 + 0 < i + 1 by XREAL_1:8,A354; then
A401: Dp1(m,D,(i+1)) = m.(D.(i+1 -1)) by A356,defDp1
.= ([.a,D.i .] --> 1) +* (]. D.i,b.] --> 0)
by A8,A377,A399,A382;
A402: Dp1(m,D,i) = m.(D.(i-1)) by A355,A376,defDp1
.= ([.a,D.(i-1) .] --> 1) +* (]. D.(i-1),b.] --> 0)
by A8,A378,A399;
A404: a <= D.i & D.i <= b by A377,XXREAL_1:1;
A405: a <= D.(i-1) & D.(i-1) <= b by A378,XXREAL_1:1;
A406: dom f1 = dom g1 \/ dom g2 by FUNCT_4:def 1
.= A by A7,B20,A404,XXREAL_1:167;
A407: dom f2 = dom h1 \/ dom h2 by FUNCT_4:def 1
.= A by A7,B20,A405,XXREAL_1:167;
rng f1 c= REAL; then
reconsider f1 as Function of A,REAL by A406,FUNCT_2:2;
rng f2 c= REAL; then
reconsider f2 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,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;
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 thesis;
end;
A410: t in [. D.(i-1),D.i .] by A379,INTEGRA1:4,A333;
B411: [. D.(i-1),D.i .] c= [.a,D.i .] by A405,XXREAL_1:34; then
A413: f1.t = ([.a,D.i .] --> 1).t
by A410,FUNCT_4:16,B20,XXREAL_1:90
.= 1 by B411,A410,FUNCOP_1:7;
D.(i-1) < t & t <= D.i by A332,INTEGRA1:def 4,A334,A376; then
A414: t in ]. D.(i-1),b.] by A408; then
f2.t = (]. D.(i-1),b.] --> 0).t by B20,FUNCT_4:13
.= 0 by A414,FUNCOP_1:7;
hence thesis by A351,A409,A413;
end;
end;
end;
for k be Nat st k in dom z & k <> i holds z.k = 0
proof
let k be Nat;
assume that
A415: k in dom z and
A416: k <> i;
consider r be 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 be Function of A,REAL such that
A423: qk = q2.k & z.k = qk.t by A344,A415;
A425: k in dom D by A344,A415,FINSEQ_1:def 3;
A426: 1 <= k <= len D by A344,A415,FINSEQ_1:1; then
k + 0 <= len D + 1 by XREAL_1:7; then
A427: k in Seg (len D + 1) by A426;
e: 1 + 0 <= k + 1 by XREAL_1:7;
k + 1 <= len D + 1 by XREAL_1:7,A426; then
A428: k + 1 in Seg (len D + 1) by e;
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;
B30: dom f0 = [.a,b.] &
dom g1 = [.a,D.k .] & dom g2 = ]. D.k,b.] &
dom h1 = [.a,D.(k-1) .] & dom h2 = ]. D.(k-1),b.] by FUNCOP_1:13;
per cases;
suppose A429: k = 1; then
A433: lower_bound divset(D,i) = D.(i-1) &
upper_bound divset(D,i) = D.i by A332,INTEGRA1:def 4,A416;
A435: i-1 in dom D by A332,A429,A416,INTEGRA1:7;
A440: D.k in [.a,b.] by A7,A425,INTEGRA1:6; then
A446: a <= D.k & D.k <= b by XXREAL_1:1;
A445: dom f0 = A by A7,FUNCOP_1:13;
A447: dom f1 = dom g1 \/ dom g2 by FUNCT_4:def 1
.= A by A7,B30,A446,XXREAL_1:167;
rng f0 c= REAL; then
reconsider f0 as Function of A,REAL by A445,FUNCT_2:2;
rng f1 c= REAL; then
reconsider f1 as Function of A,REAL by A447,FUNCT_2:2;
A451: a < D.k by A264,A429;
A452: Dp1(m,D,(k+1)) = m.(D.(k+1 -1)) by A428,defDp1,A429
.= ([.a,D.k .] --> 1) +* (]. D.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,D,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,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;
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 thesis;
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;
D.k <= D.(i-1)
proof
k = i-1 or k < i-1 by A456,XXREAL_0:1;
hence thesis by A425,A435,VALUED_0:def 13;
end; then
A457: D.k < t by A334,A429,A416,XXREAL_0:2,A433;
a <= t <= b by XXREAL_1:1,A7; then
A459: t in ].D.k,b .] by A457; then
A461: f1.t = (].D.k,b .] --> 0).t by B30,FUNCT_4:13
.= 0 by A459,FUNCOP_1:7;
f0.t = 0 by A7,FUNCOP_1:7;
hence thesis by A423,A453,A461;
end;
suppose A462: k <> 1; then
A464: D.(k-1) in [.a,b.] by A7,A425,INTEGRA1:7;
A463: D.k in [.a,b.] by A7,A425,INTEGRA1:6;
A467: k-1 in dom D by A425,A462,INTEGRA1:7; then
A468: D.(k-1) < D.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 D by A426,XXREAL_0:2; then
A471: 1 in dom D by FINSEQ_3:25;
D.1 <= D.(k-1)
proof
1 = k -1 or 1 < k -1 by A470,XXREAL_0:1;
hence thesis by A467,A471,VALUED_0:def 13;
end; then
A472: a < D.(k-1) by A264,XXREAL_0:2;
1 + 0 < k + 1 by XREAL_1:8,A426; then
A474: Dp1(m,D,(k+1)) = m.(D.(k+1 -1)) by A428,defDp1
.= ([.a,D.k .] --> 1) +* (]. D.k,b.] --> 0)
by A8,A463,A472,A468;
A475: Dp1(m,D,k) = m.(D.(k-1)) by A427,A462,defDp1
.= ([.a,D.(k-1) .] --> 1) +* (]. D.(k-1),b.] --> 0)
by A8,A464,A472;
A477: a <= D.k & D.k <= b by A463,XXREAL_1:1;
A478: a <= D.(k-1) & D.(k-1) <= b by A464,XXREAL_1:1;
A479: dom f1 = dom g1 \/ dom g2 by FUNCT_4:def 1
.= A by A7,B30,A477,XXREAL_1:167;
A480: dom f2 = dom h1 \/ dom h2 by FUNCT_4:def 1
.= A by A7,B30,A478,XXREAL_1:167;
rng f1 c= REAL; then
reconsider f1 as Function of A,REAL by A479,FUNCT_2:2;
rng f2 c= REAL; then
reconsider f2 as Function of A,REAL by A480,FUNCT_2:2;
A482: qk.t = r * (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;
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 thesis;
end;
per cases by A416,XXREAL_0:1;
suppose i < k; then
i +1 <= k by NAT_1:13; then
A485: i+1 -1 <= k-1 by XREAL_1:13;
A486: D.i <= D.(k-1)
proof
i = k -1 or i < k -1 by A485,XXREAL_0:1;
hence thesis by A332,A467,VALUED_0:def 13;
end;
A488: (upper_bound divset(D,i)) <= D.(k-1)
proof
per cases;
suppose i = 1;
hence (upper_bound divset(D,i)) <=D.(k-1)
by A486,A332,INTEGRA1:def 4;
end;
suppose i <> 1;
hence (upper_bound divset(D,i)) <=D.(k-1)
by A486,A332,INTEGRA1:def 4;
end;
end;
a <= t & t <= (upper_bound divset(D,i))
by B352,XXREAL_1:1,A7; then
A489: a <= t & t <= D.(k-1) by A488,XXREAL_0:2; then
A490: t in [.a,D.(k-1) .];
a <= t & t <= D.k by A468,A489,XXREAL_0:2; then
A491: t in [.a,D.k .]; then
A494: f1.t = ([.a,D.k .] --> 1).t
by FUNCT_4:16,B30,XXREAL_1:90
.= 1 by A491,FUNCOP_1:7;
f2.t = ([.a,D.(k-1) .] --> 1).t
by A490,FUNCT_4:16,B30,XXREAL_1:90
.= 1 by A490,FUNCOP_1:7;
hence thesis by A423,A482,A494;
end;
suppose A496: k < i; then
k +1 <= i by NAT_1:13; then
A499: k+1 -1 <= i-1 by XREAL_1:13;
A500: i-1 in dom D by A332,A496,A426,INTEGRA1:7;
A502: D.k <= D.(i-1)
proof
k = i-1 or k < i-1 by A499,XXREAL_0:1;
hence thesis by A425,A500,VALUED_0:def 13;
end;
D.(i-1) < t by A496,A426,A334,A332,INTEGRA1:def 4; then
A504: D.k < t by A502,XXREAL_0:2; then
A505: D.(k-1) < t by A468,XXREAL_0:2;
A506: a <= t & t <= b by XXREAL_1:1,A7; then
A507: t in ]. D.k,b.] by A504; then
A509: f1.t = (]. D.k,b.] --> 0).t by B30,FUNCT_4:13
.= 0 by A507,FUNCOP_1:7;
A508: t in ]. D.(k-1),b.] by A505,A506; then
f2.t = (]. D.(k-1),b.]--> 0).t by B30,FUNCT_4:13
.= 0 by A508,FUNCOP_1:7;
hence thesis by A423,A482,A509;
end;
end;
end;
hence g1.t = g.(p2.i)
by A317,A336,FUNCT_1:47,A348,A337,A347,A357,INTEGR23:6;
end;
A511: for t be Element of A holds |.g1.t - g.t.| < r/2
proof
let t be Element of A;
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 be 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 be Real st tD in dom g & t in dom g & |.tD - t.| < s
holds |.g.tD - g.t.| < r/2
proof
let tD,t be Real;
assume A544: tD in dom g & t in dom g & |.tD - t.| < s;
B545: dom g = dom(u|A) by A260,RELAT_1:62,A317; then
(u|A).tD = u.tD & (u|A).t = u.t by A544,FUNCT_1:47;
hence |.g.tD - g.t.| < r/2 by A317,B545,A323,A544;
end;
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: |.tD - t.| < s by A329,A540,A541,INTEGR20:12;
g1.t = g.tD by A331,A540,A541,A542;
hence |.g1.t - g.t.| < r/2 by B551,A543,A549,A260,A317;
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 be Function of A,REAL such that
A552: g2=g0 & g2|A is bounded;
now
let k be Real;
assume k in PreNorms g0; then
consider t be Element of A such that
A553: k = |.g0.t.|;
|.g1.t - g.t.| < r/2 by A511;
hence k <= r/2 by A553,A2,A317,A330,C0SP1:34;
end; 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 thesis by A321,XXREAL_0:2;
end;
take m0;
thus thesis by A325;
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 V by FUNCT_2:def 1; then
A557: rng xD c= dom f;
v in the carrier of V; then
A558: v in dom f by FUNCT_2:def 1;
consider K be Real such that
A559: 0 <= K &
for x be Point of V holds |. f.x .| <= K * ||. x .||
by DUALSP01:def 9;
for r be Real st 0 < r ex s be Real st 0 < s &
for x1 be Point of V st x1 in dom f & ||. x1 - v .|| < s holds
|. f/.x1 - f/.v .| < r
proof
let r be Real;
assume A561: 0 < r;
reconsider s = r/(K+1) as Real;
A563: for x1 be Point of V st x1 in dom f & ||. x1 - v .|| < s holds
|. f/.x1 - f/.v .| < r
proof
let x1 be Point of V;
assume that
x1 in dom f and
A565: ||. x1 - v .|| < s;
|. f/.x1 - f/.v .| = |. f.(x1 - v) .| by HAHNBAN:19; then
A567: |. f/.x1 - f/.v .| <= K * ||. x1 - v .|| by A559;
K < K+1 by XREAL_1:145; then
A569: K * ||. x1 - v .|| <= (K+1) * ||. x1 - v .|| by XREAL_1:64;
(K+1) * ||. x1 - v .|| < (K+1) * s by A559,A565,XREAL_1:68; then
K * ||. x1 - v .|| < (K+1) * s by A569,XXREAL_0:2; then
|. f/.x1 - f/.v .| < (K+1) * s by A567,XXREAL_0:2;
hence |. f/.x1 - f/.v .| < r by A559,XCMPLX_1:87;
end;
take s;
thus thesis by A559,A561,XREAL_1:139,A563;
end; 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;
end; then
B573: ||.x.|| <= total_vd(rho) by A251,Lm83;
take rho;
thus thesis by B250,A259,B573,A258,XXREAL_0:1;
end;