:: Dual Spaces and Hahn-Banach's Theorem
::  by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received March 31, 2014
:: Copyright (c) 2014-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 RLSUB_1, HAHNBAN, HAHNBAN1, UNIALG_1, MONOID_0, DUALSP01,
      RLVECT_1, ARYTM_1, RELAT_1, FUNCT_1, RSSPACE, RSSPACE3, VECTSP_1, REAL_1,
      TARSKI, MSSUBFAM, STRUCT_0, REALSET1, SEQ_1, FUNCOP_1, FCONT_1, NORMSP_0,
      SEQ_2, FUNCSDOM, LOPBAN_1, ORDINAL2, ARYTM_3, ALGSTR_0, NORMSP_1,
      FUNCT_2, PRE_TOPC, SUBSET_1, ZFMISC_1, NUMBERS, SEQ_4, XBOOLE_0, CARD_1,
      SUPINF_2, MESFUNC1, COMPLEX1, XXREAL_0, XXREAL_2, NAT_1, REWRITE1,
      VALUED_1, METRIC_1, RELAT_2, ASYMPT_1, FUNCT_7;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
      FUNCT_2, FUNCOP_1, REALSET1, NUMBERS, XCMPLX_0, XXREAL_0, XXREAL_2,
      XREAL_0, NAT_1, COMPLEX1, VALUED_1, SEQ_1, SEQ_2, SEQ_4, STRUCT_0,
      ALGSTR_0, NORMSP_0, NORMSP_1, PRE_TOPC, RLVECT_1, RLSUB_1, VECTSP_1,
      FUNCSDOM, MONOID_0, HAHNBAN, RSSPACE, RSSPACE3, LOPBAN_1, HAHNBAN1;
 constructors REAL_1, REALSET1, RSSPACE3, BINOP_2, RLSUB_1, LOPBAN_2, SEQ_1,
      SEQ_2, SEQ_4, HAHNBAN, HAHNBAN1, MONOID_0, COMSEQ_2;
 registrations STRUCT_0, XREAL_0, ALGSTR_0, NUMBERS, ORDINAL1, MEMBERED,
      RELAT_1, XXREAL_0, VALUED_0, MONOID_0, RLVECT_1, VECTSP_1, FUNCT_2,
      VALUED_1, FUNCOP_1, SEQ_4, HAHNBAN, HAHNBAN1, RELSET_1, FUNCT_1,
      XCMPLX_0, NORMSP_0, NAT_1, NORMSP_1, SEQ_2;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;


begin :: Dual Spaces of Real Linear Spaces

reserve V for non empty RealLinearSpace;

definition
  let X be RealLinearSpace;
  func MultF_Real*(X) -> Function of
     [:the carrier of F_Real,the carrier of X:], the carrier of X equals
:: DUALSP01:def 1
   the Mult of X;
end;

theorem :: DUALSP01:1
  for X be RealLinearSpace holds
    ModuleStr (# the carrier of X, the addF of X, the ZeroF of X,
                 MultF_Real*(X) #)
      is VectSp of F_Real;

definition
  let X be RealLinearSpace;
  func RLSp2RVSp X ->VectSp of F_Real equals
:: DUALSP01:def 2
   ModuleStr (# the carrier of X, the addF of X, the ZeroF of X,
                MultF_Real*(X) #);
end;

definition
  let X be ModuleStr over F_Real;
  func MultReal*(X)
   -> Function of [:REAL,the carrier of X:], the carrier of X equals
:: DUALSP01:def 3
     the lmult of X;
end;

theorem :: DUALSP01:2
  for X be VectSp of F_Real holds
    RLSStruct (# the carrier of X, the ZeroF of X,
                 the addF of X, MultReal*(X) #) is RealLinearSpace;

definition
  let X be VectSp of F_Real;
  func RVSp2RLSp X -> RealLinearSpace equals
:: DUALSP01:def 4
  RLSStruct (# the carrier of X, the ZeroF of X, the addF of X,
               MultReal*(X) #);
end;

theorem :: DUALSP01:3
  for X be RealLinearSpace, v,w be Element of X,
      v1,w1 be Element of RLSp2RVSp X st
   v=v1 & w=w1 holds v+w=v1+w1 & v-w = v1-w1;

theorem :: DUALSP01:4
  for X be VectSp of F_Real, v,w be Element of X,
      v1,w1 be Element of RVSp2RLSp X st
    v=v1 & w=w1 holds v+w = v1+w1 & v-w = v1-w1;

definition
  let V be non empty RealLinearSpace;
  func V*' -> strict non empty RealLinearSpace means
:: DUALSP01:def 5
  ex X be non empty VectSp of F_Real
   st X = RLSp2RVSp V & it= RVSp2RLSp X*';
end;

theorem :: DUALSP01:5
  for x be object holds
    x in the carrier of V*' iff x is linear-Functional of V;

registration
  let V be non empty RealLinearSpace;
  cluster V*' -> constituted-Functions;
end;

definition
  let V be non empty RealLinearSpace;
  let f be Element of V*';
  let v be VECTOR of V;
  redefine func f.v -> Element of REAL;
end;

theorem :: DUALSP01:6
  for V be non empty RealLinearSpace, f,g,h be VECTOR of V*' holds
    h = f+g iff for x be VECTOR of V holds h.x = f.x + g.x;

theorem :: DUALSP01:7
for V be non empty RealLinearSpace, f,h be VECTOR of V*', a be Real
  holds h = a*f iff for x be VECTOR of V holds h.x = a * f.x;

theorem :: DUALSP01:8
for V be non empty RealLinearSpace holds 0.(V*') = (the carrier of V) --> 0;

theorem :: DUALSP01:9
for X be RealLinearSpace holds
 (the carrier of X) --> 0 is linear-Functional of X;

definition
  let X be RealLinearSpace;
  func LinearFunctionals X -> Subset of RealVectSpace(the carrier of X) means
:: DUALSP01:def 6

  for x be object holds x in it iff x is linear-Functional of X;
end;

registration
  let X be RealNormSpace;
  cluster LinearFunctionals X -> non empty;
end;

registration
  let X be RealLinearSpace;
  cluster LinearFunctionals X -> non empty functional;
end;

theorem :: DUALSP01:10
for X be RealLinearSpace holds LinearFunctionals X is linearly-closed;

theorem :: DUALSP01:11
for X be RealLinearSpace holds
  RLSStruct (# LinearFunctionals X,
   Zero_(LinearFunctionals X, RealVectSpace(the carrier of X)),
   Add_(LinearFunctionals X, RealVectSpace(the carrier of X)),
   Mult_(LinearFunctionals X, RealVectSpace(the carrier of X)) #)
    is Subspace of RealVectSpace(the carrier of X);

registration
  let X be RealLinearSpace;
  cluster RLSStruct (# LinearFunctionals X,
    Zero_(LinearFunctionals X, RealVectSpace(the carrier of X)),
    Add_(LinearFunctionals X, RealVectSpace(the carrier of X)),
    Mult_(LinearFunctionals X, RealVectSpace(the carrier of X)) #)
  -> Abelian add-associative right_zeroed right_complementable
     scalar-distributive vector-distributive scalar-associative scalar-unital;
end;

definition
  let X be RealLinearSpace;
  func X*' -> strict RealLinearSpace equals
:: DUALSP01:def 7
  RLSStruct (# LinearFunctionals X,
    Zero_(LinearFunctionals X, RealVectSpace(the carrier of X)),
    Add_(LinearFunctionals X, RealVectSpace(the carrier of X)),
    Mult_(LinearFunctionals X, RealVectSpace(the carrier of X)) #);
end;

registration
  let X be RealLinearSpace;
  cluster X*' -> constituted-Functions;
end;

definition
  let X be RealLinearSpace;
  let f be Element of X*';
  let v be VECTOR of X;
  redefine func f.v -> Element of REAL;
end;

theorem :: DUALSP01:12
for X be RealLinearSpace, f,g,h be VECTOR of X*' holds
  h = f+g iff for x be VECTOR of X holds h.x = f.x + g.x;

theorem :: DUALSP01:13
for X be RealLinearSpace, f,h be VECTOR of X*', a be Real
 holds h = a*f iff for x be VECTOR of X holds h.x = a * f.x;

theorem :: DUALSP01:14
for X be RealLinearSpace holds 0.(X*') = (the carrier of X) --> 0;

begin :: Dual Spaces of Real Normed Spaces

reserve S for Real_Sequence;
reserve k,n,m,m1 for Nat;
reserve g,h,r,x for Real;

definition
  let S be Real_Sequence;
  let x be Real;
  func S - x -> Real_Sequence means
:: DUALSP01:def 8
  for n holds it.n = S.n - x;
end;

theorem :: DUALSP01:15
  S is convergent implies S - x is convergent & lim (S-x) = (lim S) - x;

definition
  let X be RealNormSpace;
  let IT be Functional of X;
  attr IT is Lipschitzian means
:: DUALSP01:def 9
  ex K be Real st 0 <= K &
   for x be VECTOR of X holds |. IT.x .| <= K * ||. x .||;
end;

theorem :: DUALSP01:16
  for X be RealNormSpace, f be Functional of X st
    (for x be VECTOR of X holds f.x=0) holds f is Lipschitzian;

registration
  let X be RealNormSpace;
  cluster Lipschitzian for linear-Functional of X;
end;

definition
  let X be RealNormSpace;
  func BoundedLinearFunctionals X -> Subset of X*' means
:: DUALSP01:def 10
  for x be set holds x in it
              iff x is Lipschitzian linear-Functional of X;
end;

registration
  let X be RealNormSpace;
  cluster BoundedLinearFunctionals X -> non empty;
end;

theorem :: DUALSP01:17
  for X be RealNormSpace holds BoundedLinearFunctionals X is linearly-closed;

theorem :: DUALSP01:18
for X be RealNormSpace holds
 RLSStruct (# BoundedLinearFunctionals X,
              Zero_(BoundedLinearFunctionals X, X*'),
              Add_(BoundedLinearFunctionals X, X*'),
              Mult_(BoundedLinearFunctionals X, X*') #) is Subspace of X*';

registration
  let X be RealNormSpace;
  cluster RLSStruct (# BoundedLinearFunctionals X,
                       Zero_(BoundedLinearFunctionals X, X*'),
                       Add_(BoundedLinearFunctionals X, X*'),
                       Mult_(BoundedLinearFunctionals X, X*') #)
             -> Abelian add-associative right_zeroed right_complementable
                vector-distributive scalar-distributive scalar-associative
                scalar-unital;
end;

definition
  let X be RealNormSpace;
  func R_VectorSpace_of_BoundedLinearFunctionals X ->
    strict RealLinearSpace equals
:: DUALSP01:def 11
  RLSStruct (# BoundedLinearFunctionals X,
               Zero_(BoundedLinearFunctionals X, X*'),
               Add_(BoundedLinearFunctionals X, X*'),
               Mult_(BoundedLinearFunctionals X, X*') #);
end;

registration
  let X be RealNormSpace;
  cluster -> Function-like Relation-like for Element of
    R_VectorSpace_of_BoundedLinearFunctionals X;
end;

definition
  let X be RealNormSpace;
  let f be Element of R_VectorSpace_of_BoundedLinearFunctionals X;
  let v be VECTOR of X;
  redefine func f.v -> Element of REAL;
end;

theorem :: DUALSP01:19
for X be RealNormSpace,
    f,g,h be VECTOR of R_VectorSpace_of_BoundedLinearFunctionals X
 holds h = f+g iff for x be VECTOR of X holds h.x = f.x + g.x;

theorem :: DUALSP01:20
  for X be RealNormSpace,
      f,h be VECTOR of R_VectorSpace_of_BoundedLinearFunctionals X,
      a be Real
   holds h = a*f iff for x be VECTOR of X holds h.x = a * f.x;

theorem :: DUALSP01:21
  for X be RealNormSpace holds
   0.(R_VectorSpace_of_BoundedLinearFunctionals X) = (the carrier of X) --> 0;

definition
  let X be RealNormSpace;
  let f be object;
  func Bound2Lipschitz(f,X) -> Lipschitzian linear-Functional of X equals
:: DUALSP01:def 12
  In(f,BoundedLinearFunctionals X);
end;

definition
  let X be RealNormSpace;
  let u be linear-Functional of X;
  func PreNorms u -> non empty Subset of REAL equals
:: DUALSP01:def 13
  {|.u.t.| where t is VECTOR of X : ||.t.|| <= 1 };
end;

registration let X be RealNormSpace,
                 g be Lipschitzian linear-Functional of X;
  cluster PreNorms g -> bounded_above;
end;

theorem :: DUALSP01:22
  for X be RealNormSpace, g be linear-Functional of X
    holds g is Lipschitzian iff PreNorms g is bounded_above;

definition
  let X be RealNormSpace;
  func BoundedLinearFunctionalsNorm X
  -> Function of BoundedLinearFunctionals X,REAL means
:: DUALSP01:def 14
  for x be object st x in BoundedLinearFunctionals X holds
     it.x = upper_bound PreNorms(Bound2Lipschitz(x,X));
end;

theorem :: DUALSP01:23
  for X be RealNormSpace, f be Lipschitzian linear-Functional of X
    holds Bound2Lipschitz(f,X)=f;

theorem :: DUALSP01:24
  for X be RealNormSpace, f be Lipschitzian linear-Functional of X
    holds (BoundedLinearFunctionalsNorm X).f = upper_bound PreNorms f;

definition
  let X be RealNormSpace;
  func DualSp X -> non empty NORMSTR equals
:: DUALSP01:def 15
       NORMSTR (# BoundedLinearFunctionals X,
                  Zero_(BoundedLinearFunctionals X, X*'),
                  Add_(BoundedLinearFunctionals X, X*'),
                  Mult_(BoundedLinearFunctionals X, X*'),
                  BoundedLinearFunctionalsNorm X #);
end;

theorem :: DUALSP01:25
  for X be RealNormSpace holds (the carrier of X) --> 0 = 0.(DualSp X);

theorem :: DUALSP01:26
  for X be RealNormSpace, f be Point of DualSp X,
      g be Lipschitzian linear-Functional of X
   st g=f holds for t be VECTOR of X holds |.g.t.| <= ||.f.|| * ||.t.||;

theorem :: DUALSP01:27
  for X be RealNormSpace, f be Point of DualSp X holds 0 <= ||.f.||;

theorem :: DUALSP01:28
  for X, Y be RealNormSpace for f be Point of DualSp X
    st f = 0.(DualSp X) holds 0 = ||.f.||;

registration
  let X be RealNormSpace;
  cluster -> Function-like Relation-like for Element of DualSp X;
end;

definition
  let X be RealNormSpace;
  let f be Element of DualSp X;
  let v be VECTOR of X;
  redefine func f.v -> Element of REAL;
end;

theorem :: DUALSP01:29
  for X be RealNormSpace, f,g,h be Point of DualSp X
    holds h = f+g iff for x be VECTOR of X holds h.x = f.x + g.x;

theorem :: DUALSP01:30
  for X be RealNormSpace, f,h be Point of DualSp X, a be Real
    holds h = a*f iff for x be VECTOR of X holds h.x = a * f.x;

theorem :: DUALSP01:31
  for X be RealNormSpace, f,g be Point of DualSp X, a be Real holds
  ( ||.f.|| = 0 iff f = 0.(DualSp X) ) &
  ||.a*f.|| = |.a.| * ||.f.|| & ||.f+g.|| <= ||.f.|| + ||.g.||;

registration
  let X be RealNormSpace;
  cluster DualSp X -> reflexive discerning RealNormSpace-like;
end;

theorem :: DUALSP01:32
  for X be RealNormSpace holds DualSp X is RealNormSpace;

registration
  let X be RealNormSpace;
  cluster DualSp X -> reflexive discerning RealNormSpace-like
   vector-distributive scalar-distributive scalar-associative scalar-unital
   Abelian add-associative right_zeroed right_complementable;
end;

theorem :: DUALSP01:33
  for X be RealNormSpace, f,g,h be Point of DualSp X
    holds h = f-g iff for x be VECTOR of X holds h.x = f.x - g.x;

definition let X be RealNormSpace;
  let s be sequence of DualSp X, n be Nat;
  redefine func s.n -> Element of DualSp X;
end;

theorem :: DUALSP01:34
  for X be RealNormSpace, seq be sequence of DualSp X
    st seq is Cauchy_sequence_by_Norm holds seq is convergent;

theorem :: DUALSP01:35
  for X be RealNormSpace holds DualSp X is RealBanachSpace;

registration
  let X be RealNormSpace;
  cluster DualSp X -> complete;
end;

begin :: Hahn-Banach's Extension Theorem

definition
  let V be RealNormSpace;
  mode SubRealNormSpace of V -> RealNormSpace means
:: DUALSP01:def 16
    the carrier of it c= the carrier of V
     & 0.it = 0.V
     & the addF of it = (the addF of V)||the carrier of it
     & the Mult of it = (the Mult of V) | [:REAL, the carrier of it:]
     & the normF of it = (the normF of V) | (the carrier of it);
end;

theorem :: DUALSP01:36
for V be RealNormSpace, X be SubRealNormSpace of V,
    f be Lipschitzian linear-Functional of X,
    F be Point of DualSp X
 st f = F holds
  ex g be Lipschitzian linear-Functional of V, G be Point of DualSp V
    st g = G & g|(the carrier of X) = f & ||.G.||=||.F.||;

::$N Hahn-Banach's extension theorem (real normed spaces)
theorem :: DUALSP01:37
for V be RealNormSpace, X be SubRealNormSpace of V,
    f be Lipschitzian linear-Functional of X,
    F be Point of DualSp X
  st ( f = F & for x be VECTOR of X, v be VECTOR of V
                  st x=v holds f.x <= ||.v.|| )
holds
  ex g be Lipschitzian linear-Functional of V, G be Point of DualSp V
   st g = G & g|(the carrier of X) = f
    & for x be VECTOR of V holds g.x <= ||.x.|| & ||.G.||=||.F.||;