:: Weak Convergence and Weak* Convergence
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received July 1, 2015
:: Copyright (c) 2015-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 RLSUB_1, HAHNBAN, UNIALG_1, DUALSP01, DUALSP02, DUALSP03, PBOOLE,
INT_1, NFCONT_1, CFCONT_1, RLVECT_1, ARYTM_1, RELAT_1, FUNCT_1, RSSPACE,
RSSPACE3, REAL_1, TARSKI, MSSUBFAM, STRUCT_0, SEQ_1, FUNCOP_1, FCONT_1,
SEQ_2, LOPBAN_1, ORDINAL2, ARYTM_3, NORMSP_1, FUNCT_2, PRE_TOPC,
SUBSET_1, ZFMISC_1, NUMBERS, SEQ_4, XBOOLE_0, CARD_1, SUPINF_2, COMPLEX1,
XXREAL_0, XXREAL_2, NAT_1, REWRITE1, VALUED_1, METRIC_1, ASYMPT_1,
PARTFUN1, RCOMP_1, NORMSP_2, RLVECT_3, NORMSP_3, TOPS_1, TOPGEN_1,
VALUED_0;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1,
ORDINAL1, RELSET_1, PARTFUN1,
FUNCT_2, FUNCOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1,
VALUED_0, COMPLEX1, XXREAL_2, VALUED_1, SEQ_1, SEQ_2, SEQ_4, RINFSUP1,
STRUCT_0, PRE_TOPC, TOPS_1, RLVECT_1, RLSUB_1, RLVECT_3, NORMSP_0,
NORMSP_1, HAHNBAN, RSSPACE, RSSPACE3, LOPBAN_1, NFCONT_1, NORMSP_2,
LOPBAN_5, DUALSP01, NORMSP_3, DUALSP02;
constructors REAL_1, EUCLID, REALSET1, RSSPACE3, BINOP_2, SEQ_1, NFCONT_1,
RELSET_1, SEQ_2, SEQ_4, HAHNBAN1, NORMSP_2, RLVECT_3, LOPBAN_5, COMSEQ_2,
NORMSP_3, TOPS_1, DUALSP02, RINFSUP1, CARD_3;
registrations STRUCT_0, XREAL_0, NUMBERS, ORDINAL1, MEMBERED, RELAT_1,
XXREAL_0, VALUED_0, FUNCT_2, VALUED_1, FUNCOP_1, SEQ_4, RELSET_1,
FUNCT_1, NORMSP_3, XCMPLX_0, NORMSP_0, NAT_1, NORMSP_1, SEQ_2, DUALSP01,
XBOOLE_0, SEQM_3, INT_1, PRE_TOPC, NORMSP_4;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions HAHNBAN, TARSKI;
equalities STRUCT_0, ALGSTR_0, NORMSP_0, SEQ_1, DUALSP02, DUALSP01;
expansions TARSKI, XBOOLE_0, FUNCT_2, SEQ_2, NORMSP_1, STRUCT_0, SEQM_3,
XXREAL_2, NFCONT_1, DUALSP01;
theorems SEQ_4, FUNCT_1, SEQ_1, SEQ_2, ABSVALUE, COMPLEX1, TARSKI, RSSPACE3,
XREAL_0, XXREAL_0, NORMSP_1, LOPBAN_1, FUNCT_2, XBOOLE_0, XREAL_1,
RLVECT_1, FUNCOP_1, HAHNBAN, NORMSP_0, ORDINAL1, NAT_1, NORMSP_3, INT_1,
NFCONT_1, XXREAL_2, SEQM_3, DUALSP01, RELAT_1, XCMPLX_1, NORMSP_2,
BINOP_2, NUMBERS, LOPBAN_5, RLVECT_3, VALUED_0, DUALSP02, RINFSUP1,
EUCLID, NORMSP_4;
schemes FUNCT_2, RECDEF_1, NAT_1, RECDEF_2;
begin :: Some properties about Dual Spaces of Real Normed Spaces
definition
let X be non empty set;
let F be sequence of Funcs(NAT,X);
let k be Nat;
redefine func F.k -> sequence of X; :: redefines . (FUNCT_1, definition)
correctness
proof
ex f being Function st F.k = f & dom f = NAT & rng f c= X by FUNCT_2:def 2;
hence thesis by FUNCT_2:2;
end;
end;
theorem Lm73:
for X be strict RealNormSpace, A be non empty Subset of X holds
(for f be Point of DualSp X st
(for x be Point of X st x in A holds (Bound2Lipschitz(f,X)).x = 0)
holds Bound2Lipschitz(f,X) = 0.(DualSp X))
implies ClNLin(A) = X
proof
let X be strict RealNormSpace, A be non empty Subset of X;
assume
A0: for f be Point of DualSp X st
(for x be Point of X st x in A holds (Bound2Lipschitz(f,X)).x = 0)
holds Bound2Lipschitz(f,X) = 0.(DualSp X);
set M = ClNLin(A);
consider Z be Subset of X such that
Q0: Z = the carrier of Lin(A)
& M = NORMSTR(# Cl(Z), Zero_(Cl(Z),X), Add_(Cl(Z),X),
Mult_(Cl(Z),X), Norm_(Cl(Z),X) #) by NORMSP_3:def 20;
reconsider Y = the carrier of M as non empty Subset of X
by DUALSP01:def 16;
Q23: Y is linearly-closed by NORMSP_3:29;
Y = the carrier of X
proof
assume Y <> the carrier of X; then
not the carrier of X c= Y; then
consider x0 be object such that
Q25: x0 in the carrier of X & not x0 in Y;
reconsider x0 as Point of X by Q25;
consider G be Point of DualSp X such that
Q26: (for x be Point of X
st x in Y holds (Bound2Lipschitz(G,X)).x = 0) and
Q27: (Bound2Lipschitz(G,X)).x0 = 1 by Q0,Q23,Q25,DUALSP02:2;
for x be Point of X
st x in A holds (Bound2Lipschitz(G,X)).x = 0
proof
let x be Point of X;
assume x in A; then
x in Lin(A) by RLVECT_3:15; then
x in Y by Q0,NORMSP_3:4,TARSKI:def 3;
hence (Bound2Lipschitz(G,X)).x = 0 by Q26;
end; then
(Bound2Lipschitz(G,X)).x0 = (0.(DualSp X)).x0 by A0
.= ((the carrier of X) --> 0).x0 by DUALSP01:25
.= 0;
hence contradiction by Q27;
end;
hence M = X by Q0,NORMSP_3:26;
end;
theorem Th73:
for X be strict RealNormSpace st DualSp X is separable holds X is separable
proof
let X be strict RealNormSpace;
set Y = DualSp X;
assume Y is separable; then
consider Yseq be sequence of Y such that
P1: rng Yseq is dense by NORMSP_3:21;
defpred P[Nat,Point of X] means
||.Yseq.$1.|| /2 <= |.(Yseq.$1).$2.| & ||.$2.|| <= 1;
F2: for n be Element of NAT ex x be Point of X st P[n,x]
proof
let n be Element of NAT;
per cases;
suppose A1: ||.Yseq.n.|| = 0;
set x = 0.X;
take x;
thus ||.Yseq.n.|| /2 <= |.(Yseq.n).x.| by A1,COMPLEX1:46;
thus ||.x.|| <= 1;
end;
suppose A21: ||.Yseq.n.|| <> 0;
assume
A31: not (ex x be Point of X st
||.Yseq.n.|| /2 <= |.(Yseq.n).x.| & ||.x.|| <= 1);
reconsider f=Yseq.n as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
now let r be Real;
assume r in PreNorms f; then
ex x be Point of X st
r = |.f.x.| & ||.x.|| <= 1;
hence r <= ||.Yseq.n.|| /2 by A31;
end; then
upper_bound PreNorms f <= ||.Yseq.n.|| /2 by SEQ_4:45; then
||.Yseq.n.|| <= ||.Yseq.n.|| /2 by DUALSP01:24;
hence contradiction by XREAL_1:216,A21;
end;
end;
consider Xseq be Function of NAT,the carrier of X such that
D4: for n be Element of NAT holds P[n,Xseq.n]
from FUNCT_2:sch 3(F2);
for n be Nat holds
||.Yseq.n.|| /2 <= |.(Yseq.n).(Xseq.n).| & ||.Xseq.n.|| <= 1
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 12;
hence thesis by D4;
end; then
consider Xseq be sequence of X such that
P2: for n be Nat holds
||.Yseq.n.|| /2 <= |.(Yseq.n).(Xseq.n).| & ||.Xseq.n.|| <= 1;
set X1 = rng Xseq;
set M = ClNLin(X1);
set Y1 = rng Yseq;
for f be Point of Y st
(for x be Point of X st x in X1 holds (Bound2Lipschitz(f,X)).x = 0)
holds Bound2Lipschitz(f,X) = 0.Y
proof
let f be Point of Y;
assume
AS: for x be Point of X st x in X1 holds (Bound2Lipschitz(f,X)).x = 0;
reconsider f1=f as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
A1: f1 = Bound2Lipschitz(f,X) by DUALSP01:23;
consider seq be sequence of Y such that
B0: rng seq c= Y1 & seq is convergent & lim seq = f
by P1,NORMSP_3:14;
B1: ||. seq - f .|| is convergent & lim ||. seq - f .|| = 0
by B0,NORMSP_1:24;
B2: ||. seq .|| is convergent by B0,LOPBAN_1:20;
for n be Nat holds ((1/2)(#)||. seq .||).n <= ||. seq - f .||.n
proof
let n be Nat;
seq.n in rng seq by FUNCT_2:4,ORDINAL1:def 12; then
consider m be object such that
E1: m in NAT & Yseq.m = seq.n by FUNCT_2:11,B0;
reconsider m as Nat by E1;
reconsider x1=Xseq.m as Point of X;
C1: f1.x1 = 0 by A1,AS,E1,FUNCT_2:4;
C2: |. (seq.n).x1 - f.x1 .| = |.(seq.n - f).x1 .| by DUALSP01:33;
reconsider g=seq.n - f as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
C3: |. g.x1 .| <= ||. seq.n - f .|| * ||. x1 .|| by DUALSP01:26;
||. seq.n - f .|| * ||. x1 .|| <= ||. seq.n - f .|| * 1
by P2,XREAL_1:64; then
C4: |. (seq.n).x1 - f.x1 .| <= ||. seq.n - f .|| by C2,C3,XXREAL_0:2;
||. seq.n .||/2 <= |. (seq.n).x1 .| by P2,E1; then
C71: (1/2)*||. seq.n .|| <= ||. seq.n - f .|| by C4,XXREAL_0:2,C1;
C8: ||. seq.n - f .|| = ||. (seq - f).n .|| by NORMSP_1:def 4
.= ||. seq - f .||.n by NORMSP_0:def 4;
(1/2)*(||. seq .||.n) = ((1/2)(#)||. seq .||).n by SEQ_1:9;
hence thesis by C71,NORMSP_0:def 4,C8;
end; then
B5: lim ((1/2)(#)||. seq .||) <= 0 by B1,B2,SEQ_2:18;
reconsider rseq=||. seq .|| as Real_Sequence;
B6: now let n be Nat;
0 <= (1/2)*||. seq.n .||; then
0 <= (1/2)*(rseq.n) by NORMSP_0:def 4;
hence 0 <= ((1/2)(#)rseq).n by SEQ_1:9;
end;
(1/2)*(lim rseq) = lim ((1/2)(#)rseq) by B0,LOPBAN_1:20,SEQ_2:8; then
lim ||. seq .|| = 0 by B5,B6,B2,SEQ_2:17; then
||. f .|| = 0 by B0,LOPBAN_1:20; then
f1 = 0.Y by DUALSP01:31;
hence thesis by DUALSP01:23;
end; then
M = X by Lm73;
hence X is separable;
end;
theorem RNS3:
for x be Real, x1 be Point of RNS_Real st x=x1 holds -x = -x1
proof
let x be Real, x1 be Point of RNS_Real;
assume AS: x=x1;
reconsider mx = -x as Point of RNS_Real by XREAL_0:def 1;
x1 + mx = x + -x by AS,BINOP_2:def 9; then
x1 + mx = 0.RNS_Real;
hence thesis by RLVECT_1:def 10;
end;
theorem RNS4:
for x,y be Real, x1,y1 be Point of RNS_Real
st x=x1 & y=y1 holds x-y = x1-y1
proof
let x,y be Real, x1,y1 be Point of RNS_Real;
assume AS: x=x1 & y=y1; then
P1: -y = -y1 by RNS3;
x-y = x + -y;
hence x-y = x1-y1 by AS,BINOP_2:def 9,P1;
end;
theorem RNS8:
for seq be Real_Sequence, seq1 be sequence of RNS_Real
st seq = seq1 holds seq is convergent iff seq1 is convergent
proof
let seq be Real_Sequence, seq1 be sequence of RNS_Real;
assume AS: seq = seq1;
hereby assume P1: seq is convergent;
reconsider s1=lim seq as Point of RNS_Real by XREAL_0:def 1;
now let p be Real;
assume 0 < p; then
consider n be Nat such that
P2: for m be Nat st n <= m holds |.seq.m - lim seq .| < p
by P1,SEQ_2:def 7;
take n;
hereby let m be Nat;
assume n <= m; then
P3: |.seq.m - lim seq .| < p by P2;
seq.m - lim seq = seq1.m - s1 by AS,RNS4;
hence ||.seq1.m - s1.|| < p by P3,EUCLID:def 2;
end;
end;
hence seq1 is convergent;
end;
assume P4: seq1 is convergent;
reconsider s1=lim seq1 as Real;
now let p be Real;
assume 0 < p; then
consider n be Nat such that
P2: for m be Nat st n <= m holds ||.seq1.m - lim seq1 .|| < p
by P4,NORMSP_1:def 7;
take n;
hereby let m be Nat;
assume n <= m; then
P3: ||.seq1.m - lim seq1 .|| < p by P2;
seq1.m - lim seq1 = seq.m - s1 by AS,RNS4;
hence |.seq.m - s1.| < p by P3,EUCLID:def 2;
end;
end;
hence seq is convergent;
end;
theorem RNS9:
for seq be Real_Sequence, seq1 be sequence of RNS_Real
st seq = seq1 & seq is convergent holds lim seq = lim seq1
proof
let seq be Real_Sequence, seq1 be sequence of RNS_Real;
assume AS: seq = seq1;
assume P1: seq is convergent; then
P5: seq1 is convergent by AS,RNS8;
reconsider s1=lim seq as Point of RNS_Real by XREAL_0:def 1;
now let p be Real;
assume 0 < p; then
consider n be Nat such that
P2: for m be Nat st n <= m holds |.seq.m - lim seq .| < p
by P1,SEQ_2:def 7;
take n;
hereby let m be Nat;
assume n <= m; then
P3: |.seq.m - lim seq .| < p by P2;
seq.m - lim seq = seq1.m - s1 by AS,RNS4;
hence ||.seq1.m - s1.|| < p by P3,EUCLID:def 2;
end;
end;
hence lim seq1 = lim seq by P5,NORMSP_1:def 7;
end;
theorem RNS11:
for seq1 be sequence of RNS_Real
st seq1 is Cauchy_sequence_by_Norm holds seq1 is convergent
proof
let seq1 be sequence of RNS_Real;
assume AS: seq1 is Cauchy_sequence_by_Norm;
reconsider seq=seq1 as Real_Sequence;
for s be Real st 0 < s ex n be Nat st
for m be Nat st n <= m holds |.seq.m - seq.n.| < s
proof
let s be Real;
assume 0 < s; then
consider k be Nat such that
P1: for n, m be Nat st n >= k & m >= k holds ||. seq1.n - seq1.m .|| < s
by AS,RSSPACE3:8;
take k;
hereby let m be Nat;
assume k <= m; then
P2: ||.(seq1.m) - (seq1.k).|| < s by P1;
(seq1.m) - (seq1.k) = (seq.m) - (seq.k) by RNS4;
hence |.seq.m - seq.k.| < s by EUCLID:def 2,P2;
end;
end; then
seq is convergent by SEQ_4:41;
hence thesis by RNS8;
end;
registration
cluster RNS_Real -> complete;
correctness by LOPBAN_1:def 15,RNS11;
end;
definition
let X be RealNormSpace,
g be sequence of DualSp X,
x be Point of X;
func g#x -> Real_Sequence means :Def1:
for i be Nat holds it.i = (g.i).x;
existence
proof
deffunc F(Element of NAT) = (g.$1).x;
consider f be Real_Sequence such that
A1: for i be Element of NAT holds f.i = F(i) from FUNCT_2:sch 4;
take f;
hereby let i be Nat;
i in NAT by ORDINAL1:def 12;
hence f.i = (g.i).x by A1;
end;
end;
uniqueness
proof
let p1,p2 be Real_Sequence;
assume
B1: (for i be Nat holds p1.i = (g.i).x)
& (for i be Nat holds p2.i = (g.i).x);
B2: dom p1 = NAT & dom p2 = NAT by FUNCT_2:def 1;
now let i be object;
assume i in dom p1; then
reconsider i1=i as Nat;
p1.i = (g.i1).x by B1;
hence p1.i = p2.i by B1;
end;
hence p1 = p2 by B2;
end;
end;
begin :: Weak Convergence and Weak* Convergence
definition
let X be RealNormSpace, x be sequence of X;
attr x is weakly-convergent means
ex x0 be Point of X st
for f be Lipschitzian linear-Functional of X
holds f*x is convergent & lim (f*x) = f.x0;
end;
theorem WEAKLM1:
for X be RealNormSpace, x be sequence of X
st rng x c= {0.X} holds x is weakly-convergent
proof
let X be RealNormSpace, x be sequence of X;
assume AS: rng x c= {0.X};
reconsider x0=0.X as Point of X;
for f be Lipschitzian linear-Functional of X
holds f*x is convergent & lim (f*x) = f.x0
proof
let f be Lipschitzian linear-Functional of X;
A2: for p be Real, n be Nat st 0 < p holds |.(f*x).n - f.x0.| < p
proof
let p be Real, n be Nat;
assume AS1: 0 < p;
C21: x.n in rng x by FUNCT_2:4,ORDINAL1:def 12;
(f*x).n = f.(x.n) by ORDINAL1:def 12,FUNCT_2:15; then
(f*x).n = f.(0.X) by TARSKI:def 1,AS,C21;
hence |.(f*x).n - f.x0.| < p by AS1,COMPLEX1:44;
end;
A1: for p be Real st 0 < p ex m be Nat st
for n be Nat st m <= n holds |.(f*x).n - f.x0.| < p
proof
let p be Real;
assume AS1: 0 < p;
take m = 0;
thus thesis by AS1,A2;
end; then
f*x is convergent;
hence thesis by A1,SEQ_2:def 7;
end;
hence x is weakly-convergent;
end;
definition
let X be RealNormSpace, x be sequence of X;
assume A1: x is weakly-convergent;
func w-lim x -> Point of X means :DefWeaklim:
for f be Lipschitzian linear-Functional of X
holds f*x is convergent & lim (f*x) = f.it;
existence by A1;
uniqueness
proof
given g1,g2 be Point of X such that
A2: for f be Lipschitzian linear-Functional of X
holds f*x is convergent & lim (f*x) = f.g1 and
A3: for f be Lipschitzian linear-Functional of X
holds f*x is convergent & lim (f*x) = f.g2 and
A4: g1 <> g2;
now let f be Lipschitzian linear-Functional of X;
f.(g1-g2) = f.g1-f.g2 by HAHNBAN:19
.= lim (f*x) - f.g2 by A2
.= lim (f*x) - lim (f*x) by A3;
hence f.(g1-g2) = 0;
end;
then g1-g2 = 0.X by DUALSP02:8;
hence contradiction by A4,RLVECT_1:21;
end;
end;
theorem
for X be RealNormSpace, x be sequence of X
st x is convergent holds x is weakly-convergent & w-lim x = lim x
proof
let X be RealNormSpace, x be sequence of X such that
A2: x is convergent;
reconsider x0=lim x as Point of X;
A3: for f be Lipschitzian linear-Functional of X
holds f*x is convergent & lim (f*x) = f.x0
proof
let f be Lipschitzian linear-Functional of X;
B1: dom f = the carrier of X by FUNCT_2:def 1;
consider K be Real such that
B3: 0 <= K & for x be VECTOR of X
holds |. f.x .| <= K * ||. x .|| by DUALSP01:def 9;
for x1, x2 be Point of X
st x1 in the carrier of X & x2 in the carrier of X
holds |.f/.x1-f/.x2.| <= (K+1)*||.x1-x2.||
proof
let x1,x2 be Point of X;
assume x1 in the carrier of X & x2 in the carrier of X;
C2: |.f/.x1-f/.x2.| = |.f.(x1-x2).| by HAHNBAN:19;
C3: |.f.(x1-x2).| <= K * ||. x1-x2 .|| by B3;
0 + K <= K + 1 by XREAL_1:8; then
K * ||. x1-x2 .|| <= (K+1) * ||. x1-x2 .|| by XREAL_1:64;
hence thesis by XXREAL_0:2,C2,C3;
end; then
f is_Lipschitzian_on (the carrier of X) by FUNCT_2:def 1,B3; then
f is_continuous_on (the carrier of X) by NFCONT_1:46; then
B81:f is_continuous_in x0;
B6: rng x c= the carrier of X; then
f/*x = f*x by B1,FUNCT_2:def 11;
hence f*x is convergent & lim (f*x) = f.x0 by B81,A2,B1,B6;
end; then
A4: x is weakly-convergent;
now let f be Lipschitzian linear-Functional of X;
f.(w-lim x - x0) = f.(w-lim x) - f.x0 by HAHNBAN:19
.= lim (f*x) - f.x0 by A4,DefWeaklim
.= lim (f*x) - lim (f*x) by A3;
hence f.(w-lim x - x0) = 0;
end; then
w-lim x - lim x = 0.X by DUALSP02:8;
hence thesis by A3,RLVECT_1:21;
end;
theorem Th79:
for X be RealNormSpace, x be sequence of X
st X is non trivial & x is weakly-convergent
holds ||.x.|| is bounded & ||. w-lim x .|| <= lim_inf ||.x.||
& w-lim x in ClNLin(rng x)
proof
let X be RealNormSpace, x be sequence of X;
assume AS: X is non trivial & x is weakly-convergent;
reconsider x0=w-lim x as Point of X;
for f be Point of DualSp X holds
ex Kf be Real st 0 <= Kf
& for y be Point of X st y in rng x holds |. f.y .| <= Kf
proof
let f be Point of DualSp X;
reconsider h=f as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
h*x is convergent by AS; then
consider Kf be Real such that
A1: 0 < Kf
& for n be Nat holds |. (h*x).n .| < Kf by SEQ_2:3;
for y be Point of X st y in rng x holds |. f.y .| <= Kf
proof
let y be Point of X;
assume y in rng x; then
consider m be Nat such that
A2: y = x.m by NFCONT_1:6;
|. (h*x).m .| = |. f.(x.m) .| by FUNCT_2:15,ORDINAL1:def 12;
hence thesis by A2,A1;
end;
hence thesis by A1;
end; then
consider K be Real such that
A4: 0 <= K
& for y be Point of X st
y in rng x holds ||. y .|| <= K by AS,DUALSP02:19;
A5: for n be Nat holds ||.x.||.n <= K
proof
let n be Nat;
n in NAT by ORDINAL1:def 12; then
||. x.n .|| <= K by A4,FUNCT_2:4;
hence thesis by NORMSP_0:def 4;
end;
A6: K + 0 < K + 1 by XREAL_1:8;
X10: for n be Nat holds |. ||.x.||.n .| < (K+1)
proof
let n be Nat;
||.x.||.n <= K by A5; then
A7: ||.x.||.n < (K+1) by A6,XXREAL_0:2;
0 <= ||. x.n .||; then
0 <= ||.x.||.n by NORMSP_0:def 4;
hence thesis by A7,ABSVALUE:def 1;
end; then
X1: ||.x.|| is bounded by A4,SEQ_2:3;
B0: for f be Point of DualSp X holds
|. f.x0 .| <= (lim_inf ||.x.||) * ||.f.||
proof
let f be Point of DualSp X;
reconsider h=f as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
B1: h*x is convergent & lim (h*x) = h.x0 by DefWeaklim,AS;
B6: for n be Nat holds |. (h*x) .|.n <= (||.f.||(#)||.x.||).n
proof
let n be Nat;
D21: |. h.(x.n) .| <= ||.f.|| * ||. x.n .|| by DUALSP01:26;
|. h.(x.n) .| = |. (h*x).n .| by FUNCT_2:15,ORDINAL1:def 12; then
|. (h*x).n .| <= ||.f.|| * (||.x.||.n) by D21,NORMSP_0:def 4; then
|.h*x.|.n <= ||.f.|| * (||.x.||.n) by SEQ_1:12;
hence thesis by SEQ_1:9;
end;
||.f.||(#)||.x.|| is bounded by A4,SEQ_2:3,X10,SEQM_3:37; then
lim_inf |. (h*x) .| <= lim_inf (||.f.||(#)||.x.||)
by B1,B6,RINFSUP1:91; then
B7: lim |. (h*x) .| <= lim_inf (||.f.||(#)||.x.||) by B1,RINFSUP1:89;
lim_inf (||.f.||(#)||.x.||) = (lim_inf ||.x.||) * ||.f.||
by X1,LOPBAN_5:1;
hence thesis by SEQ_4:14,B1,B7;
end;
now let s be Real;
assume D5: 0 < s;
for k be Nat holds 0 - s < ||.x.||.(0+k)
proof
let k be Nat;
||. x.k .|| = ||.x.||.k by NORMSP_0:def 4;
hence thesis by D5;
end;
hence ex n be Nat st for k be Nat holds 0 - s < ||.x.||.(n+k);
end; then
B8: 0 <= lim_inf ||.x.|| by X1,RINFSUP1:82;
consider Y be non empty Subset of REAL such that
B9: Y = {|.(Bound2Lipschitz(F,X)).x0.|
where F is Point of DualSp X :||.F.|| <= 1 }
& ||. x0 .|| = upper_bound Y by AS,DUALSP02:7;
X21: now let r be Real;
assume r in Y; then
consider F be Point of DualSp X such that
D7: r = |.(Bound2Lipschitz(F,X)).x0.| & ||.F.|| <= 1 by B9;
reconsider f1=F as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
D8: f1 = Bound2Lipschitz(F,X) by DUALSP01:23;
D9: |. F.x0 .| <= (lim_inf ||.x.||) * ||.F.|| by B0;
(lim_inf ||.x.||) * ||.F.|| <= (lim_inf ||.x.||) * 1
by B8,D7,XREAL_1:64;
hence r <= lim_inf ||.x.|| by D7,D8,D9,XXREAL_0:2;
end;
x0 in ClNLin(rng x)
proof
set M = ClNLin(rng x);
consider Z be Subset of X such that
C1: Z = the carrier of Lin(rng x)
& M = NORMSTR(# Cl(Z), Zero_(Cl(Z),X), Add_(Cl(Z),X), Mult_(Cl(Z),X),
Norm_(Cl(Z), X) #) by NORMSP_3:def 20;
reconsider Y = the carrier of M as Subset of X by DUALSP01:def 16;
C3: Y is linearly-closed by NORMSP_3:29;
x0 in Y
proof
assume AS0: not x0 in Y;
consider G be Point of DualSp X such that
C5: (for y be Point of X
st y in Y holds (Bound2Lipschitz(G,X)).y = 0) and
C6: (Bound2Lipschitz(G,X)).x0 = 1 by C1,C3,AS0,DUALSP02:2;
reconsider g=G as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
C7: g = Bound2Lipschitz(G,X) by DUALSP01:23;
C8: g*x is convergent by AS;
C101: for n be Nat holds (g*x).n <= (seq_const 0).n
proof
let n be Nat;
n in NAT by ORDINAL1:def 12; then
x.n in Lin(rng x) by RLVECT_3:15,FUNCT_2:4;then
x.n in Y by C1,NORMSP_3:4,TARSKI:def 3; then
g.(x.n) = 0 by C5,C7; then
(g*x).n = 0 by FUNCT_2:15,ORDINAL1:def 12;
hence thesis;
end;
C111: lim (seq_const 0) = (seq_const 0).0 by SEQ_4:26
.= 0;
lim (g*x) = g.x0 by DefWeaklim,AS
.= 1 by C6,DUALSP01:23;
hence contradiction by C111,C101,C8,SEQ_2:18;
end;
hence x0 in M;
end;
hence thesis by A4,SEQ_2:3,X10,B9,SEQ_4:45,X21;
end;
definition
let X be RealNormSpace,
g be sequence of DualSp X;
attr g is weakly*-convergent means
ex g0 be Point of DualSp X st
for x be Point of X holds g#x is convergent & lim (g#x) = g0.x;
end;
definition
let X be RealNormSpace,
g be sequence of DualSp X;
assume A1: g is weakly*-convergent;
func w*-lim g -> Point of DualSp X means :Def2:
for x be Point of X
holds g#x is convergent & lim (g#x) = it.x;
existence by A1;
uniqueness
proof
let f1,f2 be Point of DualSp X;
assume
B1: (for x be Point of X holds g#x is convergent & lim (g#x) = f1.x)
& (for x be Point of X holds g#x is convergent & lim (g#x) = f2.x);
B2: f1 is Lipschitzian linear-Functional of X
& f2 is Lipschitzian linear-Functional of X by DUALSP01:def 10;
for x be Point of X holds f1.x = f2.x
proof
let x be Point of X;
thus f1.x = lim (g#x) by B1
.= f2.x by B1;
end;
hence f1 = f2 by B2,FUNCT_2:def 8;
end;
end;
theorem
for X be RealNormSpace, g be sequence of DualSp X
st g is convergent holds g is weakly*-convergent & w*-lim g = lim g
proof
let X be RealNormSpace, g be sequence of DualSp X such that
A2: g is convergent;
reconsider g0=lim g as Point of DualSp X;
A3: for x be Point of X
holds g#x is convergent & lim (g#x) = g0.x
proof
let x be Point of X;
B2: for r be Real st 0 < r
ex m be Nat st
for n be Nat st m <= n holds |.(g#x).n - g0.x.| < r
proof
let r be Real;
set p = r/ (||.x.|| + 1);
assume C00: 0 < r; then
consider m be Nat such that
C1: for n be Nat st m <= n holds ||.g.n - g0.|| < p
by A2,NORMSP_1:def 7;
p*(||.x.|| + 1) = r by XCMPLX_1:87; then
C0: 0 < p & p*||.x.|| < r by C00,XREAL_1:29,68;
CX: for n be Nat st m <= n holds |.(g#x).n - g0.x.| < r
proof
let n be Nat;
assume m <= n; then
||.g.n - g0.|| < p by C1; then
D4: ||.g.n - g0.|| * ||.x.|| <= p * ||.x.|| by XREAL_1:64;
D2: |.(g#x).n - g0.x.| = |.(g.n).x - g0.x.| by Def1
.= |.(g.n - g0).x.| by DUALSP01:33;
reconsider h=g.n - g0 as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
|.h.x.| <= ||.g.n - g0.|| * ||.x.|| by DUALSP01:26; then
|.h.x.| <= p * ||.x.|| by D4,XXREAL_0:2;
hence thesis by D2,C0,XXREAL_0:2;
end;
take m;
thus thesis by CX;
end; then
g#x is convergent;
hence thesis by B2,SEQ_2:def 7;
end; then
g is weakly*-convergent;
hence thesis by A3,Def2;
end;
theorem Lm710A:
for X be RealNormSpace, f be sequence of DualSp X
st f is weakly-convergent holds f is weakly*-convergent
proof
let X be RealNormSpace, f be sequence of DualSp X;
assume AS: f is weakly-convergent;
reconsider f0=w-lim f as Point of DualSp X;
for x be Point of X holds f#x is convergent & lim (f#x) = f0.x
proof
let x be Point of X;
reconsider G=BiDual x as
Lipschitzian linear-Functional of DualSp X by DUALSP01:def 10;
C3: G*f is convergent & lim (G*f) = G.f0 by DefWeaklim,AS;
B4: for r be Real st 0 < r
ex m be Nat st
for n be Nat st m <= n holds |.(f#x).n - f0.x.| < r
proof
let r be Real;
assume 0 < r; then
consider m be Nat such that
C1: for n be Nat st m <= n holds |.(G*f).n - G.f0.| < r by C3,SEQ_2:def 7;
take m;
thus for n be Nat st m <= n holds |.(f#x).n - f0.x.| < r
proof
let n be Nat;
assume D3: m <= n;
B1: G.f0 = f0.x by DUALSP02:def 1;
(G*f).n = G.(f.n) by FUNCT_2:15,ORDINAL1:def 12
.= (f.n).x by DUALSP02:def 1; then
(G*f).n = (f#x).n by Def1;
hence thesis by B1,C1,D3;
end;
end; then
f#x is convergent;
hence thesis by B4,SEQ_2:def 7;
end;
hence f is weakly*-convergent;
end;
theorem
for X be RealNormSpace, f be sequence of DualSp X
st X is Reflexive holds
f is weakly-convergent iff f is weakly*-convergent
proof
let X be RealNormSpace, f be sequence of DualSp X;
assume AS: X is Reflexive;
thus f is weakly-convergent implies f is weakly*-convergent by Lm710A;
thus f is weakly*-convergent implies f is weakly-convergent
proof
assume AS1: f is weakly*-convergent;
reconsider f0=w*-lim f as Point of DualSp X;
for F be Lipschitzian linear-Functional of DualSp X
holds F*f is convergent & lim (F*f) = F.f0
proof
let F be Lipschitzian linear-Functional of DualSp X;
reconsider G=F as Point of DualSp DualSp X by DUALSP01:def 10;
consider x be Point of X such that
B1: for f be Point of DualSp X holds G.f = f.x by AS,DUALSP02:21;
C4: f#x is convergent & lim (f#x) = f0.x by AS1,Def2;
B5: for r be Real st 0 < r
ex m be Nat st
for n be Nat st m <= n holds |.(F*f).n - F.f0.| < r
proof
let r be Real;
assume 0 < r; then
consider m be Nat such that
C1: for n be Nat st m <= n holds |.(f#x).n - f0.x.| < r
by C4,SEQ_2:def 7;
take m;
hereby let n be Nat;
assume D3:m <= n;
(F*f).n = G.(f.n) by FUNCT_2:15,ORDINAL1:def 12; then
(F*f).n = (f.n).x by B1; then
(F*f).n = (f#x).n by Def1; then
|.(F*f).n - F.f0.| = |.(f#x).n - f0.x.| by B1;
hence |.(F*f).n - F.f0.| < r by C1,D3;
end;
end; then
F*f is convergent;
hence thesis by B5,SEQ_2:def 7;
end;
hence f is weakly-convergent;
end;
end;
theorem Lm55:
for X be RealBanachSpace, T be Subset of DualSp X
st ( for x be Point of X
ex K be Real st
0 <= K
& for f be Point of DualSp X st f in T holds |. f.x .| <= K ) holds
ex L be Real st
0 <= L
& for f be Point of DualSp X st f in T holds ||.f.|| <= L
proof
let X be RealBanachSpace, T be Subset of DualSp X;
assume
AS: for x be Point of X
ex K be Real st 0 <= K
& for f be Point of DualSp X st f in T holds |. f.x .| <= K;
reconsider T1=T as Subset of
R_NormSpace_of_BoundedLinearOperators(X,RNS_Real) by DUALSP02:14;
for x be Point of X
ex K be Real st
0 <= K
& for f be Point of R_NormSpace_of_BoundedLinearOperators(X,RNS_Real)
st f in T1 holds ||. f.x .|| <= K
proof
let x be Point of X;
consider K be Real such that
B1: 0 <= K
& for f be Point of DualSp X st f in T holds |. f.x .| <= K by AS;
take K;
for f be Point of R_NormSpace_of_BoundedLinearOperators(X,RNS_Real)
st f in T1 holds ||. f.x .|| <= K
proof
let f be Point of R_NormSpace_of_BoundedLinearOperators(X,RNS_Real);
assume C2: f in T1; then
reconsider f1=f as Point of DualSp X;
|. f1.x .| = ||. f.x .|| by EUCLID:def 2;
hence thesis by C2,B1;
end;
hence thesis by B1;
end; then
consider L be Real such that
A1: 0 <= L
& for f be Point of R_NormSpace_of_BoundedLinearOperators(X,RNS_Real)
st f in T1 holds ||.f.|| <= L by LOPBAN_5:5;
take L;
for f be Point of DualSp X st f in T holds ||.f.|| <= L
proof
let f be Point of DualSp X;
assume C5: f in T; then
f in T1; then
reconsider f1=f as Point of
R_NormSpace_of_BoundedLinearOperators(X,RNS_Real);
||.f1.|| = ||.f.|| by DUALSP02:18;
hence thesis by C5,A1;
end;
hence thesis by A1;
end;
theorem Th711:
for X be RealBanachSpace, f be sequence of DualSp X
st f is weakly*-convergent
holds ||.f.|| is bounded & ||. w*-lim f .|| <= lim_inf ||.f.||
proof
let X be RealBanachSpace, f be sequence of DualSp X;
assume AS: f is weakly*-convergent;
reconsider f0=w*-lim f as Point of DualSp X;
for x be Point of X
ex K be Real st
0 <= K
& for g be Point of DualSp X st g in rng f holds |. g.x .| <= K
proof
let x be Point of X;
f#x is convergent by AS; then
consider K be Real such that
A2: for n be Nat holds |. f#x .|.n < K by SEQ_2:def 3;
A3: for g be Point of DualSp X st g in rng f holds |. g.x .| <= K
proof
let g be Point of DualSp X;
assume g in rng f; then
consider n be object such that
A4: n in NAT & g=f.n by FUNCT_2:11;
reconsider n as Nat by A4;
(f.n).x = (f#x).n by Def1; then
|. g.x .| = |. f#x .|.n by A4,SEQ_1:12;
hence thesis by A2;
end;
B6: |. f#x .|.0 < K by A2;
0 <= |. (f#x).0 .| by COMPLEX1:46; then
0 <= K by B6,SEQ_1:12;
hence thesis by A3;
end; then
consider L be Real such that
A7: 0 <= L and
A8: for g be Point of DualSp X st g in rng f holds ||.g.|| <= L by Lm55;
Y1: for n be Nat holds |.||.f.||.n .| < (L+1)
proof
let n be Nat;
n in NAT by ORDINAL1:def 12; then
||.f.n.|| <= L by A8,FUNCT_2:4; then
||.f.n.|| < L + 1 by XREAL_1:39; then
|. ||.f.n.|| .| < L+1 by ABSVALUE:def 1;
hence thesis by NORMSP_0:def 4;
end; then
X1: ||.f.|| is bounded by A7,SEQ_2:3;
B1: for x be Point of X holds |.f0.x.| <= (lim_inf ||.f.||) * ||.x.||
proof
let x be Point of X;
B3: for n be Nat holds |.f#x.|.n <= (||.x.||(#)||.f.||).n
proof
let n be Nat;
reconsider h=f.n as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
B4: |. f#x .|.n = |. (f#x).n .| by SEQ_1:12;
||.f.n.|| = ||.f.||.n by NORMSP_0:def 4; then
||.f.n.|| * ||.x.|| = (||.x.||(#)||.f.||).n by SEQ_1:9; then
|. h.x .| <= (||.x.||(#)||.f.||).n by DUALSP01:26;
hence thesis by B4,Def1;
end;
B6: lim_inf (||.x.||(#)||.f.||) = (lim_inf ||.f.||) * ||.x.||
by X1,LOPBAN_5:1;
B7: f#x is convergent & lim(f#x) = f0.x by AS,Def2;
||.x.||(#)||.f.|| is bounded by A7,SEQ_2:3,Y1,SEQM_3:37; then
B9: lim_inf |. f#x .| <= lim_inf (||.x.||(#)||.f.||) by B3,RINFSUP1:91,B7;
lim |. f#x .| = |. f0.x .| by B7,SEQ_4:14;
hence thesis by B6,B7,RINFSUP1:89,B9;
end;
now
let s be Real;
assume B9: 0 < s;
for k be Nat holds 0-s < ||.f.||.(0+k)
proof
let k be Nat;
||.f.k.||=||.f.||.k by NORMSP_0:def 4;
hence thesis by B9;
end;
hence ex n be Nat st for k be Nat holds 0-s < ||.f.||.(n+k);
end;
then
B10: 0 <= lim_inf ||.f.|| by X1,RINFSUP1:82;
reconsider g=f0 as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
now let k be Real;
assume k in PreNorms g; then
consider x be Point of X such that
B11: k = |.g.x.| & ||.x.|| <= 1;
B12: |.f0.x.| <= (lim_inf ||.f.||) * ||.x.|| by B1;
(lim_inf ||.f.||) * ||.x.|| <= lim_inf ||.f.|| * 1
by B10,B11,XREAL_1:64;
hence k <= lim_inf ||.f.|| by B11,B12,XXREAL_0:2;
end; then
upper_bound PreNorms g <= lim_inf ||.f.|| by SEQ_4:45;
hence thesis by A7,SEQ_2:3,Y1,DUALSP01:24;
end;
theorem RNSBH1:
for X be RealNormSpace, x be Point of X,
vseq be sequence of DualSp X,
vseq1 be sequence of R_NormSpace_of_BoundedLinearOperators(X,RNS_Real)
st vseq = vseq1 holds vseq#x = vseq1#x
proof
let X be RealNormSpace, x be Point of X,
vseq be sequence of DualSp X,
vseq1 be sequence of R_NormSpace_of_BoundedLinearOperators(X,RNS_Real);
assume AS: vseq = vseq1;
for n be Element of NAT holds (vseq#x).n = (vseq1#x).n
proof
let n be Element of NAT;
(vseq#x).n = (vseq.n).x by Def1;
hence (vseq#x).n = (vseq1#x).n by AS,LOPBAN_5:def 2;
end;
hence thesis;
end;
theorem Th712A:
for X be RealBanachSpace, X0 be Subset of X, vseq be sequence of DualSp X
st ||.vseq.|| is bounded & X0 is dense
& (for x be Point of X st x in X0 holds vseq#x is convergent)
holds vseq is weakly*-convergent
proof
let X be RealBanachSpace, X0 be Subset of X, vseq be sequence of DualSp X;
assume that
A1: ||.vseq.|| is bounded and
A2: X0 is dense and
A3: for x be Point of X st x in X0 holds vseq#x is convergent;
reconsider vseq1=vseq as
sequence of R_NormSpace_of_BoundedLinearOperators(X,RNS_Real)
by DUALSP02:14;
reconsider X01=X0 as Subset of LinearTopSpaceNorm(X) by NORMSP_2:def 4;
B1: for x be Point of X st x in X01 holds vseq1#x is convergent
proof
let x be Point of X;
assume x in X01; then
B11: vseq#x is convergent by A3;
vseq1#x = vseq#x by RNSBH1;
hence vseq1#x is convergent by RNS8,B11;
end;
B2: for x be Point of X
ex K be Real st 0 <= K
& for n be Nat holds ||.(vseq1#x).n.|| <= K
proof
let x be Point of X;
consider K0 be Real such that
B20: 0 < K0
& for n be Nat holds |. ||.vseq.||.n .| < K0 by A1,SEQ_2:3;
reconsider K=K0*||.x.|| + 1 as Real;
take K;
C0: K0*||.x.|| + 0 < K0*||.x.|| + 1 by XREAL_1:8;
thus 0 <= K by B20;
thus for n be Nat holds ||.(vseq1#x).n.|| <= K
proof
let n be Nat;
|. ||.vseq.||.n .| < K0 by B20; then
|. ||.vseq.n.|| .| < K0 by NORMSP_0:def 4; then
A5: ||.vseq.n.|| < K0 by ABSVALUE:def 1;
reconsider h=vseq.n as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
B1: |.h.x.| <= ||.vseq.n.|| * ||.x.|| by DUALSP01:26;
C3: ||.vseq.n.|| * ||.x.|| <= K0 * ||.x.|| by A5,XREAL_1:64;
|.(vseq#x).n .| = |.(vseq.n).x.| by Def1; then
|.(vseq#x).n .| <= K0 * ||.x.|| by C3,B1,XXREAL_0:2; then
B4: |.(vseq#x).n .| <= K by C0,XXREAL_0:2;
vseq#x = vseq1#x by RNSBH1;
hence ||.(vseq1#x).n .|| <= K by B4,EUCLID:def 2;
end;
end;
X01 is dense by A2,NORMSP_3:15; then
consider tseq be Point of
R_NormSpace_of_BoundedLinearOperators(X,RNS_Real) such that
B4: ( for x be Point of X holds vseq1#x is convergent
& tseq.x=lim (vseq1#x)
& ||.tseq.x.|| <= lim_inf ||.vseq1.|| * ||.x.|| )
& ||.tseq.|| <= lim_inf ||.vseq1.|| by B1,B2,LOPBAN_5:8;
reconsider g0=tseq as Point of DualSp X by DUALSP02:14;
for x be Point of X holds vseq#x is convergent & lim (vseq#x) = g0.x
proof
let x be Point of X;
B7: vseq1#x = vseq#x by RNSBH1;
vseq1#x is convergent & tseq.x=lim (vseq1#x) by B4;
hence vseq#x is convergent by B7,RNS8;
then lim (vseq#x) = lim (vseq1#x) by RNSBH1,RNS9;
hence g0.x=lim (vseq#x) by B4;
end;
hence vseq is weakly*-convergent;
end;
theorem
for X be RealBanachSpace, f be sequence of DualSp X holds
f is weakly*-convergent
iff ( ||.f.|| is bounded
& ex X0 be Subset of X st
X0 is dense
& (for x be Point of X st x in X0 holds f#x is convergent)
)
proof
let X be RealBanachSpace,
f be sequence of DualSp X;
now assume AS: f is weakly*-convergent;
hence ||.f.|| is bounded by Th711;
set X0 = [#]X;
take X0;
thus X0 is dense;
thus for x be Point of X st x in X0 holds f#x is convergent by AS;
end;
hence thesis by Th712A;
end;
begin :: Weak Sequential Compactness of Real Banach Spaces
definition
let X be RealNormSpace, X0 be non empty Subset of X;
attr X0 is weakly-sequentially-compact means
for seq be sequence of X0
ex seq1 be sequence of X st
seq1 is subsequence of seq & seq1 is weakly-convergent
& w-lim seq1 in X;
end;
Th713A:
for X be RealBanachSpace, X0 be non empty Subset of X
st X is non trivial & X is Reflexive
& X0 is weakly-sequentially-compact
holds
ex S be non empty Subset of REAL st
S = {||.x.|| where x is Point of X : x in X0}
& S is bounded_above
proof
let X be RealBanachSpace, X0 be non empty Subset of X;
assume AS1: X is non trivial & X is Reflexive;
assume AS2: X0 is weakly-sequentially-compact;
assume
B1: not ( ex S be non empty Subset of REAL st
S = {||.x.|| where x is Point of X : x in X0}
& S is bounded_above );
set S = {||.x.|| where x is Point of X : x in X0};
now let r be object;
assume r in S; then
ex x be Point of X st r = ||.x.|| & x in X0;
hence r in REAL;
end; then
A11: S c= REAL;
consider x0 be object such that
A12: x0 in X0 by XBOOLE_0:def 1;
reconsider x0 as Point of X by A12;
||.x0.|| in S by A12; then
reconsider S as non empty Subset of REAL by A11;
defpred P[Nat,Point of X] means $1 <= ||.$2.|| & $2 in X0;
P1: for n be Element of NAT ex x be Point of X st P[n,x]
proof
assume not (for n be Element of NAT ex x be Point of X st P[n,x]); then
consider n be Element of NAT such that
Q1: for x be Point of X holds not P[n,x];
for r being ExtReal st r in S holds r <= n
proof
let r be ExtReal;
assume r in S; then
ex x be Point of X st r = ||.x.|| & x in X0;
hence r <= n by Q1;
end; then
n is UpperBound of S by XXREAL_2:def 1; then
S is bounded_above;
hence contradiction by B1;
end;
consider seq0 be Function of NAT,the carrier of X such that
P2: for n be Element of NAT holds P[n,seq0.n] from FUNCT_2:sch 3(P1);
P3: for n be Nat holds n <= ||.seq0.n.|| & seq0.n in X0
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 12;
hence thesis by P2;
end;
for n be Element of NAT holds seq0.n in X0 by P3;
then rng seq0 c= X0 by FUNCT_2:114; then
reconsider seq = seq0 as sequence of X0 by FUNCT_2:6;
consider seq1 be sequence of X such that
A3: seq1 is subsequence of seq & seq1 is weakly-convergent
& w-lim seq1 in X by AS2;
||.seq1.|| is bounded by A3,AS1,Th79; then
consider r be Real such that
A4: for n be Nat holds ||.seq1.||.n < r by SEQ_2:def 3;
set n = [/r\] + 1;
||. seq1 .||.0 < r by A4; then
||. seq1.0 .|| < r by NORMSP_0:def 4; then
0 <= n; then
n in NAT by INT_1:3; then
reconsider n as Nat;
consider N being increasing sequence of NAT such that
A52: seq1 = seq * N by A3,VALUED_0:def 17;
set m=N.n;
seq0.m = seq1.n by A52,FUNCT_2:15,ORDINAL1:def 12; then
A54: N.n <= ||. seq1.n .|| by P3;
n <= N.n by SEQM_3:14; then
B55: n <= ||. seq1.n .|| by A54,XXREAL_0:2;
||. seq1 .|| .n < r by A4; then
||. seq1.n .|| < r by NORMSP_0:def 4;
hence contradiction by B55,XXREAL_0:2,INT_1:32;
end;
theorem Lm813A:
for X be RealNormSpace, x be sequence of X st X is Reflexive holds
x is weakly-convergent iff (BidualFunc X)*x is weakly*-convergent
proof
let X be RealNormSpace, x be sequence of X;
assume AS: X is Reflexive;
set f=(BidualFunc X)*x;
hereby assume AS: x is weakly-convergent;
reconsider x0=w-lim x as Point of X;
for g be Point of DualSp X
holds f#g is convergent & lim (f#g) = (BiDual x0).g
proof
let g be Point of DualSp X;
reconsider f0=BiDual x0 as Point of DualSp DualSp X;
A3: for n be Nat holds (f#g).n = (g*x).n
proof
let n be Nat;
reconsider f1=BiDual(x.n) as Point of DualSp DualSp X;
f.n = (BidualFunc X).(x.n) by FUNCT_2:15,ORDINAL1:def 12; then
B2: f.n = BiDual(x.n) by DUALSP02:def 2;
(f#g).n = (f.n).g by Def1; then
(f#g).n = g.(x.n) by B2,DUALSP02:def 1;
hence (f#g).n = (g*x).n by FUNCT_2:15,ORDINAL1:def 12;
end;
reconsider g1=g as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
A41: g1*x is convergent & lim (g1*x) = g1.x0 by DefWeaklim,AS;
A5: for r be Real st 0 < r
ex m be Nat st
for n be Nat st m <= n holds |.(f#g).n - f0.g.| < r
proof
let r be Real;
assume 0 < r; then
consider m be Nat such that
B1: for n be Nat st m <= n holds |.(g1*x).n - g1.x0.| < r
by A41,SEQ_2:def 7;
take m;
thus for n be Nat st m <= n holds |.(f#g).n - f0.g.| < r
proof
let n be Nat;
assume C3: m <= n;
f0.g = g.x0 by DUALSP02:def 1; then
|.(f#g).n - f0.g.| = |.(g1*x).n - g1.x0.| by A3;
hence thesis by B1,C3;
end;
end; then
f#g is convergent;
hence thesis by A5,SEQ_2:def 7;
end;
hence f is weakly*-convergent;
end;
assume f is weakly*-convergent; then
consider f0 be Point of DualSp DualSp X such that
A0: for h be Point of DualSp X
holds f#h is convergent & lim (f#h) = f0.h;
consider x0 be Point of X such that
A1: for g be Point of DualSp X holds f0.g = g.x0 by AS,DUALSP02:21;
for g be Lipschitzian linear-Functional of X
holds g*x is convergent & lim (g*x) = g.x0
proof
let g be Lipschitzian linear-Functional of X;
reconsider g1=g as Point of DualSp X by DUALSP01:def 10;
A3: for n be Nat holds (g*x).n = (f#g1).n
proof
let n be Nat;
reconsider f1=BiDual(x.n) as Point of DualSp DualSp X;
B2: f.n = (BidualFunc X).(x.n) by FUNCT_2:15,ORDINAL1:def 12
.= BiDual(x.n) by DUALSP02:def 2;
thus (g*x).n = g1.(x.n) by FUNCT_2:15,ORDINAL1:def 12
.= f1.g1 by DUALSP02:def 1
.= (f#g1).n by B2,Def1;
end;
B4: f#g1 is convergent & lim (f#g1) = f0.g1 by A0;
A5: for r be Real st 0 < r
ex m be Nat st
for n be Nat st m <= n holds |.(g*x).n - g1.x0.| < r
proof
let r be Real;
assume 0 < r; then
consider m be Nat such that
B1: for n be Nat st m <= n holds |.(f#g1).n - f0.g1.| < r
by SEQ_2:def 7,B4;
take m;
hereby let n be Nat;
assume C3: m <= n;
f0.g1 = g1.x0 by A1; then
|.(g*x).n - g1.x0.| = |.(f#g1).n - f0.g1.| by A3;
hence |.(g*x).n - g1.x0.| < r by B1,C3;
end;
end; then
g*x is convergent;
hence thesis by A5,SEQ_2:def 7;
end;
hence x is weakly-convergent;
end;
theorem Lm814A:
for X be RealNormSpace, f be sequence of DualSp X, x be Point of X
st ||.f.|| is bounded holds
ex f0 be sequence of DualSp X st
f0 is subsequence of f & ||.f0.|| is bounded & f0#x is convergent
proof
let X be RealNormSpace, f be sequence of DualSp X, x be Point of X;
assume AS0:||.f.|| is bounded;
consider r0 be Real such that
B0: 0 < r0 & for m be Nat holds |. ||.f.||.m .| < r0 by AS0,SEQ_2:3;
set r = r0*||.x.|| + 1;
C1: r0*||.x.|| < r0*||.x.|| + 1 by XREAL_1:29;
BY: for m be Nat holds |.(f#x).m.| < r
proof
let m be Nat;
reconsider h=f.m as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
B5: |.h.x.| <= ||.f.m.|| * ||.x.|| by DUALSP01:26;
B3: |. ||.f.||.m .| <= r0 by B0;
||.f.||.m = ||.f.m.|| by NORMSP_0:def 4; then
||.f.m.|| <= r0 by B3,ABSVALUE:def 1; then
C6: ||.f.m.|| * ||.x.|| <= r0 * ||.x.|| by XREAL_1:64;
|.(f#x).m .| = |.(f.m).x.| by Def1; then
|.(f#x).m .| <= r0 * ||.x.|| by B5,XXREAL_0:2,C6;
hence thesis by C1,XXREAL_0:2;
end;
reconsider seq=f#x as Real_Sequence;
consider seq1 be Real_Sequence such that
X1: seq1 is subsequence of seq
& seq1 is convergent by B0,SEQ_2:3,BY,SEQ_4:40;
consider N be increasing sequence of NAT such that
X2: seq1 = seq * N by X1,VALUED_0:def 17;
set f0=f*N;
for k be Nat holds (f0#x).k = seq1.k
proof
let k be Nat;
thus (f0#x).k = (f0.k).x by Def1
.= (f.(N.k)).x by ORDINAL1:def 12,FUNCT_2:15
.= (f#x).(N.k) by Def1
.= seq1.k by X2,ORDINAL1:def 12,FUNCT_2:15;
end; then
Y5: f0#x = seq1;
for n be Nat holds |.||.f0.||.n.| < r0
proof
let n be Nat;
Y2: f0.n = f.(N.n) by ORDINAL1:def 12,FUNCT_2:15;
||.f0.||.n = ||.f0.n.|| by NORMSP_0:def 4; then
||.f0.||.n = ||.f.||.(N.n) by Y2,NORMSP_0:def 4;
hence thesis by B0;
end;
hence thesis by X1,Y5,B0,SEQ_2:3;
end;
theorem Lm814A1:
for X be RealNormSpace, f be sequence of DualSp X, x be Point of X
st ||.f.|| is bounded holds
ex f0 be sequence of DualSp X st
f0 is subsequence of f & ||.f0.|| is bounded
& f0#x is convergent & f0#x is subsequence of f#x
proof
let X be RealNormSpace, f be sequence of DualSp X, x be Point of X;
assume ||.f.|| is bounded; then
consider r0 be Real such that
B0: 0 < r0 & for m be Nat holds |. ||.f.||.m .| < r0 by SEQ_2:3;
set r=r0*||.x.|| + 1;
BS: for m be Nat holds |.(f#x).m.| < r
proof
let m be Nat;
reconsider h=f.m as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
|. h.x .| = |. (f#x).m .| by Def1; then
B5: |. (f#x).m .| <= ||.f.m.|| * ||.x.|| by DUALSP01:26;
|. ||.f.||.m .| <= r0 & ||.f.||.m = ||.f.m.|| by B0,NORMSP_0:def 4; then
||.f.m.|| <= r0 by ABSVALUE:def 1; then
||.f.m.|| * ||.x.|| <= r0 * ||.x.|| & r0*||.x.|| < r by XREAL_1:29,64; then
||.f.m.|| * ||.x.|| < r by XXREAL_0:2;
hence thesis by B5,XXREAL_0:2;
end;
reconsider seq=f#x as Real_Sequence;
consider seq1 be Real_Sequence such that
X1: seq1 is subsequence of seq & seq1 is convergent by B0,SEQ_2:3,BS,SEQ_4:40;
consider N be increasing sequence of NAT such that
X2: seq1 = seq * N by X1,VALUED_0:def 17;
reconsider f0=f*N as sequence of DualSp X;
now let k be Nat;
thus (f0#x).k = (f0.k).x by Def1
.= (f.(N.k)).x by ORDINAL1:def 12,FUNCT_2:15
.= (f#x).(N.k) by Def1
.= seq1.k by X2,ORDINAL1:def 12,FUNCT_2:15;
end; then
X5: f0#x = seq1;
for n be Nat holds |.||.f0.||.n.| < r0
proof
let n be Nat;
||.f0.||.n = ||.f0.n.|| by NORMSP_0:def 4; then
||.f0.||.n = ||. f.(N.n) .|| by ORDINAL1:def 12,FUNCT_2:15; then
||.f0.||.n = ||.f.||.(N.n) by NORMSP_0:def 4;
hence thesis by B0;
end;
hence thesis by X1,X5,B0,SEQ_2:3;
end;
theorem Lm814A2:
for X be RealNormSpace, f be sequence of DualSp X, x be Point of X
st ||.f.|| is bounded holds
ex f0 be sequence of DualSp X, N be increasing sequence of NAT st
f0 is subsequence of f & ||.f0.|| is bounded
& f0#x is convergent & f0#x is subsequence of f#x
& f0 = f*N
proof
let X be RealNormSpace, f be sequence of DualSp X, x be Point of X;
assume ||.f.|| is bounded; then
consider f0 be sequence of DualSp X such that
A1: f0 is subsequence of f & ||.f0.|| is bounded
& f0#x is convergent & f0#x is subsequence of f#x by Lm814A1;
take f0;
ex N be increasing sequence of NAT st f0 = f*N by A1,VALUED_0:def 17;
hence thesis by A1;
end;
theorem
for X be RealNormSpace, f be sequence of DualSp X, x be sequence of X
st ||.f.|| is bounded holds
ex F be sequence of Funcs(NAT,the carrier of DualSp X) st
F.0 is subsequence of f & (F.0)#(x.0) is convergent
& ( for k be Nat holds F.(k+1) is subsequence of F.k )
& ( for k be Nat holds (F.(k+1))#(x.(k+1)) is convergent)
proof
let X be RealNormSpace, f be sequence of DualSp X, x be sequence of X;
assume AS: ||.f.|| is bounded;
set D = Funcs(NAT,the carrier of DualSp X);
consider f0 be sequence of DualSp X such that
P0: f0 is subsequence of f & ||.f0.|| is bounded
& f0#(x.0) is convergent by AS,Lm814A;
reconsider A = f0 as Element of D by FUNCT_2:8;
defpred P[Nat,sequence of DualSp X,sequence of DualSp X] means
||.$2.|| is bounded implies
( $3 is subsequence of $2 & ||.$3.|| is bounded
& ($3)#(x.($1+1)) is convergent);
P1: for n being Nat for z being Element of D
ex y being Element of D st P[n,z,y]
proof
let n be Nat;
let z be Element of D;
consider f0 be sequence of DualSp X such that
X1: ||.z.|| is bounded implies
f0 is subsequence of z & ||.f0.|| is bounded
& f0#(x.(n+1)) is convergent by Lm814A;
reconsider y = f0 as Element of D by FUNCT_2:8;
take y;
thus thesis by X1;
end;
consider F be sequence of D such that
X2: F.0 = A &
for n being Nat holds P[n,F.n,F.(n+1)] from RECDEF_1:sch 2(P1);
defpred Q[Nat] means
F.($1+1) is subsequence of F.$1 & ||.F.($1+1).|| is bounded
& (F.($1+1))#(x.($1+1)) is convergent;
Q0: Q[0] by X2,P0;
Q1: for n be Nat st Q[n] holds Q[n+1] by X2;
Q2: for n be Nat holds Q[n] from NAT_1:sch 2(Q0,Q1);
take F;
thus thesis by P0,X2,Q2;
end;
theorem Lm814C:
for X be RealNormSpace, f be sequence of DualSp X, x be sequence of X
st ||.f.|| is bounded holds
ex F be sequence of Funcs(NAT,the carrier of DualSp X),
N be sequence of Funcs(NAT,NAT) st
F.0 is subsequence of f & (F.0)#(x.0) is convergent
& N.0 is increasing sequence of NAT & F.0 = f*N.0
& (for k be Nat holds F.(k+1) is subsequence of F.k)
& (for k be Nat holds (F.(k+1))#(x.(k+1)) is convergent)
& (for k be Nat holds (F.(k+1))#(x.(k+1)) is subsequence of (F.k)#(x.(k+1)))
& (for k be Nat holds N.(k+1) is increasing sequence of NAT)
& for k be Nat holds F.(k+1) = (F.k)*N.(k+1)
proof
let X be RealNormSpace, f be sequence of DualSp X, x be sequence of X;
assume ||.f.|| is bounded; then
consider f0 be sequence of DualSp X such that
P0: f0 is subsequence of f & ||.f0.|| is bounded
& f0#(x.0) is convergent & f0#(x.0) is subsequence of f#(x.0) by Lm814A1;
consider N0 be increasing sequence of NAT such that
R0: f0 = f*N0 by VALUED_0:def 17,P0;
set D1 = Funcs(NAT,the carrier of DualSp X);
set D2 = Funcs(NAT,NAT);
reconsider A=f0 as Element of D1 by FUNCT_2:8;
reconsider B=N0 as Element of D2 by FUNCT_2:8;
defpred P[Nat, sequence of DualSp X, sequence of NAT,
sequence of DualSp X, sequence of NAT] means
||.$2.|| is bounded implies
$4 is subsequence of $2 & ||.$4.|| is bounded
& ($4)#(x.($1+1)) is convergent
& ($4)#(x.($1+1)) is subsequence of ($2)#(x.($1+1))
& $5 is increasing sequence of NAT & $4 = $2*$5;
P1: for n being Nat for z being Element of D1, y being Element of D2
ex z1 being Element of D1, y1 being Element of D2 st P[n,z,y,z1,y1]
proof
let n be Nat;
let z be Element of D1, y be Element of D2;
consider f0 be sequence of DualSp X, N be increasing sequence of NAT
such that
X1: ||.z.|| is bounded implies
f0 is subsequence of z & ||.f0.|| is bounded
& f0#(x.(n+1)) is convergent
& f0#(x.(n+1)) is subsequence of z#(x.(n+1))
& f0 = z*N by Lm814A2;
reconsider z1=f0 as Element of D1 by FUNCT_2:8;
reconsider y1=N as Element of D2 by FUNCT_2:8;
take z1,y1;
thus thesis by X1;
end;
consider F be sequence of D1, N be sequence of D2 such that
X2: F.0 = A & N.0 = B &
for n being Nat holds P[n, F.n, N.n, F.(n+1), N.(n+1)]
from RECDEF_2:sch 3(P1);
defpred Q[Nat] means
( F.($1+1) is subsequence of F.$1
& ||.F.($1+1).|| is bounded & (F.($1+1))#(x.($1+1)) is convergent
& (F.($1+1))#(x.($1+1)) is subsequence of (F.$1)#(x.($1+1))
& N.($1+1) is increasing sequence of NAT
& F.($1+1) = (F.$1)*N.($1+1) );
Q0: Q[0] by X2,P0;
Q1: for n be Nat st Q[n] holds Q[n+1] by X2;
Q2: for n be Nat holds Q[n] from NAT_1:sch 2(Q0,Q1);
take F,N;
thus thesis by P0,X2,R0,Q2;
end;
theorem Lm814:
for X be RealNormSpace, f be sequence of DualSp X, x be sequence of X
st ||.f.|| is bounded holds
ex M be sequence of DualSp X st
M is subsequence of f & for k be Nat holds M#(x.k) is convergent
proof
let X be RealNormSpace, f be sequence of DualSp X, x be sequence of X;
assume ||.f.|| is bounded; then
consider F be sequence of Funcs(NAT,the carrier of DualSp X),
N be sequence of Funcs(NAT,NAT) such that
A0: F.0 is subsequence of f & (F.0)#(x.0) is convergent
& N.0 is increasing sequence of NAT & F.0 = f*N.0
& (for k be Nat holds F.(k+1) is subsequence of F.k)
& (for k be Nat holds (F.(k+1))#(x.(k+1)) is convergent)
& (for k be Nat holds (F.(k+1))#(x.(k+1)) is subsequence of (F.k)#(x.(k+1)))
& (for k be Nat holds N.(k+1) is increasing sequence of NAT)
& for k be Nat holds F.(k+1) = (F.k)*N.(k+1) by Lm814C;
deffunc F1(Element of NAT) = (F.$1).$1;
consider M be Function of NAT,DualSp X such that
A1: for k be Element of NAT holds M.k = F1(k) from FUNCT_2:sch 4;
reconsider M as sequence of DualSp X;
A2: for k be Nat holds M.k = (F.k).k
proof
let k be Nat;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
M.k1 = (F.k1).k1 by A1;
hence thesis;
end;
set D = Funcs(NAT,NAT);
reconsider A = N.0 as Element of D by FUNCT_2:8;
defpred P[Nat,sequence of NAT,sequence of NAT] means
$3 = $2*(N.($1+1));
P1: for n being Nat for x being Element of D
ex y being Element of D st P[n,x,y]
proof
let n be Nat;
let x be Element of D;
reconsider y=x*N.(n+1) as Element of D by FUNCT_2:8;
take y;
thus y = x*N.(n+1);
end;
consider J being sequence of D such that
P2: J.0 = A &
for n being Nat holds P[n, J.n, J.(n+1)] from RECDEF_1:sch 2(P1);
defpred Q[Nat] means J.$1 is increasing sequence of NAT;
Q0: Q[0] by P2,A0;
Q1: for n be Nat st Q[n] holds Q[n+1]
proof
let n be Nat;
assume X10: Q[n];
N.(n+1) is increasing sequence of NAT by A0; then
(J.n)*N.(n+1) is increasing sequence of NAT by X10;
hence J.(n+1) is increasing sequence of NAT by P2;
end;
Q2: for n be Nat holds Q[n] from NAT_1:sch 2(Q0,Q1);
defpred P1[Nat] means F.$1 = f*(J.$1);
Q0: P1[0] by P2,A0;
Q1: for n be Nat st P1[n] holds P1[n+1]
proof
let n be Nat;
assume X2: P1[n];
F.(n+1) = (F.n)*N.(n+1) by A0
.= f*((J.n)*N.(n+1)) by X2,RELAT_1:36;
hence F.(n+1) = f*(J.(n+1)) by P2;
end;
A41: for n be Nat holds P1[n] from NAT_1:sch 2(Q0,Q1);
deffunc F2(Element of NAT) = (J.$1).$1;
consider L be Function of NAT,NAT such that
A5: for k be Element of NAT holds L.k = F2(k) from FUNCT_2:sch 4;
reconsider L as sequence of NAT;
A6: for k be Nat holds L.k = (J.k).k
proof
let k be Nat;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
L.k1 = (J.k1).k1 by A5;
hence thesis;
end;
reconsider L0=L as Real_Sequence by FUNCT_2:7,NUMBERS:19;
for k be Nat holds L0.k < L0.(k+1)
proof
let k be Nat;
B2: J.k is increasing Real_Sequence by Q2,FUNCT_2:7,NUMBERS:19;
B3: L.(k+1) = (J.(k+1)).(k+1) by A6
.= ((J.k)*N.(k+1)).(k+1) by P2
.= (J.k).(N.(k+1).(k+1)) by FUNCT_2:15;
N.(k+1) is increasing sequence of NAT by A0; then
(k+1) <= N.(k+1).(k+1) by SEQM_3:14; then
k < N.(k+1).(k+1) by XREAL_1:145; then
(J.k).k < (J.k).(N.(k+1).(k+1)) by B2,SEQM_3:1;
hence thesis by B3,A6;
end; then
L0 is increasing; then
reconsider L as increasing sequence of NAT;
for k be Nat holds M.k = (f*L).k
proof
let k be Nat;
M.k = (F.k).k by A2
.= (f*(J.k)).k by A41
.= f.((J.k).k) by ORDINAL1:def 12,FUNCT_2:15
.= f.(L.k) by A6;
hence M.k = (f*L).k by ORDINAL1:def 12,FUNCT_2:15;
end; then
A71: M = f*L;
for k be Nat holds M#(x.k) is convergent
proof
let k be Nat;
Q1: (F.k)#(x.k) is convergent
proof
per cases;
suppose k = 0;
hence (F.k)#(x.k) is convergent by A0;
end;
suppose k <> 0; then
ex n be Nat st k=n+1 by NAT_1:6;
hence (F.k)#(x.k) is convergent by A0;
end;
end;
A0X: for k be Nat holds N.k is increasing sequence of NAT
proof
let k be Nat;
per cases;
suppose k = 0;
hence N.k is increasing sequence of NAT by A0;
end;
suppose k <> 0; then
ex n be Nat st k=n+1 by NAT_1:6;
hence N.k is increasing sequence of NAT by A0;
end;
end;
defpred PNk[Nat,sequence of NAT] means
for i be Nat holds ($2).i=(N.(k+$1)).(k+i)-k;
P11: for n being Element of NAT
ex y being Element of D st PNk[n,y]
proof
let n be Element of NAT;
defpred PNk1[Nat,object] means $2=(N.(k+n)).(k+$1)-k;
P111: for i being Element of NAT
ex y being Element of NAT st PNk1[i,y]
proof
let i be Element of NAT;
B5: k <= k + i by NAT_1:11;
N.(k+n) is increasing sequence of NAT by A0X; then
k+i <= N.(k+n).(k+i) by SEQM_3:14; then
k <= N.(k+n).(k+i) by B5,XXREAL_0:2; then
reconsider y = (N.(k+n)).(k+i)-k as Element of NAT
by INT_1:3,XREAL_1:48;
take y;
thus y = (N.(k+n)).(k+i)-k;
end;
consider y be Function of NAT,NAT such that
P121: for i being Element of NAT holds PNk1[i,y.i] from FUNCT_2:sch 3(P111);
reconsider y as Element of D by FUNCT_2:8;
take y;
thus for i be Nat holds y.i=(N.(k+n)).(k+i)-k
proof
let i be Nat;
i in NAT by ORDINAL1:def 12;
hence y.i=(N.(k+n)).(k+i)-k by P121;
end;
end;
consider Nk be Function of NAT,D such that
P12: for n being Element of NAT holds PNk[n,Nk.n] from FUNCT_2:sch 3(P11);
P13: for n being Element of NAT holds
Nk.n is increasing sequence of NAT
proof
let n be Element of NAT;
reconsider Nkn=Nk.n as Real_Sequence by FUNCT_2:7,NUMBERS:19;
D1: N.(k+n) is increasing Real_Sequence by FUNCT_2:7,NUMBERS:19,A0X;
for i be Nat holds Nkn.i < Nkn.(i+1)
proof
let i be Nat;
D2: (Nk.n).i = (N.(k+n)).(k+i)-k &
(Nk.n).(i+1) = (N.(k+n)).(k+(i+1))-k by P12;
(N.(k+n)).(k+i)-k < (N.(k+n)).(k+i+1)-k by XREAL_1:14,D1,SEQM_3:def 6;
hence thesis by D2;
end;
hence Nk.n is increasing sequence of NAT by SEQM_3:def 6;
end;
A0k: for n be Nat holds (F.(k+(n+1)))^\k = ((F.(k+n))^\k)*Nk.(n+1)
proof
let n be Nat;
XX1: F.(k+1+n) = F.(k+n)* N.((k+n)+1) by A0;
for i be Nat holds
(( F.(k+n))^\k *Nk.(n+1) ).i = (( F.(k+n) * N.(k+n+1))^\k).i
proof
let i be Nat;
N3: (Nk.(n+1)).i = (N.(k+(n+1))).(k+i)-k by P12;
thus ((F.(k+n))^\k *Nk.(n+1) ).i
= ((F.(k+n))^\k).((Nk.(n+1)).i) by FUNCT_2:15,ORDINAL1:def 12
.= (F.(k+n)).(k+((N.(k+(n+1))).(k+i)-k)) by NAT_1:def 3,N3
.= ( F.(k+n)*N.(k+(n+1))).(k+i) by FUNCT_2:15,ORDINAL1:def 12
.= (( F.(k+n) * N.(k+n+1))^\k).i by NAT_1:def 3;
end;
hence thesis by XX1;
end;
reconsider Ak = id NAT as Element of D by FUNCT_2:8;
defpred PJk[Nat,sequence of NAT,sequence of NAT] means
$3 = $2*(Nk.($1+1));
P14: for n being Nat for x being Element of D
ex y being Element of D st PJk[n,x,y]
proof
let n be Nat;
let x be Element of D;
reconsider y=x*(Nk.(n+1)) as Element of D by FUNCT_2:8;
take y;
thus y = x*(Nk.(n+1));
end;
consider Jk being sequence of D such that
P15: Jk.0 = Ak & for n being Nat holds PJk[n, Jk.n, Jk.(n+1)]
from RECDEF_1:sch 2(P14);
defpred QJk[Nat] means Jk.$1 is increasing sequence of NAT;
QJ0: QJk[0] by P15;
QJ1: for n be Nat st QJk[n] holds QJk[n+1]
proof
let n be Nat;
assume X10: QJk[n];
Nk.(n+1) is increasing sequence of NAT by P13; then
(Jk.n)*Nk.(n+1) is increasing sequence of NAT by X10;
hence Jk.(n+1) is increasing sequence of NAT by P15;
end;
AJ32: for n be Nat holds QJk[n] from NAT_1:sch 2(QJ0,QJ1);
defpred P1Jk[Nat] means (F.(k+$1))^\k = (F.k)^\k *(Jk.$1);
QJ0: P1Jk[0] by P15,FUNCT_2:17;
QJ1: for n be Nat st P1Jk[n] holds P1Jk[n+1]
proof
let n be Nat;
assume X2: P1Jk[n];
thus (F.(k+(n+1)))^\k = (( F.(k+n) )^\k)*Nk.(n+1) by A0k
.= (F.k)^\k *((Jk.n)*Nk.(n+1)) by X2,RELAT_1:36
.= (F.k)^\k *(Jk.(n+1)) by P15;
end;
BJ4: for n be Nat holds P1Jk[n] from NAT_1:sch 2(QJ0,QJ1);
deffunc FJk2(Element of NAT) = (Jk.$1).$1;
consider Lk be Function of NAT,NAT such that
AJ5: for n be Element of NAT holds Lk.n = FJk2(n) from FUNCT_2:sch 4;
reconsider Lk as sequence of NAT;
AJ6: for k be Nat holds Lk.k = (Jk.k).k
proof
let k be Nat;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
Lk.k1 = (Jk.k1).k1 by AJ5;
hence thesis;
end;
reconsider L0k=Lk as Real_Sequence by FUNCT_2:7,NUMBERS:19;
for k be Nat holds L0k.k < L0k.(k+1)
proof
let k be Nat;
B2: Jk.k is increasing Real_Sequence by AJ32,FUNCT_2:7,NUMBERS:19;
B3: Lk.(k+1) = (Jk.(k+1)).(k+1) by AJ6
.= ((Jk.k)*Nk.(k+1)).(k+1) by P15
.= (Jk.k).(Nk.(k+1).(k+1)) by FUNCT_2:15;
Nk.(k+1) is increasing sequence of NAT by P13; then
(k+1) <= Nk.(k+1).(k+1) by SEQM_3:14; then
k < Nk.(k+1).(k+1) by XREAL_1:145; then
(Jk.k).k < (Jk.k).(Nk.(k+1).(k+1)) by B2,SEQM_3:1;
hence thesis by B3,AJ6;
end; then
L0k is increasing; then
reconsider Lk as increasing sequence of NAT;
for n be Nat holds (M^\k).n = ((F.k)^\k *Lk).n
proof
let n be Nat;
thus (M^\k).n = M.(k+n) by NAT_1:def 3
.= (F.(k+n)).(k+n) by A2
.= ((F.(k+n))^\k).n by NAT_1:def 3
.= ((F.k)^\k *(Jk.n)).n by BJ4
.= ((F.k)^\k).((Jk.n).n) by ORDINAL1:def 12,FUNCT_2:15
.= ((F.k)^\k).(Lk.n) by AJ6
.= ((F.k)^\k *Lk).n by ORDINAL1:def 12,FUNCT_2:15;
end; then
P11: M^\k = (F.k)^\k*Lk;
Q12: for n be Nat holds ((M^\k)#(x.k)).n = ((M#(x.k))^\k).n
proof
let n be Nat;
thus ((M^\k)#(x.k)).n = ((M^\k).n).(x.k) by Def1
.= M.(k+n).(x.k) by NAT_1:def 3
.= (M#(x.k)).(k+n) by Def1
.= ((M#(x.k))^\k).n by NAT_1:def 3;
end;
for n be Nat holds (((F.k)^\k*Lk)#(x.k)).n = (((F.k)^\k)#(x.k)*Lk).n
proof
let n be Nat;
thus (((F.k)^\k*Lk)#(x.k)).n
= (((F.k)^\k*Lk).n).(x.k) by Def1
.= (((F.k)^\k).(Lk.n)).(x.k) by ORDINAL1:def 12,FUNCT_2:15
.= (((F.k)^\k)#(x.k)).(Lk.n) by Def1
.= (((F.k)^\k)#(x.k)*Lk).n by ORDINAL1:def 12,FUNCT_2:15;
end; then
((F.k)^\k*Lk)#(x.k) = ((F.k)^\k)#(x.k)*Lk; then
Q2: (M#(x.k))^\k = ((F.k)^\k)#(x.k)*Lk by P11,Q12;
for n be Nat holds (((F.k)#(x.k))^\k).n = ((F.k)^\k#(x.k)).n
proof
let n be Nat;
thus (((F.k)#(x.k))^\k).n = ((F.k)#(x.k)).(k+n) by NAT_1:def 3
.= ((F.k).(k+n)).(x.k) by Def1
.= (((F.k)^\k).n).(x.k) by NAT_1:def 3
.= ((F.k)^\k#(x.k)).n by Def1;
end; then
((F.k)#(x.k))^\k = (F.k)^\k#(x.k); then
(M#(x.k)) ^\k is convergent by Q1,Q2,SEQ_4:16;
hence M#(x.k) is convergent by SEQ_4:21;
end;
hence thesis by A71;
end;
theorem Th814:
for X be RealBanachSpace, f be sequence of DualSp X
st X is separable & ||.f.|| is bounded holds
ex f0 be sequence of DualSp X st
f0 is subsequence of f & f0 is weakly*-convergent
proof
let X be RealBanachSpace, f be sequence of DualSp X;
assume that
A1: X is separable and
A2: ||.f.|| is bounded;
consider x0 be sequence of X such that
A3: rng x0 is dense by A1,NORMSP_3:21;
set X0 = rng x0;
consider f0 be sequence of DualSp X such that
AX: f0 is subsequence of f and
A31: for n be Nat holds f0#(x0.n) is convergent by A2,Lm814;
A21: for x be Point of X ex K be Real st
0 <= K & for n be Nat holds |. (f#x).n .| <= K
proof
let x be Point of X;
consider K0 be Real such that
B0: 0 < K0 & for n be Nat holds |. ||.f.||.n .| < K0 by A2,SEQ_2:3;
reconsider K=K0*||.x.|| + 1 as Real;
take K;
B11: K0*||.x.|| + 0 < K0*||.x.|| + 1 by XREAL_1:8;
thus 0 <= K by B0;
thus for n be Nat holds |. (f#x).n .| <= K
proof
let n be Nat;
B2: |. ||.f.||.n .| <= K0 by B0;
||.f.||.n = ||.f.n.|| by NORMSP_0:def 4; then
B3: ||.f.n.|| <= K0 by B2,ABSVALUE:def 1;
reconsider h=f.n as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
B4: |.h.x.| <= ||.f.n.|| * ||.x.|| by DUALSP01:26;
B51: ||.f.n.|| * ||.x.|| <= K0 * ||.x.|| by B3,XREAL_1:64;
|.(f#x).n .| = |.(f.n).x.| by Def1; then
|.(f#x).n .| <= K0 * ||.x.|| by B51,B4,XXREAL_0:2;
hence thesis by B11,XXREAL_0:2;
end;
end;
set T = rng f0;
consider N be increasing sequence of NAT such that
AY: f0 = f * N by AX,VALUED_0:def 17;
for x be Point of X
ex K be Real st
0 <= K
& for g be Point of DualSp X st g in T holds |. g.x .| <= K
proof
let x be Point of X;
consider K be Real such that
A4: 0 <= K & for n be Nat holds |. (f#x).n .| <= K by A21;
A5: for n be Nat holds |. (f0#x).n .| <= K
proof
let n be Nat;
B3: f0.n = f.(N.n) by AY,ORDINAL1:def 12,FUNCT_2:15;
reconsider n0=N.n as Nat;
(f0#x).n = (f0.n).x by Def1
.= (f#x).n0 by B3,Def1;
hence thesis by A4;
end;
for g be Point of DualSp X st g in T holds |. g.x .| <= K
proof
let g be Point of DualSp X;
assume g in T; then
consider n be object such that
B1: n in NAT & g = f0.n by FUNCT_2:11;
reconsider n as Nat by B1;
g.x = (f0#x).n by B1,Def1;
hence thesis by A5;
end;
hence thesis by A4;
end; then
consider L be Real such that
A7: 0 <= L
& for g be Point of DualSp X st g in T holds ||.g.|| <= L by Lm55;
set M=L+1;
A8: L + 0 < M by XREAL_1:8;
A9: for g be Lipschitzian linear-Functional of X st g in T
for x,y be Point of X holds |.g.x - g.y.| <= M * ||.x-y.||
proof
let g be Lipschitzian linear-Functional of X;
reconsider g1=g as Point of DualSp X by DUALSP01:def 10;
assume g in T;
then ||.g1.|| <= L by A7; then
B1: ||.g1.|| < M by A8,XXREAL_0:2;
let x,y be Point of X;
|. g.x - g.y .| = |. g.x + (-1)*(g.y) .|; then
|. g.x - g.y .| = |. g.x + (g.((-1)*y)) .| by HAHNBAN:def 3; then
|. g.x - g.y .| = |. g.(x + (-1)*y) .| by HAHNBAN:def 2; then
B2: |. g.x - g.y .| = |. g.(x-y) .| by RLVECT_1:16;
B3: |. g.(x-y) .| <= ||.g1.|| * ||.x-y.|| by DUALSP01:26;
||.g1.|| * ||.x-y.|| <= M * ||.x-y.|| by B1,XREAL_1:64;
hence thesis by B2,B3,XXREAL_0:2;
end;
BX: for x be Point of X holds f0#x is convergent
proof
let x be Point of X;
for TK1 be Real st TK1 > 0
ex m be Nat st
for n be Nat st n >= m holds |.(f0#x).n - (f0#x).m.| < TK1
proof
let TK1 be Real;
assume B1: TK1 > 0; then
C2: 0 < TK1/(3*M) by A7;
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 X;
reconsider TKK=TK1 as Real;
V is open Subset of TopSpaceNorm X by NORMSP_2:8; then
B31: V is open by NORMSP_2:16;
||.x-x.|| < TKK/(3*M) by C2,NORMSP_1:6; then
x in V; then
consider s be object such that
B3: s in X0 & s in V by XBOOLE_0:3,B31,A3,NORMSP_3:17;
consider y be Point of X such that
B4: s=y & ||.x-y.|| < TK1/(3*M) by B3;
consider m be Element of NAT such that
B40: s=x0.m by B3,FUNCT_2:113;
consider m be Nat such that
B5: for n be Nat st m <= n holds |.(f0#y).n -(f0#y).m.| < TK1/3
by B1,A31,SEQ_4:41,B4,B40;
take m;
for n be Nat st n >= m holds |.(f0#x).n - (f0#x).m.| < TK1
proof
let n be Nat;
B6: m in NAT by ORDINAL1:def 12;
B7: n in NAT by ORDINAL1:def 12;
reconsider g=f0.n as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
reconsider h=f0.m as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
B8: |. (f0#x).n - (f0#y).m .| + |. (f0#y).m - (f0#x).m.|
<= |. (f0#x).n - (f0#y).n .| + |. (f0#y).n - (f0#y).m .|
+ |. (f0#y).m - (f0#x).m .| by XREAL_1:6,COMPLEX1:63;
assume n >= m; then
|. (f0#y).n - (f0#y).m .| < TK1/3 by B5; then
|. (f0#x).n - (f0#y).n .| + |. (f0#y).n - (f0#y).m .|
< |. (f0#x).n - (f0#y).n .| + TK1/3 by XREAL_1:8; then
B9: |. (f0#x).n - (f0#y).n .| + |. (f0#y).n - (f0#y).m .|
+ |. (f0#y).m - (f0#x).m .| < |. (f0#x).n - (f0#y).n .| + TK1/3
+ |. (f0#y).m - (f0#x).m .| by XREAL_1:8;
|. (f0#x).m - (f0#y).m .| = |. (f0.m).x-(f0#y).m .| by Def1; then
|. (f0#x).m - (f0#y).m .| = |. h.x - h.y .| by Def1; then
B10: |. (f0#x).m - (f0#y).m .| <= M * ||.x-y.|| by A9,FUNCT_2:4,B6;
M * ||.x-y.|| < M * (TK1 / (3*M)) by A7,B4,XREAL_1:68; then
M * ||.x-y.|| < TK1/3 by A7,XCMPLX_1:92; then
|. (f0#x).m - (f0#y).m .| < TK1/3 by B10,XXREAL_0:2; then
|. (f0#y).m - (f0#x).m .| < TK1/3 by COMPLEX1:60; then
B11: TK1/3 + TK1/3 + |. (f0#y).m - (f0#x).m .| < TK1/3 + TK1/3 + TK1/3
by XREAL_1:8;
|. (f0#x).n - (f0#y).n .| = |. (f0.n).x - (f0#y).n .| by Def1; then
|. (f0#x).n - (f0#y).n .| = |. g.x - g.y .| by Def1; then
B12: |. (f0#x).n - (f0#y).n .| <= M * ||.x-y.|| by A9,FUNCT_2:4,B7;
|. (f0#x).n - (f0#x).m .| <= |. (f0#x).n - (f0#y).m .|
+ |. (f0#y).m - (f0#x).m .| by COMPLEX1:63; then
|. (f0#x).n - (f0#x).m .| <= |. (f0#x).n - (f0#y).n .|
+ |. (f0#y).n - (f0#y).m .| + |. (f0#y).m - (f0#x).m .|
by B8,XXREAL_0:2; then
B13: |. (f0#x).n - (f0#x).m .| < |. (f0#x).n - (f0#y).n .|
+ TK1/3 + |. (f0#y).m - (f0#x).m .| by B9,XXREAL_0:2;
M * ||.x-y.|| < M * (TK1 / (3*M)) by A7,B4,XREAL_1:68; then
M * ||.x-y.||< TK1/3 by A7,XCMPLX_1:92; then
|. (f0#x).n - (f0#y).n.| < TK1/3 by B12,XXREAL_0:2; then
|. (f0#x).n-(f0#y).n .| + TK1/3 < TK1/3 + TK1/3 by XREAL_1:8; then
|. (f0#x).n - (f0#y).n .| + TK1/3 + |. (f0#y).m - (f0#x).m .|
< TK1/3 + TK1/3 + |. (f0#y).m - (f0#x).m .| by XREAL_1:8; then
|. (f0#x).n - (f0#y).n .| + TK1/3 + |. (f0#y).m - (f0#x).m .|
< TK1/3 + TK1/3 + TK1/3 by B11,XXREAL_0:2;
hence thesis by B13,XXREAL_0:2;
end;
hence thesis;
end;
hence thesis by SEQ_4:41;
end;
defpred FP[Element of the carrier of X, object] means
$2 = lim (f0#$1);
C01: for x being Element of the carrier of X
ex y being Element of REAL st FP[x,y]
proof
let x be Element of the carrier of X;
lim (f0#x) in REAL by XREAL_0:def 1;
hence thesis;
end;
consider f1 be Function of the carrier of X,REAL such that
C0: for x be Element of the carrier of X holds FP[x,f1.x]
from FUNCT_2:sch 3(C01);
C2: f1 is additive
proof
let x,y be Point of X;
D11: now let n be Nat;
reconsider h=f0.n as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
thus (f0#(x+y)).n = (f0.n).(x+y) by Def1
.= h.x + h.y by HAHNBAN:def 2
.= (f0#x).n + (f0.n).y by Def1
.= (f0#x).n + (f0#y).n by Def1;
end;
D2: f0#x is convergent & f0#y is convergent by BX;
thus f1.(x+y) = lim (f0#(x+y)) by C0
.= lim (f0#x + f0#y) by D11,SEQ_1:7
.= lim (f0#x) + lim (f0#y) by D2,SEQ_2:6
.= f1.x + lim (f0#y) by C0
.= f1.x + f1.y by C0;
end;
C31: f1 is homogeneous
proof
let x be Point of X, r be Real;
D31: now let n be Nat;
reconsider h=f0.n as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
thus (f0#(r*x)).n = (f0.n).(r*x) by Def1
.= r*h.x by HAHNBAN:def 3
.= r*(f0#x).n by Def1;
end;
thus f1.(r*x) = lim (f0#(r*x)) by C0
.= lim (r(#)(f0#x)) by D31,SEQ_1:9
.= r*(lim (f0#x)) by BX,SEQ_2:8
.= r*f1.x by C0;
end;
consider M be Real such that
C4: 0 < M
& for n be Nat holds |. ||.f.||.n .| < M by A2,SEQ_2:3;
now let x be Point of X;
D5: f0#x is convergent by BX;
D7: |.f1.x.| = |.lim (f0#x).| by C0
.= lim |.(f0#x).| by BX,SEQ_4:14;
D8: for n be Nat holds ||.f0.n.|| <= M
proof
let n be Nat;
f0.n = f.(N.n) by AY,ORDINAL1:def 12,FUNCT_2:15; then
E3: ||.f0.n.|| = ||.f.||.(N.n) by NORMSP_0:def 4;
|. ||.f.||.(N.n) .| < M by C4;
hence thesis by E3,ABSVALUE:def 1;
end;
reconsider s=M*||.x.|| as Real;
D91: now let n be Nat;
reconsider h=f0.n as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
E3: |.h.x.| <= ||.f0.n.||*||.x.|| by DUALSP01:26;
||.f0.n.||*||.x.|| <= M*||.x.|| by XREAL_1:64,D8; then
|.h.x.| <= M * ||.x.|| by E3,XXREAL_0:2; then
E51: |.(f0#x).n.| <= M*||.x.|| by Def1;
(seq_const s).n = s by SEQ_1:57;
hence |.(f0#x).|.n <= (seq_const s).n by E51,SEQ_1:12;
end;
lim (seq_const s) = (seq_const s).0 by SEQ_4:26
.= s;
hence |.f1.x.| <= M*||.x.|| by D7,D91,D5,SEQ_2:18;
end; then
f1 is Lipschitzian by C4; then
f1 is Point of DualSp X by DUALSP01:def 10,C31,C2; then
f0 is weakly*-convergent by BX,C0;
hence thesis by AX;
end;
theorem Th813:
for X be RealBanachSpace, x be sequence of X
st X is Reflexive & ||.x.|| is bounded holds
ex x0 be sequence of X st
x0 is subsequence of x & x0 is weakly-convergent
proof
let X be RealBanachSpace, x be sequence of X;
assume that
A2: X is Reflexive and
A3: ||.x.|| is bounded;
set L = ClNLin(rng x);
reconsider L0 = the carrier of L as Subset of X by DUALSP01:def 16;
LM1: for z be object st z in rng x holds z in the carrier of L
proof
let z be object;
assume z in rng x; then
C14: z in Lin(rng x) by RLVECT_3:15;
ex Z be Subset of X st
Z = the carrier of Lin(rng x)
& L = NORMSTR(# Cl(Z), Zero_(Cl(Z), X), Add_(Cl(Z), X),
Mult_(Cl(Z), X), Norm_(Cl(Z),X) #) by NORMSP_3:def 20;
hence z in the carrier of L by NORMSP_3:4,C14,TARSKI:def 3;
end;
per cases;
suppose XX1: rng x c= {0.X};
take x;
thus x is subsequence of x by VALUED_0:19;
thus x is weakly-convergent by XX1,WEAKLM1;
end;
suppose not rng x c= {0.X}; then
consider z be object such that
B11: z in rng x & not z in {0.X};
B12: z in rng x & z <> 0.X by B11,TARSKI:def 1;
B17: z in the carrier of L by LM1,B11;
0.X = 0.L by DUALSP01:def 16; then
A11: L is non trivial by B12,B17;
A12: L is Reflexive by A2,NORMSP_4:29;
DualSp DualSp L is separable by A11,A12,NORMSP_4:25; then
A4: DualSp L is separable by Th73;
set F=BidualFunc L;
rng x c= the carrier of L by LM1; then
reconsider x1 = x as sequence of L by FUNCT_2:6;
for i be Nat holds ||.x1.||.i = ||.x.||.i
proof
let i be Nat;
thus ||.x1.||.i = ||.x1.i.|| by NORMSP_0:def 4
.= ||.x.i.|| by NORMSP_3:28
.= ||.x.||.i by NORMSP_0:def 4;
end; then
B13: ||.x1.|| = ||.x.||; then
consider r be Real such that
A5: for n be Nat holds ||.x1.||.n < r by A3,SEQ_2:def 3;
for n be Nat holds ||.F*x1.||.n < r
proof
let n be Nat;
C2: ||.x1.||.n < r by A5;
||.x1.n.|| = ||.F.(x1.n).|| by A11,DUALSP02:9; then
||.F.(x1.n).|| < r by C2,NORMSP_0:def 4; then
||.(F*x1).n.|| < r by ORDINAL1:def 12,FUNCT_2:15;
hence thesis by NORMSP_0:def 4;
end; then
A6: ||.F*x1.|| is bounded_above;
consider s be Real such that
A7: for n be Nat holds s < ||.x1.||.n by B13,A3,SEQ_2:def 4;
for n be Nat holds s < ||.F*x1.||.n
proof
let n be Nat;
C4: s < ||.x1.||.n by A7;
||.x1.n.|| = ||.F.(x1.n).|| by A11,DUALSP02:9; then
s < ||.F.(x1.n).|| by C4,NORMSP_0:def 4; then
s < ||.(F*x1).n.|| by ORDINAL1:def 12,FUNCT_2:15;
hence thesis by NORMSP_0:def 4;
end; then
||.F*x1.|| is bounded_below; then
consider f1 be sequence of DualSp DualSp L such that
A9: f1 is subsequence of F*x1
& f1 is weakly*-convergent by A4,A6,Th814;
consider L1 be increasing sequence of NAT such that
A91: f1 = (F*x1)*L1 by A9,VALUED_0:def 17;
reconsider x01=x1*L1 as sequence of L;
f1=F*x01 by A91,RELAT_1:36; then
HX: x01 is weakly-convergent by A9,A12,Lm813A;
BX: the carrier of L c= the carrier of X by DUALSP01:def 16; then
reconsider x0=x01 as sequence of X by FUNCT_2:7;
reconsider y = w-lim x01 as Point of X by BX;
for h be Lipschitzian linear-Functional of X
holds h*x0 is convergent & lim (h*x0) = h.y
proof
let h be Lipschitzian linear-Functional of X;
reconsider h1=h| (the carrier of L)
as Lipschitzian linear-Functional of L by NORMSP_4:22;
GX3: dom h1 = the carrier of L by FUNCT_2:def 1; then
rng x01 c= dom h1; then
GX2: h1*x01 = h*x0 by RELAT_1:165;
h1*x01 is convergent & lim (h1*x01) = h1.(w-lim x01) by HX,DefWeaklim;
hence thesis by GX2,GX3,FUNCT_1:47;
end; then
x0 is weakly-convergent;
hence thesis;
end;
end;
theorem
for X be RealBanachSpace, X0 be non empty Subset of X
st X is non trivial Reflexive holds
X0 is weakly-sequentially-compact iff
ex S be non empty Subset of REAL st
S = {||.x.|| where x is Point of X : x in X0}
& S is bounded_above
proof
let X be RealBanachSpace, X0 be non empty Subset of X;
assume AS: X is non trivial Reflexive;
hence X0 is weakly-sequentially-compact implies
ex S be non empty Subset of REAL st
S = {||.x.|| where x is Point of X : x in X0}
& S is bounded_above by Th713A;
given S be non empty Subset of REAL such that
B0: S = {||.x.|| where x is Point of X : x in X0}
& S is bounded_above;
for seq be sequence of X0
ex seq1 be sequence of X st
seq1 is subsequence of seq & seq1 is weakly-convergent
& w-lim seq1 in X
proof
let seq0 be sequence of X0;
reconsider seq=seq0 as sequence of X by FUNCT_2:7;
consider r be Real such that
B1: r is UpperBound of S by B0;
B2: r + 0 < r + 1 by XREAL_1:8;
for n be Nat holds ||.seq.||.n < (r+1)
proof
let n be Nat;
seq0.n in X0; then
||.seq.n.|| in S by B0; then
||.seq.n.|| <= r by B1,XXREAL_2:def 1; then
||.seq.||.n <= r by NORMSP_0:def 4;
hence thesis by B2,XXREAL_0:2;
end; then
B5: ||.seq.|| is bounded_above;
for n be Nat holds -1 < ||.seq.||.n
proof
let n be Nat;
||.seq.n.|| = ||.seq.||.n by NORMSP_0:def 4;
hence thesis;
end; then
||.seq.|| is bounded_below; then
consider seq1 be sequence of X such that
P1: seq1 is subsequence of seq
& seq1 is weakly-convergent by AS,Th813,B5;
w-lim seq1 in X;
hence thesis by P1;
end;
hence thesis;
end;