:: Uniform Boundedness Principle
:: by Hideki Sakurai , Hisayoshi Kunimune and Yasunari Shidama
::
:: Received October 9, 2007
:: 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;

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;

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 (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ( for x being Point of X ex K being Real 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 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 sequence of 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 Nat holds it . n = (H . n) . x;

existence
ex b₁ being sequence of Y st
for n being Nat holds b₁ . n = (H . n) . x

proof end;

uniqueness
for b₁, b₂ being sequence of Y st ( for n being Nat holds b₁ . n = (H . n) . x ) & ( for n being Nat holds b₂ . n = (H . n) . x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines # LOPBAN_5:def 2 :
for X, Y being RealNormSpace
for H being sequence of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for x being Point of X
for b₅ being sequence of Y holds
( b₅ = H # x iff for n being Nat holds b₅ . 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 Lipschitzian 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;

:: 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 & ( 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 (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 st
( 0 <= K & ( for n being 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;