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


begin

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;
cluster MetricSpaceNorm X -> complete ;
coherence
MetricSpaceNorm X is complete
proof end;
end;

definition
let X be RealNormSpace;
let x0 be Point of X;
let r be real number ;
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 number holds Ball (x0,r) = { x where x is Point of X : ||.(x0 - x).|| < r } ;

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 Element of NAT holds Y . n is closed ) holds
ex n0 being Element of 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 bounded 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 (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ( for x being Point of X ex K being real number st
( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.(f . x).|| <= K ) ) ) holds
ex L being real number st
( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= L ) )
proof end;

definition
let X, Y be RealNormSpace;
let H be Function of NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y));
let x be Point of X;
func H # x -> sequence of Y means :Def2: :: LOPBAN_5:def 2
for n being Element of NAT holds it . n = (H . n) . x;
existence
ex b1 being sequence of Y st
for n being Element of NAT holds b1 . n = (H . n) . x
proof end;
uniqueness
for b1, b2 being sequence of Y st ( for n being Element of NAT holds b1 . n = (H . n) . x ) & ( for n being Element of 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 Function of NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for x being Point of X
for b5 being sequence of Y holds
( b5 = H # x iff for n being Element of 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 (R_NormSpace_of_BoundedLinearOperators (X,Y))
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 bounded LinearOperator of X,Y & ( for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) & ( for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds
||.ttseq.|| <= lim_inf ||.vseq.|| ) )
proof end;

begin

theorem Th7: :: LOPBAN_5:7
for X being RealBanachSpace
for X0 being Subset of (LinearTopSpaceNorm X)
for Y being RealBanachSpace
for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) 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 number st
( 0 <= K & ( for n being Element of 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 (LinearTopSpaceNorm X)
for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) 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 number st
( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ) holds
ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| )
proof end;