:: Uniform Boundedness Principle
:: by Hideki Sakurai , Hisayoshi Kunimune and Yasunari Shidama
::
:: Received October 9, 2007
:: Copyright (c) 2007 Association of Mizar Users
environ
vocabularies TARSKI, RLVECT_1, FUNCT_1, PRE_TOPC, ARYTM, BOOLE, ABSVALUE,
ARYTM_1, FCONT_1, FINSEQ_4, ARYTM_3, RELAT_1, SEQ_2, LATTICES, ORDINAL2,
NORMSP_1, SUBSET_1, TOPS_1, METRIC_1, PCOMPS_1, NORMSP_2, PROB_1, BHSP_3,
INT_1, SEQ_1, SEQ_4, RINFSUP1, FUNCT_2, SEQM_3, RSSPACE3, LOPBAN_1,
TDGROUP, MSUALG_3;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ENUMSET1, RELAT_1, RELSET_1,
RELSET_2, FUNCT_1, FUNCT_2, PARTFUN1, MCART_1, FUNCOP_1, FUNCT_3,
PRE_TOPC, TOPS_1, DOMAIN_1, STRUCT_0, ORDINAL1, ORDINAL2, CARD_3,
NUMBERS, XCMPLX_0, XREAL_0, SETFAM_1, RINFSUP1, COMPLEX1, REAL_1, NAT_1,
XXREAL_0, SEQ_1, SEQ_2, SEQM_3, SEQ_4, FINSEQ_4, PSCOMP_1, RLVECT_1,
MEMBERED, PROB_1, TBSP_1, METRIC_1, PCOMPS_1, NORMSP_1, NORMSP_2,
RSSPACE3, RLTOPSP1, LOPBAN_1, NFCONT_1, INTEGRA2, KURATO_2;
constructors NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, ORDINAL2, RELSET_2, REAL_1,
COMPLEX1, DOMAIN_1, SEQ_1, SEQ_2, ARYTM_3, SETFAM_1, FINSEQ_4, COMPTS_1,
TOPS_1, TBSP_1, CONNSP_2, PCOMPS_1, RLTOPSP1, SQUARE_1, NFCONT_1,
FRECHET2, YELLOW_8, NAT_1, FUNCT_1, FUNCT_2, PSCOMP_1, FUNCT_3, RELAT_2,
PARTFUN1, MCART_1, RINFSUP1, INTEGRA2, PROB_1, PARTFUN2, NORMSP_2,
RSSPACE3, LOPBAN_1;
registrations REAL_1, NUMBERS, ORDINAL2, XREAL_0, ARYTM_3, ZFMISC_1, XBOOLE_0,
METRIC_1, SEQ_1, SEQ_2, XXREAL_0, ORDINAL1, RELSET_1, STRUCT_0, MEMBERED,
RLTOPSP1, TOPS_1, KURATO_2, COMPTS_1, SUBSET_1, NAT_1, RLVECT_1,
NORMSP_1, NORMSP_2, TBSP_1, FUNCT_1, FUNCT_2, RSSPACE3, SEQM_3, PARTFUN1,
PROB_1, LOPBAN_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, RLVECT_1, METRIC_1, COMPTS_1, PCOMPS_1, NORMSP_2,
XBOOLE_0, RSSPACE3, SEQ_1, SEQ_2, SEQ_4, FINSEQ_4, LOPBAN_1, RINFSUP1,
NFCONT_1, FUNCT_1, TBSP_1, XREAL_0, FUNCT_2, SEQM_3, CARD_3, XCMPLX_0,
ABSVALUE, NORMSP_1;
theorems TARSKI, XBOOLE_1, SEQ_1, SEQ_2, RLVECT_1, FUNCT_2, XBOOLE_0, XREAL_1,
XCMPLX_1, NORMSP_1, TBSP_1, PRE_TOPC, TOPS_1, NFCONT_1, XXREAL_0,
FUNCT_1, NORMSP_2, RINFSUP1, ABSVALUE, XCMPLX_0, XREAL_0, SEQM_3,
INTEGRA2, SEQ_4, RSSPACE2, LOPBAN_1, LOPBAN_3, PROB_1, RSSPACE3,
PARTFUN1;
schemes FUNCT_2, FRAENKEL;
begin :: Uniform Boundedness Principle
theorem Th1:
for seq be Real_Sequence, r be Real st
seq is bounded & 0<=r holds lim_inf(r(#)seq)=r*(lim_inf seq)
proof
let seq be Real_Sequence, r be Real;
assume
A1: seq is bounded & 0<=r;
inferior_realsequence seq in Funcs(NAT,REAL) by FUNCT_2:11; then
A2:ex f be Function st
inferior_realsequence seq = f & dom f = NAT & rng f c= REAL
by FUNCT_2:def 2;
(inferior_realsequence seq).0 in rng inferior_realsequence seq
by FUNCT_2:6; then
reconsider X1 = rng inferior_realsequence seq as non empty Subset of REAL
by A2;
inferior_realsequence seq is bounded by A1,RINFSUP1:58; then
inferior_realsequence seq is bounded_above by SEQ_2:def 5; then
A3:X1 is bounded_above by RINFSUP1:5;
now let n be Element of NAT;
seq ^\n in Funcs(NAT,REAL) by FUNCT_2:11; then
ex f be Function st
seq ^\n = f & dom f = NAT & rng f c= REAL by FUNCT_2:def 2; then
reconsider Y1 = rng(seq ^\n) as non empty Subset of REAL by FUNCT_2:6;
consider r1 be real number such that
A4: 0 complete;
coherence
proof
now let S1 be sequence of MetricSpaceNorm X;
assume A1: S1 is Cauchy;
reconsider S2=S1 as sequence of X;
S2 is Cauchy_sequence_by_Norm
proof
let r be Real;
assume r > 0; then
consider p be Element of NAT such that
A2: for n,m be Element of NAT st p<=n & p<=m holds dist(S1.n,S1.m) < r
by A1,TBSP_1:def 5;
now
let n,m be Element of NAT;
assume p<=n & p<=m; then
dist(S1.n,S1.m) < r by A2;
hence dist(S2.n,S2.m) < r by NORMSP_2:def 1;
end;
hence thesis;
end; then
S2 is convergent by LOPBAN_1:def 16;
hence S1 is convergent by NORMSP_2:5;
end;
hence thesis by TBSP_1:def 6;
end;
end;
definition let X be RealBanachSpace, x0 be Point of X, r be real number;
func Ball (x0,r) -> Subset of X equals
{ x where x is Point of X : ||.x0-x.|| < r };
coherence
proof
defpred P[Point of X] means ||.x0 - $1.|| < r;
{y where y is Point of X : P[y]} c= the carrier of X
from FRAENKEL:sch 10;
hence thesis;
end;
end;
theorem Th3:
:: Baire category theorem - Banach space version
for X be RealBanachSpace, Y be SetSequence of X st
union rng Y = the carrier of X &
(for n be Element of NAT holds Y.n is closed)
holds
ex n0 be Element of NAT, r be Real, x0 be Point of X st
0 < r & Ball (x0,r) c= Y.n0
proof
let X be RealBanachSpace, Y be SetSequence of X;
assume
A1: union rng Y = the carrier of X &
for n be Element of NAT holds Y.n is closed;
now let n be Element of NAT;
reconsider Yn = Y.n as Subset of TopSpaceNorm X;
Y.n is closed by A1; then
Yn is closed by NORMSP_2:15; then
Yn` is open by TOPS_1:29;
hence (Y.n)` in Family_open_set MetricSpaceNorm X by PRE_TOPC:def 5;
end; then
consider n0 be Element of NAT, r be Real, xx0 be Point of MetricSpaceNorm X
such that
A2: 0 < r & Ball(xx0,r) c= Y.n0 by A1,NORMSP_2:1;
consider x0 be Point of X such that
A3: x0 = xx0 & Ball(xx0,r) = {x where x is Point of X:||.x0-x.|| < r}
by NORMSP_2:2;
Ball (x0,r) = {x where x is Point of X : ||.x0-x.|| < r };
hence thesis by A2,A3;
end;
theorem Th4:
for X,Y be RealNormSpace, f be bounded LinearOperator of X,Y holds
f is_Lipschitzian_on the carrier of X &
f is_continuous_on the carrier of X &
for x be Point of X holds f is_continuous_in x
proof
let X,Y be RealNormSpace, f be bounded LinearOperator of X,Y;
A1:dom f =the carrier of X by FUNCT_2:def 1;
consider K being Real such that
A2: 0 <= K &
for x being VECTOR of X holds ||. f.x .|| <= K * ||. x .||
by LOPBAN_1:def 9;
A3:now let x,y be Point of X;
assume x in the carrier of X & y in the carrier of X;
f/.x -f/.y = f/.x - f.y by A1,PARTFUN1:def 8; then
f/.x -f/.y = f.x - f.y by A1,PARTFUN1:def 8; then
f/.x -f/.y =f.x +(-1)* f.y by RLVECT_1:29; then
f/.x -f/.y = f.x + f.((-1)*y) by LOPBAN_1:def 6; then
f/.x -f/.y = f.(x+(-1)*y) by LOPBAN_1:def 5; then
f/.x -f/.y =f.(x+-y) by RLVECT_1:29; then
A4:||.f/.x -f/.y .||<= K * ||. x-y .|| by A2;
0<=||. x-y .|| by NORMSP_1:8; then
||.f/.x -f/.y .||<=K*||. x-y .||+||. x-y .|| by A4,XREAL_1:40;
hence ||. f/.x -f/.y .|| <= (K+1) * ||. x-y .||;
end;
0 < (K+1) by A2,XREAL_1:36;
hence f is_Lipschitzian_on the carrier of X by A1,A3,NFCONT_1:def 13;
hence
A5: f is_continuous_on the carrier of X by NFCONT_1:52;
hereby let x be Point of X;
f|(the carrier of X) = f by FUNCT_2:40;
hence f is_continuous_in x by A5,NFCONT_1:def 11;
end;
end;
theorem Th5:
for X be RealBanachSpace, Y be RealNormSpace,
T be Subset of R_NormSpace_of_BoundedLinearOperators(X,Y) st
for x be Point of X
ex K be real number st
0 <= K &
for f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) st
f in T holds ||. f.x .|| <= K
holds
ex L be real number st
0 <= L &
for f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) st
f in T holds ||.f.|| <= L
proof
let X be RealBanachSpace, Y be RealNormSpace,
T be Subset of R_NormSpace_of_BoundedLinearOperators(X,Y);
assume
A1:for x be Point of X
ex KTx be real number st
0 <= KTx &
for f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) st
f in T holds ||. f.x .|| <= KTx;
per cases;
suppose A2:T <> {};
deffunc S0(Point of X,Real) = Ball($1,$2);
defpred P[Point of X,set] means
$2={||. f.$1 .|| where f is bounded LinearOperator of X,Y :f in T};
A3: for x be Point of X ex y be Element of bool REAL st P[x,y]
proof
let x be Point of X;
take y = {||. f.x .|| where f is bounded LinearOperator of X,Y :f in T};
now let z be set;
assume z in y; then
ex f be bounded LinearOperator of X,Y st z=||. f.x .|| & f in T;
hence z in REAL;
end;
hence thesis by TARSKI:def 3;
end;
ex Ta be Function of the carrier of X,bool REAL st
for x be Element of the carrier of X holds P[x,Ta.x]
from FUNCT_2:sch 3(A3); then
consider Ta be Function of X,bool REAL such that
A4: for x be Point of X holds
Ta.x = {||. f.x .|| where f is bounded LinearOperator of X,Y :f in T};
A5:for x be Point of X holds Ta.x is non empty
proof
let x be Point of X;
A6: Ta.x = {||. f.x .|| where f is bounded LinearOperator of X,Y :f in T}
by A4;
consider f0 be set such that
A7: f0 in T by A2,XBOOLE_0:def 1;
reconsider f0 as bounded LinearOperator of X,Y by A7,LOPBAN_1:def 10;
||. f0.x .|| in Ta.x by A6,A7;
hence Ta.x is non empty;
end;
defpred P[Element of NAT,set] means
$2={x where x is Point of X: Ta.x is bounded_above & sup(Ta.x) <= $1};
A8:for n be Element of NAT
ex y be Element of bool the carrier of X st P[n,y]
proof
let n be Element of NAT;
take y = {x where x is Point of X:
Ta.x is bounded_above & sup(Ta.x) <= n};
now let z be set;
assume z in y; then
ex x be Point of X st z=x & Ta.x is bounded_above & sup(Ta.x) <= n;
hence z in the carrier of X;
end;
hence thesis by TARSKI:def 3;
end;
ex Xn be Function of NAT,bool the carrier of X st
for n be Element of NAT holds P[n,Xn.n] from FUNCT_2:sch 3(A8); then
consider Xn be Function of NAT, bool the carrier of X such that
A9: for n be Element of NAT holds
Xn.n = {x where x is Point of X: Ta.x is bounded_above & sup(Ta.x) <= n};
reconsider Xn as SetSequence of X;
A10:for n be Element of NAT holds Xn.n is closed
proof
let n be Element of NAT;
for s1 be sequence of X st
rng s1 c= Xn.n & s1 is convergent holds lim s1 in Xn.n
proof
let s1 be sequence of X;
assume
A11: rng s1 c= Xn.n & s1 is convergent;
A12: Ta.(lim s1) = {||. f.(lim s1) .||
where f is bounded LinearOperator of X,Y :f in T} by A4;
A13: for y be real number st y in Ta.(lim s1) holds y <= n
proof
let y be real number;
assume y in Ta.(lim s1); then
consider f be bounded LinearOperator of X,Y such that
A14: y=||. f.(lim s1) .|| & f in T by A12;
A15: f is_continuous_in lim s1 by Th4;
A16: dom f=the carrier of X by FUNCT_2:def 1; then
A17: rng s1 c= dom f by A11,XBOOLE_1:1; then
A18: f*s1 is convergent & f/.(lim s1) = lim (f*s1)
by A11,A15,NFCONT_1:def 9; then
lim (||. f*s1 .||) = ||. f/.(lim s1) .|| by LOPBAN_1:24; then
A19: lim (||. f*s1 .||) = ||. f.(lim s1) .|| by A16,PARTFUN1:def 8;
for k be Element of NAT holds ||. f*s1 .||.k <= n
proof
let k be Element of NAT;
||. f*s1 .||.k = ||. (f*s1).k .|| by NORMSP_1:def 10; then
||. f*s1 .||.k =||. f/.(s1.k) .|| by A17,NFCONT_1:8; then
A20: ||. f*s1 .||.k =||. f.(s1.k) .|| by FUNCT_2:176;
dom s1= NAT by FUNCT_2:def 1; then
s1.k in rng s1 by FUNCT_1:12; then
s1.k in Xn.n by A11; then
s1.k in {x where x is Point of X :
Ta.x is bounded_above & sup (Ta.x) <= n} by A9; then
consider x be Point of X such that
A21: x=s1.k & Ta.x is bounded_above & sup(Ta.x) <=n;
Ta.x = {||. g.x .|| where g is bounded LinearOperator of X,Y :g in T}
by A4; then
||. f.(s1.k) .|| in Ta.(s1.k) by A14,A21; then
||. f.(s1.k) .|| <= sup (Ta.(s1.k)) by A21,SEQ_4:def 4;
hence thesis by A20,A21,XXREAL_0:2;
end; then
A22: for i being Element of NAT st 0 <= i holds ||. f*s1 .||.i <=n;
||. f*s1 .|| is convergent by A18,NORMSP_1:39;
hence y<=n by A14,A19,A22,RSSPACE2:6;
end;
Ta.(lim s1) is non empty by A5; then
A23: sup(Ta.(lim s1)) <= n by A13,SEQ_4:62;
A24:Ta.(lim s1) is bounded_above by A13,SEQ_4:def 1;
Xn.n = {x where x is Point of X :
Ta.x is bounded_above & sup (Ta.x) <= n} by A9;
hence thesis by A23,A24;
end;
hence thesis by NFCONT_1:def 5;
end;
A25:union rng Xn is Subset of X by PROB_1:23;
the carrier of X c= union rng Xn
proof
let x be set;
assume x in the carrier of X; then
reconsider x1=x as Point of X;
A26: Ta.x1 = {||. f.x1 .|| where f is bounded LinearOperator of X,Y :f in T}
by A4;
consider f be set such that
A27: f in T by A2,XBOOLE_0:def 1;
reconsider f as bounded LinearOperator of X,Y by A27,LOPBAN_1:def 10;
A28:||. f.x1 .|| in Ta.x by A26,A27;
consider KTx1 be real number such that
A29:0 <= KTx1 &
for f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) st
f in T holds ||. f.x1 .|| <= KTx1 by A1;
A30:for p be real number st p in Ta.x1 holds p <= KTx1
proof
let p be real number;
assume p in Ta.x1; then
ex f be bounded LinearOperator of X,Y st p=||. f.x1 .|| & f in T by A26;
hence p <= KTx1 by A29;
end; then
A31:Ta.x1 is bounded_above by SEQ_4:def 1;
consider n be Element of NAT such that
A32: KTx1 0.X holds r/(2*||.x.||)*x+x0 in S0(x0,r)
proof
let x be Point of X;
assume x <> 0.X; then
A38:||.x.|| <> 0 by NORMSP_1:def 2;
A39:||.x.|| >=0 by NORMSP_1:8;
abs( ||.x.||") =abs( 1/||.x.||); then
abs( ||.x.||") =1/abs( ||.x.||) by ABSVALUE:15; then
A40:abs( ||.x.||") =||.x.||" by A39,ABSVALUE:def 1;
A41:0=0 by XREAL_1:35; then
A47:2*(M+n0)>=0 by XREAL_1:129; then
A48: 0 <= KT by A33,XREAL_1:138;
A49:now let f be bounded LinearOperator of X,Y;
assume
A50: f in T;
A51: for x be Point of X st x <> 0.X holds ||.f.x.|| <= KT*||.x.||
proof
let x be Point of X;
assume A52: x <> 0.X; then
||.x.|| <> 0 by NORMSP_1:def 2; then
||.x.|| >0 by NORMSP_1:8; then
A53:2*||.x.|| >0 by XREAL_1:131; then
A54:r/(2*||.x.||) >0 by A33,XREAL_1:141;
r/(2*||.x.||)*x+x0 in S0(x0,r) by A37,A52; then
A55:||. f.(r/(2*||.x.||)*x+x0) .|| <= n0 by A34,A50;
A56:(2*||.x.||)/r >0 by A33,A53,XREAL_1:141;
set nrp1=r/(2*||.x.||);
set nrp2=(2*||.x.||)/r;
||. f.(r/(2*||.x.||)*x).||
=||.(r/(2*||.x.||))*f.x.|| by LOPBAN_1:def 6; then
||. f.(r/(2*||.x.||)*x).||
=abs(r/(2*||.x.||))*||.f.x.|| by NORMSP_1:def 2; then
A57:||. f.(r/(2*||.x.||)*x).||
=(r/(2*||.x.||))*||.f.x.|| by A54,ABSVALUE:def 1;
A58:||.f.(r/(2*||.x.||)*x)+f.x0.|| =||.f.(r/(2*||.x.||)*x+x0).||
by LOPBAN_1:def 5;
set nr1=||.f.(r/(2*||.x.||)*x)+f.x0.||;
set nr2=||.f.(r/(2*||.x.||)*x).||;
set nr3=||.f.x0.||;
||.-(f.x0).||=||.f.x0.|| by NORMSP_1:6; then
nr2-nr3<=||.f.(r/(2*||.x.||)*x)-(-f.x0).|| by NORMSP_1:12; then
(r/(2*||.x.||))*||.f.x.||-nr3<=nr1 by A57,RLVECT_1:30; then
A59:(r/(2*||.x.||))*||.f.x.||-nr3<=n0 by A55,A58,XXREAL_0:2;
||.x0-x0.||=||.0.X.|| by RLVECT_1:16; then
x0 in S0(x0,r) by A33; then
x0 in Xn.n0 by A33; then
x0 in {x1 where x1 is Point of X :
Ta.x1 is bounded_above & sup(Ta.x1) <= n0} by A9; then
consider x1 be Point of X such that
A60: x1=x0 & Ta.x1 is bounded_above & sup (Ta.x1) <= n0;
Ta.x1 = {||. g.x1 .|| where g is bounded LinearOperator of X,Y
:g in T } by A4; then
||. f.x0 .|| in Ta.x0 by A50,A60; then
||. f.x0 .|| <= sup (Ta.x0) by A60,SEQ_4:def 4; then
nrp1*||.f.x.|| - M <= nrp1*||.f.x.|| - nr3 by XREAL_1:12; then
nrp1*||.f.x.|| - M <= n0 by A59,XXREAL_0:2; then
nrp1*||.f.x.|| + -M + M <= n0 + M by XREAL_1:8; then
nrp2*(nrp1*||.f.x.||) <= nrp2*(n0+M) by A56,XREAL_1:66; then
nrp1*nrp2*||.f.x.|| <= nrp2*(n0+M); then
1*||.f.x.|| <= nrp2*(n0+M) by A33,A53,XCMPLX_1:113;
hence ||.f.x.|| <= KT*||.x.||;
end;
A61: for x be Point of X holds ||.f.x.|| <= KT*||.x.||
proof
let x be Point of X;
now assume A62: x = 0.X; then
f.x = f.(0*0.X) by RLVECT_1:23; then
f.x =0*f.(0.X) by LOPBAN_1:def 6; then
A63: f.x =0.Y by RLVECT_1:23;
||.x.||= 0 by A62,NORMSP_1:5;
hence ||.f.x.|| <= KT*||.x.|| by A63,NORMSP_1:def 2;
end;
hence thesis by A51;
end;
thus
for k be real number st
k in {||.f.x1.|| where x1 is Point of X : ||.x1.|| <= 1 } holds k <= KT
proof
let k be real number;
assume k in {||.f.x1.|| where x1 is Point of X : ||.x1.|| <= 1}; then
consider x be Point of X such that
A64: k=||.f.x.|| & ||.x.|| <= 1;
k <= KT*||.x.|| & KT*||.x.|| <=KT by A48,A61,A64,XREAL_1:155;
hence thesis by XXREAL_0:2;
end;
end;
for f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) st
f in T holds ||.f.|| <= KT
proof
let f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
reconsider f1=f as bounded LinearOperator of X,Y by LOPBAN_1:def 10;
assume f in T; then
A65: for k be real number st k in PreNorms(f1) holds k <= KT by A49;
||. f .|| = sup PreNorms(f1) by LOPBAN_1:36;
hence ||. f .|| <= KT by A65,SEQ_4:62;
end;
hence thesis by A33,A47,XREAL_1:138;
end;
suppose A66:T = {};
take L = 0;
thus thesis by A66;
end;
end;
definition let X, Y be RealNormSpace,
H be Function of NAT,
the carrier of R_NormSpace_of_BoundedLinearOperators(X,Y),
x be Point of X;
func H # x -> sequence of Y means :Def2:
for n be Element of NAT holds it.n = (H.n).x;
existence
proof
deffunc U(Element of NAT) = (H.$1).x;
thus ex f being Function of NAT, the carrier of Y st
for n be Element of NAT holds f.n = U(n) from FUNCT_2:sch 4;
end;
uniqueness
proof
let S1,S2 be sequence of Y such that
A1: (for n be Element of NAT holds S1.n = (H.n).x) &
for n be Element of NAT holds S2.n = (H.n).x;
now let n be Element of NAT;
S1.n = (H.n).x & S2.n = (H.n).x by A1;
hence S1.n = S2.n;
end;
hence thesis by FUNCT_2:113;
end;
end;
theorem Th6:
for X be RealBanachSpace, Y be RealNormSpace,
vseq be sequence of R_NormSpace_of_BoundedLinearOperators(X,Y),
tseq be Function of X,Y st
( for x be Point of X holds vseq#x is convergent & tseq.x = lim(vseq#x) )
holds
tseq is bounded LinearOperator of X,Y &
(for x be Point of X holds ||.tseq.x.|| <=( lim_inf ||.vseq.|| ) * ||.x.|| ) &
for ttseq be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) st
ttseq = tseq holds ||.ttseq.|| <= lim_inf ||.vseq.||
proof
let X be RealBanachSpace, Y be RealNormSpace,
vseq be sequence of R_NormSpace_of_BoundedLinearOperators(X,Y),
tseq be Function of X,Y;
assume
A1:for x be Point of X holds vseq#x is convergent & tseq.x = lim(vseq#x);
set T=rng vseq;
set RNS=R_NormSpace_of_BoundedLinearOperators(X,Y);
vseq in Funcs(NAT,the carrier of RNS) by FUNCT_2:11; then
consider f0 being Function such that
A2: vseq = f0 & dom f0 = NAT & rng f0 c= the carrier of RNS by FUNCT_2:def 2;
for x be Point of X
ex K be real number st
0 <= K &
for f be Point of RNS st f in T holds ||. f.x .|| <= K
proof
let x be Point of X;
vseq#x is convergent by A1; then
||. vseq#x .|| is convergent by NORMSP_1:39; then
||. vseq#x .|| is bounded by SEQ_2:27; then
||. vseq#x .|| is bounded_above by SEQ_2:def 5; then
consider K be real number such that
A3: for n be Element of NAT holds ||. vseq#x .||.n< K by SEQ_2:def 3;
||. vseq#x .||.0< K by A3; then
||. (vseq#x).0 .|| < K by NORMSP_1:def 10; then
A4: 0 <= K by NORMSP_1:8;
for f be Point of RNS st f in T holds ||. f.x .|| <= K
proof
let f be Point of RNS;
assume f in T; then
consider n be set such that
A5: n in NAT & f=vseq.n by FUNCT_2:17;
reconsider n as Element of NAT by A5;
(vseq.n).x = (vseq#x).n by Def2; then
||. f.x .|| = ||. vseq#x .||.n by A5,NORMSP_1:def 10;
hence ||. f.x .|| <= K by A3;
end;
hence thesis by A4;
end; then
consider L be real number such that
A6: 0 <= L &
for f be Point of RNS st f in T holds ||.f.|| <= L by A2,Th5;
A7:L + 0 < 1+ L by XREAL_1:10;
for n be Element of NAT holds abs(||.vseq.||.n ) < (1+L)
proof
let n be Element of NAT;
vseq.n in T by FUNCT_2:6; then
||.vseq.n.|| <= L by A6; then
||.vseq.||.n <= L by NORMSP_1:def 10; then
A8:||.vseq.||.n <(1+L) by A7,XXREAL_0:2;
0<=||.vseq.n.|| by NORMSP_1:8; then
0<=||.vseq.||.n by NORMSP_1:def 10;
hence thesis by A8,ABSVALUE:def 1;
end; then
A9:||.vseq.|| is bounded by A6,A7,SEQ_2:15;
A10: for x,y be Point of X holds tseq.(x+y)= tseq.x + tseq.y
proof
let x,y be Point of X;
A11: (for n be Element of NAT holds (vseq.n).x = (vseq#x).n) &
vseq#x is convergent & tseq.x = lim (vseq#x) by A1,Def2;
A12: (for n be Element of NAT holds (vseq.n).y = (vseq#y).n) &
vseq#y is convergent & tseq.y = lim (vseq#y) by A1,Def2;
now let n be Element of NAT;
A13:(vseq.n).y = (vseq#y).n by Def2;
A14:
vseq.n is bounded LinearOperator of X,Y by LOPBAN_1:def 10;
(vseq#(x+y)).n=(vseq.n).(x+y) by Def2; then
(vseq#(x+y)).n=(vseq.n).x + (vseq.n).y by A14,LOPBAN_1:def 5;
hence (vseq#(x+y)).n=(vseq#x).n + (vseq#y).n by A13,Def2;
end; then
A15: vseq#(x+y) = vseq#x + vseq#y by NORMSP_1:def 5;
tseq.(x+y) = lim (vseq#(x+y)) by A1;
hence tseq.(x+y) = tseq.x + tseq.y by A11,A12,A15,NORMSP_1:42;
end;
A16:for x be Point of X, r be Element of REAL holds tseq.(r*x)= r*tseq.x
proof
let x be Point of X, r be Element of REAL;
A17:(for n be Element of NAT holds (vseq.n).x = (vseq#x).n) &
vseq#x is convergent & tseq.x = lim(vseq#x) by A1,Def2;
A18: now let n be Element of NAT;
A19: vseq.n is bounded LinearOperator of X,Y by LOPBAN_1:def 10;
(vseq#(r*x)).n=(vseq.n).(r*x) by Def2; then
(vseq#(r*x)).n=r*(vseq.n).x by A19,LOPBAN_1:def 6;
hence (vseq#(r*x)).n=r*(vseq#x).n by Def2;
end;
tseq.(r*x) = lim (vseq#(r*x)) by A1; then
tseq.(r*x) = lim (r*(vseq#x)) by A18,NORMSP_1:def 8;
hence tseq.(r*x) = r*tseq.x by A17,NORMSP_1:45;
end;
A20:
for x be Point of X holds ||.tseq.x.|| <=( lim_inf ||.vseq.|| ) * ||.x.||
proof
let x be Point of X;
A21:
for n be Element of NAT holds ||.(vseq#x).n.|| <= ||.vseq.n.|| * ||.x.||
proof
let n be Element of NAT;
A22:(vseq.n).x = (vseq#x).n by Def2;
vseq.n is bounded LinearOperator of X,Y by LOPBAN_1:def 10;
hence thesis by A22,LOPBAN_1:38;
end;
A23: (for n be Element of NAT holds (vseq.n).x = (vseq#x).n) &
vseq#x is convergent & tseq.x = lim(vseq#x) by A1,Def2; then
A24: ||. vseq#x .|| is convergent by LOPBAN_1:24; then
A25: ||. vseq#x .|| is bounded by SEQ_2:27;
A26: ||.x.|| (#) ||.vseq .|| is bounded by A9,SEQM_3:70;
A27: for n be Element of NAT holds
||. vseq#x .||.n <= (||.x.|| (#) ||.vseq .||).n
proof
let n be Element of NAT;
A28: ||. vseq#x .||.n = ||.(vseq#x).n .|| by NORMSP_1:def 10;
A29: ||.(vseq#x).n .|| <= ||.vseq.n.|| * ||.x.|| by A21;
||.vseq.n.|| = ||.vseq.||.n by NORMSP_1:def 10;
hence thesis by A28,A29,SEQ_1:13;
end;
0<=||.x.|| by NORMSP_1:8; then
A30: lim_inf (||.x.|| (#) ||.vseq .||)
= ( lim_inf ||.vseq.|| ) * ||.x.|| by A9,Th1;
A31: lim ||. vseq#x .|| = lim_inf ||. vseq#x .|| by A24,RINFSUP1:91;
lim_inf ||. vseq#x .|| <=lim_inf (||.x.|| (#) ||.vseq .||)
by A25,A26,A27,RINFSUP1:93;
hence thesis by A23,A30,A31,LOPBAN_1:24;
end;
now let s be real number;
assume A32: 0~~ 0
ex n0 be Element of NAT st
for n,m be Element of NAT st n >= n0 & m >= n0 holds
||.(vseq#x).n -(vseq#x).m.||< TK1
proof
let TK1 be Real such that
A14: TK1 > 0;
set V = {z where z is Point of X : ||.x-z.|| = n0 & m >= n0 holds
||.((vseq#y).n) - ((vseq#y).m).|| < TK1/3 by A18,RSSPACE3:10;
take n0;
for n, m be Element of NAT st n >= n0 & m >= n0 holds
||.(vseq#x).n -(vseq#x).m.||< TK1
proof
let n,m be Element of NAT;
assume n >= n0 & m >= n0; then
||. (vseq#y).n - (vseq#y).m .|| < TK1/3 by A19; then
||. (vseq#x).n - (vseq#y).n .|| + ||. (vseq#y).n - (vseq#y).m .||
< ||. (vseq#x).n - (vseq#y).n .||+ TK1/3 by XREAL_1:10; then
A20: ||. (vseq#x).n - (vseq#y).n .||+ ||. (vseq#y).n - (vseq#y).m .||
+ ||. (vseq#y).m - (vseq#x).m .||
< ||. (vseq#x).n - (vseq#y).n .||+ TK1/3
+ ||. (vseq#y).m - (vseq#x).m .|| by XREAL_1:10;
||. (vseq#x).n - (vseq#y).m .||
<= ||. (vseq#x).n - (vseq#y).n .||
+ ||. (vseq#y).n - (vseq#y).m .|| by NORMSP_1:14; then
A21: ||. (vseq#x).n - (vseq#y).m .|| + ||. (vseq#y).m - (vseq#x).m .||
<= ||. (vseq#x).n - (vseq#y).n .||
+ ||. (vseq#y).n - (vseq#y).m .||
+ ||. (vseq#y).m - (vseq#x).m .|| by XREAL_1:8;
||. (vseq#x).n - (vseq#x).m .||
<= ||. (vseq#x).n - (vseq#y).m .||
+ ||. (vseq#y).m - (vseq#x).m .|| by NORMSP_1:14; then
||. (vseq#x).n -(vseq#x).m .||
<= ||. (vseq#x).n - (vseq#y).n .||
+ ||. (vseq#y).n - (vseq#y).m .||
+ ||. (vseq#y).m - (vseq#x).m .|| by A21,XXREAL_0:2; then
A22: ||. (vseq#x).n -(vseq#x).m .||
< ||. (vseq#x).n - (vseq#y).n .||+ TK1/3
+ ||. (vseq#y).m - (vseq#x).m .|| by A20,XXREAL_0:2;
reconsider f = vseq.n as bounded LinearOperator of X,Y
by LOPBAN_1:def 10;
A23: f in T by FUNCT_2:6;
||. (vseq#x).n-(vseq#y).n .||
= ||. (vseq.n).x-(vseq#y).n .|| by Def2; then
||. (vseq#x).n-(vseq#y).n .|| = ||.f.x-f.y.|| by Def2; then
A24: ||. (vseq#x).n-(vseq#y).n .|| <= M*||.x-y.|| by A9,A23;
M*||.x-y.||~~