DUALSP03: Weak Convergence and Weak* Convergence

:: Weak Convergence and Weak* Convergence
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received July 1, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users

definition

let X be non empty set ;
let F be sequence of (Funcs (NAT,X));
let k be Nat;
:: original: .
redefine func F . k -> sequence of X;
correctness

proof end;

end;

theorem Lm73: :: DUALSP03:1

for X being strict RealNormSpace
for A being non empty Subset of X st ( for f being Point of (DualSp X) st ( for x being Point of X st x in A holds
(Bound2Lipschitz (f,X)) . x = 0 ) holds
Bound2Lipschitz (f,X) = 0. (DualSp X) ) holds
ClNLin A = X

proof end;

theorem Th73: :: DUALSP03:2

for X being strict RealNormSpace st DualSp X is separable holds
X is separable

proof end;

theorem RNS3: :: DUALSP03:3

for x being Real
for x1 being Point of RNS_Real st x = x1 holds
- x = - x1

proof end;

theorem RNS4: :: DUALSP03:4

for x, y being Real
for x1, y1 being Point of RNS_Real st x = x1 & y = y1 holds
x - y = x1 - y1

proof end;

theorem RNS8: :: DUALSP03:5

for seq being Real_Sequence
for seq1 being sequence of RNS_Real st seq = seq1 holds
( seq is convergent iff seq1 is convergent )

proof end;

theorem RNS9: :: DUALSP03:6

for seq being Real_Sequence
for seq1 being sequence of RNS_Real st seq = seq1 & seq is convergent holds
lim seq = lim seq1

proof end;

theorem RNS11: :: DUALSP03:7

for seq1 being sequence of RNS_Real st seq1 is Cauchy_sequence_by_Norm holds
seq1 is convergent

proof end;

registration

cluster RNS_Real -> complete ;

correctness by LOPBAN_1:def 15, RNS11;

end;

definition

let X be RealNormSpace;
let g be sequence of (DualSp X);
let x be Point of X;

func g # x -> Real_Sequence means :Def1: :: DUALSP03:def 1
for i being Nat holds it . i = (g . i) . x;

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines # DUALSP03:def 1 :

definition

let X be RealNormSpace;
let x be sequence of X;

attr x is weakly-convergent means :: DUALSP03:def 2
ex x0 being Point of X st
for f being Lipschitzian linear-Functional of X holds
( f * x is convergent & lim (f * x) = f . x0 );

end;

:: deftheorem defines weakly-convergent DUALSP03:def 2 :

theorem WEAKLM1: :: DUALSP03:8

for X being RealNormSpace
for x being sequence of X st rng x c= {(0. X)} holds
x is weakly-convergent

proof end;

definition

let X be RealNormSpace;
let x be sequence of X;
assume A1: x is weakly-convergent ;

func w-lim x -> Point of X means :DefWeaklim: :: DUALSP03:def 3
for f being Lipschitzian linear-Functional of X holds
( f * x is convergent & lim (f * x) = f . it );

existence by A1;
uniqueness

proof end;

end;

:: deftheorem DefWeaklim defines w-lim DUALSP03:def 3 :

theorem :: DUALSP03:9

for X being RealNormSpace
for x being sequence of X st x is convergent holds
( x is weakly-convergent & w-lim x = lim x )

proof end;

theorem Th79: :: DUALSP03:10

for X being 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) )

proof end;

definition

let X be RealNormSpace;
let g be sequence of (DualSp X);

attr g is weakly*-convergent means :: DUALSP03:def 4
ex g0 being Point of (DualSp X) st
for x being Point of X holds
( g # x is convergent & lim (g # x) = g0 . x );

end;

:: deftheorem defines weakly*-convergent DUALSP03:def 4 :

definition

let X be RealNormSpace;
let g be sequence of (DualSp X);
assume A1: g is weakly*-convergent ;

func w*-lim g -> Point of (DualSp X) means :Def2: :: DUALSP03:def 5
for x being Point of X holds
( g # x is convergent & lim (g # x) = it . x );

existence by A1;
uniqueness

proof end;

end;

:: deftheorem Def2 defines w*-lim DUALSP03:def 5 :

theorem :: DUALSP03:11

for X being RealNormSpace
for g being sequence of (DualSp X) st g is convergent holds
( g is weakly*-convergent & w*-lim g = lim g )

proof end;

theorem Lm710A: :: DUALSP03:12

for X being RealNormSpace
for f being sequence of (DualSp X) st f is weakly-convergent holds
f is weakly*-convergent

proof end;

theorem :: DUALSP03:13

for X being RealNormSpace
for f being sequence of (DualSp X) st X is Reflexive holds
( f is weakly-convergent iff f is weakly*-convergent )

proof end;

theorem Lm55: :: DUALSP03:14

for X being RealBanachSpace
for T being Subset of (DualSp X) st ( for x being Point of X ex K being Real st
( 0 <= K & ( for f being Point of (DualSp X) st f in T holds
|.(f . x).| <= K ) ) ) holds
ex L being Real st
( 0 <= L & ( for f being Point of (DualSp X) st f in T holds
||.f.|| <= L ) )

proof end;

theorem Th711: :: DUALSP03:15

for X being RealBanachSpace
for f being sequence of (DualSp X) st f is weakly*-convergent holds
( ||.f.|| is bounded & ||.(w*-lim f).|| <= lim_inf ||.f.|| )

proof end;

theorem RNSBH1: :: DUALSP03:16

for X being RealNormSpace
for x being Point of X
for vseq being sequence of (DualSp X)
for vseq1 being sequence of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st vseq = vseq1 holds
vseq # x = vseq1 # x

proof end;

theorem Th712A: :: DUALSP03:17

for X being RealBanachSpace
for X0 being Subset of X
for vseq being sequence of (DualSp X) st ||.vseq.|| is bounded & X0 is dense & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) holds
vseq is weakly*-convergent

proof end;

theorem :: DUALSP03:18

for X being RealBanachSpace
for f being sequence of (DualSp X) holds
( f is weakly*-convergent iff ( ||.f.|| is bounded & ex X0 being Subset of X st
( X0 is dense & ( for x being Point of X st x in X0 holds
f # x is convergent ) ) ) )

proof end;

definition

let X be RealNormSpace;
let X0 be non empty Subset of X;

attr X0 is weakly-sequentially-compact means :: DUALSP03:def 6
for seq being sequence of X0 ex seq1 being sequence of X st
( seq1 is subsequence of seq & seq1 is weakly-convergent & w-lim seq1 in X );

end;

:: deftheorem defines weakly-sequentially-compact DUALSP03:def 6 :

Th713A: for X being RealBanachSpace
for X0 being non empty Subset of X st not X is trivial & X is Reflexive & X0 is weakly-sequentially-compact holds
ex S being non empty Subset of REAL st
( S = { ||.x.|| where x is Point of X : x in X0 } & S is bounded_above )

proof end;

theorem Lm813A: :: DUALSP03:19

for X being RealNormSpace
for x being sequence of X st X is Reflexive holds
( x is weakly-convergent iff (BidualFunc X) * x is weakly*-convergent )

proof end;

theorem Lm814A: :: DUALSP03:20

for X being RealNormSpace
for f being sequence of (DualSp X)
for x being Point of X st ||.f.|| is bounded holds
ex f0 being sequence of (DualSp X) st
( f0 is subsequence of f & ||.f0.|| is bounded & f0 # x is convergent )

proof end;

theorem Lm814A1: :: DUALSP03:21

proof end;

theorem Lm814A2: :: DUALSP03:22

for X being RealNormSpace
for f being sequence of (DualSp X)
for x being Point of X st ||.f.|| is bounded holds
ex f0 being sequence of (DualSp X) ex N being V132() 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 end;

theorem :: DUALSP03:23

for X being RealNormSpace
for f being sequence of (DualSp X)
for x being sequence of X st ||.f.|| is bounded holds
ex F being sequence of (Funcs (NAT, the carrier of (DualSp X))) st
( F . 0 is subsequence of f & (F . 0) # (x . 0) is convergent & ( for k being Nat holds F . (k + 1) is subsequence of F . k ) & ( for k being Nat holds (F . (k + 1)) # (x . (k + 1)) is convergent ) )

proof end;

theorem Lm814C: :: DUALSP03:24

for X being RealNormSpace
for f being sequence of (DualSp X)
for x being sequence of X st ||.f.|| is bounded holds
ex F being sequence of (Funcs (NAT, the carrier of (DualSp X))) ex N being sequence of (Funcs (NAT,NAT)) st
( F . 0 is subsequence of f & (F . 0) # (x . 0) is convergent & N . 0 is V132() sequence of NAT & F . 0 = f * (N . 0) & ( for k being Nat holds F . (k + 1) is subsequence of F . k ) & ( for k being Nat holds (F . (k + 1)) # (x . (k + 1)) is convergent ) & ( for k being Nat holds (F . (k + 1)) # (x . (k + 1)) is subsequence of (F . k) # (x . (k + 1)) ) & ( for k being Nat holds N . (k + 1) is V132() sequence of NAT ) & ( for k being Nat holds F . (k + 1) = (F . k) * (N . (k + 1)) ) )

proof end;

theorem Lm814: :: DUALSP03:25

for X being RealNormSpace
for f being sequence of (DualSp X)
for x being sequence of X st ||.f.|| is bounded holds
ex M being sequence of (DualSp X) st
( M is subsequence of f & ( for k being Nat holds M # (x . k) is convergent ) )

proof end;

theorem Th814: :: DUALSP03:26

for X being 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 )

proof end;

theorem Th813: :: DUALSP03:27

for X being RealBanachSpace
for x being sequence of X st X is Reflexive & ||.x.|| is bounded holds
ex x0 being sequence of X st
( x0 is subsequence of x & x0 is weakly-convergent )

proof end;

theorem :: DUALSP03:28

for X being RealBanachSpace
for X0 being non empty Subset of X st not X is trivial & X is Reflexive holds
( X0 is weakly-sequentially-compact iff ex S being non empty Subset of REAL st
( S = { ||.x.|| where x is Point of X : x in X0 } & S is bounded_above ) )

proof end;