:: Formalization of Separable Version of {B}anach {A}laoglu Theorem
:: by Hiroyuki Okazaki and Takehiko Mieno
::
:: Received December 21, 2025
:: Copyright (c) 2025-2026 Association of Mizar Users

:: Weak* Sequentially Compactness in Separable Dual Normed Spaces

theorem Th1: :: DUALSP07:1

for X being RealNormSpace
for vseq being sequence of (DualSp X)
for x, y being Point of X st vseq # x is convergent & vseq # y is convergent holds
( vseq # (x + y) is convergent & lim (vseq # (x + y)) = (lim (vseq # x)) + (lim (vseq # y)) )

proof end;

theorem Th2: :: DUALSP07:2

for X being RealNormSpace
for vseq being sequence of (DualSp X)
for x being Point of X
for a being Real st vseq # x is convergent holds
( vseq # (a * x) is convergent & lim (vseq # (a * x)) = a * (lim (vseq # x)) )

proof end;

theorem Th3: :: DUALSP07:3

for X being RealNormSpace
for X0 being Subset of X
for vseq being sequence of (DualSp X) st ( for x being Point of X st x in X0 holds
vseq # x is convergent ) holds
for x being Point of X st x in Lin X0 holds
vseq # x is convergent

proof end;

theorem Th4: :: DUALSP07:4

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

proof end;

theorem Th5: :: DUALSP07:5

for V being RealLinearSpace
for v being VECTOR of V
for a being Real st a <> 0 holds
ex l being Linear_Combination of V st
( l . v = a & Carrier l = {v} )

proof end;

theorem Th6: :: DUALSP07:6

for X being RealLinearSpace holds [#] (Lin ([#] X)) = [#] X

proof end;

theorem :: DUALSP07:7

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

proof end;

::$INSERT Weak* Sequentially Compactness in Separable Dual Normed Spaces

definition

let X be RealNormSpace;
let X0 be non empty Subset of (DualSp X);

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

end;

:: deftheorem defines weakly*-sequentially-compact DUALSP07:def 1 :
for X being RealNormSpace
for X0 being non empty Subset of (DualSp X) holds
( X0 is weakly*-sequentially-compact iff for seq being sequence of X0 ex seq1 being sequence of (DualSp X) st
( seq1 is subsequence of seq & seq1 is weakly*-convergent & w*-lim seq1 in X0 ) );

::$MR Banach Alaoglu theorem (case of separable)

theorem :: DUALSP07:8

for X being RealBanachSpace
for M being Real
for X0 being non empty Subset of (DualSp X) st X is separable & 0 <= M & cl_Ball ((0. (DualSp X)),M) = X0 holds
X0 is weakly*-sequentially-compact

proof end;

::$INSERT Weakly* sequentially continuous mappings on Normed Spaces

definition

let X be RealNormSpace;
let f be PartFunc of X,REAL;
let x0 be Point of X;

pred f is_weakly_continuous_in x0 means :: DUALSP07:def 2
( x0 in dom f & ( for e being Real st 0 < e holds
ex d being Real ex Y being Subset of (DualSp X) st
( 0 < d & Y is finite & Y <> {} & ( for x being Point of X st x in dom f & ( for y being Point of (DualSp X) st y in Y holds
|.(y . (x - x0)).| < d ) holds
|.((f . x) - (f . x0)).| < e ) ) ) );

end;

:: deftheorem defines is_weakly_continuous_in DUALSP07:def 2 :
for X being RealNormSpace
for f being PartFunc of X,REAL
for x0 being Point of X holds
( f is_weakly_continuous_in x0 iff ( x0 in dom f & ( for e being Real st 0 < e holds
ex d being Real ex Y being Subset of (DualSp X) st
( 0 < d & Y is finite & Y <> {} & ( for x being Point of X st x in dom f & ( for y being Point of (DualSp X) st y in Y holds
|.(y . (x - x0)).| < d ) holds
|.((f . x) - (f . x0)).| < e ) ) ) ) );

definition

let X be RealNormSpace;
let f be PartFunc of X,REAL;
let X0 be Subset of X;

pred f is_weakly_continuous_on X0 means :: DUALSP07:def 3
( X0 c= dom f & ( for x0 being Point of X st x0 in X0 holds
for e being Real st 0 < e holds
ex d being Real ex Y being Subset of (DualSp X) st
( 0 < d & Y is finite & Y <> {} & ( for x being Point of X st x in X0 & ( for y being Point of (DualSp X) st y in Y holds
|.(y . (x - x0)).| < d ) holds
|.((f . x) - (f . x0)).| < e ) ) ) );

end;

:: deftheorem defines is_weakly_continuous_on DUALSP07:def 3 :
for X being RealNormSpace
for f being PartFunc of X,REAL
for X0 being Subset of X holds
( f is_weakly_continuous_on X0 iff ( X0 c= dom f & ( for x0 being Point of X st x0 in X0 holds
for e being Real st 0 < e holds
ex d being Real ex Y being Subset of (DualSp X) st
( 0 < d & Y is finite & Y <> {} & ( for x being Point of X st x in X0 & ( for y being Point of (DualSp X) st y in Y holds
|.(y . (x - x0)).| < d ) holds
|.((f . x) - (f . x0)).| < e ) ) ) ) );

theorem :: DUALSP07:9

for X being RealNormSpace
for f being PartFunc of X,REAL
for X0 being Subset of X holds
( f is_weakly_continuous_on X0 iff ( X0 c= dom f & ( for x0 being Point of X st x0 in X0 holds
f | X0 is_weakly_continuous_in x0 ) ) )

proof end;

definition

let X be RealNormSpace;
let f be PartFunc of (DualSp X),REAL;
let x0 be Point of (DualSp X);

pred f is_weakly*_continuous_in x0 means :: DUALSP07:def 4
( x0 in dom f & ( for e being Real st 0 < e holds
ex d being Real ex Y being Subset of X st
( 0 < d & Y is finite & Y <> {} & ( for x being Point of (DualSp X) st x in dom f & ( for y being Point of X st y in Y holds
|.((x - x0) . y).| < d ) holds
|.((f . x) - (f . x0)).| < e ) ) ) );

end;

:: deftheorem defines is_weakly*_continuous_in DUALSP07:def 4 :
for X being RealNormSpace
for f being PartFunc of (DualSp X),REAL
for x0 being Point of (DualSp X) holds
( f is_weakly*_continuous_in x0 iff ( x0 in dom f & ( for e being Real st 0 < e holds
ex d being Real ex Y being Subset of X st
( 0 < d & Y is finite & Y <> {} & ( for x being Point of (DualSp X) st x in dom f & ( for y being Point of X st y in Y holds
|.((x - x0) . y).| < d ) holds
|.((f . x) - (f . x0)).| < e ) ) ) ) );

definition

let X be RealNormSpace;
let f be PartFunc of (DualSp X),REAL;
let X0 be Subset of (DualSp X);

pred f is_weakly*_continuous_on X0 means :: DUALSP07:def 5
( X0 c= dom f & ( for x0 being Point of (DualSp X) st x0 in X0 holds
for e being Real st 0 < e holds
ex d being Real ex Y being Subset of X st
( 0 < d & Y is finite & Y <> {} & ( for x being Point of (DualSp X) st x in X0 & ( for y being Point of X st y in Y holds
|.((x - x0) . y).| < d ) holds
|.((f . x) - (f . x0)).| < e ) ) ) );

end;

:: deftheorem defines is_weakly*_continuous_on DUALSP07:def 5 :
for X being RealNormSpace
for f being PartFunc of (DualSp X),REAL
for X0 being Subset of (DualSp X) holds
( f is_weakly*_continuous_on X0 iff ( X0 c= dom f & ( for x0 being Point of (DualSp X) st x0 in X0 holds
for e being Real st 0 < e holds
ex d being Real ex Y being Subset of X st
( 0 < d & Y is finite & Y <> {} & ( for x being Point of (DualSp X) st x in X0 & ( for y being Point of X st y in Y holds
|.((x - x0) . y).| < d ) holds
|.((f . x) - (f . x0)).| < e ) ) ) ) );

theorem Th10: :: DUALSP07:10

for X being RealNormSpace
for f being PartFunc of (DualSp X),REAL
for X0 being Subset of (DualSp X) holds
( f is_weakly*_continuous_on X0 iff ( X0 c= dom f & ( for x0 being Point of (DualSp X) st x0 in X0 holds
f | X0 is_weakly*_continuous_in x0 ) ) )

proof end;

theorem :: DUALSP07:11

for X being RealNormSpace
for f being PartFunc of X,REAL
for x0 being Point of X
for x being sequence of X st f is_weakly_continuous_in x0 & rng x c= dom f & x is weakly-convergent & w-lim x = x0 holds
( f /* x is convergent & lim (f /* x) = f . x0 )

proof end;

theorem Th12: :: DUALSP07:12

for X being RealNormSpace
for f being PartFunc of (DualSp X),REAL
for x0 being Point of (DualSp X)
for x being sequence of (DualSp X) st f is_weakly*_continuous_in x0 & rng x c= dom f & x is weakly*-convergent & w*-lim x = x0 holds
( f /* x is convergent & lim (f /* x) = f . x0 )

proof end;

theorem :: DUALSP07:13

for X being RealNormSpace
for f being PartFunc of (DualSp X),REAL
for S being non empty Subset of (DualSp X) st S is weakly*-sequentially-compact & f is_weakly*_continuous_on S holds
( ex r being Real st
for x being Point of (DualSp X) st x in S holds
|.(f . x).| <= r & ex x0 being Point of (DualSp X) st
( x0 in S & ( for x being Point of (DualSp X) st x in S holds
f . x <= f . x0 ) ) & ex v0 being Point of (DualSp X) st
( v0 in S & ( for x being Point of (DualSp X) st x in S holds
f . v0 <= f . x ) ) )

proof end;