:: Dual Spaces and Hahn-Banach's Theorem
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received March 31, 2014
:: Copyright (c) 2014-2016 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, 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.||;