:: by Keiko Narita , Noboru Endou and Yasunari Shidama

::

:: Received July 1, 2015

:: Copyright (c) 2015-2016 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;

end;
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;

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

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 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 )

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

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

lim seq = lim seq1

proof end;

definition

let X be RealNormSpace;

let g be sequence of (DualSp X);

let x be Point of X;

ex b_{1} being Real_Sequence st

for i being Nat holds b_{1} . i = (g . i) . x

for b_{1}, b_{2} being Real_Sequence st ( for i being Nat holds b_{1} . i = (g . i) . x ) & ( for i being Nat holds b_{2} . i = (g . i) . x ) holds

b_{1} = b_{2}

end;
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 for i being Nat holds it . i = (g . i) . x;

ex b

for i being Nat holds b

proof end;

uniqueness for b

b

proof 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 b_{4} being Real_Sequence holds

( b_{4} = g # x iff for i being Nat holds b_{4} . i = (g . i) . x );

for X being RealNormSpace

for g being sequence of (DualSp X)

for x being Point of X

for b

( b

definition

let X be RealNormSpace;

let x be sequence of X;

end;
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 );

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 );

:: 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 ) );

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

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 ;

ex b_{1} being Point of X st

for f being Lipschitzian linear-Functional of X holds

( f * x is convergent & lim (f * x) = f . b_{1} )
by A1;

uniqueness

for b_{1}, b_{2} being Point of X st ( for f being Lipschitzian linear-Functional of X holds

( f * x is convergent & lim (f * x) = f . b_{1} ) ) & ( for f being Lipschitzian linear-Functional of X holds

( f * x is convergent & lim (f * x) = f . b_{2} ) ) holds

b_{1} = b_{2}

end;
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 for f being Lipschitzian linear-Functional of X holds

( f * x is convergent & lim (f * x) = f . it );

ex b

for f being Lipschitzian linear-Functional of X holds

( f * x is convergent & lim (f * x) = f . b

uniqueness

for b

( f * x is convergent & lim (f * x) = f . b

( f * x is convergent & lim (f * x) = f . b

b

proof 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 b_{3} being Point of X holds

( b_{3} = w-lim x iff for f being Lipschitzian linear-Functional of X holds

( f * x is convergent & lim (f * x) = f . b_{3} ) );

for X being RealNormSpace

for x being sequence of X st x is weakly-convergent holds

for b

( b

( f * x is convergent & lim (f * x) = f . b

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 )

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) )

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);

end;
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 );

ex g0 being Point of (DualSp X) st

for x being Point of X holds

( g # x is convergent & lim (g # x) = g0 . x );

:: 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 ) );

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 ;

ex b_{1} being Point of (DualSp X) st

for x being Point of X holds

( g # x is convergent & lim (g # x) = b_{1} . x )
by A1;

uniqueness

for b_{1}, b_{2} being Point of (DualSp X) st ( for x being Point of X holds

( g # x is convergent & lim (g # x) = b_{1} . x ) ) & ( for x being Point of X holds

( g # x is convergent & lim (g # x) = b_{2} . x ) ) holds

b_{1} = b_{2}

end;
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 for x being Point of X holds

( g # x is convergent & lim (g # x) = it . x );

ex b

for x being Point of X holds

( g # x is convergent & lim (g # x) = b

uniqueness

for b

( g # x is convergent & lim (g # x) = b

( g # x is convergent & lim (g # x) = b

b

proof 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 b_{3} being Point of (DualSp X) holds

( b_{3} = w*-lim g iff for x being Point of X holds

( g # x is convergent & lim (g # x) = b_{3} . x ) );

for X being RealNormSpace

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

for b

( b

( g # x is convergent & lim (g # x) = b

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 )

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

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 )

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 ) )

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.|| )

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

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

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 ) ) ) )

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;

end;
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 );

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 );

:: 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 ) );

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 )

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 )

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 )

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 )

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 ) )

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)) ) )

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 ) )

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 )

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 )

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 ) )

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;