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


begin

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

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

registration
let X be RealBanachSpace;
cluster MetricSpaceNorm X ->  complete ;
coherence
 MetricSpaceNorm X is complete
proofend;
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
proofend;
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  }  ;

:: [WP: ] 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 &amp; ( 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 &amp; Ball (x0,r) c= Y . n0 )
proofend;

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 &amp; f is_continuous_on the carrier of X &amp; ( for x being Point of X holds f is_continuous_in x ) )
proofend;

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 &amp; ( 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 &amp; ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= L ) )
proofend;

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;
funcH # 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
proofend;
uniqueness
 for b1, b2 being sequence of Y st ( for n being Element of NAT holds b1 . n = (H . n) . x ) &amp; ( for n being Element of NAT holds b2 . n = (H . n) . x ) holds
b1 = b2
proofend;
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 &amp; tseq . x = lim (vseq # x) ) ) holds
( tseq is Lipschitzian LinearOperator of X,Y &amp; ( for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) &amp; ( for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds
||.ttseq.|| <= lim_inf ||.vseq.|| ) )
proofend;

begin

:: [WP: ] Banach-Steinhaus_theorem_(uniform_boundedness)
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 &amp; ( for x being Point of X st x in X0 holds
vseq # x is convergent ) &amp; ( for x being Point of X ex K being real number st
( 0 <= K &amp; ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ) holds
for x being Point of X holds vseq # x is convergent
proofend;

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 &amp; ( for x being Point of X st x in X0 holds
vseq # x is convergent ) &amp; ( for x being Point of X ex K being real number st
( 0 <= K &amp; ( 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 &amp; tseq . x = lim (vseq # x) &amp; ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) &amp; ||.tseq.|| <= lim_inf ||.vseq.|| )
proofend;