let X be RealBanachSpace; for f being sequence of (DualSp X) st X is separable & ||.f.|| is bounded holds
ex f0 being sequence of (DualSp X) st
( f0 is subsequence of f & f0 is weakly*-convergent )
let f be sequence of (DualSp X); ( X is separable & ||.f.|| is bounded implies ex f0 being sequence of (DualSp X) st
( f0 is subsequence of f & f0 is weakly*-convergent ) )
assume that
A1:
X is separable
and
A2:
||.f.|| is bounded
; ex f0 being sequence of (DualSp X) st
( f0 is subsequence of f & f0 is weakly*-convergent )
consider x0 being sequence of X such that
A3:
rng x0 is dense
by A1, NORMSP_3:21;
set X0 = rng x0;
consider f0 being sequence of (DualSp X) such that
AX:
f0 is subsequence of f
and
A31:
for n being Nat holds f0 # (x0 . n) is convergent
by A2, Lm814;
A21:
for x being Point of X ex K being Real st
( 0 <= K & ( for n being Nat holds |.((f # x) . n).| <= K ) )
set T = rng f0;
consider N being V132() sequence of NAT such that
AY:
f0 = f * N
by AX, VALUED_0:def 17;
for x being Point of X ex K being Real st
( 0 <= K & ( for g being Point of (DualSp X) st g in rng f0 holds
|.(g . x).| <= K ) )
then consider L being Real such that
A7:
( 0 <= L & ( for g being Point of (DualSp X) st g in rng f0 holds
||.g.|| <= L ) )
by Lm55;
set M = L + 1;
A8:
L + 0 < L + 1
by XREAL_1:8;
A9:
for g being Lipschitzian linear-Functional of X st g in rng f0 holds
for x, y being Point of X holds |.((g . x) - (g . y)).| <= (L + 1) * ||.(x - y).||
BX:
for x being Point of X holds f0 # x is convergent
proof
let x be
Point of
X;
f0 # x is convergent
for
TK1 being
Real st
TK1 > 0 holds
ex
m being
Nat st
for
n being
Nat st
n >= m holds
|.(((f0 # x) . n) - ((f0 # x) . m)).| < TK1
proof
let TK1 be
Real;
( TK1 > 0 implies ex m being Nat st
for n being Nat st n >= m holds
|.(((f0 # x) . n) - ((f0 # x) . m)).| < TK1 )
assume B1:
TK1 > 0
;
ex m being Nat st
for n being Nat st n >= m holds
|.(((f0 # x) . n) - ((f0 # x) . m)).| < TK1
then C2:
0 < TK1 / (3 * (L + 1))
by A7;
set V =
{ z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (L + 1)) } ;
{ z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (L + 1)) } c= the
carrier of
X
then reconsider V =
{ z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (L + 1)) } 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 * (L + 1))
by C2, NORMSP_1:6;
then
x in V
;
then consider s being
object such that B3:
(
s in rng x0 &
s in V )
by XBOOLE_0:3, B31, A3, NORMSP_3:17;
consider y being
Point of
X such that B4:
(
s = y &
||.(x - y).|| < TK1 / (3 * (L + 1)) )
by B3;
consider m being
Element of
NAT such that B40:
s = x0 . m
by B3, FUNCT_2:113;
consider m being
Nat such that B5:
for
n being
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 being Nat st n >= m holds
|.(((f0 # x) . n) - ((f0 # x) . m)).| < TK1
for
n being
Nat st
n >= m holds
|.(((f0 # x) . n) - ((f0 # x) . m)).| < TK1
proof
let n be
Nat;
( n >= m implies |.(((f0 # x) . n) - ((f0 # x) . m)).| < TK1 )
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
;
|.(((f0 # x) . n) - ((f0 # x) . m)).| < TK1
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)).| <= (L + 1) * ||.(x - y).||
by A9, FUNCT_2:4, B6;
(L + 1) * ||.(x - y).|| < (L + 1) * (TK1 / (3 * (L + 1)))
by A7, B4, XREAL_1:68;
then
(L + 1) * ||.(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)).| <= (L + 1) * ||.(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;
(L + 1) * ||.(x - y).|| < (L + 1) * (TK1 / (3 * (L + 1)))
by A7, B4, XREAL_1:68;
then
(L + 1) * ||.(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
|.(((f0 # x) . n) - ((f0 # x) . m)).| < TK1
by B13, XXREAL_0:2;
verum
end;
hence
for
n being
Nat st
n >= m holds
|.(((f0 # x) . n) - ((f0 # x) . m)).| < TK1
;
verum
end;
hence
f0 # x is
convergent
by SEQ_4:41;
verum
end;
defpred S1[ 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 S1[x,y]
consider f1 being Function of the carrier of X,REAL such that
C0:
for x being Element of the carrier of X holds S1[x,f1 . x]
from FUNCT_2:sch 3(C01);
C2:
f1 is additive
C31:
f1 is homogeneous
consider M being Real such that
C4:
( 0 < M & ( for n being Nat holds |.(||.f.|| . n).| < M ) )
by A2, SEQ_2:3;
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
ex f0 being sequence of (DualSp X) st
( f0 is subsequence of f & f0 is weakly*-convergent )
by AX; verum