let X be RealNormSpace; for x being sequence of X st not X is trivial & x is weakly-convergent holds
( ||.x.|| is bounded & ||.(w-lim x).|| <= lim_inf ||.x.|| & w-lim x in ClNLin (rng x) )
let x be sequence of X; ( not X is trivial & x is weakly-convergent implies ( ||.x.|| is bounded & ||.(w-lim x).|| <= lim_inf ||.x.|| & w-lim x in ClNLin (rng x) ) )
assume AS:
( not X is trivial & x is weakly-convergent )
; ( ||.x.|| is bounded & ||.(w-lim x).|| <= lim_inf ||.x.|| & w-lim x in ClNLin (rng x) )
reconsider x0 = w-lim x as Point of X ;
for f being Point of (DualSp X) ex Kf being Real st
( 0 <= Kf & ( for y being Point of X st y in rng x holds
|.(f . y).| <= Kf ) )
then consider K being Real such that
A4:
( 0 <= K & ( for y being Point of X st y in rng x holds
||.y.|| <= K ) )
by AS, DUALSP02:19;
A5:
for n being Nat holds ||.x.|| . n <= K
A6:
K + 0 < K + 1
by XREAL_1:8;
X10:
for n being Nat holds |.(||.x.|| . n).| < K + 1
then X1:
||.x.|| is bounded
by A4, SEQ_2:3;
B0:
for f being Point of (DualSp X) holds |.(f . x0).| <= (lim_inf ||.x.||) * ||.f.||
proof
let f be
Point of
(DualSp X);
|.(f . x0).| <= (lim_inf ||.x.||) * ||.f.||
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 being
Nat holds
|.(h * x).| . n <= (||.f.|| (#) ||.x.||) . n
||.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
|.(f . x0).| <= (lim_inf ||.x.||) * ||.f.||
by SEQ_4:14, B1, B7;
verum
end;
then B8:
0 <= lim_inf ||.x.||
by X1, RINFSUP1:82;
consider Y being 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;
x0 in ClNLin (rng x)
proof
set M =
ClNLin (rng x);
consider Z being
Subset of
X such that C1:
(
Z = the
carrier of
(Lin (rng x)) &
ClNLin (rng x) = 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
(ClNLin (rng x)) 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
;
contradiction
consider G being
Point of
(DualSp X) such that C5:
for
y being
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 being
Nat holds
(g * x) . n <= (seq_const 0) . n
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;
verum
end;
hence
x0 in ClNLin (rng x)
;
verum
end;
hence
( ||.x.|| is bounded & ||.(w-lim x).|| <= lim_inf ||.x.|| & w-lim x in ClNLin (rng x) )
by A4, SEQ_2:3, X10, B9, SEQ_4:45, X21; verum