:: Uniform Boundedness Principle
:: by Hideki Sakurai , Hisayoshi Kunimune and Yasunari Shidama
::
:: Copyright (c) 2007-2021 Association of Mizar Users

theorem Th1: :: LOPBAN_5:1
for seq being Real_Sequence
for r being Real st seq is bounded & 0 <= r holds
lim_inf (r (#) seq) = r * (lim_inf seq)
proof end;

theorem :: LOPBAN_5:2
for seq being Real_Sequence
for r being Real st seq is bounded & 0 <= r holds
lim_sup (r (#) seq) = r * (lim_sup seq)
proof end;

registration
let X be RealBanachSpace;
coherence
proof end;
end;

definition
let X be RealNormSpace;
let x0 be Point of X;
let r be Real;
func Ball (x0,r) -> Subset of X equals :: LOPBAN_5:def 1
{ x where x is Point of X : ||.(x0 - x).|| < r } ;
coherence
{ x where x is Point of X : ||.(x0 - x).|| < r } is Subset of X
proof end;
end;

:: deftheorem defines Ball LOPBAN_5:def 1 :
for X being RealNormSpace
for x0 being Point of X
for r being Real holds Ball (x0,r) = { x where x is Point of X : ||.(x0 - x).|| < r } ;

:: Baire Category Theorem (Banach spaces)
theorem Th3: :: LOPBAN_5:3
for X being RealBanachSpace
for Y being SetSequence of X st union (rng Y) = the carrier of X & ( for n being Nat holds Y . n is closed ) holds
ex n0 being Nat ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 )
proof end;

theorem Th4: :: LOPBAN_5:4
for X, Y being RealNormSpace
for f being Lipschitzian LinearOperator of X,Y holds
( f is_Lipschitzian_on the carrier of X & f is_continuous_on the carrier of X & ( for x being Point of X holds f is_continuous_in x ) )
proof end;

theorem Th5: :: LOPBAN_5:5
for X being RealBanachSpace
for Y being RealNormSpace
for T being Subset of st ( for x being Point of X ex K being Real st
( 0 <= K & ( for f being Point of st f in T holds
||.(f . x).|| <= K ) ) ) holds
ex L being Real st
( 0 <= L & ( for f being Point of st f in T holds
<= L ) )
proof end;

definition
let X, Y be RealNormSpace;
let H be sequence of the carrier of ;
let x be Point of X;
func H # x -> sequence of Y means :Def2: :: LOPBAN_5:def 2
for n being Nat holds it . n = (H . n) . x;
existence
ex b1 being sequence of Y st
for n being Nat holds b1 . n = (H . n) . x
proof end;
uniqueness
for b1, b2 being sequence of Y st ( for n being Nat holds b1 . n = (H . n) . x ) & ( for n being Nat holds b2 . n = (H . n) . x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines # LOPBAN_5:def 2 :
for X, Y being RealNormSpace
for H being sequence of the carrier of
for x being Point of X
for b5 being sequence of Y holds
( b5 = H # x iff for n being Nat holds b5 . n = (H . n) . x );

theorem Th6: :: LOPBAN_5:6
for X being RealBanachSpace
for Y being RealNormSpace
for vseq being sequence of
for tseq being Function of X,Y st ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) ) ) holds
( tseq is Lipschitzian LinearOperator of X,Y & ( for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ) & ( for ttseq being Point of st ttseq = tseq holds
||.ttseq.|| <= lim_inf ||.vseq.|| ) )
proof end;

:: Banach-Steinhaus theorem (uniform boundedness)
theorem Th7: :: LOPBAN_5:7
for X being RealBanachSpace
for X0 being Subset of
for Y being RealBanachSpace
for vseq being sequence of st X0 is dense & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) & ( for x being Point of X ex K being Real st
( 0 <= K & ( for n being Nat holds ||.((vseq # x) . n).|| <= K ) ) ) holds
for x being Point of X holds vseq # x is convergent
proof end;

theorem :: LOPBAN_5:8
for X, Y being RealBanachSpace
for X0 being Subset of
for vseq being sequence of st X0 is dense & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) & ( for x being Point of X ex K being Real st
( 0 <= K & ( for n being Nat holds ||.((vseq # x) . n).|| <= K ) ) ) holds
ex tseq being Point of st
( ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| )
proof end;