:: 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
coherence
F . k is sequence of X
;
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
coherence
RNS_Real is complete
;
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
ex b1 being Real_Sequence st
for i being Nat holds b1 . i = (g . i) . x
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for i being Nat holds b1 . i = (g . i) . x ) & ( for i being Nat holds b2 . i = (g . i) . x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines # DUALSP03:def 1 :
for X being RealNormSpace
for g being sequence of (DualSp X)
for x being Point of X
for b4 being Real_Sequence holds
( b4 = g # x iff for i being Nat holds b4 . i = (g . i) . x );

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 :
for X being RealNormSpace
for x being sequence of X holds
( x is weakly-convergent iff 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 ) );

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
ex b1 being Point of X st
for f being Lipschitzian linear-Functional of X holds
( f * x is convergent & lim (f * x) = f . b1 )
by A1;
uniqueness
for b1, b2 being Point of X st ( for f being Lipschitzian linear-Functional of X holds
( f * x is convergent & lim (f * x) = f . b1 ) ) & ( for f being Lipschitzian linear-Functional of X holds
( f * x is convergent & lim (f * x) = f . b2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem DefWeaklim defines w-lim DUALSP03:def 3 :
for X being RealNormSpace
for x being sequence of X st x is weakly-convergent holds
for b3 being Point of X holds
( b3 = w-lim x iff for f being Lipschitzian linear-Functional of X holds
( f * x is convergent & lim (f * x) = f . b3 ) );

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 :
for X being RealNormSpace
for g being sequence of (DualSp X) holds
( g is weakly*-convergent iff ex g0 being Point of (DualSp X) st
for x being Point of X holds
( g # x is convergent & lim (g # x) = g0 . x ) );

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
ex b1 being Point of (DualSp X) st
for x being Point of X holds
( g # x is convergent & lim (g # x) = b1 . x )
by A1;
uniqueness
for b1, b2 being Point of (DualSp X) st ( for x being Point of X holds
( g # x is convergent & lim (g # x) = b1 . x ) ) & ( for x being Point of X holds
( g # x is convergent & lim (g # x) = b2 . x ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines w*-lim DUALSP03:def 5 :
for X being RealNormSpace
for g being sequence of (DualSp X) st g is weakly*-convergent holds
for b3 being Point of (DualSp X) holds
( b3 = w*-lim g iff for x being Point of X holds
( g # x is convergent & lim (g # x) = b3 . x ) );

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 :
for X being RealNormSpace
for X0 being non empty Subset of X holds
( X0 is weakly-sequentially-compact iff 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 ) );

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
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 & f0 # x is subsequence of f # x )
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;