:: Dual Spaces and Hahn-Banach's Theorem
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received March 31, 2014
:: Copyright (c) 2014-2026 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;
definitions ALGSTR_0, FUNCT_1, RLVECT_1, VECTSP_1, HAHNBAN, HAHNBAN1,
XXREAL_2;
equalities XBOOLE_0, BINOP_1, RLVECT_1, STRUCT_0, REALSET1, ALGSTR_0,
NORMSP_0, SEQ_1, VECTSP_1, FUNCSDOM;
expansions FUNCT_1, RLSUB_1, TARSKI, XBOOLE_0, FUNCT_2, SEQ_2, NORMSP_0,
NORMSP_1, VECTSP_1, RLVECT_1, ALGSTR_0;
theorems SEQ_4, FUNCT_1, SEQ_1, SEQ_2, ABSVALUE, ALGSTR_0, COMPLEX1, TARSKI,
RSSPACE3, XREAL_0, XXREAL_0, FUNCSDOM, NORMSP_1, LOPBAN_1, FUNCT_2,
XBOOLE_0, XREAL_1, XCMPLX_0, RLVECT_1, FUNCOP_1, VECTSP_1, HAHNBAN,
HAHNBAN1, RLSUB_1, RSSPACE, MONOID_0, NORMSP_0, ORDINAL1, NAT_1,
SUBSET_1;
schemes SEQ_1, FUNCT_2, XBOOLE_0;
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
the Mult of X;
correctness;
end;
theorem Lm01:
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
proof
let X be RealLinearSpace;
set XP=ModuleStr (# the carrier of X, the addF of X, the ZeroF of X,
MultF_Real*(X) #);
Q1:XP is scalar-distributive vector-distributive
scalar-associative scalar-unital
proof
now let x,y be Element of F_Real;
let v be Element of XP;
reconsider v1=v as Element of X;
reconsider x1=x,y1=y as Real;
(x+y)*v = (x1+y1)*v1
= x1*v1+y1*v1 by RLVECT_1:def 6;
hence (x+y)*v = x*v+y*v;
end;
hence XP is scalar-distributive;
now let x be Element of F_Real;
let v,w be Element of XP;
reconsider v1=v,w1=w as Element of X;
reconsider x1=x as Real;
x*(v+w) = x1*(v1+w1)
.= x1*v1+x1*w1 by RLVECT_1:def 5;
hence x*(v+w) = x*v+x*w;
end;
hence XP is vector-distributive;
now let x,y be Element of F_Real;
let v be Element of XP;
reconsider v1=v as Element of X;
reconsider x1=x,y1=y as Real;
(x*y)*v = (x1*y1)*v1
.= x1*(y1*v1) by RLVECT_1:def 7;
hence (x*y)*v = x*(y*v);
end;
hence XP is scalar-associative;
now let v be Element of XP;
reconsider v1=v as Element of X;
(1.F_Real)*v = 1*v1;
hence (1.F_Real)*v = v by RLVECT_1:def 8;
end;
hence XP is scalar-unital;
end;
now let u,v,w be Element of XP;
reconsider u1=u,v1=v,w1=w as Element of X;
u+(v + w) = u1+(v1+w1)
.= (u1+v1)+w1 by RLVECT_1:def 3;
hence u+(v + w) = (u+v)+w;
end; then
Q2: XP is add-associative;
now let v be Element of XP;
reconsider v1=v as Element of X;
v + 0.XP = v1+0.X;
hence v + 0.XP = v;
end; then
Q3: XP is right_zeroed;
now let v be Element of XP;
reconsider v1=v as Element of X;
consider w1 be Element of X such that
A1: v1+w1= 0.X by ALGSTR_0:def 11;
reconsider w=w1 as Element of XP;
v + w = 0.XP by A1;
hence v is right_complementable;
end;
then
Q4: XP is right_complementable;
now let v,w be Element of XP;
reconsider v1=v,w1=w as Element of X;
v + w = v1+w1 .= w1+v1;
hence v + w = w+v;
end;
then XP is Abelian;
hence XP is VectSp of F_Real by Q1,Q2,Q3,Q4;
end;
definition
let X be RealLinearSpace;
func RLSp2RVSp X ->VectSp of F_Real equals
ModuleStr (# the carrier of X, the addF of X, the ZeroF of X,
MultF_Real*(X) #);
correctness by Lm01;
end;
definition
let X be ModuleStr over F_Real;
func MultReal*(X)
-> Function of [:REAL,the carrier of X:], the carrier of X equals
the lmult of X;
correctness;
end;
theorem Lm02:
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
proof
let X be VectSp of F_Real;
set XQ=RLSStruct (# the carrier of X, the ZeroF of X,
the addF of X, MultReal*(X) #);
A1: for vZ1,wZ1 be Element of X, v,w be Element of XQ
st v = vZ1 & w = wZ1 holds v + w = vZ1 + wZ1;
XQ is Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital
proof
hereby let v,w be VECTOR of XQ;
reconsider vZ1 = v, wZ1 = w as Element of X;
thus v + w = wZ1 + vZ1 by A1
.= w + v;
end;
hereby let u,v,w be VECTOR of XQ;
reconsider uZ1 = u, vZ1 = v, wZ1 = w as Element of X;
(u + v) + w = (uZ1 + vZ1) + wZ1
.= uZ1 + (vZ1 + wZ1) by RLVECT_1:def 3;
hence (u + v) + w = u + (v + w);
end;
hereby let v be VECTOR of XQ;
reconsider vZ1 = v as Element of X;
thus v + 0.XQ = vZ1 + 0.X .= v;
end;
thus XQ is right_complementable
proof
let v be VECTOR of XQ;
reconsider vZ1 = v as Element of X;
consider wZ1 be Element of X such that
A2: vZ1 + wZ1 = 0.X by ALGSTR_0:def 11;
reconsider w = wZ1 as VECTOR of XQ;
take w;
thus v + w = 0.XQ by A2;
end;
hereby let a,b be Real, v be VECTOR of XQ;
reconsider vZ1=v as Element of X;
reconsider aZ1=a, bZ1=b as Element of F_Real by XREAL_0:def 1;
(a + b) * v = (aZ1 + bZ1) * vZ1
.= aZ1* vZ1 + bZ1* vZ1 by VECTSP_1:def 15;
hence (a + b) * v = a * v + b * v;
end;
hereby let a be Real, v,w be VECTOR of XQ;
reconsider aZ1=a as Element of F_Real by XREAL_0:def 1;
reconsider vZ1 = v, wZ1 = w as Element of X;
a * (v + w) = aZ1*(vZ1+wZ1)
.= aZ1*vZ1 + aZ1*wZ1 by VECTSP_1:def 14;
hence a * (v + w) =a*v + a*w;
end;
hereby let a,b be Real, v be VECTOR of XQ;
reconsider vZ1=v as Element of X;
reconsider aZ1=a, bZ1=b as Element of F_Real by XREAL_0:def 1;
(a * b) * v = (aZ1 * bZ1) * vZ1
.= aZ1 * (bZ1 * vZ1) by VECTSP_1:def 16;
hence (a * b) * v = a * (b * v);
end;
let v be VECTOR of XQ;
reconsider vZ1=v as Element of X;
thus 1 * v = 1.(F_Real) *vZ1
.= v;
end;
hence thesis;
end;
definition
let X be VectSp of F_Real;
func RVSp2RLSp X -> RealLinearSpace equals
RLSStruct (# the carrier of X, the ZeroF of X, the addF of X,
MultReal*(X) #);
correctness by Lm02;
end;
theorem
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
proof
let X be RealLinearSpace, v,w be Element of X,
v1,w1 be Element of RLSp2RVSp X;
assume AS: v=v1 & w=w1;
hence v+w=v1+w1;
-w = (-1)*w by RLVECT_1:16
.= (-1.F_Real)*w1 by AS
.= -w1 by VECTSP_1:14;
hence v-w = v1-w1 by AS;
end;
theorem
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
proof
let X be VectSp of F_Real, v,w be Element of X,
v1,w1 be Element of RVSp2RLSp X;
assume AS: v=v1 & w=w1;
-w1 = (-1)*w1 by RLVECT_1:16
.= (-1.F_Real)*w by AS
.= -w by VECTSP_1:14;
hence v+w = v1+w1 & v-w = v1-w1 by AS;
end;
definition
let V be non empty RealLinearSpace;
func V*' -> strict non empty RealLinearSpace means :def2:
ex X be non empty VectSp of F_Real
st X = RLSp2RVSp V & it= RVSp2RLSp X*';
correctness
proof
reconsider X = RLSp2RVSp V as non empty VectSp of F_Real;
RVSp2RLSp X*' is non empty RealLinearSpace;
hence thesis;
end;
end;
theorem Th1:
for x be object holds
x in the carrier of V*' iff x is linear-Functional of V
proof
let x be object;
consider X be non empty VectSp of F_Real such that
AS1:X = RLSp2RVSp V & V*'= RVSp2RLSp X*' by def2;
x is linear-Functional of X iff x is linear-Functional of V
proof
hereby assume A21: x is linear-Functional of X;
then
reconsider f=x as Functional of V by AS1;
reconsider g=x as linear-Functional of X by A21;
A1: f is additive
proof
let v,w be Element of V;
reconsider v1=v,w1=w as Element of X by AS1;
f.(v+w) = g.(v1+w1) by AS1
.= g.v1 + g.w1 by VECTSP_1:def 20;
hence f.(v+w) = f.v+f.w;
end;
f is homogeneous
proof
let v be VECTOR of V, r be Real;
reconsider v1=v as Element of X by AS1;
reconsider r1 =r as Scalar of X by XREAL_0:def 1;
f.(r*v) = g.(r1*v1) by AS1
.= r1*g.v1 by HAHNBAN1:def 8;
hence f.(r*v) = r*f.v;
end;
hence x is linear-Functional of V by A1;
end;
assume
A21: x is linear-Functional of V; then
reconsider f=x as Functional of X by AS1;
reconsider g = x as linear-Functional of V by A21;
A1:f is additive
proof
let v,w be Element of X;
reconsider v1=v,w1=w as VECTOR of V by AS1;
f.(v+w) = g.(v1+w1) by AS1;
hence f.(v+w) = f.v+f.w by HAHNBAN:def 2;
end;
f is homogeneous
proof
let v be Element of X, r be Element of F_Real;
reconsider v1=v as Element of V by AS1;
reconsider r1=r as Element of REAL;
f.(r*v) = g.(r1*v1) by AS1;
hence f.(r*v) = r*f.v by HAHNBAN:def 3;
end;
hence x is linear-Functional of X by A1;
end;
hence thesis by AS1,HAHNBAN1:def 10;
end;
registration
let V be non empty RealLinearSpace;
cluster V*' -> constituted-Functions;
coherence
proof
the carrier of V*' is functional by Th1;
hence thesis by MONOID_0:80;
end;
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; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider f as Functional of V by Th1;
f.v is Element of REAL;
hence thesis;
end;
end;
theorem
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
proof
let V be non empty RealLinearSpace;
let f,g,h be VECTOR of V*';
consider Y be non empty VectSp of F_Real such that
AS1:Y = RLSp2RVSp V & V*'= RVSp2RLSp Y*' by def2;
reconsider f1=f, g1=g, h1=h as linear-Functional of Y by AS1,HAHNBAN1:def 10;
A2:now assume A3: h = f+g;
let x be Element of V;
reconsider x1=x as Element of Y by AS1;
h1 = f1+g1 by A3,AS1,HAHNBAN1:def 10;
then h1.x1=f1.x1+g1.x1 by HAHNBAN1:def 3;
hence h.x=f.x+g.x;
end;
now
assume for x be Element of V holds h.x=f.x+g.x;
then
for x be Element of Y holds h1.x=f1.x+g1.x by AS1;
then
h1 = f1+g1 by HAHNBAN1:def 3;
hence h=f+g by AS1,HAHNBAN1:def 10;
end;
hence thesis by A2;
end;
theorem
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
proof
let V be non empty RealLinearSpace, f,h be VECTOR of V*', a be Real;
reconsider a1=a as Element of F_Real by XREAL_0:def 1;
consider Y be non empty VectSp of F_Real such that
AS1:Y = RLSp2RVSp V & V*'= RVSp2RLSp Y*' by def2;
reconsider f1=f, h1=h as linear-Functional of Y by AS1,HAHNBAN1:def 10;
hereby assume A3: h = a*f;
hereby let x be Element of V;
reconsider x1=x as Element of Y by AS1;
h1 = a1*f1 by A3,AS1,HAHNBAN1:def 10;
then h1.x1=a1*f1.x1 by HAHNBAN1:def 6;
hence h.x=a*f.x;
end;
end;
assume for x be Element of V holds h.x=a*f.x;
then
for x be Element of Y holds h1.x=a1*f1.x by AS1;
then
h1 = a1*f1 by HAHNBAN1:def 6;
hence h=a*f by AS1,HAHNBAN1:def 10;
end;
theorem
for V be non empty RealLinearSpace holds 0.(V*') = (the carrier of V) --> 0
proof
let V be non empty RealLinearSpace;
consider Y be non empty VectSp of F_Real such that
AS1:Y = RLSp2RVSp V & V*'= RVSp2RLSp Y*' by def2;
0.(V*') = 0.(Y*') by AS1
.= 0Functional Y by HAHNBAN1:def 10
.= ([#]Y --> 0.(F_Real)) by HAHNBAN1:def 7;
hence 0.(V*') = ((the carrier of V) --> 0) by AS1;
end;
theorem Th23:
for X be RealLinearSpace holds
(the carrier of X) --> 0 is linear-Functional of X
proof
let X be RealLinearSpace;
set f=(the carrier of X) --> 0;
reconsider f as Functional of X by FUNCOP_1:45,XREAL_0:def 1;
A1: f is additive
proof
let x,y be VECTOR of X;
thus f.(x+y) = f.x+f.y;
end;
f is homogeneous
proof
let x be VECTOR of X, r be Real;
thus f.(r*x) = r*f.x;
end;
hence thesis by A1;
end;
definition
let X be RealLinearSpace;
func LinearFunctionals X -> Subset of RealVectSpace(the carrier of X) means
:Def7:
for x be object holds x in it iff x is linear-Functional of X;
existence
proof
defpred P[object] means $1 is linear-Functional of X;
consider IT be set such that
A1: for x be object holds x in IT
iff x in Funcs(the carrier of X,REAL) & P[x] from XBOOLE_0:sch 1;
for x be object st x in IT holds x in Funcs(the carrier of X,REAL) by A1;
then
reconsider IT as Subset of RealVectSpace(the carrier of X) by TARSKI:def 3;
take IT;
let x be object;
thus x in IT implies x is linear-Functional of X by A1;
assume
A3: x is linear-Functional of X;
then x in Funcs(the carrier of X,REAL) by FUNCT_2:8;
hence thesis by A1,A3;
end;
uniqueness
proof
let X1,X2 be Subset of RealVectSpace(the carrier of X);
assume that
A4: for x be object holds x in X1 iff x is linear-Functional of X and
A5: for x be object holds x in X2 iff x is linear-Functional of X;
now let x be object;
assume x in X1;
then x is linear-Functional of X by A4;
hence x in X2 by A5;
end;
then
A6: X1 c= X2;
now let x be object;
assume x in X2;
then x is linear-Functional of X by A5;
hence x in X1 by A4;
end;
then X2 c= X1;
hence thesis by A6;
end;
end;
registration
let X be RealNormSpace;
cluster LinearFunctionals X -> non empty;
coherence
proof
(the carrier of X) --> 0 is linear-Functional of X by Th23;
hence thesis by Def7;
end;
end;
registration
let X be RealLinearSpace;
cluster LinearFunctionals X -> non empty functional;
coherence
proof
(the carrier of X) --> 0 is linear-Functional of X by Th23;
hence LinearFunctionals X is non empty by Def7;
let x be object;
assume x in LinearFunctionals X;
hence thesis;
end;
end;
theorem Th17:
for X be RealLinearSpace holds LinearFunctionals X is linearly-closed
proof
let X be RealLinearSpace;
set W = LinearFunctionals X;
A1: for v,u be VECTOR of RealVectSpace(the carrier of X) st
v in LinearFunctionals X & u in LinearFunctionals X
holds v + u in LinearFunctionals X
proof
let v,u be VECTOR of RealVectSpace(the carrier of X) such that
A2: v in W & u in W;
reconsider f=v+u as Functional of X by FUNCT_2:66;
A3: f is additive
proof
let x,y be VECTOR of X;
reconsider vZ1=v, uZ1=u as Element of Funcs(the carrier of X,REAL);
A4: uZ1 is linear-Functional of X by A2,Def7;
reconsider uZ11=uZ1 as additive homogeneous Functional of X by A2,Def7;
reconsider x1=x, y1=y as Element of X;
A5: vZ1 is linear-Functional of X by A2,Def7;
f.(x+y) = uZ1.(x+y)+vZ1.(x+y) by FUNCSDOM:1
.= (uZ1.x+uZ1.y)+vZ1.(x+y) by A4,HAHNBAN:def 2
.= uZ1.x+uZ1.y+(vZ1.x+vZ1.y) by A5,HAHNBAN:def 2
.= uZ1.x+vZ1.x+uZ1.y+vZ1.y
.= f.x+ uZ1.y+vZ1.y by FUNCSDOM:1
.= f.x+ (uZ1.y+vZ1.y);
hence f.(x+y) = f.x+f.y by FUNCSDOM:1;
end;
f is homogeneous
proof
let x be VECTOR of X, s be Real;
reconsider v1 = v, u1 = u as Element of Funcs(the carrier of X,REAL);
A6: u1 is linear-Functional of X & v1 is linear-Functional of X by A2,Def7;
f.(s*x) = u1.(s*x)+v1.(s*x) by FUNCSDOM:1
.= (s*(u1.x))+v1.(s*x) by A6,HAHNBAN:def 3
.= s*u1.x+s*v1.x by A6,HAHNBAN:def 3
.= s*(u1.x+v1.x);
hence f.(s*x) = s*f.x by FUNCSDOM:1;
end;
hence v+u in W by A3,Def7;
end;
for a be Real, v be VECTOR of RealVectSpace(the carrier of X)
st v in W holds a * v in W
proof
let a be Real;
let v be VECTOR of RealVectSpace(the carrier of X) such that
A8: v in W;
reconsider f=a*v as Functional of X by FUNCT_2:66;
A9: f is additive
proof
let x,y be VECTOR of X;
reconsider vZ1=v as Element of Funcs(the carrier of X,REAL);
A10: vZ1 is linear-Functional of X by Def7,A8;
f.(x+y) = a*(vZ1.(x+y)) by FUNCSDOM:4
.= a*(vZ1.x+vZ1.y) by A10,HAHNBAN:def 2
.= a*vZ1.x+a*vZ1.y
.= f.x+a*vZ1.y by FUNCSDOM:4;
hence f.(x+y) = f.x+ f.y by FUNCSDOM:4;
end;
f is homogeneous
proof
let x be VECTOR of X, s be Real;
reconsider vZ1=v as Element of Funcs(the carrier of X,REAL);
A11: vZ1 is linear-Functional of X by Def7,A8;
f.(s*x) = a*vZ1.(s*x) by FUNCSDOM:4
.= a*(s*(vZ1.x)) by A11,HAHNBAN:def 3
.= s*(a*vZ1.x);
hence f.(s*x) = s*f.x by FUNCSDOM:4;
end;
hence thesis by A9,Def7;
end;
hence thesis by A1;
end;
theorem
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) by Th17,RSSPACE:11;
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;
coherence by Th17,RSSPACE:11;
end;
definition
let X be RealLinearSpace;
func X*' -> strict RealLinearSpace equals
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)) #);
coherence;
end;
registration
let X be RealLinearSpace;
cluster X*' -> constituted-Functions;
coherence by MONOID_0:80;
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; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider f as Functional of X by Def7;
f.v is Element of REAL;
hence thesis;
end;
end;
theorem Th20b:
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
proof
let X be RealLinearSpace, f,g,h be VECTOR of X*';
A1:X*' is Subspace of RealVectSpace(the carrier of X) by Th17,RSSPACE:11;
then reconsider f1=f, g1=g, h1=h as VECTOR
of RealVectSpace(the carrier of X) by RLSUB_1:10;
hereby assume
A3: h = f+g;
let x be Element of X;
h1=f1+g1 by A1,A3,RLSUB_1:13;
hence h.x=f.x+g.x by FUNCSDOM:1;
end;
assume for x be Element of X holds h.x=f.x+g.x;
then h1=f1+g1 by FUNCSDOM:1;
hence h =f+g by A1,RLSUB_1:13;
end;
theorem Th21b:
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
proof
let X be RealLinearSpace;
let f,h be VECTOR of X*';
let a be Real;
A1: X*' is Subspace of RealVectSpace(the carrier of X) by Th17,RSSPACE:11;
then reconsider f1=f, h1=h as VECTOR
of RealVectSpace(the carrier of X) by RLSUB_1:10;
hereby assume
A3: h = a*f;
let x be Element of X;
h1=a*f1 by A1,A3,RLSUB_1:14;
hence h.x = a*f.x by FUNCSDOM:4;
end;
assume for x be Element of X holds h.x=a*f.x;
then h1 = a*f1 by FUNCSDOM:4;
hence h = a*f by A1,RLSUB_1:14;
end;
theorem Th22b:
for X be RealLinearSpace holds 0.(X*') = (the carrier of X) --> 0
proof
let X be RealLinearSpace;
A1: X*' is Subspace of RealVectSpace(the carrier of X) by Th17,RSSPACE:11;
0.(RealVectSpace(the carrier of X )) = (the carrier of X) --> 0;
hence thesis by A1,RLSUB_1:11;
end;
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 :Def14:
for n holds it.n = S.n - x;
existence
proof
deffunc F(Nat) = S.$1 - x;
consider S be Real_Sequence such that
A1: for n be Nat holds S.n = F(n) from SEQ_1:sch 1;
take S;
let n;
thus thesis by A1;
end;
uniqueness
proof
let S1,S2 be Real_Sequence;
assume that
A2: for n holds S1.n = S.n - x and
A3: for n holds S2.n = S.n - x;
for n be Nat holds S1.n = S2.n
proof
let n be Nat;
S1.n = S.n - x by A2;
hence thesis by A3;
end;
hence thesis;
end;
end;
theorem Th121:
S is convergent implies S - x is convergent & lim (S-x) = (lim S) - x
proof
assume B1: S is convergent;
set g = lim S;
set h = g - x;
X1: now let r;
assume 0 < r;
then consider m1 such that
A2: for n st m1 <= n holds |.(S.n) - g.| < r by B1,SEQ_2:def 7;
take k = m1;
let n;
assume B3: k <= n;
|.(S.n) - g.| = |.((S.n) - x) - h.|
.= |.(S - x).n - h.| by Def14;
hence |.(S - x).n - h.| < r by A2,B3;
end;
hence S - x is convergent;
hence lim (S-x) = (lim S) - x by X1,SEQ_2:def 7;
end;
definition
let X be RealNormSpace;
let IT be Functional of X;
attr IT is Lipschitzian means :Def8:
ex K be Real st 0 <= K &
for x be VECTOR of X holds |. IT.x .| <= K * ||. x .||;
end;
theorem Th21:
for X be RealNormSpace, f be Functional of X st
(for x be VECTOR of X holds f.x=0) holds f is Lipschitzian
proof
let X be RealNormSpace;
let f be Functional of X;
assume
A1: for x be VECTOR of X holds f.x=0;
take 0;
thus thesis by A1,COMPLEX1:44;
end;
Th21X:
for X be RealNormSpace, F be Functional of X
st F = (the carrier of X) --> 0
holds F is linear-Functional of X & F is Lipschitzian
proof
let X be RealNormSpace,
F be Functional of X;
assume A1: F = (the carrier of X) --> 0; then
reconsider F as linear-Functional of X by Th23;
for x be VECTOR of X holds F.x =0 by A1;
hence thesis by Th21;
end;
registration
let X be RealNormSpace;
cluster Lipschitzian for linear-Functional of X;
existence
proof
set f=(the carrier of X) --> 0;
reconsider f as Function of the carrier of X,REAL
by FUNCOP_1:45,XREAL_0:def 1;
reconsider f as Functional of X;
reconsider f as linear-Functional of X by Th21X;
f is Lipschitzian by Th21X;
hence thesis;
end;
end;
definition
let X be RealNormSpace;
func BoundedLinearFunctionals X -> Subset of X*' means :Def9:
for x be set holds x in it
iff x is Lipschitzian linear-Functional of X;
existence
proof
defpred P[object] means $1 is
Lipschitzian linear-Functional of X;
consider IT be set such that
A1: for x be object holds x in IT
iff x in LinearFunctionals X & P[x] from XBOOLE_0:sch 1;
take IT;
for x be object st x in IT holds x in LinearFunctionals X by A1;
hence IT is Subset of X*' by TARSKI:def 3;
let x be set;
thus x in IT implies x is Lipschitzian linear-Functional of X by A1;
assume
A2: x is Lipschitzian linear-Functional of X;
then x in LinearFunctionals X by Def7;
hence thesis by A1,A2;
end;
uniqueness
proof
let X1,X2 be Subset of X*';
assume that
A3: for x be set holds x in X1 iff
x is Lipschitzian linear-Functional of X and
A4: for x be set holds x in X2 iff
x is Lipschitzian linear-Functional of X;
now let x be object;
assume x in X2;
then x is Lipschitzian linear-Functional of X by A4;
hence x in X1 by A3;
end;
then
A5: X2 c= X1;
now let x be object;
assume x in X1;
then x is Lipschitzian linear-Functional of X by A3;
hence x in X2 by A4;
end;
then X1 c= X2;
hence thesis by A5;
end;
end;
registration
let X be RealNormSpace;
cluster BoundedLinearFunctionals X -> non empty;
coherence
proof
set f = the Lipschitzian linear-Functional of X;
f in BoundedLinearFunctionals X by Def9;
hence thesis;
end;
end;
theorem Th22:
for X be RealNormSpace holds BoundedLinearFunctionals X is linearly-closed
proof
let X be RealNormSpace;
set W = BoundedLinearFunctionals X;
A1: for v,u be VECTOR of X*' st v in W & u in W holds v + u in W
proof
let v,u be VECTOR of X*' such that
A2: v in W & u in W;
reconsider f=v+u as linear-Functional of X by Def7;
f is Lipschitzian
proof
reconsider v1=v, u1=u as Lipschitzian Functional of X by A2,Def9;
consider K2 be Real such that
A4: 0 <= K2 and
A5: for x be VECTOR of X holds |. v1.x .| <= K2*||. x .|| by Def8;
consider K1 be Real such that
A6: 0 <= K1 and
A7: for x be VECTOR of X holds |. u1.x .| <= K1*||. x .|| by Def8;
take K3=K1+K2;
now
let x be VECTOR of X;
A8: |. u1.x+v1.x .| <= |. u1.x .|+ |. v1.x .| by COMPLEX1:56;
A9: |. v1.x .| <= K2*||. x .|| by A5;
|. u1.x .| <= K1*||. x .|| by A7;
then
A10: |. u1.x .| + |. v1.x .| <= K1*||. x .|| +K2*||. x .||
by A9,XREAL_1:7;
|. f.x .| =|. u1.x+v1.x .| by Th20b;
hence |. f.x .| <= K3*||. x .|| by A8,A10,XXREAL_0:2;
end;
hence thesis by A6,A4;
end;
hence thesis by Def9;
end;
for a be Real, v be VECTOR of X*' st v in W holds a * v in W
proof
let a be Real;
let v be VECTOR of X*' such that
A11: v in W;
reconsider f=a*v as linear-Functional of X by Def7;
f is Lipschitzian
proof
reconsider v1=v as Lipschitzian Functional of X by A11,Def9;
consider K be Real such that
A12: 0 <= K and
A13: for x be VECTOR of X holds |. v1.x .| <= K*||. x .|| by Def8;
take |.a.|*K;
A14: now
let x be VECTOR of X;
0 <=|.a.| by COMPLEX1:46; then
A15: |.a.|* |. v1.x .| <= |.a.|* (K*||. x .||) by A13,XREAL_1:64;
|. a*v1.x .| = |.a.|* |. v1.x .| by COMPLEX1:65;
hence |. f.x .| <= |.a.|* K*||. x .|| by A15,Th21b;
end;
0 <=|.a.| by COMPLEX1:46;
hence thesis by A12,A14;
end;
hence thesis by Def9;
end;
hence thesis by A1;
end;
theorem
for X be RealNormSpace holds
RLSStruct (# BoundedLinearFunctionals X,
Zero_(BoundedLinearFunctionals X, X*'),
Add_(BoundedLinearFunctionals X, X*'),
Mult_(BoundedLinearFunctionals X, X*') #) is Subspace of X*'
by Th22,RSSPACE:11;
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;
coherence by Th22,RSSPACE:11;
end;
definition
let X be RealNormSpace;
func R_VectorSpace_of_BoundedLinearFunctionals X ->
strict RealLinearSpace equals
RLSStruct (# BoundedLinearFunctionals X,
Zero_(BoundedLinearFunctionals X, X*'),
Add_(BoundedLinearFunctionals X, X*'),
Mult_(BoundedLinearFunctionals X, X*') #);
coherence;
end;
registration
let X be RealNormSpace;
cluster -> Function-like Relation-like for Element of
R_VectorSpace_of_BoundedLinearFunctionals X;
coherence;
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; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider f as Functional of X by Def9;
f.v is Element of REAL;
hence thesis;
end;
end;
theorem Th24:
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
proof
let X be RealNormSpace;
let f,g,h be VECTOR of R_VectorSpace_of_BoundedLinearFunctionals X;
A1: R_VectorSpace_of_BoundedLinearFunctionals X is Subspace of X*'
by Th22,RSSPACE:11;
then reconsider f1=f, h1=h, g1=g as VECTOR of X*' by RLSUB_1:10;
hereby
assume
A2: h = f+g;
let x be Element of X;
h1=f1+g1 by A1,A2,RLSUB_1:13;
hence h.x=f.x+g.x by Th20b;
end;
assume for x be Element of X holds h.x=f.x+g.x;
then h1=f1+g1 by Th20b;
hence thesis by A1,RLSUB_1:13;
end;
theorem Th25:
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
proof
let X be RealNormSpace;
let f,h be VECTOR of R_VectorSpace_of_BoundedLinearFunctionals X;
let a be Real;
A1: R_VectorSpace_of_BoundedLinearFunctionals X is Subspace of X*'
by Th22,RSSPACE:11;
then reconsider f1=f, h1=h as VECTOR of X*' by RLSUB_1:10;
hereby
assume
A2: h = a*f;
let x be Element of X;
h1=a*f1 by A1,A2,RLSUB_1:14;
hence h.x=a*f.x by Th21b;
end;
assume for x be Element of X holds h.x=a*f.x;
then h1=a*f1 by Th21b;
hence thesis by A1,RLSUB_1:14;
end;
theorem Th26:
for X be RealNormSpace holds
0.(R_VectorSpace_of_BoundedLinearFunctionals X) = (the carrier of X) --> 0
proof
let X be RealNormSpace;
A1: 0.(X*') =(the carrier of X) -->0 by Th22b;
R_VectorSpace_of_BoundedLinearFunctionals X is Subspace of X*'
by Th22,RSSPACE:11;
hence thesis by A1,RLSUB_1:11;
end;
definition
let X be RealNormSpace;
let f be object;
func Bound2Lipschitz(f,X) -> Lipschitzian linear-Functional of X equals
In(f,BoundedLinearFunctionals X);
coherence by Def9;
end;
definition
let X be RealNormSpace;
let u be linear-Functional of X;
func PreNorms u -> non empty Subset of REAL equals
{|.u.t.| where t is VECTOR of X : ||.t.|| <= 1 };
coherence
proof
A1: now
let x be object;
now
assume x in {|.u.t.| where t is VECTOR of X : ||.t.|| <= 1 };
then ex t be VECTOR of X st x=|.u.t.| & ||.t.|| <= 1;
hence x in REAL by XREAL_0:def 1;
end;
hence x in {|.u.t.| where t is VECTOR of X : ||.t.|| <= 1 } implies x
in REAL;
end;
||.0.X.|| = 0; then
|.u.(0.X).| in {|.u.t.| where t is VECTOR of X : ||.t.|| <= 1 };
hence thesis by A1,TARSKI:def 3;
end;
end;
Th27:
for X be RealNormSpace, g be Lipschitzian linear-Functional of X
holds PreNorms g is bounded_above
proof
let X be RealNormSpace;
let g be Lipschitzian linear-Functional of X;
consider K be Real such that
A1: 0 <= K & for x be VECTOR of X holds |. g.x .| <= K*||. x .|| by Def8;
take K;
let r be ExtReal;
assume r in PreNorms g;
then consider t be VECTOR of X such that
A3: r=|.g.t.| & ||.t.|| <= 1;
A5: |.g.t.| <= K*||. t .|| by A1;
K*||. t .|| <= K *1 by A1,A3,XREAL_1:64;
hence r <=K by A3,A5,XXREAL_0:2;
end;
registration let X be RealNormSpace,
g be Lipschitzian linear-Functional of X;
cluster PreNorms g -> bounded_above;
coherence by Th27;
end;
theorem
for X be RealNormSpace, g be linear-Functional of X
holds g is Lipschitzian iff PreNorms g is bounded_above
proof
let X be RealNormSpace;
let g be linear-Functional of X;
now
reconsider K=upper_bound PreNorms g as Real;
assume
A1: PreNorms g is bounded_above;
A2: now
let t be VECTOR of X;
per cases;
suppose
A3: t = 0.X; then
A4: ||.t.|| = 0;
g.t = g.(0*0.X) by A3
.=0*g.(0.X) by HAHNBAN:def 3
.=0;
hence |.g.t.| <= K*||.t.|| by A4,COMPLEX1:44;
end;
suppose
A5: t <> 0.X;
reconsider t1= ( ||.t.||")*t as VECTOR of X;
A6: ||.t.|| <> 0 by A5,NORMSP_0:def 5;
A7: |.g.t.|/||.t.||*||.t.|| = |.g.t.|*||.t.||"*||.t.|| by XCMPLX_0:def 9
.= |.g.t.|*(||.t.||"*||.t.||)
.= |.g.t.|*1 by A6,XCMPLX_0:def 7
.= |.g.t.|;
A8: |. ||.t.||".| = |. 1*||.t.||".| .=|. 1/||.t.||.| by XCMPLX_0:def 9
.= 1/||.t.|| by ABSVALUE:def 1
.= 1*||.t.||" by XCMPLX_0:def 9
.= ||.t.||";
||.t1.|| =|. ||.t.||".|*||.t.|| by NORMSP_1:def 1
.= 1 by A6,A8,XCMPLX_0:def 7; then
A9: |.g.t1.| in {|.g.s.| where s is VECTOR of X : ||.s.|| <= 1 };
|.g.t.|/||.t.|| = |.g.t.|*||.t.||" by XCMPLX_0:def 9
.= |. ||.t.||"*g.t .| by A8,COMPLEX1:65
.= |.g.t1.| by HAHNBAN:def 3;
then |.g.t.|/||.t.|| <= K by A1,A9,SEQ_4:def 1;
hence |.g.t.| <= K *||.t.|| by A7,XREAL_1:64;
end;
end;
take K;
0 <= K
proof
consider r0 be object such that
A10: r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 as Real by A10;
now
let r be Real;
assume r in PreNorms g;
then ex t be VECTOR of X st r=|.g.t.| & ||.t.|| <= 1;
hence 0 <= r by COMPLEX1:46;
end;
then 0 <= r0 by A10;
hence thesis by A1,A10,SEQ_4:def 1;
end;
hence g is Lipschitzian by A2;
end;
hence thesis;
end;
definition
let X be RealNormSpace;
func BoundedLinearFunctionalsNorm X
-> Function of BoundedLinearFunctionals X,REAL means :Def13:
for x be object st x in BoundedLinearFunctionals X holds
it.x = upper_bound PreNorms(Bound2Lipschitz(x,X));
existence
proof
deffunc F(object) = upper_bound PreNorms(Bound2Lipschitz($1,X));
A1: for z be object st z in BoundedLinearFunctionals X holds F(z) in REAL
by XREAL_0:def 1;
thus ex f be Function of BoundedLinearFunctionals X,REAL st
for x be object st x in BoundedLinearFunctionals X holds f.x = F(x)
from FUNCT_2:sch 2(A1);
end;
uniqueness
proof
let NORM1,NORM2 be Function of BoundedLinearFunctionals X,REAL such that
A2: for x be object st x in BoundedLinearFunctionals X holds NORM1.x =
upper_bound PreNorms(Bound2Lipschitz(x,X)) and
A3: for x be object st x in BoundedLinearFunctionals X holds NORM2.x =
upper_bound PreNorms(Bound2Lipschitz(x,X));
for z be object st z in BoundedLinearFunctionals X
holds NORM1.z = NORM2 .z
proof
let z be object such that
A5: z in BoundedLinearFunctionals X;
NORM1.z = upper_bound PreNorms(Bound2Lipschitz(z,X)) by A2,A5;
hence thesis by A3,A5;
end;
hence thesis;
end;
end;
theorem Th29:
for X be RealNormSpace, f be Lipschitzian linear-Functional of X
holds Bound2Lipschitz(f,X)=f
proof
let X be RealNormSpace;
let f be Lipschitzian linear-Functional of X;
f in BoundedLinearFunctionals X by Def9;
hence thesis by SUBSET_1:def 8;
end;
theorem Th30:
for X be RealNormSpace, f be Lipschitzian linear-Functional of X
holds (BoundedLinearFunctionalsNorm X).f = upper_bound PreNorms f
proof
let X be RealNormSpace;
let f be Lipschitzian linear-Functional of X;
reconsider f9=f as set;
f in BoundedLinearFunctionals X by Def9;
hence (BoundedLinearFunctionalsNorm X).f =
upper_bound PreNorms(Bound2Lipschitz(f9,X)) by Def13
.= upper_bound PreNorms f by Th29;
end;
definition
let X be RealNormSpace;
func DualSp X -> non empty NORMSTR equals
NORMSTR (# BoundedLinearFunctionals X,
Zero_(BoundedLinearFunctionals X, X*'),
Add_(BoundedLinearFunctionals X, X*'),
Mult_(BoundedLinearFunctionals X, X*'),
BoundedLinearFunctionalsNorm X #);
coherence;
end;
theorem Th31:
for X be RealNormSpace holds (the carrier of X) --> 0 = 0.(DualSp X)
proof
let X be RealNormSpace;
(the carrier of X) --> 0
= 0.R_VectorSpace_of_BoundedLinearFunctionals X by Th26
.= 0.(DualSp X);
hence thesis;
end;
theorem Th32:
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.||
proof
let X be RealNormSpace;
let f be Point of DualSp X;
let g be Lipschitzian linear-Functional of X such that
A1: g=f;
now
let t be VECTOR of X;
per cases;
suppose
A3: t = 0.X; then
A4: ||.t.|| = 0;
g.t =g.(0*0.X) by A3
.=0*g.(0.X) by HAHNBAN:def 3
.=0;
hence |.g.t.| <= ||.f.||*||.t.|| by A4,COMPLEX1:44;
end;
suppose
A5: t <> 0.X;
reconsider t1= ( ||.t.||")*t as VECTOR of X;
A6: ||.t.|| <> 0 by A5,NORMSP_0:def 5;
A7: |. ||.t.||".| =|. 1*||.t.||".| .=|. 1/||.t.||.| by XCMPLX_0:def 9
.=1/||.t.|| by ABSVALUE:def 1
.=1*||.t.||" by XCMPLX_0:def 9
.=||.t.||";
A8: |.g.t.|/||.t.|| = |.g.t.|*||.t.||" by XCMPLX_0:def 9
.=|. ||.t.||"*g.t.| by A7,COMPLEX1:65
.=|.g.t1.| by HAHNBAN:def 3;
||.t1.|| =|. ||.t.||".|*||.t.|| by NORMSP_1:def 1
.=1 by A6,A7,XCMPLX_0:def 7;
then |.g.t.|/||.t.|| in {|.g.s.| where s is VECTOR of X : ||.s.||
<= 1 } by A8;
then |.g.t.|/||.t.|| <= upper_bound PreNorms g by SEQ_4:def 1;
then
A9: |.g.t.|/||.t.|| <= ||.f.|| by A1,Th30;
|.g.t.|/||.t.||*||.t.|| = |.g.t.|*||.t.||"*||.t.|| by XCMPLX_0:def 9
.=|.g.t.|*(||.t.||"*||.t.||)
.=|.g.t.|*1 by A6,XCMPLX_0:def 7
.=|.g.t.|;
hence |.g.t.| <= ||.f.||*||.t.|| by A9,XREAL_1:64;
end;
end;
hence thesis;
end;
theorem Th33:
for X be RealNormSpace, f be Point of DualSp X holds 0 <= ||.f.||
proof
let X be RealNormSpace;
let f be Point of DualSp X;
reconsider g=f as Lipschitzian linear-Functional of X by Def9;
consider r0 be object such that
A1: r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 as Real by A1;
A3: (BoundedLinearFunctionalsNorm X).f = upper_bound PreNorms g by Th30;
now
let r be Real;
assume r in PreNorms g;
then ex t be VECTOR of X st r=|.g.t.| & ||.t.|| <= 1;
hence 0 <= r by COMPLEX1:46;
end;
then 0 <= r0 by A1;
hence thesis by A1,SEQ_4:def 1,A3;
end;
theorem Th34:
for X, Y be RealNormSpace for f be Point of DualSp X
st f = 0.(DualSp X) holds 0 = ||.f.||
proof
let X, Y be RealNormSpace;
let f be Point of DualSp X such that
A1: f = 0.(DualSp X);
thus ||.f.|| = 0
proof
reconsider g=f as Lipschitzian linear-Functional of X by Def9;
set z = (the carrier of X) --> 0;
reconsider z as Function of the carrier of X,REAL
by FUNCOP_1:45,XREAL_0:def 1;
consider r0 be object such that
A2: r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 as Real by A2;
A3: (for s be Real st s in PreNorms g holds s <= 0) implies upper_bound
PreNorms g <= 0 by SEQ_4:45;
A5: z=g by A1,Th31;
A6: now
let r be Real;
assume r in PreNorms g;
then ex t be VECTOR of X st r=|.g.t.| & ||.t.|| <= 1;
hence 0 <= r & r <=0 by A5,COMPLEX1:44;
end;
then 0 <= r0 by A2;
then upper_bound PreNorms g = 0 by A6,A2,A3,SEQ_4:def 1;
hence thesis by Th30;
end;
end;
registration
let X be RealNormSpace;
cluster -> Function-like Relation-like for Element of DualSp X;
coherence;
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; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider f as linear-Functional of X by Def9;
f.v is Element of REAL;
hence thesis;
end;
end;
theorem Th35:
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
proof
let X be RealNormSpace;
let f,g,h be Point of DualSp X;
reconsider f1=f, g1=g, h1=h as VECTOR of
R_VectorSpace_of_BoundedLinearFunctionals X;
h=f+g iff h1=f1+g1;
hence thesis by Th24;
end;
theorem Th36:
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
proof
let X be RealNormSpace;
let f,h be Point of DualSp X;
let a be Real;
reconsider f1=f, h1=h
as VECTOR of R_VectorSpace_of_BoundedLinearFunctionals X;
h=a*f iff h1=a*f1;
hence thesis by Th25;
end;
theorem Th37:
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.||
proof
let X be RealNormSpace;
let f,g be Point of DualSp X;
let a be Real;
A1: now
assume
A2: f = 0.(DualSp X);
reconsider g=f as Lipschitzian linear-Functional of X by Def9;
set z = (the carrier of X) --> 0;
reconsider z as Function of the carrier of X,REAL
by FUNCOP_1:45,XREAL_0:def 1;
consider r0 be object such that
A3: r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 as Real by A3;
A4: (for s be Real st s in PreNorms g holds s <= 0)
implies upper_bound PreNorms g <= 0 by SEQ_4:45;
A6: z=g by A2,Th31;
A7: now
let r be Real;
assume r in PreNorms g;
then consider t be VECTOR of X such that
A8: r=|.g.t.| and ||.t.|| <= 1;
thus 0 <= r & r <=0 by A8,A6,COMPLEX1:44;
end;
then 0<=r0 by A3;
then upper_bound PreNorms g = 0 by A7,A3,A4,SEQ_4:def 1;
hence ||.f.|| = 0 by Th30;
end;
A9: ||.f+g.|| <= ||.f.|| + ||.g.||
proof
reconsider f1=f, g1=g, h1=f+g as Lipschitzian linear-Functional of X
by Def9;
A10: ( for s be Real st s in PreNorms h1 holds s <= ||.f.|| + ||.g.||)
implies upper_bound PreNorms h1 <= ||.f.|| + ||.g.|| by SEQ_4:45;
A11: now
let t be VECTOR of X such that
A12: ||.t.|| <= 1;
0 <= ||.f.|| & 0 <= ||.g.|| by Th33;
then ||.f.||*||.t.|| <= ||.f.||*1
& ||.g.||*||.t.|| <= ||.g.||*1 by A12,XREAL_1:64;
then
A14: ||.f.||*||.t.|| + ||.g.||*||.t.|| <= ||.f.||*1 + ||.g.||*1 by XREAL_1:7;
A15: |.f1.t+g1.t.| <=|.f1.t.|+|.g1.t.| by COMPLEX1:56;
|.g1.t.|<= ||.g.||*||.t.|| & |.f1.t.|<= ||.f.||*||.t.|| by Th32;
then |.f1.t.|+|.g1.t.| <= ||.f.||*||.t.|| + ||.g.||*||.t.||
by XREAL_1:7;
then
A17: |.f1.t.|+|.g1.t.| <= ||.f.|| + ||.g.|| by A14,XXREAL_0:2;
|.h1.t.|= |.f1.t+g1.t.| by Th35;
hence |.h1.t.| <= ||.f.|| + ||.g.|| by A15,A17,XXREAL_0:2;
end;
now
let r be Real;
assume r in PreNorms h1;
then ex t be VECTOR of X st r=|.h1.t.| & ||.t.|| <= 1;
hence r <= ||.f.|| + ||.g.|| by A11;
end;
hence thesis by A10,Th30;
end;
A19: ||.a*f.|| = |.a.| * ||.f.||
proof
reconsider f1=f, h1=a*f as Lipschitzian linear-Functional of X by Def9;
A21: now
A22: 0 <= ||.f.|| by Th33;
let t be VECTOR of X;
assume ||.t.|| <= 1; then
A23: ||.f.||*||.t.|| <= ||.f.||*1 by A22,XREAL_1:64;
|.f1.t.|<= ||.f.||*||.t.|| by Th32; then
A24: |.f1.t.| <= ||.f.|| by A23,XXREAL_0:2;
A25: |.a*f1.t.| =|.a.|*|.f1.t.| by COMPLEX1:65;
A26: 0<= |.a.| by COMPLEX1:46;
|.h1.t.|= |.a*f1.t.| by Th36;
hence |.h1.t.| <= |.a.|*||.f.|| by A25,A24,A26,XREAL_1:64;
end;
A27: now
let r be Real;
assume r in PreNorms h1;
then ex t be VECTOR of X st r=|.h1.t.| & ||.t.|| <= 1;
hence r <= |.a.|*||.f.|| by A21;
end;
A28: now
per cases;
case
A29: a <> 0;
A30: now
A31: 0 <= ||.a*f.|| by Th33;
let t be VECTOR of X;
assume ||.t.|| <= 1; then
A32: ||.a*f.||*||.t.|| <= ||.a*f.||*1 by A31,XREAL_1:64;
|.h1.t.|<= ||.a*f.||*||.t.|| by Th32; then
A33: |.h1.t.| <= ||.a*f.|| by A32,XXREAL_0:2;
h1.t=a*f1.t by Th36; then
A34: a"*h1.t = (a"* a)*f1.t
.= 1*f1.t by A29,XCMPLX_0:def 7
.= f1.t;
A35: |.a".| =|.1*a".| .=|. 1/a.| by XCMPLX_0:def 9
.=1/|.a.| by ABSVALUE:7
.=1*|.a.|" by XCMPLX_0:def 9
.=|.a.|";
A36: 0<= |.a".| by COMPLEX1:46;
|.a"*h1.t.| =|.a".|*|.h1.t.| by COMPLEX1:65;
hence |.f1.t.| <= |.a.|"*||.a*f.|| by A34,A33,A36,A35,XREAL_1:64;
end;
A37: now
let r be Real;
assume r in PreNorms f1;
then ex t be VECTOR of X st r=|.f1.t.| & ||.t.|| <= 1;
hence r <= |.a.|"*||.a*f.|| by A30;
end;
A38: ( for s be Real st s in PreNorms f1 holds s <= |.a.|"*
||.a*f.|| ) implies upper_bound PreNorms f1 <= |.a.|"*||.a*f.||
by SEQ_4:45;
A39: 0 <= |.a.| by COMPLEX1:46;
||.f.|| <=|.a.|"*||.a*f.|| by A37,A38,Th30;
then |.a.|*||.f.|| <=|.a.|*(|.a.|"*||.a*f.||) by A39,XREAL_1:64;
then
A40: |.a.|*||.f.|| <=(|.a.|*|.a.|")*||.a*f.||;
|.a.| <>0 by A29,COMPLEX1:47;
then |.a.|*||.f.|| <=1*||.a*f.|| by A40,XCMPLX_0:def 7;
hence |.a.|* ||.f.|| <=||.a*f.||;
end;
case
A41: a=0;
reconsider fz=f as
VECTOR of R_VectorSpace_of_BoundedLinearFunctionals X;
A42: a*f = a*fz
.= 0.R_VectorSpace_of_BoundedLinearFunctionals X by A41,RLVECT_1:10
.= 0.(DualSp X);
thus |.a.|* ||.f.|| =0 * ||.f.|| by A41,ABSVALUE:2
.=||.a*f.|| by A42,Th34;
end;
end;
(BoundedLinearFunctionalsNorm X).(a*f) = upper_bound PreNorms h1 by Th30;
then ||.a*f.|| <= |.a.|*||.f.|| by A27,SEQ_4:45;
hence thesis by A28,XXREAL_0:1;
end;
now
reconsider g=f as Lipschitzian linear-Functional of X by Def9;
set z = (the carrier of X) --> 0;
reconsider z as Function of the carrier of X,REAL
by FUNCOP_1:45,XREAL_0:def 1;
assume
A43: ||.f.|| = 0;
now
let t be VECTOR of X;
|.g.t.| <= ||.f.|| *||.t.|| by Th32;
then |.g.t.| = 0 by A43,COMPLEX1:46;
hence g.t = 0 by COMPLEX1:45
.= z.t;
end;
then g=z;
hence f=0.(DualSp X) by Th31;
end;
hence thesis by A1,A19,A9;
end;
registration
let X be RealNormSpace;
cluster DualSp X -> reflexive discerning RealNormSpace-like;
correctness by Th37;
end;
theorem Th39:
for X be RealNormSpace holds DualSp X is RealNormSpace
proof
let X be RealNormSpace;
RLSStruct (# BoundedLinearFunctionals X,
Zero_(BoundedLinearFunctionals X, X*'),
Add_(BoundedLinearFunctionals X, X*'),
Mult_(BoundedLinearFunctionals X, X*') #) is RealLinearSpace;
hence thesis by RSSPACE3:2;
end;
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;
coherence by Th39;
end;
theorem Th40:
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
proof
let X be RealNormSpace;
let f,g,h be Point of DualSp X;
reconsider f9=f,g9=g,h9=h as Lipschitzian linear-Functional of X by Def9;
hereby
assume h=f-g; then
h+g=f-(g-g) by RLVECT_1:29;
then
A11: h+g=f-0.DualSp X by RLVECT_1:15;
now
let x be VECTOR of X;
f9.x=h9.x + g9.x by A11,Th35;
hence f9.x-g9.x=h9.x;
end;
hence for x be VECTOR of X holds h.x = f.x - g.x;
end;
assume
A2: for x be VECTOR of X holds h.x = f.x - g.x;
now
let x be VECTOR of X;
h9.x = f9.x - g9.x by A2;
hence h9.x + g9.x= f9.x;
end;
then
f=h+g by Th35; then
f-g=h+(g-g) by RLVECT_1:def 3;
then f-g=h+0.(DualSp X) by RLVECT_1:15;
hence thesis;
end;
Lm3: for e be Real, seq be Real_Sequence st
( seq is convergent
& ex k be Nat st for i be Nat st k <= i holds seq.i <=e )
holds lim seq <=e
proof
let e be Real;
let seq be Real_Sequence such that
A1: seq is convergent and
A2: ex k be Nat st for i be Nat st k <= i holds
seq.i <=e;
consider k be Nat such that
A3: for i be Nat st k <= i holds seq.i <=e by A2;
reconsider ee=e as Element of REAL by XREAL_0:def 1;
set cseq = seq_const e;
A4: lim cseq = cseq.0 by SEQ_4:26
.= e;
A5: now
let i be Nat;
A6: (seq ^\k).i = seq.(k+i) by NAT_1:def 3;
seq.(k+i) <=e by A3,NAT_1:11;
hence (seq ^\k) .i <= cseq.i by A6,SEQ_1:57;
end;
lim (seq ^\k)=lim seq by A1,SEQ_4:20;
hence thesis by A1,A5,A4,SEQ_2:18;
end;
definition let X be RealNormSpace;
let s be sequence of DualSp X, n be Nat;
redefine func s.n -> Element of DualSp X; :: redefines . (FUNCT_1, definition)
coherence
proof reconsider n as Element of NAT by ORDINAL1:def 12;
s.n is Element of DualSp X;
hence thesis;
end;
end;
theorem Th42:
for X be RealNormSpace, seq be sequence of DualSp X
st seq is Cauchy_sequence_by_Norm holds seq is convergent
proof
let X be RealNormSpace;
let vseq be sequence of DualSp X such that
A2: vseq is Cauchy_sequence_by_Norm;
defpred P[set, set] means ex xseq be sequence of REAL st
(for n be Nat holds xseq.n=(Bound2Lipschitz((vseq.n),X)).$1 ) &
xseq is convergent & $2= lim xseq;
A3: for x be Element of X ex y be Element of REAL st P[x,y]
proof
let x be Element of X;
deffunc F(Nat) = (Bound2Lipschitz((vseq.$1),X)).x;
consider xseq be Real_Sequence such that
A4: for n be Nat holds xseq.n = F(n) from SEQ_1:sch 1;
reconsider y = lim xseq as Element of REAL by XREAL_0:def 1;
take y;
A6: for m,k be Nat holds |.xseq.m-xseq.k.| <= ||.vseq.m -
vseq.k.|| * ||.x.||
proof
let m,k be Nat;
reconsider h1=vseq.m-vseq.k as Lipschitzian linear-Functional of X
by Def9;
A7: xseq.k =(Bound2Lipschitz(vseq.k,X)).x
& xseq.m =(Bound2Lipschitz(vseq.m,X)).x by A4;
vseq.m is Lipschitzian linear-Functional of X
& vseq.k is Lipschitzian linear-Functional of X by Def9;
then
Bound2Lipschitz(vseq.m,X)=vseq.m &
Bound2Lipschitz(vseq.k,X)=vseq.k by Th29;
then xseq.m - xseq.k = h1.x by A7,Th40;
hence thesis by Th32;
end;
now
let e be Real such that
A10: e > 0;
per cases;
suppose
A11: x=0.X;
reconsider k=0 as Nat;
take k;
thus for n be Nat st n >= k holds |.xseq.n - xseq.k.| < e
proof
let n be Nat such that
n >= k;
A12: xseq.k =(Bound2Lipschitz((vseq.k),X)).(0 * x) by A4,A11
.=0* (Bound2Lipschitz((vseq.k),X)).x by HAHNBAN:def 3;
xseq.n =(Bound2Lipschitz((vseq.n),X)).(0*x) by A4,A11
.=0*(Bound2Lipschitz((vseq.n),X)).x by HAHNBAN:def 3;
hence thesis by A10,A12,COMPLEX1:44;
end;
end;
suppose x <>0.X; then
A13: ||.x.|| <> 0 by NORMSP_0:def 5; then
consider k be Nat such that
X2: for n,m be Nat st n >= k & m>=k holds
||.(vseq.n) - (vseq.m).|| < e/||.x.|| by A10,A2,RSSPACE3:8;
take k;
thus for n be Nat st n >= k holds |.xseq.n-xseq.k.| < e
proof
let n be Nat;
assume n >=k; then
||.(vseq.n) - (vseq.k).|| < e/||.x.|| by X2; then
A18: ||.(vseq.n) - (vseq.k).|| * ||.x.|| < e/||.x.|| * ||.x.||
by A13,XREAL_1:68;
A19: e/||.x.|| * ||.x.|| = e*||.x.||"* ||.x.|| by XCMPLX_0:def 9
.= e*(||.x.||"* ||.x.||)
.= e*1 by A13,XCMPLX_0:def 7;
|.xseq.n-xseq.k.| <= ||.(vseq.n) - (vseq.k).|| * ||.x.|| by A6;
hence thesis by A18,A19,XXREAL_0:2;
end;
end;
end;
hence thesis by A4,SEQ_4:41;
end;
consider f be Function of the carrier of X,REAL such that
A20: for x be Element of X holds P[x,f.x] from FUNCT_2:sch 3(A3);
reconsider tseq=f as Function of the carrier of X,REAL;
A21: now
let x,y be VECTOR of X;
consider xseq be sequence of REAL such that
A22: ( for n be Nat holds xseq.n=(Bound2Lipschitz(vseq.n,X)).x )
& xseq is convergent & tseq.x = lim xseq by A20;
consider zseq be sequence of REAL such that
A25: ( for n be Nat holds zseq.n=(Bound2Lipschitz(vseq.n,X)).(x+y) )
& zseq is convergent & tseq.(x+y) = lim zseq by A20;
consider yseq be sequence of REAL such that
A27: ( for n be Nat holds yseq.n=(Bound2Lipschitz(vseq.n,X)).y )
& yseq is convergent & tseq.y = lim yseq by A20;
now
let n be Nat;
thus zseq.n=(Bound2Lipschitz(vseq.n,X)).(x+y) by A25
.= (Bound2Lipschitz(vseq.n,X)).x+(Bound2Lipschitz(vseq.n,X)).y
by HAHNBAN:def 2
.= xseq.n + (Bound2Lipschitz(vseq.n,X)).y by A22
.= xseq.n +yseq.n by A27;
end;
then zseq=xseq+yseq by SEQ_1:7;
hence tseq.(x+y)=tseq.x+tseq.y by A22,A27,A25,SEQ_2:6;
end;
now
let x be VECTOR of X;
let a be Real;
consider xseq be sequence of REAL such that
A30: ( for n be Nat holds xseq.n=(Bound2Lipschitz(vseq.n,X)).x )
& xseq is convergent & tseq.x = lim xseq by A20;
consider zseq be sequence of REAL such that
A33: ( for n be Nat holds zseq.n=(Bound2Lipschitz(vseq.n,X)).(a*x) )
& zseq is convergent & tseq.(a*x) = lim zseq by A20;
now
let n be Nat;
thus zseq.n=(Bound2Lipschitz((vseq.n),X)).(a*x) by A33
.= a*(Bound2Lipschitz((vseq.n),X)).x by HAHNBAN:def 3
.= a*xseq.n by A30;
end;
then zseq=a(#)xseq by SEQ_1:9;
hence tseq.(a*x)=a*tseq.x by A30,A33,SEQ_2:8;
end;
then reconsider tseq as linear-Functional of X by A21,HAHNBAN:def 2,def 3;
B40: now
let e be Real;
assume e >0; then
consider k be Nat such that
A36: for n,m be Nat st n >= k & m >= k holds ||.vseq.n - vseq.m.|| < e
by A2,RSSPACE3:8;
take k;
hereby let m be Nat;
assume m >= k; then
A37: ||.(vseq.m) - (vseq.k).|| <e by A36;
A38: ||.vseq.m.||= ||.vseq.||.m & ||.vseq.k.||= ||.vseq.||.k by NORMSP_0:def 4;
|. ||.vseq.m.||- ||.vseq.k.|| .| <= ||.(vseq.m) - (vseq.k).||
by NORMSP_1:9;
hence |. ||.vseq.||.m - ||.vseq.||.k .| <e by A38,A37,XXREAL_0:2;
end;
end; then
A40: ||.vseq.|| is convergent by SEQ_4:41;
A41: tseq is Lipschitzian
proof
take lim ||.vseq.||;
A42: now
let x be VECTOR of X;
consider xseq be sequence of REAL such that
A43: ( for n be Nat holds xseq.n=(Bound2Lipschitz(vseq.n,X)).x )
& xseq is convergent & tseq.x = lim xseq by A20;
A46: |.tseq.x.| = lim |.xseq.| by A43,SEQ_4:14;
A49: for n be Nat holds |.xseq.| .n <= ( ||.x.||(#)||.vseq .||).n
proof
let n be Nat;
A50: |.xseq.|.n = |.(xseq.n).| by SEQ_1:12;
A51: ||.vseq.n.|| = ||.vseq.||.n by NORMSP_0:def 4;
A48: xseq.n =(Bound2Lipschitz((vseq.n),X)).x by A43;
vseq.n is Lipschitzian linear-Functional of X by Def9; then
|.(xseq.n).| <= ||.vseq.n.|| * ||.x.|| by A48,Th29,Th32;
hence thesis by A50,A51,SEQ_1:9;
end;
lim ( ||.x.||(#)||.vseq.|| ) = lim (||.vseq.|| )* ||.x.||
by B40,SEQ_4:41,SEQ_2:8;
hence |.tseq.x.| <= lim (||.vseq.|| )* ||.x.||
by A46,A49,A40,SEQ_2:18,A43;
end;
now
let n be Nat;
||.vseq.n.|| >=0;
hence ||.vseq.||.n >=0 by NORMSP_0:def 4;
end;
hence thesis by B40,SEQ_4:41,A42,SEQ_2:17;
end;
A54: for e be Real
st e > 0 ex k be Nat st for n be Nat st n >= k
holds for x be VECTOR of X holds
|.(Bound2Lipschitz((vseq.n),X)).x - tseq.x.| <= e* ||.x.||
proof
let e be Real;
assume e > 0;
then consider k be Nat such that
A55: for n, m be Nat st n >= k & m >= k holds ||.vseq.n - vseq.m.|| < e
by A2,RSSPACE3:8;
take k;
now
let n be Nat such that
A56: n >= k;
now
let x be VECTOR of X;
consider xseq be sequence of REAL such that
A57: for n be Nat holds xseq.n=(Bound2Lipschitz(vseq.n,X)). x
& xseq is convergent & tseq.x = lim xseq by A20;
A60: for m,k be Nat holds
|.xseq.m-xseq.k.| <= ||.vseq.m - vseq.k.|| * ||.x.||
proof
let m,k be Nat;
reconsider h1=vseq.m-vseq.k as Lipschitzian linear-Functional of X
by Def9;
A61: xseq.k =(Bound2Lipschitz((vseq.k),X)).x
& xseq.m =(Bound2Lipschitz((vseq.m),X)).x by A57;
vseq.m is Lipschitzian linear-Functional of X
& vseq.k is Lipschitzian linear-Functional of X by Def9;
then Bound2Lipschitz(vseq.m,X)=vseq.m &
Bound2Lipschitz(vseq.k,X)=vseq.k by Th29;
then xseq.m - xseq.k =h1.x by A61,Th40;
hence thesis by Th32;
end;
A64: for m be Nat st m >=k holds |.xseq.n-xseq.m.| <= e *||.x.||
proof
let m be Nat;
assume m >=k;
then ||.vseq.n - vseq.m.|| <e by A55,A56;
then
A66: ||.vseq.n - vseq.m.|| * ||.x.|| <= e* ||.x.|| by XREAL_1:64;
|.xseq.n-xseq.m.| <= ||.vseq.n - vseq.m.|| * ||.x.|| by A60;
hence thesis by A66,XXREAL_0:2;
end;
|.xseq.n-tseq.x.| <= e * ||.x.||
proof
deffunc F(Nat) = |.xseq.$1 - xseq.n.|;
consider rseq be Real_Sequence such that
A67: for m be Nat holds rseq.m = F(m) from SEQ_1:sch 1;
now
let x be object;
assume x in NAT;
then reconsider k=x as Nat;
thus rseq.x = |.xseq.k - xseq.n.| by A67
.= |.(xseq - xseq.n).k.| by Def14
.= |.(xseq - xseq.n).|.x by SEQ_1:12;
end; then
A68: rseq = |.xseq - xseq.n.|;
A69: xseq- xseq.n is convergent by A57,Th121;
lim (xseq-xseq.n) = tseq.x - xseq.n by A57,Th121;
then
A70: lim rseq = |.tseq.x-xseq.n.| by A57,Th121,A68,SEQ_4:14;
for m be Nat st m >= k holds rseq.m <= e * ||.x.||
proof
let m be Nat such that
A71: m >=k;
rseq.m = |.xseq.m-xseq.n.| by A67
.= |.xseq.n-xseq.m.| by COMPLEX1:60;
hence thesis by A64,A71;
end;
then lim rseq <= e * ||.x.|| by A69,A68,Lm3;
hence thesis by A70,COMPLEX1:60;
end;
hence |.(Bound2Lipschitz((vseq.n),X)).x - tseq.x.|
<= e* ||.x.|| by A57;
end;
hence
for x be VECTOR of X holds |.(Bound2Lipschitz((vseq.n),X)).x - tseq.x.|
<= e* ||.x.||;
end;
hence thesis;
end;
reconsider tseq as Lipschitzian linear-Functional of X by A41;
reconsider tv=tseq as Point of DualSp X by Def9;
A72: for e be Real st e > 0
ex k be Nat st for n be Nat st n >= k holds ||.vseq.n - tv.|| <= e
proof
let e be Real such that
A73: e > 0;
consider k be Nat such that
A74: for n be Nat st n >= k holds for x be VECTOR of X
holds |.(Bound2Lipschitz((vseq.n),X)).x - tseq.x.| <= e* ||.x.||
by A54,A73;
now
set g1=tseq;
let n be Nat such that
A75: n >= k;
reconsider h1=vseq.n-tv as Lipschitzian linear-Functional of X by Def9;
set f1=Bound2Lipschitz((vseq.n),X);
A76: now
let t be VECTOR of X;
assume ||.t.|| <= 1; then
A77: e*||.t.|| <= e*1 by A73,XREAL_1:64;
A78: |.f1.t-g1.t.| <=e* ||.t.|| by A74,A75;
vseq.n is Lipschitzian linear-Functional of X by Def9;
then Bound2Lipschitz((vseq.n),X)=vseq.n by Th29;
then |.h1.t.|= |.f1.t-g1.t.| by Th40;
hence |.h1.t.| <=e by A78,A77,XXREAL_0:2;
end;
A79: now
let r be Real;
assume r in PreNorms h1;
then ex t be VECTOR of X st r=|.h1.t.| & ||.t.|| <= 1;
hence r <=e by A76;
end;
(for s be Real st s in PreNorms h1 holds s <= e) implies
upper_bound PreNorms h1 <=e by SEQ_4:45;
hence ||.vseq.n-tv.|| <=e by A79,Th30;
end;
hence thesis;
end;
for e be Real st e > 0 ex m be Nat st for n be Nat st n >= m
holds ||.(vseq.n) - tv.|| < e
proof
let e be Real;
assume A81: e > 0; then
consider m be Nat such that
A82: for n be Nat st n >= m holds ||.(vseq.n) - tv.|| <= e/2 by A72;
take m;
hereby let n be Nat;
assume n >= m;
then ||.(vseq.n) - tv.|| <= e/2 & e/2 < e by A82,A81,XREAL_1:216;
hence ||.(vseq.n) - tv.|| < e by XXREAL_0:2;
end;
end;
hence thesis;
end;
theorem Th43:
for X be RealNormSpace holds DualSp X is RealBanachSpace
proof
let X be RealNormSpace;
for seq be sequence of DualSp X st seq
is Cauchy_sequence_by_Norm holds seq is convergent by Th42;
hence thesis by LOPBAN_1:def 15;
end;
registration
let X be RealNormSpace;
cluster DualSp X -> complete;
coherence by Th43;
end;
begin :: Hahn-Banach's Extension Theorem
definition
let V be RealNormSpace;
mode SubRealNormSpace of V -> RealNormSpace means :DefSubSP:
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);
existence
proof
the addF of V = (the addF of V)||the carrier of V
& the Mult of V = (the Mult of V) | [:REAL, the carrier of V:]
& the normF of V = (the normF of V) | (the carrier of V);
hence thesis;
end;
end;
theorem Th44:
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.||
proof
let V be RealNormSpace, X be SubRealNormSpace of V,
f be Lipschitzian linear-Functional of X,
F be Point of DualSp X such that
A1:f=F;
reconsider X0 = X as RealLinearSpace;
B1: the carrier of X0 c= the carrier of V
& 0.X0 = 0.V
& the addF of X0 = (the addF of V)||the carrier of X0
& the Mult of X0 = (the Mult of V) | [:REAL, the carrier of X0:]
by DefSubSP; then
reconsider X0 as Subspace of V by RLSUB_1:def 2;
reconsider fi0=f as linear-Functional of X0;
deffunc F(Element of the carrier of V) = ||.F.|| * ||.$1.||;
D0:for v be Element of the carrier of V
holds F(v) in REAL by XREAL_0:def 1;
consider q be Function of the carrier of V,REAL such that
D1: for v be Element of the carrier of V holds q.v = F(v)
from FUNCT_2:sch 8(D0);
q is Banach-Functional of V
proof
E0: q is subadditive
proof
let x,y be VECTOR of V;
E2: q.x = ||.F.|| * ||.x.|| & q.y = ||.F.|| * ||.y.|| by D1;
||.F.|| * ||.x+y.|| <= ||.F.|| * (||.x.|| + ||.y.||)
by XREAL_1:64,NORMSP_1:def 1;
hence thesis by D1,E2;
end;
q is absolutely_homogeneous
proof
let x be VECTOR of V, r be Real;
E5: ||.r*x.|| = |.r.| * ||.x.|| by NORMSP_1:def 1;
q.(r*x) = ||.F.|| * ||.r*x.|| by D1
.= |.r.| * (||.F.|| * ||.x.||) by E5;
hence thesis by D1;
end;
hence thesis by E0;
end; then
reconsider q as Banach-Functional of V;
for x be VECTOR of X0, v be VECTOR of V st x=v holds fi0.x <= q.v
proof
let x0 be VECTOR of X0, v be VECTOR of V;
assume D21: x0=v;
reconsider x=x0 as VECTOR of X;
D22: fi0.x0 <= |. fi0.x0 .| by ABSVALUE:4;
D23:|. fi0.x .| <= ||.F.|| * ||.x.|| by A1,Th32;
||.x.|| = ((the normF of V) | (the carrier of X)).v by D21,DefSubSP
.= ||.v.|| by FUNCT_1:49,D21;
then
|. fi0.x0 .| <= q.v by D1,D23;
hence thesis by D22,XXREAL_0:2;
end; then
consider g be linear-Functional of V such that
A3: g|the carrier of X0=fi0 &
for x be VECTOR of V holds g.x <= q.x by HAHNBAN:22;
B4: for x be VECTOR of V holds |. g.x .| <= ||.F.|| * ||.x.||
proof
let x be VECTOR of V;
g.x <= q.x by A3; then
A31: g.x <= ||.F.|| * ||.x.|| by D1;
A32: -(g.x) = (-1)* (g.x)
.= g.((-1)*x) by HAHNBAN:def 3;
g.((-1)*x) <= q.((-1)*x) by A3;
then g.((-1)*x) <= ||.F.|| * ||.(-1)*x.|| by D1;
then g.((-1)*x) <= ||.F.|| * ||.-x.|| by RLVECT_1:16;
then -(g.x) <= ||.F.|| * ||.x.|| by A32,NORMSP_1:2;
then - (||.F.|| * ||.x.||) <= g.x by XREAL_1:26;
hence thesis by ABSVALUE:5,A31;
end;
then
reconsider g as Lipschitzian linear-Functional of V by Def8;
reconsider G=g as Point of DualSp V by Def9;
now let r be Real;
assume r in PreNorms g; then
consider t be VECTOR of V such that
C1: r = |.g.t.| and
C2: ||.t.|| <= 1;
C3: |.g.t.| <= ||.F.|| * ||.t.|| by B4;
||.F.|| * ||.t.|| <= ||.F.|| * 1 by C2,XREAL_1:64;
hence r <= ||.F.|| by C1,C3,XXREAL_0:2;
end; then
upper_bound PreNorms g
<= (BoundedLinearFunctionalsNorm X).f by A1,SEQ_4:45;
then
A41: (BoundedLinearFunctionalsNorm V).g
<= (BoundedLinearFunctionalsNorm X).f by Th30;
now let r be object;
assume r in PreNorms f; then
consider t be VECTOR of X such that
C1: r = |.f.t.| and
C2: ||.t.|| <= 1;
reconsider td=t as VECTOR of V by B1;
||.t.|| = ((the normF of V) | (the carrier of X)).td by DefSubSP
.= ||.td.|| by FUNCT_1:49;
then
r = |.g.td.| & ||.td.|| <= 1 by C1,A3,FUNCT_1:49,C2;
hence r in PreNorms g;
end; then
A42: PreNorms f c= PreNorms g;
upper_bound PreNorms f
<= upper_bound PreNorms g by A42,SEQ_4:48; then
(BoundedLinearFunctionalsNorm X).f
<= upper_bound PreNorms g by Th30; then
B4: (BoundedLinearFunctionalsNorm X).f
<= (BoundedLinearFunctionalsNorm V).g by Th30;
take g,G;
thus thesis by A3,A1,A41,XXREAL_0:1,B4;
end;
::$N Hahn-Banach's extension theorem (real normed spaces)
theorem
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.||
proof
let V be RealNormSpace, X be SubRealNormSpace of V,
f be Lipschitzian linear-Functional of X,
F be Point of DualSp X such that
A11: f=F and
A12: for x be VECTOR of X, v be VECTOR of V st x=v
holds f.x <= ||.v.||;
consider g be Lipschitzian linear-Functional of V,
G be Point of DualSp V such that
A2: g=G &
g|the carrier of X=f & ||.G.||=||.F.|| by A11,Th44;
reconsider X0 = X as RealLinearSpace;
B1: the carrier of X0 c= the carrier of V
& 0.X0 = 0.V
& the addF of X0 = (the addF of V)||the carrier of X0
& the Mult of X0 = (the Mult of V) | [:REAL, the carrier of X0:]
by DefSubSP;
now let r be Real;
assume r in PreNorms f; then
consider t be VECTOR of X such that
C1: r = |.f.t.| & ||.t.|| <= 1;
reconsider td=t as VECTOR of V by B1;
C7: ||.t.|| = ((the normF of V) | (the carrier of X)).td by DefSubSP
.= ||.td.|| by FUNCT_1:49;
C5: -(f.t) = (-1)* (f.t)
.= f.((-1)*t) by HAHNBAN:def 3;
reconsider t0=t as VECTOR of X0;
D6: X0 is Subspace of V by B1,RLSUB_1:def 2;
(-1)*td = -td & (-1)*t = -t by RLVECT_1:16; then
(-1)*td = (-1)*t by RLSUB_1:15,D6; then
f.((-1)*t) <= ||.(-1)*td.|| by A12; then
f.((-1)*t) <= ||.-td.|| by RLVECT_1:16; then
-(f.t) <= ||.td.|| by C5,NORMSP_1:2; then
- (||.td.||) <= f.t by XREAL_1:26; then
|.f.t.| <= ||.td.|| by A12,ABSVALUE:5;
hence r <= 1 by C1,C7,XXREAL_0:2;
end; then
upper_bound PreNorms f <= 1 by SEQ_4:45; then
A3: ||.G.|| <= 1 by A2,A11,Th30;
for x be VECTOR of V holds g.x <= ||.x.||
proof
let x be VECTOR of V;
C1: g.x <= |.g.x.| by ABSVALUE:4;
|.g.x.| <= ||.G.|| * ||.x.|| by A2,Th32; then
C2: g.x <= ||.G.|| * ||.x.|| by C1,XXREAL_0:2;
||.G.|| * ||.x.|| <= 1 * ||.x.|| by A3,XREAL_1:64;
hence thesis by C2,XXREAL_0:2;
end;
hence thesis by A2;
end;