:: Bilinear Operators on Normed Linear Spaces
::  by Kazuhisa Nakasho
:: 
:: 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 NUMBERS, REAL_1, ZFMISC_1, NORMSP_1, PRE_TOPC, FUNCT_1, NAT_1,
      SUBSET_1, SEQ_1, RSSPACE3, RELAT_1, LOPBAN_1, TARSKI, ARYTM_3, VALUED_1,
      FUNCT_2, ARYTM_1, SEQ_2, ORDINAL2, SUPINF_2, FCONT_1, STRUCT_0, CARD_1,
      FUNCOP_1, SEQ_4, ASYMPT_1, XXREAL_2, FUNCSDOM, RLSUB_1, RSSPACE, RELAT_2,
      METRIC_1, ALGSTR_0, MONOID_0, XXREAL_0, XBOOLE_0, RLVECT_1, REWRITE1,
      COMPLEX1, LOPBAN_8, LOPBAN_9;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
      FUNCT_2, BINOP_1, FUNCOP_1, NUMBERS, MONOID_0, XCMPLX_0, XXREAL_0,
      XXREAL_2, XREAL_0, NAT_1, COMPLEX1, VALUED_1, SEQ_1, SEQ_2, SEQ_4,
      STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, RLSUB_1, RSSPACE3, NORMSP_0,
      NORMSP_1, RSSPACE, LOPBAN_1, PRVECT_3, LOPBAN_8;
 constructors SEQ_2, SEQ_4, RLSUB_1, COMSEQ_2, RELSET_1, DUALSP01, NAT_D,
      RSSPACE3, NDIFF_5, DOMAIN_1, MONOID_0, SEQ_1, LOPBAN_8, REAL_1;
 registrations RELSET_1, STRUCT_0, XREAL_0, MEMBERED, FUNCT_1, VALUED_1,
      FUNCT_2, NUMBERS, XBOOLE_0, ORDINAL1, NORMSP_0, NAT_1, SEQ_4, NORMSP_1,
      RLVECT_1, MONOID_0, SEQ_1, SEQ_2, LOPBAN_1;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;


begin :: Real Vector Space of Bilinear Operators

definition
  let X, Y, Z be RealLinearSpace;
  func BilinearOperators(X,Y,Z)
   -> Subset of RealVectSpace(the carrier of [:X,Y:],Z) means
:: LOPBAN_9:def 1
  for x being set holds x in it
        iff x is BilinearOperator of X,Y,Z;
end;

registration
  let X, Y, Z be RealLinearSpace;
  cluster BilinearOperators(X,Y,Z) -> non empty functional;
end;

registration
  let X, Y, Z be RealLinearSpace;
  cluster BilinearOperators(X,Y,Z) -> linearly-closed;
end;

definition
  let X, Y, Z be RealLinearSpace;
  func R_VectorSpace_of_BilinearOperators(X,Y,Z) -> strict RLSStruct equals
:: LOPBAN_9:def 2
    RLSStruct (# BilinearOperators(X,Y,Z),
      Zero_(BilinearOperators(X,Y,Z),
        RealVectSpace(the carrier of [:X,Y:],Z)),
      Add_(BilinearOperators(X,Y,Z),
        RealVectSpace(the carrier of [:X,Y:],Z)),
      Mult_(BilinearOperators(X,Y,Z),
        RealVectSpace(the carrier of [:X,Y:],Z)) #);
end;

registration
  let X, Y, Z be RealLinearSpace;
  cluster R_VectorSpace_of_BilinearOperators(X,Y,Z) -> non empty;
end;

registration
  let X, Y, Z be RealLinearSpace;
  cluster R_VectorSpace_of_BilinearOperators(X,Y,Z) ->
    Abelian add-associative right_zeroed right_complementable
    vector-distributive scalar-distributive scalar-associative scalar-unital;
end;

registration
  let X,Y, Z be RealLinearSpace;
  cluster R_VectorSpace_of_BilinearOperators(X,Y,Z) -> constituted-Functions;
end;

theorem :: LOPBAN_9:1
  for X, Y, Z be RealLinearSpace holds
    R_VectorSpace_of_BilinearOperators(X,Y,Z)
      is Subspace of RealVectSpace(the carrier of [:X,Y:],Z);

definition
  let X,Y,Z be RealLinearSpace;
  let f be Element of R_VectorSpace_of_BilinearOperators(X,Y,Z);
  let v be VECTOR of X, w be VECTOR of Y;
  redefine func f. (v,w) -> VECTOR of Z;
end;

theorem :: LOPBAN_9:2
  for X, Y, Z be RealLinearSpace
  for f,g,h be VECTOR of R_VectorSpace_of_BilinearOperators(X,Y,Z)
  holds
    h = f+g
  iff
    for x be VECTOR of X,y be VECTOR of Y
    holds h.(x,y) = f.(x,y) + g.(x,y);

theorem :: LOPBAN_9:3
  for X, Y, Z be RealLinearSpace
  for f,h be VECTOR of R_VectorSpace_of_BilinearOperators(X,Y,Z)
  for a be Real
  holds
    h = a*f
  iff
    for x be VECTOR of X, y be VECTOR of Y
    holds h.(x,y) = a * f.(x,y);

theorem :: LOPBAN_9:4
  for X, Y, Z be RealLinearSpace holds
  0.R_VectorSpace_of_BilinearOperators(X,Y,Z)
    = (the carrier of [:X,Y:] ) -->0.Z;

theorem :: LOPBAN_9:5
  for X,Y, Z be RealLinearSpace holds
  (the carrier of [:X,Y:] ) --> 0.Z is BilinearOperator of X,Y,Z;

begin :: Real Normed Linear Space of Bounded Bilinear Operators

definition
  let X, Y, Z be RealNormSpace;
  let IT be BilinearOperator of X,Y,Z;
  attr IT is Lipschitzian means
:: LOPBAN_9:def 3
  ex K being Real st 0 <= K &
  for x being VECTOR of X, y being VECTOR of Y
  holds ||. IT.(x,y) .|| <= K * ||. x .|| * ||. y .||;
end;

theorem :: LOPBAN_9:6
  for X, Y, Z be RealNormSpace holds
    for f be BilinearOperator of X,Y,Z
    st (for x be VECTOR of X,y be VECTOR of Y holds f.(x,y) = 0.Z)
    holds f is Lipschitzian;

theorem :: LOPBAN_9:7
  for X,Y,Z be RealNormSpace holds
  (the carrier of [:X,Y:]) --> 0.Z is BilinearOperator of X,Y,Z;

registration
  let X, Y, Z be RealNormSpace;
  cluster Lipschitzian for BilinearOperator of X,Y,Z;
end;

theorem :: LOPBAN_9:8
  for X, Y, Z be RealNormSpace, z be object holds
    ( z in BilinearOperators(X,Y,Z)
  iff
    z is BilinearOperator of X,Y,Z );

definition
  let X, Y, Z be RealNormSpace;
  func BoundedBilinearOperators(X,Y,Z)
    -> Subset of R_VectorSpace_of_BilinearOperators(X,Y,Z) means
:: LOPBAN_9:def 4
  for x being set holds x in it
  iff x is Lipschitzian BilinearOperator of X,Y,Z;
end;

registration
  let X, Y, Z be RealNormSpace;
  cluster BoundedBilinearOperators(X,Y,Z) -> non empty;
end;

registration
  let X, Y, Z be RealNormSpace;
  cluster BoundedBilinearOperators(X,Y,Z) -> linearly-closed;
end;

definition
  let X, Y, Z be RealNormSpace;
  func R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z) -> strict RLSStruct
  equals
:: LOPBAN_9:def 5
  RLSStruct (# BoundedBilinearOperators(X,Y,Z),
    Zero_(BoundedBilinearOperators(X,Y,Z),
      R_VectorSpace_of_BilinearOperators(X,Y,Z)),
    Add_(BoundedBilinearOperators(X,Y,Z),
      R_VectorSpace_of_BilinearOperators(X,Y,Z)),
    Mult_(BoundedBilinearOperators(X,Y,Z),
      R_VectorSpace_of_BilinearOperators(X,Y,Z)) #);
end;

theorem :: LOPBAN_9:9
  for X, Y, Z be RealNormSpace holds
    R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z)
      is Subspace of R_VectorSpace_of_BilinearOperators(X,Y,Z);

registration
  let X, Y, Z be RealNormSpace;
  cluster R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z) -> non empty;
end;

registration
  let X, Y, Z be RealNormSpace;
  cluster R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z) ->
    Abelian add-associative right_zeroed
      right_complementable vector-distributive
      scalar-distributive scalar-associative scalar-unital;
end;

registration
  let X,Y, Z be RealNormSpace;
  cluster R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z) ->
    constituted-Functions;
end;

definition
  let X,Y,Z be RealNormSpace;
  let f be Element of R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z);
  let v be VECTOR of X,w be VECTOR of Y;
  redefine func f.(v,w) -> VECTOR of Z;
end;

theorem :: LOPBAN_9:10
  for X, Y, Z be RealNormSpace
  for f,g,h be VECTOR of R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z)
  holds
    h = f+g
  iff
    for x be VECTOR of X, y be VECTOR of Y
    holds h.(x,y) = f.(x,y) + g.(x,y);

theorem :: LOPBAN_9:11
  for X, Y, Z be RealNormSpace
  for f,h be VECTOR of R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z)
  for a be Real holds
    h = a * f
  iff
    for x be VECTOR of X,y be VECTOR of Y holds
    h.(x,y) = a * f.(x,y);

theorem :: LOPBAN_9:12
  for X, Y, Z be RealNormSpace holds
  0.R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z)
  = (the carrier of [:X,Y:]) --> 0.Z;

definition
  let X,Y,Z be RealNormSpace;
  let f be object such that
   f in BoundedBilinearOperators(X,Y,Z);
  func modetrans(f,X,Y,Z) -> Lipschitzian BilinearOperator of X,Y,Z
  equals
:: LOPBAN_9:def 6
  f;
end;

definition
  let X, Y, Z be RealNormSpace;
  let u be BilinearOperator of X,Y,Z;
  func PreNorms(u) -> non empty Subset of REAL equals
:: LOPBAN_9:def 7
  {||.u.(t,s) .|| where t is VECTOR of X, s is VECTOR of Y
    : ||.t.|| <= 1 & ||.s.|| <= 1 };
end;

registration
  let X, Y, Z be RealNormSpace;
  let g be Lipschitzian BilinearOperator of X,Y,Z;
  cluster PreNorms(g) -> bounded_above;
end;

theorem :: LOPBAN_9:13
  for X, Y, Z be RealNormSpace
  for g be BilinearOperator of X,Y,Z
  holds g is Lipschitzian iff PreNorms(g) is bounded_above;

definition
  let X, Y, Z be RealNormSpace;
  func BoundedBilinearOperatorsNorm(X,Y,Z)
    -> Function of BoundedBilinearOperators(X,Y,Z), REAL means
:: LOPBAN_9:def 8
  for x be object st x in BoundedBilinearOperators(X,Y,Z) holds
  it.x = upper_bound PreNorms(modetrans(x,X,Y,Z));
end;

registration
  let X, Y, Z be RealNormSpace;
  let f be Lipschitzian BilinearOperator of X,Y,Z;
  reduce modetrans(f,X,Y,Z) to f;
end;

theorem :: LOPBAN_9:14
  for X, Y, Z be RealNormSpace for f be Lipschitzian BilinearOperator of X,Y,Z
  holds BoundedBilinearOperatorsNorm(X,Y,Z).f = upper_bound PreNorms(f);

definition
  let X, Y, Z be RealNormSpace;
  func R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) -> non empty NORMSTR
  equals
:: LOPBAN_9:def 9
  NORMSTR (# BoundedBilinearOperators(X,Y,Z),
    Zero_(BoundedBilinearOperators(X,Y,Z),
      R_VectorSpace_of_BilinearOperators(X,Y,Z)),
    Add_(BoundedBilinearOperators(X,Y,Z),
      R_VectorSpace_of_BilinearOperators(X,Y,Z)),
    Mult_(BoundedBilinearOperators(X,Y,Z),
      R_VectorSpace_of_BilinearOperators(X,Y,Z)),
    BoundedBilinearOperatorsNorm(X,Y,Z) #);
end;

theorem :: LOPBAN_9:15
  for X,Y,Z be RealNormSpace holds
  (the carrier of [:X,Y:]) --> 0.Z
    = 0.R_NormSpace_of_BoundedBilinearOperators(X,Y,Z);

theorem :: LOPBAN_9:16
  for X,Y,Z be RealNormSpace
  for f being Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
  for g be Lipschitzian BilinearOperator of X,Y,Z st g=f
  holds
    for t be VECTOR of X, s be VECTOR of Y
    holds ||.g.(t,s).|| <= ||.f.|| * ||.t.|| * ||.s.||;

theorem :: LOPBAN_9:17
  for X,Y,Z be RealNormSpace
  for f being Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
  holds 0 <= ||.f.||;

theorem :: LOPBAN_9:18
  for X, Y, Z be RealNormSpace
  for f being Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
  st f = 0.R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
  holds 0 = ||.f.||;

registration
  let X,Y,Z be RealNormSpace;
  cluster -> Function-like Relation-like for Element of
    R_NormSpace_of_BoundedBilinearOperators(X,Y,Z);
end;

definition
  let X,Y,Z be RealNormSpace;
  let f be Element of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z);
  let v be VECTOR of X,w be VECTOR of Y;
  redefine func f.(v,w) -> VECTOR of Z;
end;

theorem :: LOPBAN_9:19
  for X, Y, Z be RealNormSpace
  for f,g,h be Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
  holds
    h = f+g
  iff
    for x be VECTOR of X,y be VECTOR of Y
    holds h.(x,y) = f.(x,y) + g.(x,y);

theorem :: LOPBAN_9:20
  for X, Y, Z be RealNormSpace
  for f,h be Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
  for a be Real
  holds
    h = a*f
  iff
    for x be VECTOR of X,y be VECTOR of Y
    holds h.(x,y) = a * f.(x,y);

theorem :: LOPBAN_9:21
  for X,Y,Z be RealNormSpace
  for f, g being Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
  for a be Real
  holds
  ( ||.f.|| = 0 iff f = 0.R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) )
  & ||.a*f.|| = |.a.| * ||.f.||
  & ||.f+g.|| <= ||.f.|| + ||.g.||;

registration let X, Y, Z be RealNormSpace;
  cluster R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) -> non empty;
end;

registration let X, Y, Z be RealNormSpace;
  cluster R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) ->
    reflexive discerning RealNormSpace-like;
end;

theorem :: LOPBAN_9:22
  for X, Y, Z be RealNormSpace holds
  R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) is RealNormSpace;

registration
  let X, Y, Z be RealNormSpace;
  cluster R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) ->
    vector-distributive scalar-distributive scalar-associative scalar-unital
    Abelian add-associative right_zeroed right_complementable;
end;

theorem :: LOPBAN_9:23
  for X,Y,Z be RealNormSpace
  for f,g,h be Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
  holds
    h = f-g
  iff
    for x be VECTOR of X,y be VECTOR of Y
    holds h.(x,y) = f.(x,y) - g.(x,y);

begin

theorem :: LOPBAN_9:24
  for X, Y, Z be RealNormSpace st Z is complete
  for seq be sequence of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
  st seq is Cauchy_sequence_by_Norm
  holds seq is convergent;

theorem :: LOPBAN_9:25
  for X,Y be RealNormSpace, Z be RealBanachSpace
  holds R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) is RealBanachSpace;

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

begin :: Isomorphic Mappings between the Space of Bilinear Operators
      :: and the Space of Composition of Linear Operators

reserve X,Y,Z for RealLinearSpace;

theorem :: LOPBAN_9:26
  ex I be LinearOperator of
    R_VectorSpace_of_LinearOperators(X,R_VectorSpace_of_LinearOperators(Y,Z)),
    R_VectorSpace_of_BilinearOperators(X,Y,Z) st I is bijective
   & for u be Point of
     R_VectorSpace_of_LinearOperators(X,R_VectorSpace_of_LinearOperators(Y,Z))
     holds
       for x be Point of X,y be Point of Y
       holds (I.u).(x,y) = (u.x).y;

 reserve X,Y,Z for RealNormSpace;

theorem :: LOPBAN_9:27
  ex I be LinearOperator of
    R_NormSpace_of_BoundedLinearOperators
    (X,R_NormSpace_of_BoundedLinearOperators(Y,Z)),
    R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
  st I is bijective
   & for u be Point of
      R_NormSpace_of_BoundedLinearOperators
        (X,R_NormSpace_of_BoundedLinearOperators(Y,Z))
      holds
        ||.u.|| = ||. I.u .||
      & for x be Point of X,y be Point of Y
        holds (I.u).(x,y) = (u.x).y;