:: Uniform Boundedness Principle
:: by Hideki Sakurai , Hisayoshi Kunimune and Yasunari Shidama
::
:: Received October 9, 2007
:: Copyright (c) 2007-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 NUMBERS, SEQ_1, REAL_1, XXREAL_2, CARD_1, XXREAL_0, ORDINAL2,
VALUED_1, RELAT_1, RINFSUP1, FUNCT_2, FUNCT_1, TARSKI, XBOOLE_0,
SUBSET_1, ARYTM_3, COMPLEX1, NAT_1, SEQ_4, MEMBER_1, LOPBAN_1, NORMSP_2,
REWRITE1, BHSP_3, RSSPACE3, METRIC_1, SEQ_2, NORMSP_1, PRE_TOPC, ARYTM_1,
STRUCT_0, PROB_1, RCOMP_1, PCOMPS_1, NFCONT_1, CFCONT_1, FCONT_1,
RLVECT_1, PARTFUN1, ZFMISC_1, CARD_3, SUPINF_2, PBOOLE, TOPS_1;
notations TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
XCMPLX_0, PRE_TOPC, TOPS_1, COMPLEX1, REAL_1, ORDINAL1, NAT_1, STRUCT_0,
CARD_3, NUMBERS, XREAL_0, RINFSUP1, XXREAL_0, VALUED_1, SEQ_1, SEQ_2,
SEQ_4, XXREAL_2, RLVECT_1, TBSP_1, METRIC_1, PCOMPS_1, NORMSP_0,
NORMSP_1, NORMSP_2, RSSPACE3, LOPBAN_1, NFCONT_1, INTEGRA2, KURATO_2;
constructors REAL_1, COMPLEX1, TOPS_1, TBSP_1, NFCONT_1, RINFSUP1, INTEGRA2,
PROB_1, NORMSP_2, RSSPACE3, LOPBAN_1, RVSUM_1, SEQ_4, RELSET_1, BINOP_2,
SEQ_2, PCOMPS_1, COMSEQ_2, BINOP_1;
registrations NUMBERS, XREAL_0, XBOOLE_0, ORDINAL1, RELSET_1, STRUCT_0,
MEMBERED, SUBSET_1, NAT_1, NORMSP_1, NORMSP_2, FUNCT_2, LOPBAN_1,
VALUED_0, VALUED_1, SEQ_2, NORMSP_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, RSSPACE3, XXREAL_2;
equalities RLVECT_1, METRIC_1, PCOMPS_1, NORMSP_2, RSSPACE3, LOPBAN_1,
RINFSUP1, CARD_3, XCMPLX_0, NORMSP_0;
expansions XXREAL_2;
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, SEQM_3, INTEGRA2, SEQ_4,
RSSPACE2, LOPBAN_1, LOPBAN_3, PROB_1, RSSPACE3, NAT_1, RELSET_1,
VECTSP_1, NORMSP_0, XXREAL_2, ORDINAL1;
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 that
A1: seq is bounded and
A2: 0<=r;
inferior_realsequence seq in Funcs(NAT,REAL) by FUNCT_2:8;
then
A3: 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:4;
then reconsider
X1 = rng inferior_realsequence seq as non empty Subset of REAL by A3;
now
let n be Element of NAT;
consider r1 be Real such that
A4: 0<r1 and
A5: for k be Nat holds |.seq.k.|<r1 by A1,SEQ_2:3;
seq ^\n in Funcs(NAT,REAL) by FUNCT_2:8;
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:4;
now
let k be Nat;
|.(seq ^\n).k.| = |.seq.(n+k).| by NAT_1:def 3;
hence |.(seq ^\n).k.| < r1 by A5;
end;
then seq ^\n is bounded by A4,SEQ_2:3;
then
A6: Y1 is bounded_below by RINFSUP1:6;
(inferior_realsequence (r(#)seq)).n = lower_bound((r(#)seq)^\n)
by RINFSUP1:36
.= lower_bound(r(#)(seq^\n)) by SEQM_3:21
.= lower_bound(r**Y1) by INTEGRA2:17
.= r * lower_bound(seq ^\n) by A2,A6,INTEGRA2:15
.= r * (inferior_realsequence seq).n by RINFSUP1:36;
hence
(inferior_realsequence (r (#) seq)).n = (r (#) (inferior_realsequence
seq)).n by SEQ_1:9;
end;
then inferior_realsequence (r (#) seq) = r (#) (inferior_realsequence seq)
by FUNCT_2:63;
then
A7: rng inferior_realsequence (r (#) seq) = r ** X1 by INTEGRA2:17;
inferior_realsequence seq is bounded by A1,RINFSUP1:56;
then X1 is bounded_above by RINFSUP1:5;
hence thesis by A2,A7,INTEGRA2:13;
end;
theorem
for seq be Real_Sequence, r be Real st seq is bounded & 0<=r holds
lim_sup(r(#)seq)=r*(lim_sup seq)
proof
let seq be Real_Sequence, r be Real;
assume that
A1: seq is bounded and
A2: 0<=r;
superior_realsequence seq in Funcs(NAT,REAL) by FUNCT_2:8;
then
A3: ex f be Function st superior_realsequence seq = f & dom f = NAT & rng f
c= REAL by FUNCT_2:def 2;
(superior_realsequence seq).0 in rng superior_realsequence seq by FUNCT_2:4;
then reconsider
X1 = rng superior_realsequence seq as non empty Subset of REAL by A3;
now
let n be Element of NAT;
consider r1 be Real such that
A4: 0<r1 and
A5: for k be Nat holds |.seq.k.|<r1 by A1,SEQ_2:3;
seq ^\n in Funcs(NAT,REAL) by FUNCT_2:8;
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:4;
now
let k be Nat;
|.(seq ^\n).k.| = |.seq.(n+k).| by NAT_1:def 3;
hence |.(seq ^\n).k.| < r1 by A5;
end;
then seq ^\n is bounded by A4,SEQ_2:3;
then
A6: Y1 is bounded_above by RINFSUP1:5;
(superior_realsequence (r (#) seq)).n = upper_bound ((r (#) seq) ^\n) by
RINFSUP1:37
.= upper_bound (r (#) (seq^\n)) by SEQM_3:21
.= upper_bound (r ** Y1) by INTEGRA2:17
.= r * upper_bound (seq ^\n) by A2,A6,INTEGRA2:13
.= r * (superior_realsequence seq).n by RINFSUP1:37;
hence
(superior_realsequence (r (#) seq)).n = (r (#) (superior_realsequence
seq)).n by SEQ_1:9;
end;
then superior_realsequence (r (#) seq) = r (#) (superior_realsequence seq)
by FUNCT_2:63;
then
A7: rng superior_realsequence (r (#) seq) = r ** X1 by INTEGRA2:17;
superior_realsequence seq is bounded by A1,RINFSUP1:56;
then X1 is bounded_below by RINFSUP1:6;
hence thesis by A2,A7,INTEGRA2:15;
end;
registration
let X be RealBanachSpace;
cluster MetricSpaceNorm X -> complete;
coherence
proof
now
let S1 be sequence of MetricSpaceNorm X;
reconsider S2=S1 as sequence of X;
assume
A1: S1 is Cauchy;
S2 is Cauchy_sequence_by_Norm
proof
let r be Real;
assume r > 0;
then consider p be Nat such that
A2: for n,m be Nat st p<=n & p<=m holds dist(S1.n,S1.m)
< r by A1,TBSP_1:def 4;
now
let n,m be 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 15;
hence S1 is convergent by NORMSP_2:5;
end;
hence thesis by TBSP_1:def 5;
end;
end;
definition
let X be RealNormSpace, x0 be Point of X, r be Real;
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;
::$N Baire Category Theorem (Banach spaces)
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 Nat holds Y.n is closed)
ex n0 be 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 that
A1: union rng Y = the carrier of X and
A2: for n be Nat holds Y.n is closed;
now
let n be Nat;
reconsider Yn = Y.n as Subset of TopSpaceNorm X;
Y.n is closed by A2;
then Yn is closed by NORMSP_2:15;
then Yn` is open by TOPS_1:3;
hence (Y.n)` in Family_open_set MetricSpaceNorm X by PRE_TOPC:def 2;
end;
then consider
n0 be Nat, r be Real, xx0 be Point of MetricSpaceNorm X
such that
A3: 0 < r & Ball(xx0,r) c= Y.n0 by A1,NORMSP_2:1;
consider x0 be Point of X such that
x0 = xx0 and
A4: 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 A3,A4;
end;
theorem Th4:
for X,Y be RealNormSpace, f be Lipschitzian 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 Lipschitzian LinearOperator of X,Y;
consider K being Real such that
A1: 0 <= K and
A2: for x being VECTOR of X holds ||. f.x .|| <= K * ||. x .|| by
LOPBAN_1:def 8;
A3: now
let x,y be Point of X;
assume that
x in the carrier of X and
y in the carrier of X;
f/.x -f/.y =f.x +(-1)* f.y by RLVECT_1:16;
then f/.x -f/.y = f.x + f.((-1)*y) by LOPBAN_1:def 5;
then f/.x -f/.y = f.(x+(-1)*y) by VECTSP_1:def 20;
then
A4: f/.x -f/.y =f.(x+-y) by RLVECT_1:16;
||.f/.x -f/.y .||<=K*||. x-y .||+||. x-y .|| by A2,A4,XREAL_1:38;
hence ||. f/.x -f/.y .|| <= (K+1) * ||. x-y .||;
end;
dom f =the carrier of X by FUNCT_2:def 1;
hence f is_Lipschitzian_on the carrier of X by A1,A3,NFCONT_1:def 9;
hence
A5: f is_continuous_on the carrier of X by NFCONT_1:45;
hereby
let x be Point of X;
f|(the carrier of X) = f by RELSET_1:19;
hence f is_continuous_in x by A5,NFCONT_1:def 7;
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
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 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 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 Lipschitzian
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 Lipschitzian LinearOperator of X,Y :
f in T};
now
let z be object;
assume z in y;
then
ex f be Lipschitzian 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 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 Lipschitzian
LinearOperator of X,Y :f in T};
defpred P[Nat,set] means $2={x where x is Point of X: Ta.x is
bounded_above & upper_bound(Ta.x) <= $1};
A5: 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 &
upper_bound(Ta.x) <=
n};
now
let z be object;
assume z in y;
then ex x be Point of X st z=x & Ta.x is bounded_above &
upper_bound(Ta.x) <=
n;
hence z in the carrier of X;
end;
hence thesis by TARSKI:def 3;
end;
ex Xn be sequence of bool the carrier of X st for n be Element of
NAT holds P[n,Xn.n] from FUNCT_2:sch 3(A5);
then consider Xn be sequence of bool the carrier of X such that
A6: for n be Element of NAT holds Xn.n = {x where x is Point of X: Ta
.x is bounded_above & upper_bound(Ta.x) <= n};
reconsider Xn as SetSequence of X;
A7: the carrier of X c= union rng Xn
proof
let x be object;
assume x in the carrier of X;
then reconsider x1=x as Point of X;
consider KTx1 be Real such that
0 <= KTx1 and
A8: for f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) st
f in T holds ||. f.x1 .|| <= KTx1 by A1;
A9: Ta.x1 = {||. f.x1 .|| where f is Lipschitzian LinearOperator of X,Y :f
in T} by A4;
A10: for p be Real st p in Ta.x1 holds p <= KTx1
proof
let p be Real;
assume p in Ta.x1;
then ex f be Lipschitzian LinearOperator of X,Y st p=||. f.x1 .|| &
f in T by A9;
hence thesis by A8;
end;
KTx1 is UpperBound of Ta.x1
proof
let p be ExtReal;
assume p in Ta.x1;
then ex f be Lipschitzian LinearOperator of X,Y st p=||. f.x1 .|| &
f in T by A9;
hence thesis by A8;
end;
then
A11: Ta.x1 is bounded_above;
consider n be Nat such that
A12: KTx1 <n by SEQ_4:3;
A13: n in NAT by ORDINAL1:def 12;
consider f be object such that
A14: f in T by A2,XBOOLE_0:def 1;
reconsider f as Lipschitzian LinearOperator of X,Y by A14,LOPBAN_1:def 9;
||. f.x1 .|| in Ta.x by A9,A14;
then upper_bound (Ta.x1) <= KTx1 by A10,SEQ_4:45;
then upper_bound (Ta.x1) <= n by A12,XXREAL_0:2;
then
x1 in {z1 where z1 is Point of X : Ta.z1 is bounded_above &
upper_bound (Ta.z1) <= n} by A11;
then x1 in Xn.n by A6,A13;
then x1 in Union Xn by PROB_1:12;
hence thesis;
end;
A15: for x be Point of X holds Ta.x is non empty
proof
let x be Point of X;
consider f0 be object such that
A16: f0 in T by A2,XBOOLE_0:def 1;
reconsider f0 as Lipschitzian LinearOperator of X,Y
by A16,LOPBAN_1:def 9;
Ta.x = {||. f.x .|| where f is Lipschitzian LinearOperator of X,Y :f in
T} by A4;
then ||. f0.x .|| in Ta.x by A16;
hence thesis;
end;
A17: for n be Nat holds Xn.n is closed
proof
let n be Nat;
A18: n in NAT by ORDINAL1:def 12;
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 that
A19: rng s1 c= Xn.n and
A20: s1 is convergent;
A21: Ta.(lim s1) = {||. f.(lim s1) .|| where f is Lipschitzian
LinearOperator of X,Y :f in T} by A4;
A22: for y be Real st y in Ta.(lim s1) holds y <= n
proof
let y be Real;
assume y in Ta.(lim s1);
then consider f be Lipschitzian LinearOperator of X,Y such that
A23: y=||. f.(lim s1) .|| and
A24: f in T by A21;
A25: f is_continuous_in lim s1 by Th4;
A26: dom f=the carrier of X by FUNCT_2:def 1;
then
A27: rng s1 c= dom f by A19,XBOOLE_1:1;
then
A28: f/*s1 is convergent by A20,A25,NFCONT_1:def 5;
for k be Nat holds ||. f/*s1 .||.k <= n
proof
let k be Nat;
A29: k in NAT by ORDINAL1:def 12;
||. f/*s1 .||.k = ||. (f/*s1).k .|| by NORMSP_0:def 4;
then
A30: ||. f/*s1 .||.k =||. f/.(s1.k) .|| by A19,A26,FUNCT_2:109,A29
,XBOOLE_1:1;
dom s1= NAT by FUNCT_2:def 1;
then s1.k in rng s1 by FUNCT_1:3,A29;
then s1.k in Xn.n by A19;
then s1.k in {x where x is Point of X : Ta.x is bounded_above &
upper_bound (Ta.x) <= n} by A6,A18;
then consider x be Point of X such that
A31: x=s1.k and
A32: Ta.x is bounded_above and
A33: upper_bound(Ta.x) <=n;
Ta.x = {||. g.x .|| where g is Lipschitzian LinearOperator of X,Y
:g in T} by A4;
then ||. f.(s1.k) .|| in Ta.(s1.k) by A24,A31;
then ||. f.(s1.k) .|| <= upper_bound (Ta.(s1.k))
by A31,A32,SEQ_4:def 1;
hence thesis by A30,A31,A33,XXREAL_0:2;
end;
then
A34: for i being Nat st 0 <= i holds ||. f/*s1 .||.i <=n;
f/.(lim s1) = lim (f/*s1) by A20,A25,A27,NFCONT_1:def 5;
then lim (||. f/*s1 .||) = ||. f/.(lim s1) .|| by A28,LOPBAN_1:20;
hence thesis by A23,A28,A34,NORMSP_1:23,RSSPACE2:5;
end;
then for y be ExtReal st y in Ta.(lim s1) holds y <= n;
then
A35: n is UpperBound of Ta.(lim s1) by XXREAL_2:def 1;
Ta.(lim s1) is non empty by A15;
then
A36: upper_bound(Ta.(lim s1)) <= n by A22,SEQ_4:45;
A37: Xn.n = {x where x is Point of X : Ta.x is bounded_above &
upper_bound (Ta
.x) <= n} by A6,A18;
Ta.(lim s1) is bounded_above by A35;
hence thesis by A36,A37;
end;
hence thesis by NFCONT_1:def 3;
end;
consider f be object such that
A38: f in T by A2,XBOOLE_0:def 1;
reconsider f as Lipschitzian LinearOperator of X,Y by A38,LOPBAN_1:def 9;
union rng Xn is Subset of X by PROB_1:11;
then union rng Xn = the carrier of X by A7,XBOOLE_0:def 10;
then consider n0 be Nat, r be Real,
x0 be Point of X such that
A39: 0 < r and
A40: S0(x0,r) c= Xn.n0 by A17,Th3;
A41: n0 in NAT by ORDINAL1:def 12;
||.x0-x0.||=||.0.X.|| by RLVECT_1:5;
then x0 in S0(x0,r) by A39;
then x0 in Xn.n0 by A40;
then x0 in {x1 where x1 is Point of X : Ta.x1 is bounded_above &
upper_bound (Ta.
x1) <= n0} by A6,A41;
then consider xx1 be Point of X such that
A42: xx1=x0 and
A43: Ta.xx1 is bounded_above and
upper_bound (Ta.xx1) <= n0;
Ta.xx1 = {||. g.xx1 .|| where g is Lipschitzian LinearOperator of X,Y :g
in T } by A4;
then ||. f.x0 .|| in Ta.x0 by A42,A38;
then ||. f.x0 .|| <= upper_bound(Ta.x0) by A42,A43,SEQ_4:def 1;
then
A44: 0<= upper_bound (Ta.x0);
A45: for x be Point of X st x <> 0.X holds r/(2*||.x.||)*x+x0 in S0(x0,r)
proof
let x be Point of X;
reconsider x1= (||.x.||")*x as Point of X;
A46: ||.(r/2)*x1.|| = |.r/2.|*||.x1.|| by NORMSP_1:def 1;
assume x <> 0.X;
then
A47: ||.x.|| <> 0 by NORMSP_0:def 5;
||. r/(2*||.x.||)*x+x0-x0.|| =||.r/(2*||.x.||)*x+(x0+-x0).|| by
RLVECT_1:def 3;
then ||. r/(2*||.x.||)*x+x0-x0.|| =||.r/(2*||.x.||)*x+0.X.|| by
RLVECT_1:5;
then ||. r/(2*||.x.||)*x+x0-x0.|| =||.r/(2*||.x.||)*x.|| by
RLVECT_1:def 4;
then ||. r/(2*||.x.||)*x+x0-x0.|| =||.r/2/(||.x.||)*x.|| by XCMPLX_1:78;
then
A48: ||. r/(2*||.x.||)*x+x0-x0.|| =||.(r/2)*x1.|| by RLVECT_1:def 7;
A49: |. ||.x.||".| =||.x.||" by ABSVALUE:def 1;
||.x1.|| = |. ||.x.||".|*||.x.|| by NORMSP_1:def 1;
then ||.x1.|| = 1 by A47,A49,XCMPLX_0:def 7;
then ||.(r/2)*x1.|| = r/2 by A39,A46,ABSVALUE:def 1;
then
A50: ||.x0-(r/(2*||.x.||)*x+x0).|| =r/2 by A48,NORMSP_1:7;
r/2<r by A39,XREAL_1:216;
hence thesis by A50;
end;
set M=upper_bound(Ta.x0);
take KT=2*(M+n0)/r;
A51: for f be Lipschitzian LinearOperator of X,Y st f in T for x be Point of X
st x in S0(x0,r) holds ||. f.x .|| <= n0
proof
let f be Lipschitzian LinearOperator of X,Y;
assume
A52: f in T;
A53: n0 in NAT by ORDINAL1:def 12;
let x be Point of X;
assume x in S0(x0,r);
then x in Xn.n0 by A40;
then
x in {x1 where x1 is Point of X : Ta.x1 is bounded_above &
upper_bound (Ta.
x1) <= n0} by A6,A53;
then consider x1 be Point of X such that
A54: x1=x and
A55: Ta.x1 is bounded_above and
A56: upper_bound(Ta.x1) <= n0;
Ta.x1 = {||. g.x1 .|| where g is Lipschitzian LinearOperator of X,Y :g
in T} by A4;
then ||. f.x .|| in Ta.x by A52,A54;
then ||. f.x .|| <= upper_bound (Ta.x) by A54,A55,SEQ_4:def 1;
hence thesis by A54,A56,XXREAL_0:2;
end;
A57: now
let f be Lipschitzian LinearOperator of X,Y;
assume
A58: f in T;
A59: for x be Point of X st x <> 0.X holds ||.f.x.|| <= KT*||.x.||
proof
A60: n0 in NAT by ORDINAL1:def 12;
||.x0-x0.||=||.0.X.|| by RLVECT_1:5;
then x0 in S0(x0,r) by A39;
then x0 in Xn.n0 by A40;
then
A61: x0 in {x1 where x1 is Point of X : Ta.x1 is bounded_above &
upper_bound(
Ta.x1) <= n0} by A6,A60;
set nr3=||.f.x0.||;
let x be Point of X;
set nrp1=r/(2*||.x.||);
set nrp2=(2*||.x.||)/r;
set nr1=||.f.(r/(2*||.x.||)*x)+f.x0.||;
set nr2=||.f.(r/(2*||.x.||)*x).||;
||.-(f.x0).||=||.f.x0.|| by NORMSP_1:2;
then
A62: nr2-nr3<=||.f.(r/(2*||.x.||)*x)-(-f.x0).|| by NORMSP_1:8;
assume
A63: x <> 0.X;
then
A64: ||. f.(r/(2*||.x.||)*x+x0) .|| <= n0 by A51,A45,A58;
consider x1 be Point of X such that
A65: x1=x0 and
A66: Ta.x1 is bounded_above and
upper_bound (Ta.x1) <= n0 by A61;
Ta.x1 = {||. g.x1 .|| where g is Lipschitzian LinearOperator of X,Y :
g in T } by A4;
then ||. f.x0 .|| in Ta.x0 by A58,A65;
then ||. f.x0 .|| <= upper_bound (Ta.x0) by A65,A66,SEQ_4:def 1;
then
A67: nrp1*||.f.x.|| - M <= nrp1*||.f.x.|| - nr3 by XREAL_1:10;
||.x.|| <> 0 by A63,NORMSP_0:def 5;
then
A68: ||.x.|| >0;
||. f.(r/(2*||.x.||)*x).|| =||.(r/(2*||.x.||))*f.x.|| by LOPBAN_1:def 5
;
then
||. f.(r/(2*||.x.||)*x).|| =|.r/(2*||.x.||).|*||.f.x.|| by NORMSP_1:def 1;
then ||. f.(r/(2*||.x.||)*x).|| =(r/(2*||.x.||))*||.f.x.|| by A39,
ABSVALUE:def 1;
then ||.f.(r/(2*||.x.||)*x)+f.x0.|| =||.f.(r/(2*||.x.||)*x+x0).|| & (
r/(2*||.x.|| ))*||.f.x.||-nr3<=nr1 by A62,RLVECT_1:17,VECTSP_1:def 20;
then (r/(2*||.x.||))*||.f.x.||-nr3<=n0 by A64,XXREAL_0:2;
then nrp1*||.f.x.|| - M <= n0 by A67,XXREAL_0:2;
then nrp1*||.f.x.|| + -M + M <= n0 + M by XREAL_1:6;
then nrp2*(nrp1*||.f.x.||) <= nrp2*(n0+M) by A39,XREAL_1:64;
then
A69: nrp1*nrp2*||.f.x.|| <= nrp2*(n0+M);
2*||.x.|| >0 by A68,XREAL_1:129;
then 1*||.f.x.|| <= nrp2*(n0+M) by A39,A69,XCMPLX_1:112;
hence thesis;
end;
A70: for x be Point of X holds ||.f.x.|| <= KT*||.x.||
proof
let x be Point of X;
now
assume
A71: x = 0.X;
then f.x = f.(0*0.X) by RLVECT_1:10;
then f.x =0*f.(0.X) by LOPBAN_1:def 5;
then
A72: f.x =0.Y by RLVECT_1:10;
||.x.||= 0 by A71;
hence thesis by A72;
end;
hence thesis by A59;
end;
thus for k be Real st k in {||.f.x1.|| where x1 is Point of X :
||.x1.|| <= 1 } holds k <= KT
proof
let k be Real;
assume k in {||.f.x1.|| where x1 is Point of X : ||.x1.|| <= 1};
then consider x be Point of X such that
A73: k=||.f.x.|| & ||.x.|| <= 1;
k <= KT*||.x.|| & KT*||.x.|| <=KT by A39,A44,A70,A73,XREAL_1:153;
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 Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
assume f in T;
then
A74: for k be Real st k in PreNorms(f1) holds k <= KT by A57;
||. f .|| = upper_bound PreNorms(f1) by LOPBAN_1:30;
hence thesis by A74,SEQ_4:45;
end;
hence thesis by A39,A44;
end;
suppose
A75: T = {};
take 0;
thus thesis by A75;
end;
end;
definition
let X, Y be RealNormSpace, H be sequence of 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 Nat holds it.n = (H.n).x;
existence
proof
deffunc U(Nat) = (H.$1).x;
consider f being sequence of the carrier of Y such that
A1: for n be Element of NAT holds f.n = U(n) from FUNCT_2:sch 4;
take f;
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
uniqueness
proof
let S1,S2 be sequence of Y such that
A2: for n be Nat holds S1.n = (H.n).x and
A3: for n be Nat holds S2.n = (H.n).x;
now
let n be Element of NAT;
S1.n = (H.n).x by A2;
hence S1.n = S2.n by A3;
end;
hence thesis by FUNCT_2:63;
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
Lipschitzian 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;
set T=rng vseq;
set RNS=R_NormSpace_of_BoundedLinearOperators(X,Y);
assume
A1: for x be Point of X holds vseq#x is convergent & tseq.x = lim(vseq#x );
A2: for x,y be Point of X holds tseq.(x+y)= tseq.x + tseq.y
proof
let x,y be Point of X;
A3: vseq#y is convergent & tseq.y = lim (vseq#y) by A1;
A4: tseq.(x+y) = lim (vseq#(x+y)) by A1;
now
let n be Nat;
vseq.n is Lipschitzian LinearOperator of X,Y & (vseq#(x+y)).n=(vseq.n).(
x+y) by Def2,LOPBAN_1:def 9;
then
A5: (vseq#(x+y)).n=(vseq.n).x + (vseq.n).y by VECTSP_1:def 20;
(vseq.n).y = (vseq#y).n by Def2;
hence (vseq#(x+y)).n=(vseq#x).n + (vseq#y).n by A5,Def2;
end;
then
A6: vseq#(x+y) = vseq#x + vseq#y by NORMSP_1:def 2;
vseq#x is convergent & tseq.x = lim (vseq#x) by A1;
hence thesis by A3,A6,A4,NORMSP_1:25;
end;
A7: for x be Point of X ex K be Real 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 bounded by NORMSP_1:23,SEQ_2:13;
then consider K be Real such that
A8: for n be Nat holds ||. vseq#x .||.n< K by SEQ_2:def 3;
A9: 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 object such that
A10: n in NAT and
A11: f=vseq.n by FUNCT_2:11;
reconsider n as Nat by A10;
(vseq.n).x = (vseq#x).n by Def2;
then ||. f.x .|| = ||. vseq#x .||.n by A11,NORMSP_0:def 4;
hence thesis by A8;
end;
||. vseq#x .||.0< K by A8;
then ||. (vseq#x).0 .|| < K by NORMSP_0:def 4;
then 0 <= K;
hence thesis by A9;
end;
vseq in Funcs(NAT,the carrier of RNS) by FUNCT_2:8;
then
ex f0 being Function st vseq = f0 & dom f0 = NAT & rng f0 c= the carrier
of RNS by FUNCT_2:def 2;
then consider L be Real such that
A12: 0 <= L and
A13: for f be Point of RNS st f in T holds ||.f.|| <= L by A7,Th5;
A14: L + 0 < 1+ L by XREAL_1:8;
for n be Nat holds |.||.vseq.||.n .| < (1+L)
proof
let n be Nat;
A15: n in NAT by ORDINAL1:def 12;
||.vseq.n.|| <= L by A13,FUNCT_2:4,A15;
then ||.vseq.||.n <= L by NORMSP_0:def 4;
then
A16: ||.vseq.||.n <(1+L) by A14,XXREAL_0:2;
0<=||.vseq.n.||;
then 0<=||.vseq.||.n by NORMSP_0:def 4;
hence thesis by A16,ABSVALUE:def 1;
end;
then
A17: ||.vseq.|| is bounded by A12,SEQ_2:3;
A18: for x be Point of X holds ||.tseq.x.|| <=( lim_inf ||.vseq.|| ) * ||.x .||
proof
let x be Point of X;
A19: ||.x.|| (#) ||.vseq .|| is bounded by A17,SEQM_3:37;
A20: for n be Nat holds ||.(vseq#x).n.|| <= ||.vseq.n.|| * ||.x .||
proof
let n be Nat;
(vseq.n).x = (vseq#x).n & vseq.n is Lipschitzian LinearOperator of X,Y
by Def2,LOPBAN_1:def 9;
hence thesis by LOPBAN_1:32;
end;
A21: for n be Nat holds ||. vseq#x .||.n <= (||.x.|| (#) ||.
vseq .||).n
proof
let n be Nat;
A22: ||.vseq.n.|| = ||.vseq.||.n by NORMSP_0:def 4;
||. vseq#x .||.n = ||.(vseq#x).n .|| & ||.(vseq#x).n .|| <= ||.vseq
.n.|| * ||.x.|| by A20,NORMSP_0:def 4;
hence thesis by A22,SEQ_1:9;
end;
A23: lim_inf (||.x.|| (#) ||.vseq .||) = ( lim_inf ||.vseq.|| ) * ||.x.||
by A17,Th1;
A24: vseq#x is convergent & tseq.x = lim(vseq#x) by A1;
then ||. vseq#x .|| is convergent by LOPBAN_1:20;
then
A25: lim ||. vseq#x .|| = lim_inf ||. vseq#x .|| by RINFSUP1:89;
||. vseq#x .|| is bounded by A24,LOPBAN_1:20,SEQ_2:13;
then lim_inf ||. vseq#x .|| <=lim_inf (||.x.|| (#) ||.vseq .||) by A19,A21,
RINFSUP1:91;
hence thesis by A24,A23,A25,LOPBAN_1:20;
end;
now
let s be Real;
assume
A26: 0<s;
for k be Nat holds 0-s < ||.vseq.||.(0+k)
proof
let k be Nat;
||.vseq.k.||=||.vseq.||.k by NORMSP_0:def 4;
then 0<=||.vseq.||.k;
hence thesis by A26;
end;
hence ex n be Nat st for k be Nat holds 0-s<||.vseq.||.(n+k);
end;
then
A27: 0 <= lim_inf||.vseq.|| by A17,RINFSUP1:82;
A28: for x be Point of X, r be Real holds tseq.(r*x)= r*tseq.x
proof
let x be Point of X, r be Real;
A29: tseq.x = lim(vseq#x) by A1;
A30: now
let n be Nat;
vseq.n is Lipschitzian LinearOperator of X,Y & (vseq#(r*x)).n=(vseq.n).(
r*x) by Def2,LOPBAN_1:def 9;
then (vseq#(r*x)).n=r*(vseq.n).x by LOPBAN_1:def 5;
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 A30,NORMSP_1:def 5;
hence thesis by A1,A29,NORMSP_1:28;
end;
then reconsider tseq1 = tseq as Lipschitzian LinearOperator of X,Y
by A2,A18,A27,LOPBAN_1:def 5,def 8,VECTSP_1:def 20;
for ttseq be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) st
ttseq = tseq holds ||.ttseq.|| <=( lim_inf ||.vseq.|| )
proof
for k be Real st k in {||.tseq.x1.|| where x1 is Point of X :
||.x1.|| <= 1 } holds k <= ( lim_inf ||.vseq.|| )
proof
let k be Real;
assume k in {||.tseq.x1.|| where x1 is Point of X : ||.x1.|| <= 1 };
then consider x be Point of X such that
A31: k=||.tseq.x.|| & ||.x.|| <= 1;
k <= (lim_inf ||.vseq.||) * ||.x.|| & (lim_inf ||.vseq.||) * ||.x
.|| <= lim_inf ||.vseq.|| by A18,A27,A31,XREAL_1:153;
hence thesis by XXREAL_0:2;
end;
then
A32: upper_bound PreNorms(tseq1) <=lim_inf ||.vseq.|| by SEQ_4:45;
let ttseq be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
assume ttseq=tseq;
hence thesis by A32,LOPBAN_1:30;
end;
hence thesis by A2,A28,A18,A27,LOPBAN_1:def 5,def 8,VECTSP_1:def 20;
end;
begin :: Banach-Steinhaus Principle
::$N Banach-Steinhaus theorem (uniform boundedness)
theorem Th7:
for X be RealBanachSpace, X0 be Subset of LinearTopSpaceNorm(X),
Y be RealBanachSpace, vseq be sequence of R_NormSpace_of_BoundedLinearOperators
(X,Y) st X0 is dense & (for x be Point of X st x in X0 holds vseq#x is
convergent) & (for x be Point of X ex K be Real st 0<=K & for n be
Nat holds ||.(vseq#x).n.|| <=K) holds for x be Point of X holds vseq
#x is convergent
proof
let X be RealBanachSpace, X0 be Subset of LinearTopSpaceNorm(X), Y be
RealBanachSpace, vseq be sequence of R_NormSpace_of_BoundedLinearOperators(X,Y)
;
assume
A1: X0 is dense;
set T=rng vseq;
assume
A2: for x be Point of X st x in X0 holds vseq#x is convergent;
vseq in Funcs(NAT,the carrier of R_NormSpace_of_BoundedLinearOperators(X
,Y) ) by FUNCT_2:8;
then
ex f0 being Function st vseq = f0 & dom f0 = NAT & rng f0 c= the carrier
of R_NormSpace_of_BoundedLinearOperators(X,Y) by FUNCT_2:def 2;
then reconsider T as Subset of R_NormSpace_of_BoundedLinearOperators(X,Y);
assume
A3: for x be Point of X ex K be Real st 0<=K &
for n be Nat holds ||.(vseq#x).n.|| <=K;
for x be Point of X ex K be Real st 0 <= K & for f be Point of
R_NormSpace_of_BoundedLinearOperators(X,Y) st f in T holds ||. f.x .|| <= K
proof
let x be Point of X;
consider K be Real such that
A4: 0<= K and
A5: for n be Nat holds ||.(vseq#x).n.|| <=K by A3;
take K;
now
let f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
assume f in T;
then consider n be object such that
A6: n in NAT and
A7: f=vseq.n by FUNCT_2:11;
reconsider n as Nat by A6;
||. f.x .|| = ||.(vseq#x).n.|| by A7,Def2;
hence ||. f.x .|| <= K by A5;
end;
hence thesis by A4;
end;
then consider L be Real such that
A8: 0 <= L and
A9: for f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y) st f
in T holds ||.f.|| <= L by Th5;
set M=1+L;
A10: L+0<M by XREAL_1:8;
A11: for f be Lipschitzian LinearOperator of X,Y st f in T for x,y be Point
of X holds ||. f.x -f.y.|| <= M*||.x-y.||
proof
let f be Lipschitzian LinearOperator of X,Y;
reconsider f1=f as Point of R_NormSpace_of_BoundedLinearOperators(X,Y) by
LOPBAN_1:def 9;
assume f in T;
then ||.f1.|| <= L by A9;
then
A12: ||.f1.|| < M by A10,XXREAL_0:2;
let x,y be Point of X;
||. f.x -f.y.|| = ||. f.x +(-1)*(f.y).|| by RLVECT_1:16;
then ||. f.x -f.y.|| = ||. f.x +(f.((-1)*y)).|| by LOPBAN_1:def 5;
then ||. f.x -f.y.|| = ||. f.(x +(-1)*y).|| by VECTSP_1:def 20;
then
A13: ||. f.x -f.y.|| = ||. f.(x -y).||by RLVECT_1:16;
||. f.(x -y).|| <=||.f1.|| * ||.x-y.|| & ||.f1.||* ||.x-y.|| <= M*
||.x-y.|| by A12,LOPBAN_1:32,XREAL_1:64;
hence thesis by A13,XXREAL_0:2;
end;
hereby
let x be Point of X;
for TK1 be Real st TK1 > 0 ex n0 be Nat st for n,m be
Nat st n >= n0 & m >= n0 holds ||.(vseq#x).n -(vseq#x).m.||< TK1
proof
let TK1 be Real such that
A14: TK1 > 0;
A15: 0<TK1/3 by A14,XREAL_1:222;
set V = {z where z is Point of X : ||.x-z.|| <TK1/(3*M) };
V c= the carrier of X
proof
let s be object;
assume s in V;
then ex z be Point of X st s=z & ||.x-z.|| <TK1/(3*M);
hence thesis;
end;
then reconsider V as Subset of LinearTopSpaceNorm(X) by NORMSP_2:def 4;
reconsider TKK=TK1 as Real;
0 < (3*M) by A8,XREAL_1:129;
then 0 < TK1/(3*M) by A14,XREAL_1:139;
then ||.x-x.|| <TKK/(3*M) by NORMSP_1:6;
then V is open & x in V by NORMSP_2:23;
then X0 meets V by A1,TOPS_1:45;
then consider s be object such that
A16: s in X0 and
A17: s in V by XBOOLE_0:3;
consider y be Point of X such that
A18: s=y and
A19: ||.x-y.|| < TK1/(3*M) by A17;
for s be Real st 0<s ex n1 be Nat st
for m1 be Nat st n1<=m1 holds ||.(vseq#y).m1 -(vseq#y).n1.||<s
by A2,A16,A18,
LOPBAN_3:4;
then vseq#y is Cauchy_sequence_by_Norm by LOPBAN_3:5;
then consider n0 be Nat such that
A20: for n, m be Nat st n >= n0 & m >= n0 holds ||.((vseq
#y).n) - ((vseq#y).m).|| < TK1/3 by A15,RSSPACE3:8;
take n0;
for n, m be Nat st n >= n0 & m >= n0 holds ||.(vseq#x).n
-(vseq#x).m.||< TK1
proof
let n,m be Nat;
A21: m in NAT by ORDINAL1:def 12;
A22: n in NAT by ORDINAL1:def 12;
reconsider f = vseq.n as Lipschitzian LinearOperator of X,Y by
LOPBAN_1:def 9;
reconsider g =vseq.m as Lipschitzian LinearOperator of X,Y
by LOPBAN_1:def 9;
||. (vseq#x).n - (vseq#y).m .|| <= ||. (vseq#x).n - (vseq#y).n
.|| + ||. (vseq#y).n - (vseq#y).m .|| by NORMSP_1:10;
then
A23: ||. (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:6;
assume n >= n0 & m >= n0;
then ||. (vseq#y).n - (vseq#y).m .|| < TK1/3 by A20;
then
||. (vseq#x).n - (vseq#y).n .|| + ||. (vseq#y).n - (vseq#y).m .||
< ||. (vseq#x).n - (vseq#y).n .||+ TK1/3 by XREAL_1:8;
then
A24: ||. (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:8;
||. (vseq#x).m-(vseq#y).m .|| = ||. (vseq.m).x-(vseq#y).m .|| by Def2;
then ||. (vseq#x).m-(vseq#y).m .|| = ||. g.x-g.y.|| by Def2;
then
A25: ||. (vseq#x).m-(vseq#y).m .|| <= M*||.x-y.|| by A11,FUNCT_2:4,A21;
M*||.x-y.||<M* (TK1 / (3*M)) by A8,A19,XREAL_1:68;
then M*||.x-y.||< TK1/3 by A8,XCMPLX_1:92;
then ||. (vseq#x).m-(vseq#y).m .|| < TK1/3 by A25,XXREAL_0:2;
then ||. (vseq#y).m-(vseq#x).m .||< TK1/3 by NORMSP_1:7;
then
A26: TK1/3 + TK1/3 + ||. (vseq#y).m-(vseq#x).m .|| < TK1/3 + TK1/3 +
TK1/3 by XREAL_1:8;
||. (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
A27: ||. (vseq#x).n-(vseq#y).n .|| <= M*||.x-y.|| by A11,FUNCT_2:4,A22;
||. (vseq#x).n - (vseq#x).m .|| <= ||. (vseq#x).n - (vseq#y).m
.|| + ||. (vseq#y).m - (vseq#x).m .|| by NORMSP_1:10;
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 A23,
XXREAL_0:2;
then
A28: ||. (vseq#x).n -(vseq#x).m .|| < ||. (vseq#x).n - (vseq#y).n .||+
TK1/3 + ||. (vseq#y).m - (vseq#x).m .|| by A24,XXREAL_0:2;
M*||.x-y.||<M* (TK1 / (3*M)) by A8,A19,XREAL_1:68;
then M*||.x-y.||< TK1/3 by A8,XCMPLX_1:92;
then ||. (vseq#x).n - (vseq#y).n.|| < TK1/3 by A27,XXREAL_0:2;
then ||. (vseq#x).n-(vseq#y).n .||+ TK1/3 < TK1/3+TK1/3 by XREAL_1:8;
then
||. (vseq#x).n - (vseq#y).n .||+ TK1/3 + ||. (vseq#y).m - (vseq#x
).m .|| < TK1/3 + TK1/3 + ||. (vseq#y).m - (vseq#x).m .|| by XREAL_1:8;
then
||. (vseq#x).n-(vseq#y).n .|| + TK1/3 + ||. (vseq#y).m-(vseq#x).m
.|| < TK1/3 + TK1/3 + TK1/3 by A26,XXREAL_0:2;
hence thesis by A28,XXREAL_0:2;
end;
hence thesis;
end;
then vseq#x is Cauchy_sequence_by_Norm by RSSPACE3:8;
hence vseq#x is convergent by LOPBAN_1:def 15;
end;
end;
theorem
for X,Y be RealBanachSpace, X0 be Subset of LinearTopSpaceNorm(X),
vseq be sequence of R_NormSpace_of_BoundedLinearOperators(X,Y) st X0 is dense &
( for x be Point of X st x in X0 holds vseq#x is convergent ) & ( for x be
Point of X ex K be Real st 0<=K & ( for n be Nat holds ||. (
vseq#x).n .|| <= K ) ) holds ex tseq be Point of
R_NormSpace_of_BoundedLinearOperators(X,Y) st ( for x be Point of X holds vseq#
x is convergent & tseq.x=lim (vseq#x) & ||.tseq.x.|| <= lim_inf ||.vseq.|| *
||.x.|| ) & ||.tseq.|| <= lim_inf ||.vseq.||
proof
let X,Y be RealBanachSpace, X0 be Subset of LinearTopSpaceNorm(X), vseq be
sequence of R_NormSpace_of_BoundedLinearOperators(X,Y);
assume
A1: X0 is dense;
deffunc F(Point of X) = lim(vseq#$1);
assume
A2: for x be Point of X st x in X0 holds vseq#x is convergent;
consider tseq be Function of X,Y such that
A3: for x be Point of X holds tseq.x=F(x) from FUNCT_2:sch 4;
assume for x be Point of X ex K be Real st 0<=K &
for n be Nat holds ||.(vseq#x).n.|| <= K;
then
A4: for x be Point of X holds vseq#x is convergent by A1,A2,Th7;
then reconsider tseq as Lipschitzian LinearOperator of X,Y by A3,Th6;
reconsider tseq as Point of R_NormSpace_of_BoundedLinearOperators(X,Y) by
LOPBAN_1:def 9;
take tseq;
thus thesis by A4,A3,Th6;
end;