:: Continuity of Multilinear Operator on Normed Linear Spaces
::  by Kazuhisa Nakasho and Yasunari Shidama
::
:: Received February 27, 2019
:: Copyright (c) 2019-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 LOPBAN10, NUMBERS, REAL_1, ZFMISC_1, NORMSP_1, PRE_TOPC,
      PARTFUN1, FUNCT_1, ORDINAL4, ORDINAL1, NEWTON, NAT_1, SUBSET_1, SEQ_1,
      RSSPACE3, FINSEQ_2, RELAT_1, LOPBAN_1, SQUARE_1, TARSKI, ARYTM_3,
      VALUED_1, GROUP_2, FUNCT_4, ARYTM_1, SEQ_2, ORDINAL2, SUPINF_2, FCONT_1,
      STRUCT_0, CARD_1, SEQ_4, METRIC_1, XXREAL_0, XBOOLE_0, FINSEQ_1,
      CFCONT_1, PRVECT_1, RVSUM_1, PRVECT_2, CARD_3, PDIFF_1, REWRITE1, POWER,
      COMPLEX1;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
      FUNCT_7, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1,
      CARD_3, NAT_1, COMPLEX1, FINSEQ_1, FINSEQ_2, VALUED_1, NAT_D, SEQ_1,
      SEQ_2, SEQ_4, NEWTON, POWER, STRUCT_0, PRE_TOPC, RLVECT_1, RSSPACE3,
      NORMSP_0, NORMSP_1, RVSUM_1, EUCLID, LOPBAN_1, LOPBAN_5, NFCONT_1,
      PRVECT_1, PRVECT_2, NDIFF_5, LOPBAN10;
 constructors SQUARE_1, SEQ_2, SEQ_4, NFCONT_1, COMSEQ_2, RELSET_1, NAT_D,
      SERIES_1, RSSPACE3, NDIFF_5, NEWTON, ABIAN, NDIFF_8, MONOID_0, SEQ_1,
      LOPBAN_5, REAL_1, PARTFUN3, LOPBAN10, FOMODEL0;
 registrations RELSET_1, STRUCT_0, XREAL_0, MEMBERED, FUNCT_1, VALUED_0,
      VALUED_1, FINSEQ_1, FINSEQ_2, FUNCT_2, NUMBERS, XBOOLE_0, RELAT_1,
      ORDINAL1, INT_1, PRVECT_2, XXREAL_0, NORMSP_0, NAT_1, NORMSP_1, SQUARE_1,
      RLVECT_1, MONOID_0, RVSUM_1, XCMPLX_0, PARTFUN3, SEQ_2, POWER, LOPBAN10,
      NEWTON, PRVECT_1;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;


begin :: Completeness of the Space of Multilinear Operators

theorem :: LOPBAN11:1  :::: preliminaries
  for n be Nat, r be Real st 0 < r
  ex s be Real st 0 < s & s < r & sqrt((s*s) * n) < r;

theorem :: LOPBAN11:2
  for R1,R2 be FinSequence of REAL,
      n,i be Nat,
      r be Real st i in dom R1
   & R1 = n |-> (1 qua Real)
   & R2 = R1 +* (i,r)
  holds Product R2 = r;

theorem :: LOPBAN11:3 ::::
  for F being FinSequence of REAL st (for k being Element of NAT
  st k in dom F holds 0 <= F.k) holds 0 <= Product F;

::: generalize NAT_4:54 in FINSEQ_9:34

reserve X,G for RealNormSpace-Sequence,
          Y for RealNormSpace;
reserve f for MultilinearOperator of X,Y;

theorem :: LOPBAN11:4  ::: should be proven before
  dom carr X = dom X;

theorem :: LOPBAN11:5
  for z be Element of product X st z = 0.product X
  holds for i be Element of dom X holds z.i = 0.(X.i);

theorem :: LOPBAN11:6
  f.(0.product X) = 0.Y;

theorem :: LOPBAN11:7  ::: LOPBAN10 lemma; NAT_4:42
  for F be FinSequence of REAL
  st for i be Element of dom F holds F.i > 0
  holds Product F > 0;

theorem :: LOPBAN11:8
  for X be RealNormSpace-Sequence, Y be RealNormSpace st Y is complete
  for seq be sequence of R_NormSpace_of_BoundedMultilinearOperators(X,Y)
    st seq is Cauchy_sequence_by_Norm
  holds seq is convergent;

theorem :: LOPBAN11:9
  for X be RealNormSpace-Sequence for Y be RealBanachSpace holds
  R_NormSpace_of_BoundedMultilinearOperators(X,Y) is RealBanachSpace;

registration
  let X be RealNormSpace-Sequence;
  let Y be RealBanachSpace;
  cluster R_NormSpace_of_BoundedMultilinearOperators (X,Y) -> complete;
end;

begin :: Equivalence of Continuity Definition of Multilinear Operator

theorem :: LOPBAN11:10
  for n be Nat, F be Element of REAL n, s be Real
  st for i be Nat st i in dom F holds 0 <= F.i & F.i <= s
  holds |.F.| <= sqrt((s*s) * len F);

theorem :: LOPBAN11:11
  for X be RealNormSpace-Sequence,
      Y be RealNormSpace,
      f be MultilinearOperator of X,Y,
      K being Real
  st
  ( 0 <= K & for x be Point of product X
    holds ||. f.x .|| <= K * NrProduct x )
  holds
  for v0,v1 being Point of product X,
      Cv0,Cv1 be FinSequence,
      i be Element of dom X
  st Cv0 = v0 & Cv1 = v1
   & ||.v1-v0.|| <= 1
   & for j be Element of dom X st i <> j holds Cv1.j = Cv0.j
  holds ||. f/.v1 - f/.v0 .||
    <= (||.v0.|| + 1) |^ len X * K * ||.(v1-v0).i.||;

theorem :: LOPBAN11:12
  for X be RealNormSpace-Sequence,
    Y be RealNormSpace,
    f be MultilinearOperator of X,Y,
    K being Real
  st (0 <= K &
      for x being Point of product X
      holds ||. f.x .|| <= K * NrProduct x) holds
  for v0 being Point of product X
  ex M be Real
  st 0 <= M
   & for v1 be Point of product X
     st ||.v1-v0.|| <= 1
     holds
     ex F be FinSequence of REAL
     st dom F = dom X
      & ||.f/.v1 - f/.v0.|| <= M * K * Sum F
      & for i be Element of dom X
        holds F.i = ||.(v1-v0).i.||;

theorem :: LOPBAN11:13
  for x be Point of product X,
      r be Real
  st 0 < r
  ex s be FinSequence of REAL,
     Y be non empty non-empty FinSequence
  st dom s = dom X & dom Y = dom X
   & product Y c= Ball(x,r)
   & for i be Element of dom X holds 0 < s.i & s.i < r
   & Y.i = Ball(x.i,s.i);

theorem :: LOPBAN11:14
  for X be RealNormSpace-Sequence,
      Y be RealNormSpace,
      f be MultilinearOperator of X,Y
  holds
  ( f is_continuous_on the carrier of product X
    iff
    f is_continuous_in 0.( product X ) )
  &
  ( f is_continuous_on the carrier of product X
    iff
    f is Lipschitzian );