:: Uniform Boundedness Principle
::  by Hideki Sakurai , Hisayoshi Kunimune and Yasunari Shidama
::
:: Received October 9, 2007
:: Copyright (c) 2007-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SEQ_1, REAL_1, XXREAL_2, CARD_1, XXREAL_0, ORDINAL2,
      VALUED_1, RELAT_1, RINFSUP1, FUNCT_2, FUNCT_1, TARSKI, XBOOLE_0,
      SUBSET_1, ARYTM_3, COMPLEX1, NAT_1, SEQ_4, MEMBER_1, LOPBAN_1, NORMSP_2,
      REWRITE1, BHSP_3, RSSPACE3, METRIC_1, SEQ_2, NORMSP_1, PRE_TOPC, ARYTM_1,
      STRUCT_0, PROB_1, RCOMP_1, PCOMPS_1, NFCONT_1, CFCONT_1, FCONT_1,
      RLVECT_1, PARTFUN1, ZFMISC_1, CARD_3, SUPINF_2, PBOOLE, TOPS_1;
 notations TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
      XCMPLX_0, PRE_TOPC, TOPS_1, COMPLEX1, REAL_1, ORDINAL1, NAT_1, STRUCT_0,
      CARD_3, NUMBERS, XREAL_0, RINFSUP1, XXREAL_0, VALUED_1, SEQ_1, SEQ_2,
      SEQ_4, XXREAL_2, RLVECT_1, TBSP_1, METRIC_1, PCOMPS_1, NORMSP_0,
      NORMSP_1, NORMSP_2, RSSPACE3, LOPBAN_1, NFCONT_1, INTEGRA2, KURATO_2;
 constructors REAL_1, COMPLEX1, TOPS_1, TBSP_1, NFCONT_1, RINFSUP1, INTEGRA2,
      PROB_1, NORMSP_2, RSSPACE3, LOPBAN_1, RVSUM_1, SEQ_4, RELSET_1, BINOP_2,
      SEQ_2, PCOMPS_1, COMSEQ_2, BINOP_1;
 registrations NUMBERS, XREAL_0, XBOOLE_0, ORDINAL1, RELSET_1, STRUCT_0,
      MEMBERED, SUBSET_1, NAT_1, NORMSP_1, NORMSP_2, FUNCT_2, LOPBAN_1,
      VALUED_0, VALUED_1, SEQ_2, NORMSP_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: Uniform Boundedness Principle

theorem :: LOPBAN_5:1
  for seq be Real_Sequence, r be Real st seq is bounded & 0<=r
  holds lim_inf(r(#)seq)=r*(lim_inf seq);

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

registration
  let X be RealBanachSpace;
  cluster MetricSpaceNorm X -> complete;
end;

definition
  let X be RealNormSpace, x0 be Point of X, 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 };
end;

::$N Baire Category Theorem (Banach spaces)
theorem :: LOPBAN_5:3
:: Baire category theorem - Banach space version
  for X be RealBanachSpace, Y be SetSequence of X st union rng Y =
the carrier of X & (for n be Nat holds Y.n is closed)
 ex n0 be Nat, r be Real, x0 be Point of X
    st 0 < r & Ball (x0,r) c= Y.n0;

theorem :: LOPBAN_5:4
  for X,Y be RealNormSpace, f be Lipschitzian LinearOperator of X,Y
holds f is_Lipschitzian_on the carrier of X & f is_continuous_on the carrier of
  X & for x be Point of X holds f is_continuous_in x;

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

definition
  let X, Y be RealNormSpace, H be sequence of  the carrier of
  R_NormSpace_of_BoundedLinearOperators(X,Y), x be Point of X;
  func H # x -> sequence of Y means
:: LOPBAN_5:def 2

  for n be Nat holds it.n = (H.n).x;
end;

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

begin :: Banach-Steinhaus Principle

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

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