:: Bidual Spaces and Reflexivity of Real Normed Spaces
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received November 29, 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, UNIALG_1, DUALSP01, DUALSP02, RLVECT_1,
ARYTM_1, RELAT_1, FUNCT_1, RSSPACE, RSSPACE3, REAL_1, TARSKI, MSSUBFAM,
STRUCT_0, FUNCOP_1, FCONT_1, NORMSP_0, SEQ_2, 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, COMPLEX1, XXREAL_0, XXREAL_2,
NAT_1, REWRITE1, METRIC_1, RELAT_2, FUNCT_7, RCOMP_1, NORMSP_2, RLVECT_3,
BINOP_2, NORMSP_3, EUCLID, MOD_4, MEMBERED;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, EUCLID, FUNCT_2, BINOP_1, BINOP_2, DOMAIN_1, FUNCOP_1, NUMBERS,
MEMBERED, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, COMPLEX1, XXREAL_2, SEQ_4,
STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, RLVECT_3, RLSUB_1, VECTSP_1,
NORMSP_0, NORMSP_1, NORMSP_2, HAHNBAN, RSSPACE, RSSPACE3, LOPBAN_1,
NFCONT_1, DUALSP01, NORMSP_3;
constructors REAL_1, EUCLID, REALSET1, RSSPACE3, BINOP_2, RELSET_1, SEQ_4,
HAHNBAN1, NORMSP_2, PCOMPS_1, RLVECT_3, NORMSP_3, NFCONT_1, MEMBERED;
registrations STRUCT_0, XREAL_0, NUMBERS, ORDINAL1, MEMBERED, XXREAL_0,
VALUED_0, RLVECT_1, FUNCT_2, SEQ_4, RELSET_1, FUNCT_1, NORMSP_3,
NORMSP_0, NORMSP_1, DUALSP01, XBOOLE_0, LOPBAN_1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions ALGSTR_0, VECTSP_1, HAHNBAN, LOPBAN_1, TARSKI;
equalities RLVECT_1, STRUCT_0, ALGSTR_0, NORMSP_0, FUNCSDOM, NORMSP_3,
PCOMPS_1, DUALSP01, NORMSP_2;
expansions FUNCT_1, RLSUB_1, TARSKI, XBOOLE_0, FUNCT_2, NORMSP_0, NORMSP_1,
VECTSP_1, STRUCT_0, RLVECT_1, NORMSP_3, XXREAL_2, MEMBERED, DUALSP01;
theorems SEQ_4, FUNCT_1, ABSVALUE, COMPLEX1, TARSKI, RSSPACE3, XREAL_0,
XXREAL_0, NORMSP_1, LOPBAN_1, FUNCT_2, XBOOLE_0, XREAL_1, RLVECT_1,
FUNCOP_1, VECTSP_1, HAHNBAN, RLSUB_1, NORMSP_0, ORDINAL1, NORMSP_3,
SUBSET_1, ZFMISC_1, XXREAL_2, DUALSP01, RELAT_1, XCMPLX_1, NORMSP_2,
BINOP_2, LOPBAN_5, RLVECT_4, EUCLID;
schemes FUNCT_2;
begin :: The application of Hahn-Banach's Theorem
theorem Th63:
for V be RealNormSpace, X be SubRealNormSpace of V,
x0 be Point of V, d be Real st
ex Z be non empty Subset of REAL
st Z = {||.x-x0.|| where x is Point of V : x in X} &
d = lower_bound Z > 0 holds
not x0 in X &
ex G be Point of DualSp V st
( for x be Point of V st x in X
holds (Bound2Lipschitz(G,V)).x = 0 )
& (Bound2Lipschitz(G,V)).x0 = 1 & ||.G.|| = 1/d
proof
let V be RealNormSpace, X be SubRealNormSpace of V,
x0 be Point of V, d be Real;
assume ex Z be non empty Subset of REAL
st Z = {||.x-x0.|| where x is Point of V : x in X}
& d = lower_bound Z > 0; then
consider Z be non empty Subset of REAL such that
AS2:Z = {||.x-x0.|| where x is Point of V : x in X}
& d = lower_bound Z > 0;
set M0 = {z+a*x0 where z is Point of V, a is Real : z in X};
A1:0.V = 0.V + 0 * x0 by RLVECT_1:10;
0.V = 0.X by DUALSP01:def 16; then
D1:0.V in X; then
0.V in M0 by A1; then
reconsider M0 as non empty set;
now let x be object;
assume x in M0; then
ex z be Point of V, a be Real st x = z+a*x0 & z in X;
hence x in the carrier of V;
end; then
M0 c= the carrier of V; then
reconsider M0 as non empty Subset of V;
B0:X is Subspace of V by NORMSP_3:27;
set M = NLin(M0);
AD1: M0 is linearly-closed
proof
A0: for v,u be VECTOR of V st v in M0 & u in M0 holds v+u in M0
proof
let v,u be VECTOR of V;
assume A1: v in M0 & u in M0; then
consider z1 be Point of V, a be Real such that
A3: v = z1+a*x0 & z1 in X;
consider z2 be Point of V, b be Real such that
A5: u = z2+b*x0 & z2 in X by A1;
A7: v+u = z1 + (a*x0 + (z2 + b*x0)) by A3,A5,RLVECT_1:def 3
.= z1 + (z2 + (a*x0 + b*x0)) by RLVECT_1:def 3
.= (z1+z2) + (a*x0+b*x0) by RLVECT_1:def 3
.= (z1+z2) + (a+b)*x0 by RLVECT_1:def 6;
z1+z2 in X by B0,A3,A5,RLSUB_1:20;
hence thesis by A7;
end;
for r be Real, v be VECTOR of V st v in M0 holds r*v in M0
proof
let r be Real;
let v be VECTOR of V;
assume v in M0; then
consider z be Point of V, a be Real such that
A9: v = z+a*x0 & z in X;
A11: r*v = r*z + r*(a*x0) by A9,RLVECT_1:def 5
.= r*z + (r*a)*x0 by RLVECT_1:def 7;
r*z in X by B0,A9,RLSUB_1:21;
hence thesis by A11;
end;
hence thesis by A0;
end; then
X01:the carrier of M = M0 by NORMSP_3:31;
V2:x0 = 0.V + 1*x0 by RLVECT_1:def 8; then
V21: x0 in M by D1,X01;
AD2: for v be Point of M
ex x be Point of V, a be Real st v = x+a*x0 & x in X
proof
let v be Point of M;
v in the carrier of Lin(M0); then
v in M0 by AD1,NORMSP_3:31;
hence thesis;
end;
reconsider r0=0 as Real;
for r be ExtReal st r in Z holds r0 <= r
proof
let r be ExtReal;
assume r in Z; then
ex x be Point of V st r = ||.x-x0.|| & x in X by AS2;
hence r0 <= r;
end; then
r0 is LowerBound of Z by XXREAL_2:def 2; then
U2:Z is bounded_below;
P4:now assume Q1: x0 in X;
reconsider x0 as Point of V;
||.x0 - x0.|| = ||. 0.V .|| by RLVECT_1:15; then
r0 in Z by Q1,AS2;
hence contradiction by AS2,U2,SEQ_4:def 2;
end;
hence not x0 in X;
AD3: for x1,x2 be Point of V, a1,a2 be Real
st x1 in X & x2 in X & x1+a1*x0 = x2+a2*x0
holds x1=x2 & a1=a2
proof
let x1,x2 be Point of V, a1,a2 be Real;
assume P1: x1 in X & x2 in X & x1+a1*x0 = x2+a2*x0; then
x1 + a1*x0 - x2
= (x2 + -x2) + a2*x0 by RLVECT_1:def 3
.= 0.V + a2*x0 by RLVECT_1:5; then
P5: x1 + a1*x0 - x2 - a1*x0 = (a2 - a1)*x0 by RLVECT_1:35;
P6: x1 + a1*x0 - x2 - a1*x0
= (x1 + a1*x0) + (-x2 - a1*x0) by RLVECT_1:def 3
.= x1 + (a1*x0 + (-x2 - a1*x0)) by RLVECT_1:def 3
.= x1 + ((a1*x0 + -x2) - a1*x0) by RLVECT_1:def 3
.= x1 + (-x2 + (a1*x0 - a1*x0)) by RLVECT_1:def 3
.= x1 + (-x2 + 0.V) by RLVECT_1:15;
P7: a2 = a1
proof
assume a2 <> a1; then
Q0: a2 - a1 <> 0; then
Q1: (a2-a1)*(1/(a2-a1)) = 1 by XCMPLX_1:106;
1*(x1 - x2) = (a2 - a1)*x0 by P5,P6,RLVECT_1:def 8; then
(a2-a1)*((1/(a2-a1))*(x1-x2)) = (a2-a1)*x0 by Q1,RLVECT_1:def 7; then
Q2: (1/(a2-a1))*(x1-x2) = x0 by Q0,RLVECT_1:36;
reconsider r=1/(a2-a1) as Real;
Q4: r*x1 in X & r*x2 in X by B0,P1,RLSUB_1:21;
r*(x1-x2) = r*x1-r*x2 by RLVECT_1:34;
hence contradiction by P4,Q2,B0,Q4,RLSUB_1:23;
end; then
x1 - x2 = 0.V by P5,P6,RLVECT_1:10;
hence thesis by P7,RLVECT_1:21;
end;
defpred P[object,object] means
ex z be Point of V, a be Real st z in X & $1 = z+a*x0 & $2 = a;
F1:for v being Element of M
ex a being Element of REAL st P[v,a]
proof
let v be Element of M;
consider z be Point of V, a be Real such that
B0: v = z+a*x0 & z in X by AD2;
reconsider aa=a as Element of REAL by XREAL_0:def 1;
take aa;
thus thesis by B0;
end;
consider f being Function of M,REAL such that
A1F:for x being Element of M holds P[x,f.x] from FUNCT_2:sch 3(F1);
A1:for v be Point of M, z be Point of V, a be Real st
z in X & v= z+a*x0 holds f.v = a
proof
let v be Point of M, z be Point of V, a be Real;
assume AS0: z in X & v = z+a*x0;
ex z1 be Point of V, a1 be Real st
z1 in X & v = z1+a1*x0 & f.v = a1 by A1F;
hence f.v = a by AS0,AD3;
end;
f is linear-Functional of M
proof
B1: f is additive
proof
let v,w be VECTOR of M;
consider x1 be Point of V, a1 be Real such that
B11: v = x1+a1*x0 & x1 in X by AD2;
consider x2 be Point of V, a2 be Real such that
B13: w = x2+a2*x0 & x2 in X by AD2;
B14: f.v = a1 & f.w = a2 by A1,B11,B13;
v+w = (x1 + a1*x0) + (x2 + a2*x0) by B11,B13,NORMSP_3:28
.= x1 + (a1*x0 + (x2 + a2*x0)) by RLVECT_1:def 3
.= x1 + (x2 + (a1*x0 + a2*x0)) by RLVECT_1:def 3
.= (x1+x2) + (a1*x0+a2*x0) by RLVECT_1:def 3
.= (x1+x2) + (a1+a2)*x0 by RLVECT_1:def 6;
hence f.(v+w) = f.v + f.w by B14,A1,B0,B11,B13,RLSUB_1:20;
end;
f is homogeneous
proof
let v be VECTOR of M, r be Real;
consider x be Point of V, a be Real such that
B11: v = x+a*x0 & x in X by AD2;
r*v = r*(x+a*x0) by B11,NORMSP_3:28
.= r*x + r*(a*x0) by RLVECT_1:def 5
.= r*x + (r*a)*x0 by RLVECT_1:def 7;
hence f.(r*v) = r*a by A1,B0,B11,RLSUB_1:21
.= r*f.v by A1,B11;
end;
hence thesis by B1;
end; then
reconsider f as linear-Functional of M;
A5:for v be Point of M holds |.f.v.| <= (1/d)*||.v.||
proof
let v be Point of M;
consider x be Point of V, a be Real such that
B5: v = x+a*x0 & x in X by AD2;
per cases;
suppose a = 0; then
|.f.(x+a*x0).| = 0 by A1,B5,ABSVALUE:2;
hence |.f.v.| <= (1/d)*||.v.|| by AS2,B5;
end;
suppose B6: a <> 0;
C3: ||.x+a*x0.|| = ||.1*x + a*x0.|| by RLVECT_1:def 8
.= ||.(a*(1/a))*x + a*x0.|| by B6,XCMPLX_1:106
.= ||.a*((1/a)*x) + a*x0.|| by RLVECT_1:def 7
.= ||.a*((1/a)*x + x0).|| by RLVECT_1:def 5
.= |.a.|*||.(1/a)*x + x0.|| by NORMSP_1:def 1;
C4: ||.(1/a)*x + x0.|| = ||.-((1/a)*x + x0).|| by NORMSP_1:2
.= ||.-(1/a)*x -x0.|| by RLVECT_1:30;
set s = ||.-(1/a)*x-x0.||;
C52: -(1/a)*x = (1/a)*(-x) by RLVECT_1:25;
-x in X by B0,B5,RLSUB_1:22; then
-(1/a)*x in X by B0,C52,RLSUB_1:21; then
s in Z by AS2; then
C5: ||.-(1/a)*x-x0.|| >= d by AS2,U2,SEQ_4:def 2;
|.a.| >= 0 by COMPLEX1:46; then
|.a.|*||.-(1/a)*x -x0.|| >= |.a.|*d by C5,XREAL_1:64; then
||.x+a*x0.||/d >= |.a.| by AS2,C3,C4,XREAL_1:77; then
(1/d)*||.x+a*x0.|| >= |.a.| by XCMPLX_1:99; then
|.f.(x+a*x0).| <= (1/d)* ||.x+a*x0.|| by A1,B5;
hence |.f.v.| <= (1/d)*||.v.|| by B5,NORMSP_3:28;
end;
end; then
f is Lipschitzian by AS2; then
reconsider f as Lipschitzian linear-Functional of M;
reconsider F=f as Point of DualSp M by DUALSP01:def 10;
consider g be Lipschitzian linear-Functional of V, G be Point of DualSp V
such that
C1: g = G & g| (the carrier of M) = f & ||.G.||=||.F.|| by DUALSP01:36;
A31:for x be Point of V st x in X holds (Bound2Lipschitz(G,V)).x = 0
proof
let x be Point of V;
assume A32: x in X;
x = x + 0.V; then
A33:x = x + 0 * x0 by RLVECT_1:10; then
A34:x in M by X01,A32;
thus (Bound2Lipschitz(G,V)).x = G.x by SUBSET_1:def 8
.= f.x by A34,C1,FUNCT_1:49
.= 0 by A33,A32,A34,A1;
end;
A12:
(Bound2Lipschitz(G,V)).x0 = G.x0 by SUBSET_1:def 8
.= f.x0 by C1,V21,FUNCT_1:49
.= 1 by A1,V2,D1,V21;
take G;
now let r be Real;
assume r in PreNorms f; then
consider t be VECTOR of M such that
C1: r = |.f.t.| & ||.t.|| <= 1;
C3: |.f.t.| <= (1/d)*||.t.|| by A5;
(1/d) * ||.t.|| <= (1/d) * 1 by AS2,C1,XREAL_1:64;
hence r <= (1/d) by C1,C3,XXREAL_0:2;
end; then
upper_bound PreNorms f <= (1/d) by SEQ_4:45; then
B3: ||.F.|| <= 1/d by DUALSP01:24;
now let s be Real;
assume 0 < s; then
consider r be Real such that
B32: r in Z & r < (lower_bound Z) + s by U2,SEQ_4:def 2;
consider x be Point of V such that
B34: r = ||.x-x0.|| & x in X by B32,AS2;
B35:x-x0 = x+(-1)*x0 by RLVECT_1:16; then
x-x0 in M0 by B34; then
reconsider xx0=x-x0 as Point of M by AD1,NORMSP_3:31;
|. f.xx0 .| = |. -1 .| by B35,A1,B34
.= |. 1 .| by COMPLEX1:52
.= 1 by COMPLEX1:43; then
B38:1 <= ||.F.|| * ||.xx0.|| by DUALSP01:26;
||.xx0.|| = r by NORMSP_3:28,B34; then
||.F.|| * ||.xx0.|| <= ||.F.|| * (d+s) by AS2,B32,XREAL_1:64;
hence 1 <= ||.F.|| * d + ||.F.|| * s by B38,XXREAL_0:2;
end; then
1 <= ||.F.|| * d by NORMSP_3:22; then
1/d <= (||.F.|| *d) /d by XREAL_1:72,AS2; then
1/d <= ||.F.|| by XCMPLX_1:89,AS2;
hence thesis by A31,A12,C1,B3,XXREAL_0:1;
end;
theorem Lm64:
for V be RealNormSpace, Y be non empty Subset of V,
x0 be Point of V
st Y is linearly-closed & Y is closed & not x0 in Y holds
ex G be Point of DualSp V st
(for x be Point of V st x in Y holds (Bound2Lipschitz(G,V)).x = 0 )
& (Bound2Lipschitz(G,V)).x0 = 1
proof
let V be RealNormSpace, Y be non empty Subset of V,
x0 be Point of V;
assume AS: Y is linearly-closed & Y is closed & not x0 in Y;
set X = NLin(Y);
X1:the carrier of X = Y by NORMSP_3:31,AS;
set Z = {||.x-x0.|| where x is Point of V : x in X};
X is Subspace of V by NORMSP_3:27; then
0.V in X by RLSUB_1:17; then
X2: ||.0.V-x0.|| in Z;
now let z be object;
assume z in Z; then
ex x be Point of V st z = ||.x-x0.|| & x in X;
hence z in REAL;
end; then
Z c= REAL; then
reconsider Z as non empty Subset of REAL by X2;
reconsider r0 = 0 as Real;
for r be ExtReal st r in Z holds r0 <= r
proof
let r be ExtReal;
assume r in Z; then
ex x be Point of V st r = ||.x-x0.|| & x in X;
hence r0 <= r;
end; then
U1:r0 is LowerBound of Z by XXREAL_2:def 2; then
Z is bounded_below; then
reconsider Z as non empty bounded_below real-membered
Subset of REAL;
reconsider d = lower_bound Z as Real;
X3:r0 <= inf Z by U1,XXREAL_2:def 4;
d > 0
proof
assume not d > 0; then
X22:d = 0 by X3;
reconsider Yt = Y` as Subset of TopSpaceNorm V;
Z24:Yt is open by AS,NORMSP_2:16;
x0 in (the carrier of V) \ Y by AS,XBOOLE_0:def 5; then
x0 in Yt by SUBSET_1:def 4; then
consider s be Real such that
X23: 0 < s
& {y where y is Point of V : ||.x0-y.|| < s} c= Yt by Z24,NORMSP_2:7;
consider r be Real such that
X24: r in Z & r < 0 + s by X22,X23,SEQ_4:def 2;
consider x be Point of V such that
X25: r = ||.x-x0.|| & x in X by X24;
||.x0-x.||< s by X24,X25,NORMSP_1:7; then
x in {x where x is Point of V : ||.x0-x.|| < s}; then
x in Yt by X23; then
x in (the carrier of V) \ Y by SUBSET_1:def 4;
hence contradiction by X1,X25,XBOOLE_0:def 5;
end; then
consider G be Point of DualSp V such that
X3: ( for x be Point of V st x in X holds (Bound2Lipschitz(G,V)).x = 0 )
& (Bound2Lipschitz(G,V)).x0 = 1 & ||.G.|| = 1/d by Th63;
take G;
now let x be Point of V;
assume x in Y; then
x in X by NORMSP_3:31,AS;
hence (Bound2Lipschitz(G,V)).x = 0 by X3;
end;
hence thesis by X3;
end;
theorem Lm65a:
for V be RealNormSpace, x0 be Point of V st x0 <> 0.V holds
ex G be Point of DualSp V
st (Bound2Lipschitz(G,V)).x0 = 1 & ||.G.|| = 1/||.x0.||
proof
let V be RealNormSpace, x0 be Point of V;
assume AS0: x0 <> 0.V;
set X = NLin({0.V});
set Y = the carrier of Lin({0.V});
for s be object holds s in Y iff s in {0.V}
proof
let s be object;
hereby assume s in Y; then
s in Lin({0.V}); then
ex a be Real st s=a*0.V by RLVECT_4:8;
hence s in {0.V} by TARSKI:def 1;
end;
assume s in {0.V}; then
s = 1*0.V by TARSKI:def 1; then
s in Lin{0.V} by RLVECT_4:8;
hence s in Y;
end; then
Y1:the carrier of X = {0.V} by TARSKI:2;
set Z = {||.x-x0.|| where x is Point of V : x in X};
Y2:for s be object holds s in Z iff s in {||.x0.||}
proof
let s be object;
hereby assume s in Z; then
consider x be Point of V such that
Y11: s=||.x-x0.|| & x in X;
x = 0.V by Y1,Y11,TARSKI:def 1; then
||.x-x0.|| = ||.x0.|| by NORMSP_1:2;
hence s in {||.x0.||} by TARSKI:def 1,Y11;
end;
assume s in {||.x0.||}; then
s = ||.x0.|| by TARSKI:def 1; then
X1: s = ||.0.V-x0.|| by NORMSP_1:2;
0.V in X by Y1,TARSKI:def 1;
hence s in Z by X1;
end; then
reconsider Z as non empty Subset of REAL by TARSKI:2;
reconsider d = lower_bound Z as Real;
Y3:Z = {||.x0.||} by Y2; then
X4:d = ||.x0.|| by SEQ_4:9; then
d <> 0 by AS0,NORMSP_0:def 5; then
consider G be Point of DualSp V such that
X3: ( for x be Point of V st x in X holds (Bound2Lipschitz(G,V)).x = 0 )
& (Bound2Lipschitz(G,V)).x0 = 1 & ||.G.|| = 1/d by X4,Th63;
take G;
thus thesis by X3,SEQ_4:9,Y3;
end;
theorem Lm65:
for V be RealNormSpace, x0 be Point of V st x0 <> 0.V holds
ex F be Point of DualSp V
st ||.F.|| = 1 & (Bound2Lipschitz(F,V)).x0 =||.x0.||
proof
let V be RealNormSpace, x0 be Point of V;
assume AS: x0 <> 0.V; then
consider G be Point of DualSp V such that
A2: (Bound2Lipschitz(G,V)).x0 = 1 & ||.G.|| = 1/||.x0.|| by Lm65a;
reconsider d=||.x0.|| as Real;
reconsider F=d*G as Point of DualSp V;
take F;
A4: ||.F.|| = |.d.|*||.G.|| by NORMSP_1:def 1
.= d*(1/d) by A2,ABSVALUE:def 1
.= 1 by AS,NORMSP_0:def 5,XCMPLX_1:106;
(Bound2Lipschitz(F,V)).x0
= d * G.x0 by DUALSP01:30,SUBSET_1:def 8
.= d *(Bound2Lipschitz(G,V)).x0 by SUBSET_1:def 8;
hence thesis by A2,A4;
end;
theorem Lm65A:
for V be RealNormSpace st V is non trivial holds
ex F be Point of DualSp V st ||.F.|| = 1
proof
let V be RealNormSpace;
assume V is non trivial; then
consider x0 be Element of V such that
P1: x0 <> 0.V;
ex F be Point of DualSp V
st ||.F.|| = 1 & (Bound2Lipschitz(F,V)).x0 =||.x0.|| by Lm65,P1;
hence thesis;
end;
theorem Lm65A1:
for V be RealNormSpace st V is non trivial holds
DualSp V is non trivial
proof
let V be RealNormSpace;
assume V is non trivial; then
consider F be Point of DualSp V such that
A1: ||.F.|| = 1 by Lm65A;
F <> 0.(DualSp V) by A1;
hence thesis;
end;
begin :: Bidual Spaces of Real Normed Spaces
theorem Th71:
for V be RealNormSpace, x be Point of V st V is non trivial holds
( ex X be non empty Subset of REAL st
X = {|.(Bound2Lipschitz(F,V)).x.|
where F is Point of DualSp V :||.F.|| = 1 }
& ||.x.|| = upper_bound X ) &
( ex Y be non empty Subset of REAL st
Y = {|.(Bound2Lipschitz(F,V)).x.|
where F is Point of DualSp V :||.F.|| <= 1 }
& ||.x.|| = upper_bound Y )
proof
let V be RealNormSpace, x be Point of V;
assume AS: V is non trivial;
set X = {|.(Bound2Lipschitz(F,V)).x.|
where F is Point of DualSp V :||.F.|| = 1 };
set Y = {|.(Bound2Lipschitz(F,V)).x.|
where F is Point of DualSp V :||.F.|| <= 1 };
consider F0 be Point of DualSp V such that
P1: ||.F0.|| = 1 by AS,Lm65A;
P2: |.(Bound2Lipschitz(F0,V)).x.| in X
& |.(Bound2Lipschitz(F0,V)).x.| in Y by P1;
P3: X c= Y
proof
let z be object;
assume z in X; then
ex F be Point of DualSp V st
z = |.(Bound2Lipschitz(F,V)).x.| & ||.F.|| = 1;
hence z in Y;
end;
P4:Y c= REAL
proof
let z be object;
assume z in Y; then
ex F be Point of DualSp V st
z = |.(Bound2Lipschitz(F,V)).x.| & ||.F.|| <= 1;
hence z in REAL by XREAL_0:def 1;
end; then
reconsider Y as non empty Subset of REAL by P2;
X c= REAL by P3,P4; then
reconsider X as non empty Subset of REAL by P2;
per cases;
suppose X1: x = 0.V;
for t be object st t in Y holds t in {0 qua Real}
proof
let t be object;
assume t in Y; then
ex F be Point of DualSp V st
t = |.(Bound2Lipschitz(F,V)).x.| & ||.F.|| <= 1; then
t = 0 by ABSVALUE:2,X1,HAHNBAN:20;
hence t in {0 qua Real} by TARSKI:def 1;
end; then
P6: Y c= {0 qua Real} & X c= {0 qua Real} by P3;
ex z be object st z in X by XBOOLE_0:def 1; then
0 in X by P6,TARSKI:def 1; then
X = {0 qua Real} & Y = {0 qua Real} by P6,P3,ZFMISC_1:31; then
upper_bound X = 0 & upper_bound Y = 0 by SEQ_4:9; then
||.x.|| = upper_bound X & ||.x.|| = upper_bound Y by X1;
hence thesis;
end;
suppose Z1:x <> 0.V;
X6: for r be ExtReal st r in Y holds r<=||. x .||
proof
let r be ExtReal;
assume r in Y; then
consider F be Point of DualSp V such that
X4: r = |.(Bound2Lipschitz(F,V)).x.| & ||.F.|| <= 1;
X5: |.(Bound2Lipschitz(F,V)).x.|
<= ||.F.|| * ||.x.|| by DUALSP01:26,SUBSET_1:def 8;
||.F.|| * ||.x.|| <= 1 * ||.x.|| by X4,XREAL_1:64;
hence r <= ||.x.|| by X4,X5,XXREAL_0:2;
end; then
||.x.|| is UpperBound of Y by XXREAL_2:def 1; then
X7: Y is bounded_above; then
X8: upper_bound X <= upper_bound Y by P3,SEQ_4:48;
for r be Real st r in Y holds r <= ||. x .|| by X6; then
X9: upper_bound Y <= ||.x.|| by SEQ_4:45; then
X10:upper_bound X <= ||.x.|| by X8,XXREAL_0:2;
consider F0 be Point of DualSp V such that
Y1: ||.F0.|| = 1 & (Bound2Lipschitz(F0,V)).x = ||.x.|| by Lm65,Z1;
|.(Bound2Lipschitz(F0,V)).x.| = ||.x.|| by Y1,ABSVALUE:def 1; then
Y3: ||.x.|| in X by Y1;
X is bounded_above by P3,X7,XXREAL_2:43; then
||.x.|| <= upper_bound X by Y3,SEQ_4:def 1; then
||.x.|| = upper_bound X by X10,XXREAL_0:1;
hence thesis by X9,X8,XXREAL_0:1;
end;
end;
theorem Lm72:
for V be RealNormSpace, x be Point of V st
for f be Lipschitzian linear-Functional of V holds f.x = 0
holds x = 0.V
proof
let V be RealNormSpace, x be Point of V;
assume AS: for f be Lipschitzian linear-Functional of V holds f.x = 0;
assume x <> 0.V; then
ex G be Point of DualSp V st
(Bound2Lipschitz(G,V)).x = 1 & ||.G.|| = 1/||.x.|| by Lm65a;
hence contradiction by AS;
end;
definition
let X be RealNormSpace;
let x be Point of X;
func BiDual x -> Point of DualSp DualSp X means :Def1:
for f be Point of DualSp X holds it.f = f.x;
existence
proof
deffunc F(Element of DualSp X) = $1.x;
P0:ex f be Function of the carrier of DualSp X,REAL st
for fai be Element of DualSp X holds f.fai = F(fai)
from FUNCT_2:sch 4;
consider f be Function of the carrier of DualSp X,REAL such that
P1: for fai be Point of DualSp X holds f.fai = fai.x by P0;
P2:f is additive
proof
let y,z be Point of DualSp X;
f.(y+z) = (y+z).x by P1
.= y.x + z.x by DUALSP01:29
.= f.y + z.x by P1;
hence f.(y+z) = f.y + f.z by P1;
end;
P3:f is homogeneous
proof
let y be Point of DualSp X, r be Real;
f.(r*y) = (r*y).x by P1
.= r*(y.x) by DUALSP01:30;
hence f.(r*y) = r*(f.y) by P1;
end;
for y be Point of DualSp X holds |. f.y .| <= ||.x.|| * ||.y.||
proof
let y be Point of DualSp X;
reconsider y1=y as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
|. y1.x .| <= ||. y .||*||. x .|| by DUALSP01:26;
hence thesis by P1;
end; then
f is Lipschitzian; then
reconsider f as Point of DualSp DualSp X by P2,P3,DUALSP01:def 10;
take f;
thus thesis by P1;
end;
uniqueness
proof
let F1,F2 be Point of DualSp DualSp X;
assume A1: (for f be Point of DualSp X holds F1.f = f.x)
& (for f be Point of DualSp X holds F2.f = f.x);
A2:F1 is Lipschitzian linear-Functional of DualSp X
& F2 is Lipschitzian linear-Functional of DualSp X by DUALSP01:def 10; then
A3:dom F1 = the carrier of DualSp X & dom F2 = the carrier of DualSp X
by FUNCT_2:def 1;
now let f be object;
assume f in dom F1; then
reconsider f1=f as Point of DualSp X by A2,FUNCT_2:def 1;
F1.f = f1.x by A1;
hence F1.f = F2.f by A1;
end;
hence F1 = F2 by A3;
end;
end;
definition
let X be RealNormSpace;
func BidualFunc X -> Function of X, DualSp DualSp X means :Def2:
for x be Point of X holds it.x = BiDual x;
existence
proof
deffunc F(Element of X) = BiDual $1;
ex f be Function of X, DualSp DualSp X st
for x be Element of the carrier of X holds f.x = F(x)
from FUNCT_2:sch 4; then
consider f be Function of X, DualSp DualSp X such that
P1: for x be Point of X holds f.x = BiDual x;
take f;
thus thesis by P1;
end;
uniqueness
proof
let f1,f2 be Function of X, DualSp DualSp X;
assume
A1: (for x be Point of X holds f1.x = BiDual x)
& (for x be Point of X holds f2.x = BiDual x);
A3:dom f1 = the carrier of X & dom f2 = the carrier of X by FUNCT_2:def 1;
now let x be object;
assume x in dom f1; then
reconsider x1=x as Point of X;
f1.x = BiDual x1 by A1;
hence f1.x = f2.x by A1;
end;
hence f1 = f2 by A3;
end;
end;
registration
let X be RealNormSpace;
cluster BidualFunc X -> additive homogeneous;
coherence
proof
reconsider f = BidualFunc X as Function of X, DualSp DualSp X;
A0:f is additive
proof
let x,y be Point of X;
A1: f.(x+y) is Function of the carrier of DualSp X,REAL
& f.x+f.y is Function of the carrier of DualSp X,REAL by DUALSP01:def 10;
for g be Point of DualSp X holds (f.(x+y)).g = (f.x+f.y).g
proof
let g be Point of DualSp X;
reconsider g1=g as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
thus (f.(x+y)).g = (BiDual(x+y)).g by Def2
.= g.(x+y) by Def1
.= g1.x + g1.y by HAHNBAN:def 2
.= (BiDual x).g + g.y by Def1
.= (BiDual x).g + (BiDual y).g by Def1
.= (f.x).g + (BiDual y).g by Def2
.= (f.x).g + (f.y).g by Def2
.= (f.x + f.y).g by DUALSP01:29;
end;
hence f.(x+y) = f.x+f.y by A1,FUNCT_2:def 8;
end;
f is homogeneous
proof
let x be Point of X, r be Real;
A3: f.(r*x) is Function of the carrier of DualSp X, REAL
& r*(f.x) is Function of the carrier of DualSp X, REAL by DUALSP01:def 10;
for g be Point of DualSp X holds (f.(r*x)).g = (r*(f.x)).g
proof
let g be Point of DualSp X;
reconsider g1=g as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
thus (f.(r*x)).g = (BiDual(r*x)).g by Def2
.= g.(r*x) by Def1
.= r*(g1.x) by HAHNBAN:def 3
.= r*((BiDual x).g) by Def1
.= r*((f.x).g) by Def2
.= (r*(f.x)).g by DUALSP01:30;
end;
hence f.(r*x) = r*(f.x) by A3,FUNCT_2:def 8;
end;
hence thesis by A0;
end;
end;
registration
let X be RealNormSpace;
cluster BidualFunc X -> one-to-one;
coherence
proof
reconsider f = BidualFunc X as Function of X, DualSp DualSp X;
A0:f is additive homogeneous;
for x1,x2 be object st x1 in dom f & x2 in dom f & f.x1 = f.x2
holds x1 = x2
proof
let x1,x2 be object;
assume A1: x1 in dom f & x2 in dom f & f.x1 = f.x2; then
reconsider y1=x1, y2=x2 as Point of X;
A3: f.(y1-y2) = BiDual(y1-y2) by Def2;
y1-y2 = y1 + (-1)*y2 by RLVECT_1:16; then
A5: f.(y1-y2) = f.y1 + f.((-1)*y2) by A0;
f.((-1)*y2) = (-1)*(f.y2) by LOPBAN_1:def 5; then
f.(y1-y2) = f.y1 - f.y2 by A5,RLVECT_1:16; then
A7: BiDual(y1-y2) = 0.(DualSp DualSp X) by A3,A1,RLVECT_1:15;
for g be Lipschitzian linear-Functional of X
holds g.(y1-y2) = 0
proof
let g be Lipschitzian linear-Functional of X;
reconsider g1=g as Point of DualSp X by DUALSP01:def 10;
A8: (BiDual(y1-y2)).g1 = g1.(y1-y2) by Def1;
(the carrier of DualSp X) --> 0 = 0.(DualSp DualSp X)
by DUALSP01:25;
hence g.(y1-y2) = 0 by A7,A8,FUNCOP_1:7;
end; then
y1-y2 = 0.X by Lm72;
hence x1 = x2 by RLVECT_1:21;
end;
hence thesis;
end;
end;
LMNORM:
for X be RealNormSpace, x be Point of X st X is non trivial
holds ||.x.|| = ||. (BidualFunc X).x .||
proof
let X be RealNormSpace, x be Point of X;
assume AS: X is non trivial;
reconsider f=BiDual x
as Lipschitzian linear-Functional of DualSp X by DUALSP01:def 10;
consider Y be non empty Subset of REAL such that
A1: Y = {|.(Bound2Lipschitz(s,X)).x.|
where s is Point of DualSp X :||.s.|| <= 1 }
& ||.x.|| = upper_bound Y by AS,Th71;
set Z = {|.f.t.| where t is Point of DualSp X : ||.t.|| <= 1 };
A2: Y c= Z
proof
let y be object;
assume y in Y; then
consider s be Point of DualSp X such that
B1: y = |.(Bound2Lipschitz(s,X)).x.| & ||.s.|| <= 1 by A1;
s is Lipschitzian linear-Functional of X by DUALSP01:def 10; then
B2: |.(Bound2Lipschitz(s,X)).x.| = |. s.x .| by DUALSP01:23;
f.s = s.x by Def1;
hence y in Z by B1,B2;
end;
upper_bound Y <= upper_bound PreNorms f by A2,SEQ_4:48; then
A4: ||. x .|| <= ||. BiDual x .|| by A1,DUALSP01:24;
Z c= Y
proof
let y be object;
assume y in Z; then
consider t be Point of DualSp X such that
C1: y = |.f.t.| & ||.t.|| <= 1;
t is Lipschitzian linear-Functional of X by DUALSP01:def 10; then
C2: |.(Bound2Lipschitz(t,X)).x.| = |. t.x .| by DUALSP01:23;
|. f.t .| = |. t.x .| by Def1;
hence y in Y by C1,C2,A1;
end; then
Y = Z by A2; then
upper_bound PreNorms f <= upper_bound Y; then
||. BiDual x .|| <= upper_bound Y by DUALSP01:24; then
||. BiDual x .|| = ||. x .|| by A1,A4,XXREAL_0:1;
hence thesis by Def2;
end;
theorem
for X be RealNormSpace
st X is non trivial holds
BidualFunc X is LinearOperator of X, DualSp DualSp X &
for x be Point of X
holds ||.x.|| = ||. (BidualFunc X).x .|| by LMNORM;
theorem IMDDX:
for X be RealNormSpace st X is non trivial holds
ex DuX be SubRealNormSpace of DualSp DualSp X,
L be Lipschitzian LinearOperator of X, DuX
st L is bijective
& DuX = Im(BidualFunc X)
& (for x be Point of X holds L.x = BiDual x)
& for x be Point of X holds ||.x.|| = ||. L.x .||
proof
let X be RealNormSpace;
assume A0: X is non trivial;
set F = BidualFunc X;
set V1 = rng F;
D0: V1 is linearly-closed by NORMSP_3:35;
V1 <> {}
proof
assume V1 = {}; then
dom F = {} by RELAT_1:42;
hence thesis by FUNCT_2:def 1;
end; then
the carrier of Lin(V1) = V1 by NORMSP_3:31,D0; then
C4: the carrier of Im(F) = rng F; then
reconsider L = BidualFunc X as Function of X, Im(F) by FUNCT_2:6;
A3:F is additive homogeneous;
B0:L is additive
proof
let x,y be Point of X;
L.(x+y) = F.x + F.y by A3;
hence L.(x+y) = L.x + L.y by NORMSP_3:28;
end;
L is homogeneous
proof
let x be Point of X, r be Real;
L.(r*x) = r*(F.x) by LOPBAN_1:def 5;
hence L.(r*x) = r*(L.x) by NORMSP_3:28;
end; then
reconsider L as LinearOperator of X,Im(F) by B0;
P5:for x be Point of X holds ||.x.|| = ||. L.x .||
proof
let x be Point of X;
||.x.|| = ||. (BidualFunc X).x .|| by A0,LMNORM;
hence thesis by NORMSP_3:28;
end; then
for x be Point of X holds ||. L.x .|| <= 1* ||.x.||; then
reconsider L as Lipschitzian LinearOperator of X, Im(BidualFunc X)
by LOPBAN_1:def 8;
take Im(BidualFunc X), L;
L is one-to-one onto by C4;
hence thesis by Def2,P5;
end;
begin :: Uniform Boundedness Theorem for Linear Functionals
definition
func RNS_Real -> RealNormSpace equals
NORMSTR (# REAL, In(0,REAL), addreal, multreal, absreal #);
coherence
proof
set T=NORMSTR (# REAL, In(0,REAL), addreal, multreal, absreal #);
reconsider T as non empty NORMSTR;
now let v,w be Element of T;
reconsider v1 = v, w1 = w as Element of REAL;
thus v + w = v1 + w1 by BINOP_2:def 9
.= w + v by BINOP_2:def 9;
end; then
A1:T is Abelian;
now let u,v,w be Element of T;
reconsider u1 = u, v1 = v, w1 = w as Element of REAL;
B1: addreal.(u,v) = u1 + v1 & addreal.(v,w) = v1 + w1 by BINOP_2:def 9;
thus (u + v) + w = (u1 + v1) + w1 by B1,BINOP_2:def 9
.= u1 + (v1 + w1)
.= u + (v + w) by B1,BINOP_2:def 9;
end; then
A2:T is add-associative;
now let v be Element of T;
reconsider v1 = v as Element of REAL;
thus v + 0.T = v1 + 0 by BINOP_2:def 9 .= v;
end; then
A3:T is right_zeroed;
A4:T is right_complementable
proof
let v be Element of T;
reconsider v1 = v as Element of REAL;
reconsider w1 = -v1 as Element of REAL;
reconsider w = w1 as Element of T;
take w;
thus v + w = v1 + w1 by BINOP_2:def 9 .= 0.T;
end;
now let a,b be Real, v be Element of T;
reconsider v1=v as Element of REAL;
B1: multreal.(a,v) = a * v1 & multreal.(b,v) = b * v1 by BINOP_2:def 11;
thus (a + b) * v = (a + b) * v1 by BINOP_2:def 11
.= v1 * a + v1 * b
.= a * v + b * v by B1,BINOP_2:def 9;
end; then
A5:T is scalar-distributive;
now let a be Real, v,w be Element of T;
reconsider v1 = v, w1 = w as Element of REAL;
B1: addreal.(v,w) = v1 + w1 by BINOP_2:def 9;
B2: multreal.(a,v) = a * v1 & multreal.(a,w) = a * w1 by BINOP_2:def 11;
thus a * (v + w) = a * (v1 + w1) by B1,BINOP_2:def 11
.= a * v1 + a * w1
.= a * v + a * w by B2,BINOP_2:def 9;
end; then
A6:T is vector-distributive;
now let a,b be Real, v be Element of T;
reconsider v1=v as Element of REAL;
B1: multreal.(b,v) = b * v1 by BINOP_2:def 11;
thus (a * b) * v = (a * b) * v1 by BINOP_2:def 11
.= a * (b * v1)
.= a * (b * v) by B1,BINOP_2:def 11;
end; then
A7:T is scalar-associative;
now let v be Element of T;
reconsider v1=v as Element of REAL;
thus 1 * v = 1 * v1 by BINOP_2:def 11 .= v;
end; then
A8:T is scalar-unital;
A9:T is reflexive by EUCLID:def 2,COMPLEX1:44;
now let v be Element of T;
assume AS: ||. v .|| = 0;
reconsider v1=v as Element of REAL;
|. v1 .| = 0 by AS,EUCLID:def 2;
hence v = 0.T by COMPLEX1:45;
end; then
A10: T is discerning;
now let a be Real, v,w be Element of T;
reconsider v1 = v, w1 = w as Element of REAL;
(the normF of T).(a*v) = absreal.(a*v1) by BINOP_2:def 11;
hence ||. a*v .|| = |. a*v1 .| by EUCLID:def 2
.= |. a .| * |. v1 .| by COMPLEX1:65
.= |. a .| * ||. v .|| by EUCLID:def 2;
(the normF of T).(v+w) = absreal.(v1+w1) by BINOP_2:def 9; then
C3: ||. v + w .|| = |. v1 + w1 .| by EUCLID:def 2;
||. v .|| + ||. w .|| = |. v1 .| + absreal.w1 by EUCLID:def 2
.= |. v1 .| + |. w1 .| by EUCLID:def 2;
hence ||. v + w .|| <= ||. v .|| + ||. w .|| by C3,COMPLEX1:56;
end; then
T is RealNormSpace-like;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10;
end;
end;
theorem
for X be RealNormSpace, x be Element of REAL, v be Point of RNS_Real
st x=v holds -x = -v
proof
let X be RealNormSpace, x be Element of REAL, v be Point of RNS_Real;
assume x=v; then
(-1)*x = (-1)*v by BINOP_2:def 11;
hence thesis by RLVECT_1:16;
end;
theorem LMN6:
for X be RealNormSpace, x be object holds
x is additive homogeneous Function of X,REAL
iff
x is additive homogeneous Function of X,RNS_Real
proof
let X be RealNormSpace, x be object;
hereby assume A1: x is additive homogeneous Function of X,REAL; then
reconsider f=x as linear-Functional of X;
reconsider g=x as Function of X,RNS_Real by A1;
A2: for v,w be Element of X holds g.(v+w) = g.v + g.w
proof
let v,w be Element of X;
thus g.(v+w) = f.v + f.w by HAHNBAN:def 2
.= g.v + g.w by BINOP_2:def 9;
end;
for v being VECTOR of X, r being Real holds g.(r*v) = r*g.v
proof
let v be VECTOR of X, r be Real;
thus g.(r*v) = r*f.v by HAHNBAN:def 3
.= r*g.v by BINOP_2:def 11;
end; then
g is additive homogeneous by LOPBAN_1:def 5,A2;
hence x is additive homogeneous Function of X,RNS_Real;
end;
assume B1: x is additive homogeneous Function of X,RNS_Real; then
reconsider g=x as additive homogeneous Function of X,RNS_Real;
reconsider f=x as Function of X,REAL by B1;
B2:for v,w be Element of X holds f.(v+w) = f.v + f.w
proof
let v,w be Element of X;
thus f.(v+w) = g.v + g.w by VECTSP_1:def 20
.= f.v + f.w by BINOP_2:def 9;
end;
for v being VECTOR of X, r being Real holds f.(r*v) = r*f.v
proof
let v be VECTOR of X, r be Real;
thus f.(r*v) = r*g.v by LOPBAN_1:def 5
.= r*f.v by BINOP_2:def 11;
end;
hence thesis by B2,HAHNBAN:def 2,def 3;
end;
theorem LMN7:
for X be RealNormSpace, x be object holds
x is Lipschitzian additive homogeneous Function of X,REAL
iff
x is Lipschitzian additive homogeneous Function of X,RNS_Real
proof
let X be RealNormSpace, x be object;
hereby
assume A1: x is Lipschitzian additive homogeneous Function of X,REAL; then
reconsider f=x as Lipschitzian linear-Functional of X;
reconsider g=x as additive homogeneous Function of X,RNS_Real by A1,LMN6;
consider K being Real such that
X1: 0 <= K &
for v being VECTOR of X holds |. f.v .| <= K * ||. v .||
by DUALSP01:def 9;
for v being VECTOR of X holds ||. g.v .|| <= K * ||. v .||
proof
let v be VECTOR of X;
|. f.v .| <= K * ||. v .|| by X1;
hence ||. g.v .|| <= K * ||. v .|| by EUCLID:def 2;
end;
hence x is Lipschitzian additive homogeneous Function of X,RNS_Real
by X1,LOPBAN_1:def 8;
end;
assume B1: x is Lipschitzian additive homogeneous
Function of X,RNS_Real; then
reconsider g=x as Lipschitzian additive homogeneous
Function of X,RNS_Real;
reconsider f=x as additive homogeneous Function of X,REAL by LMN6,B1;
consider K being Real such that
X1: 0 <= K &
for v being VECTOR of X holds ||. g.v .|| <= K * ||. v .||
by LOPBAN_1:def 8;
for v being VECTOR of X holds |. f.v .| <= K * ||. v .||
proof
let v be VECTOR of X;
||. g.v .|| <= K * ||. v .|| by X1;
hence |. f.v .| <= K * ||. v .|| by EUCLID:def 2;
end; then
f is Lipschitzian additive homogeneous by X1;
hence x is Lipschitzian additive homogeneous Function of X,REAL;
end;
theorem Th75A:
for X be RealNormSpace holds
the carrier of DualSp X
= the carrier of R_NormSpace_of_BoundedLinearOperators(X,RNS_Real)
proof
let X be RealNormSpace;
A1:for x be object holds
x in BoundedLinearFunctionals X iff x in BoundedLinearOperators(X,RNS_Real)
proof
let x be object;
hereby assume x in BoundedLinearFunctionals X; then
x is Lipschitzian additive homogeneous Functional of X
by DUALSP01:def 10; then
x is Lipschitzian additive homogeneous Function of X,RNS_Real by LMN7;
hence x in BoundedLinearOperators(X,RNS_Real) by LOPBAN_1:def 9;
end;
assume x in BoundedLinearOperators(X,RNS_Real); then
x is Lipschitzian LinearOperator of X,RNS_Real by LOPBAN_1:def 9; then
x is Lipschitzian additive homogeneous Functional of X by LMN7;
hence x in BoundedLinearFunctionals X by DUALSP01:def 10;
end;
R_NormSpace_of_BoundedLinearOperators(X,RNS_Real)
= NORMSTR (# BoundedLinearOperators(X,RNS_Real),
Zero_(BoundedLinearOperators(X,RNS_Real),
R_VectorSpace_of_LinearOperators(X,RNS_Real)),
Add_(BoundedLinearOperators(X,RNS_Real),
R_VectorSpace_of_LinearOperators(X,RNS_Real)),
Mult_(BoundedLinearOperators(X,RNS_Real),
R_VectorSpace_of_LinearOperators(X,RNS_Real)),
BoundedLinearOperatorsNorm(X,RNS_Real) #) by LOPBAN_1:def 14;
hence thesis by A1,TARSKI:2;
end;
theorem
for X be RealNormSpace,
x,y be Point of DualSp X,
v,w be Point of R_NormSpace_of_BoundedLinearOperators(X,RNS_Real)
st x=v & y=w holds x + y = v + w
proof
let X be RealNormSpace,
x,y be Point of DualSp X,
v,w be Point of R_NormSpace_of_BoundedLinearOperators(X,RNS_Real);
assume AS: x=v & y=w;
reconsider z=x+y as Point of DualSp X;
reconsider u=v+w as
Point of R_NormSpace_of_BoundedLinearOperators(X,RNS_Real);
BX:R_NormSpace_of_BoundedLinearOperators(X,RNS_Real)
= NORMSTR (# BoundedLinearOperators(X,RNS_Real),
Zero_(BoundedLinearOperators(X,RNS_Real),
R_VectorSpace_of_LinearOperators(X,RNS_Real)),
Add_(BoundedLinearOperators(X,RNS_Real),
R_VectorSpace_of_LinearOperators(X,RNS_Real)),
Mult_(BoundedLinearOperators(X,RNS_Real),
R_VectorSpace_of_LinearOperators(X,RNS_Real)),
BoundedLinearOperatorsNorm(X,RNS_Real) #) by LOPBAN_1:def 14;
A1:z is Lipschitzian additive homogeneous
Function of the carrier of X,REAL by DUALSP01:def 10; then
A5:dom z = the carrier of X by FUNCT_2:def 1;
A2:u is Lipschitzian additive homogeneous Function of X,RNS_Real
by LOPBAN_1:def 9,BX;
for t be object st t in dom z holds z.t = u.t
proof
let t be object;
assume t in dom z; then
reconsider t as VECTOR of X by FUNCT_2:def 1,A1;
z.t = x.t + y.t by DUALSP01:29
.= v.t + w.t by AS,BINOP_2:def 9;
hence thesis by LOPBAN_1:35;
end;
hence thesis by A2,A5,FUNCT_2:def 1;
end;
theorem LMN9:
for X be RealNormSpace,
a be Element of REAL, x be Point of DualSp X,
v be Point of R_NormSpace_of_BoundedLinearOperators(X,RNS_Real)
st x=v holds a*x = a*v
proof
let X be RealNormSpace,
a be Element of REAL, x be Point of DualSp X,
v be Point of R_NormSpace_of_BoundedLinearOperators(X,RNS_Real);
assume AS: x=v;
reconsider z=a*x as Point of DualSp X;
reconsider u=a*v as
Point of R_NormSpace_of_BoundedLinearOperators(X,RNS_Real);
BX:R_NormSpace_of_BoundedLinearOperators(X,RNS_Real)
= NORMSTR (# BoundedLinearOperators(X,RNS_Real),
Zero_(BoundedLinearOperators(X,RNS_Real),
R_VectorSpace_of_LinearOperators(X,RNS_Real)),
Add_(BoundedLinearOperators(X,RNS_Real),
R_VectorSpace_of_LinearOperators(X,RNS_Real)),
Mult_(BoundedLinearOperators(X,RNS_Real),
R_VectorSpace_of_LinearOperators(X,RNS_Real)),
BoundedLinearOperatorsNorm(X,RNS_Real) #) by LOPBAN_1:def 14;
A1:z is Lipschitzian additive homogeneous
Function of the carrier of X,REAL by DUALSP01:def 10; then
A5:dom z = the carrier of X by FUNCT_2:def 1;
A2:u is Lipschitzian additive homogeneous Function of X,RNS_Real
by LOPBAN_1:def 9,BX;
for t be object st t in dom z holds z.t = u.t
proof
let t be object;
assume t in dom z; then
reconsider t as VECTOR of X by FUNCT_2:def 1,A1;
z.t = a*x.t by DUALSP01:30
.= a*v.t by AS,BINOP_2:def 11;
hence thesis by LOPBAN_1:36;
end;
hence thesis by A5,FUNCT_2:def 1,A2;
end;
theorem
for X be RealNormSpace,
x be Point of DualSp X,
v be Point of R_NormSpace_of_BoundedLinearOperators(X,RNS_Real)
st x=v holds -x = -v
proof
let X be RealNormSpace,
x be Point of DualSp X,
v be Point of R_NormSpace_of_BoundedLinearOperators(X,RNS_Real);
assume AS: x=v;
A1: (-1) is Element of REAL by XREAL_0:def 1;
thus -x = (-1)*x by RLVECT_1:16
.= (-1)*v by AS,A1,LMN9
.= -v by RLVECT_1:16;
end;
theorem LMN11:
for X be RealNormSpace,
x be Point of DualSp X,
v be Point of R_NormSpace_of_BoundedLinearOperators(X,RNS_Real)
st x=v holds ||.x.|| = ||.v.||
proof
let X be RealNormSpace,
x be Point of DualSp X,
v be Point of R_NormSpace_of_BoundedLinearOperators(X,RNS_Real);
assume AS: x=v;
BX:R_NormSpace_of_BoundedLinearOperators(X,RNS_Real)
= NORMSTR (# BoundedLinearOperators(X,RNS_Real),
Zero_(BoundedLinearOperators(X,RNS_Real),
R_VectorSpace_of_LinearOperators(X,RNS_Real)),
Add_(BoundedLinearOperators(X,RNS_Real),
R_VectorSpace_of_LinearOperators(X,RNS_Real)),
Mult_(BoundedLinearOperators(X,RNS_Real),
R_VectorSpace_of_LinearOperators(X,RNS_Real)),
BoundedLinearOperatorsNorm(X,RNS_Real) #) by LOPBAN_1:def 14;
reconsider x1=x as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
reconsider v1=v as Lipschitzian LinearOperator of X,RNS_Real
by LOPBAN_1:def 9,BX;
now let r be Real;
assume AS2: r in PreNorms(v1);
PreNorms(v1) = {||.v.t.|| where t is VECTOR of X : ||.t.|| <= 1 }
by LOPBAN_1:def 12; then
consider t be VECTOR of X such that
B1: r = ||. v.t .|| & ||.t.|| <= 1 by AS2;
|. x1.t .| <= ||.x.|| * ||.t.|| by DUALSP01:26; then
B2: ||. v.t .|| <= ||.x.|| * ||.t.|| by AS,EUCLID:def 2;
||.x.|| * ||.t.|| <= ||.x.|| * 1 by B1,XREAL_1:64;
hence r <= ||.x.|| by B1,B2,XXREAL_0:2;
end; then
upper_bound PreNorms(v1) <= ||.x.|| by SEQ_4:45; then
A4: ||.v.|| <= ||.x.|| by BX,LOPBAN_1:30;
now let r be Real;
assume r in PreNorms(x1); then
consider t be VECTOR of X such that
B1: r = |. x.t .| & ||.t.|| <= 1;
||. v1.t .|| <= ||.v.|| * ||.t.|| by LOPBAN_1:32; then
B2: |. x.t .| <= ||.v.|| * ||.t.|| by AS,EUCLID:def 2;
||.v.|| * ||.t.|| <= ||.v.|| * 1 by B1,XREAL_1:64;
hence r <= ||.v.|| by B1,B2,XXREAL_0:2;
end; then
upper_bound PreNorms(x1) <= ||.v.|| by SEQ_4:45; then
||.x.|| <= ||.v.|| by DUALSP01:24;
hence thesis by A4,XXREAL_0:1;
end;
theorem Th75:
for X be RealNormSpace, L be Subset of X
st X is non trivial
& (for f be Point of DualSp X holds
ex Kf be Real st
0 <= Kf
& for x be Point of X st x in L holds |. f.x .| <= Kf)
holds
ex M be Real st 0 <= M
& for x be Point of X st x in L holds ||.x.|| <= M
proof
let X be RealNormSpace, L be Subset of X;
assume
AS: X is non trivial
& for f be Point of DualSp X holds
ex Kf be Real st 0 <= Kf &
for x be Point of X st x in L holds |. f.x .| <= Kf;
set T = (BidualFunc X).:L;
XX:T is Subset of
R_NormSpace_of_BoundedLinearOperators(DualSp X,RNS_Real) by Th75A;
for f be Point of DualSp X
ex Kf be Real st
0 <= Kf &
for g be Point of
R_NormSpace_of_BoundedLinearOperators(DualSp X,RNS_Real)
st g in T holds ||. g.f .|| <= Kf
proof
let f be Point of DualSp X;
consider Kf be Real such that
A0: 0 <= Kf &
for x be Point of X st x in L holds |. f.x .| <= Kf by AS;
for g be Point of R_NormSpace_of_BoundedLinearOperators(DualSp X,RNS_Real)
st g in T holds ||. g.f .|| <= Kf
proof
let g be Point of
R_NormSpace_of_BoundedLinearOperators(DualSp X,RNS_Real);
assume g in T; then
consider x be object such that
A1: x in dom (BidualFunc X) & x in L & g = (BidualFunc X).x
by FUNCT_1:def 6;
reconsider x as Point of X by A1;
A2: |. f.x .| <= Kf by A1,A0;
g = BiDual x by A1,Def2; then
f.x = g.f by Def1;
hence ||. g.f .|| <= Kf by A2,EUCLID:def 2;
end;
hence thesis by A0;
end; then
consider M be Real such that
B0: 0 <= M
& for g be Point of R_NormSpace_of_BoundedLinearOperators(DualSp X,RNS_Real)
st g in T holds ||.g.|| <= M by XX,LOPBAN_5:5;
B1:for x be Point of X st x in L holds ||.x.|| <= M
proof
let x be Point of X;
assume B2: x in L;
x in the carrier of X; then
B3: x in dom(BidualFunc X) by FUNCT_2:def 1;
reconsider g=(BidualFunc X).x as Point of
R_NormSpace_of_BoundedLinearOperators(DualSp X,RNS_Real) by Th75A;
B4: g in T by B2,B3,FUNCT_1:def 6;
||.x.|| = ||. (BidualFunc X).x .|| by AS,LMNORM
.= ||. g .|| by LMN11;
hence thesis by B0,B4;
end;
take M;
thus thesis by B1,B0;
end;
theorem
for X be RealNormSpace, L be non empty Subset of X st
X is non trivial &
( for f be Point of DualSp X holds
ex Y1 be Subset of REAL st
Y1 = {|. f.x .| where x is Point of X : x in L}
& sup Y1 < +infty ) holds
ex Y be Subset of REAL st
Y = {||.x.|| where x is Point of X : x in L}
& sup Y < +infty
proof
let X be RealNormSpace, L be non empty Subset of X;
assume that
A1: X is non trivial and
A2: for f be Point of DualSp X holds
ex Y1 be Subset of REAL st
Y1 = {|. f.x .| where x is Point of X : x in L}
& sup Y1 < +infty;
A3:for f be Point of DualSp X holds
ex Kf be Real st
0 <= Kf
& for x be Point of X st x in L holds |. f.x .| <= Kf
proof
let f be Point of DualSp X;
reconsider f1=f as
Lipschitzian linear-Functional of X by DUALSP01:def 10;
consider Y1 be Subset of REAL such that
B1: Y1 = {|. f.x .| where x is Point of X : x in L}
& sup Y1 < +infty by A2;
reconsider r0=0 as Real;
for r be ExtReal st r in Y1 holds r0 <= r
proof
let r be ExtReal;
assume r in Y1; then
ex x be Point of X st r = |. f.x .| & x in L by B1;
hence r0 <= r by COMPLEX1:46;
end; then
U5: r0 is LowerBound of Y1 by XXREAL_2:def 2; then
U3: r0 <= inf Y1 by XXREAL_2:def 4;
consider x0 be object such that
B11: x0 in L by XBOOLE_0:def 1;
reconsider x0 as Point of X by B11;
set y1=|. f.x0 .|;
y1 in Y1 by B1,B11; then
U6: inf Y1 <= y1 & y1 <= sup Y1 by XXREAL_2:3,4; then
B2: sup Y1 in REAL by B1,U3,XXREAL_0:14;
reconsider Kf=sup Y1 as Real by B2;
BX: for x be Point of X st x in L holds |. f.x .| <= Kf
proof
let x be Point of X;
assume C0: x in L;
reconsider r=|. f.x .| as Real;
r in Y1 by C0,B1;
hence |. f.x .| <= Kf by XXREAL_2:4;
end;
take Kf;
thus thesis by U5,U6,BX,XXREAL_2:def 4;
end;
consider M be Real such that
D1: 0 <= M &
for x be Point of X st x in L holds ||.x.|| <= M by A1,A3,Th75;
set f = 0.(DualSp X);
consider x0 be object such that
B11: x0 in L by XBOOLE_0:def 1;
reconsider x0 as Point of X by B11;
set y1=|. f.x0 .|;
set Y = {||.x.|| where x is Point of X : x in L};
D2: ||.x0.|| in Y by B11;
Y c= REAL
proof
let z be object;
assume z in Y; then
ex x be Point of X st z = ||. x .|| & x in L;
hence z in REAL;
end; then
reconsider Y as non empty Subset of REAL by D2;
for r be ExtReal st r in Y holds r <= M
proof
let r be ExtReal;
assume r in Y; then
ex x be Point of X st r = ||. x .|| & x in L;
hence r <= M by D1;
end; then
M is UpperBound of Y by XXREAL_2:def 1; then
D3:sup Y <= M by XXREAL_2:def 3;
take Y;
M in REAL by XREAL_0:def 1;
hence thesis by D3,XXREAL_0:2,9;
end;
begin :: Reflexivity of Real Normed Spaces
definition
let X be RealNormSpace;
attr X is Reflexive means
BidualFunc X is onto;
end;
theorem REFF1:
for X be RealNormSpace holds X is Reflexive
iff
for f be Point of DualSp DualSp X
ex x be Point of X st
for g be Point of DualSp X holds f.g = g.x
proof
let X be RealNormSpace;
hereby assume X is Reflexive; then
A1: BidualFunc X is onto;
thus for f be Point of DualSp DualSp X
ex x be Point of X st
for g be Point of DualSp X holds f.g = g.x
proof
let f be Point of DualSp DualSp X;
consider x be object such that
A2: x in dom(BidualFunc X) & f = (BidualFunc X).x by A1,FUNCT_1:def 3;
reconsider x as Point of X by A2;
take x;
f = BiDual x by A2,Def2;
hence thesis by Def1;
end;
end;
assume B1: for f be Point of DualSp DualSp X
ex x be Point of X st
for g be Point of DualSp X holds f.g = g.x;
for v being object st v in the carrier of DualSp DualSp X
ex s being object st s in the carrier of X
& v = (BidualFunc X).s
proof
let v be object;
assume v in the carrier of DualSp DualSp X; then
reconsider f = v as Point of DualSp DualSp X;
consider s be Point of X such that
B2: for g be Point of DualSp X holds f.g = g.s by B1;
take s;
thus s in the carrier of X;
f = BiDual s by B2,Def1;
hence v = (BidualFunc X).s by Def2;
end; then
BidualFunc X is onto by FUNCT_2:10;
hence thesis;
end;
theorem
for X be RealNormSpace holds
X is Reflexive iff Im (BidualFunc X) = DualSp DualSp X
proof
let X be RealNormSpace;
thus X is Reflexive implies Im(BidualFunc X) =
DualSp DualSp X by NORMSP_3:46;
assume
A1: Im BidualFunc X = DualSp DualSp X;
dom BidualFunc X <> {} by FUNCT_2:def 1; then
rng BidualFunc X <> {} & rng BidualFunc X is linearly-closed
by NORMSP_3:35,RELAT_1:42; then
the carrier of Lin rng BidualFunc X = rng BidualFunc X by NORMSP_3:31;
then
BidualFunc X is onto by A1;
hence X is Reflexive;
end;
theorem
for X be RealNormSpace st X is non trivial Reflexive holds
X is RealBanachSpace
proof
let X be RealNormSpace;
assume AS: X is non trivial Reflexive; then
P1:BidualFunc X is onto;
for seq be sequence of X
st seq is Cauchy_sequence_by_Norm holds seq is convergent
proof
let seq be sequence of X;
assume P2: seq is Cauchy_sequence_by_Norm;
reconsider seq1= (BidualFunc X) * seq as sequence of DualSp DualSp X;
XX:BidualFunc X is additive homogeneous;
for r be Real st r > 0
ex k be Nat st for n, m be Nat st n >= k & m >= k
holds ||.(seq1.n) - (seq1.m).|| < r
proof
let r be Real;
assume r > 0; then
consider k be Nat such that
A1: for n, m be Nat st n >= k & m >= k
holds ||.(seq.n) - (seq.m).|| < r by P2,RSSPACE3:8;
AK: for n, m be Nat st n >= k & m >= k holds ||.(seq1.n) - (seq1.m).|| < r
proof
let n, m be Nat;
assume n >= k & m >= k; then
A2: ||.(seq.n) - (seq.m).|| < r by A1;
n in NAT & m in NAT by ORDINAL1:def 12; then
n in dom seq & m in dom seq by FUNCT_2:def 1; then
A4: seq1.n = (BidualFunc X).(seq.n)
& seq1.m = (BidualFunc X).(seq.m) by FUNCT_1:13;
seq.n - seq.m = seq.n + (-1)*seq.m by RLVECT_1:16; then
A7: (BidualFunc X).(seq.n - seq.m)
= (BidualFunc X).(seq.n) + (BidualFunc X).((-1)*seq.m) by XX;
(BidualFunc X).((-1)*seq.m)
= (-1)*(BidualFunc X).(seq.m) by LOPBAN_1:def 5; then
(BidualFunc X).(seq.n - seq.m)
= (BidualFunc X).(seq.n) - (BidualFunc X).(seq.m) by A7,RLVECT_1:16;
hence thesis by A2,AS,A4,LMNORM;
end;
take k;
thus thesis by AK;
end; then
P5:seq1 is convergent by LOPBAN_1:def 15,RSSPACE3:8;
consider s be Point of X such that
P7: lim seq1 = (BidualFunc X).s by P1,FUNCT_2:113;
for r be Real st 0 < r ex m be Nat st for n be Nat
st m <= n holds ||.(seq.n) - s .|| < r
proof
let r be Real;
assume 0 < r; then
consider m be Nat such that
B1: for n be Nat st m <= n holds ||.(seq1.n) - lim seq1 .|| < r
by P5,NORMSP_1:def 7;
BK: for n be Nat st m <= n holds ||.(seq.n) - s .|| < r
proof
let n be Nat;
assume m <= n; then
B2: ||.(seq1.n) - lim seq1 .|| < r by B1;
n in NAT by ORDINAL1:def 12; then
n in dom seq by FUNCT_2:def 1; then
B4: seq1.n = (BidualFunc X).(seq.n) by FUNCT_1:13;
seq.n - s = seq.n + (-1)*s by RLVECT_1:16; then
B6: (BidualFunc X).(seq.n - s)
= (BidualFunc X).(seq.n) + (BidualFunc X).((-1)*s) by XX;
(BidualFunc X).((-1)*s)
= (-1)*(BidualFunc X).s by LOPBAN_1:def 5; then
(BidualFunc X).(seq.n - s)
= (BidualFunc X).(seq.n) - (BidualFunc X).s by B6,RLVECT_1:16;
hence thesis by B2,AS,P7,B4,LMNORM;
end;
take m;
thus thesis by BK;
end;
hence seq is convergent;
end;
hence thesis by LOPBAN_1:def 15;
end;
theorem Th76:
for X be RealBanachSpace, M be non empty Subset of X st
X is Reflexive & M is linearly-closed closed holds
NLin(M) is Reflexive
proof
let X be RealBanachSpace, M be non empty Subset of X;
assume that
A2: X is Reflexive and
A3: M is linearly-closed and
A4: M is closed;
set M0 = NLin(M);
X1:the carrier of M0 = M by NORMSP_3:31,A3;
X2:the carrier of M0 c= the carrier of X by DUALSP01:def 16;
for y be Point of DualSp DualSp M0
ex x be Point of M0 st
for g be Point of DualSp M0 holds y.g = g.x
proof
let y be Point of DualSp DualSp M0;
reconsider y1=y as Lipschitzian linear-Functional of DualSp M0
by DUALSP01:def 10;
defpred P[Function,Function] means $2=$1|M;
P0: for x be Element of DualSp X ex y be Element of DualSp M0
st P[x,y]
proof
let x be Element of DualSp X;
reconsider x0=x as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
reconsider y0=x0|M as Function of M0,REAL by X1,FUNCT_2:32;
B1: y0 is additive
proof
let s,t be Point of M0;
reconsider s1=s, t1=t as Point of X by X2;
C1: s+t = s1+t1 by NORMSP_3:28;
thus y0.(s+t) = x0.(s+t) by X1,FUNCT_1:49
.= x0.s1 + x0.t1 by C1,HAHNBAN:def 2
.= (x0|M).s + x0.t by X1,FUNCT_1:49
.= y0.s + y0.t by X1,FUNCT_1:49;
end;
B2: y0 is homogeneous
proof
let s be Point of M0, r be Real;
reconsider s1=s as Point of X by X2;
C2: r*s = r*s1 by NORMSP_3:28;
thus y0.(r*s) = x0.(r*s) by X1,FUNCT_1:49
.= r*x0.s by C2,HAHNBAN:def 3
.= r*y0.s by X1,FUNCT_1:49;
end;
for s be Point of M0 holds |. y0.s .| <= ||. x .|| * ||. s .||
proof
let s be Point of M0;
reconsider s1=s as Point of X by X2;
C3: ||. s .|| = ||. s1 .|| by NORMSP_3:28;
|. y0.s .| = |. x0.s .| by X1,FUNCT_1:49;
hence thesis by C3,DUALSP01:26;
end; then
y0 is Lipschitzian; then
reconsider y=y0 as Element of DualSp M0 by B1,B2,DUALSP01:def 10;
take y;
thus y = x|M;
end;
consider T be Function of DualSp X, DualSp M0 such that
P11: for x being Element of DualSp X holds P[x,T.x] from FUNCT_2:sch 3(P0);
D1: T is additive
proof
let f,g be Point of DualSp X;
E1: T.(f+g) is Function of M0,REAL
& T.f + T.g is Function of M0,REAL by DUALSP01:def 10;
for x be Point of M0 holds (T.(f+g)).x = (T.f + T.g).x
proof
let x be Point of M0;
reconsider x1=x as Point of X by X2;
T.f = f|M & T.g = g|M by P11; then
reconsider fm=f|M, gm=g|M as Point of DualSp M0;
F2: fm.x = f.x & gm.x = g.x by X1,FUNCT_1:49;
thus (T.(f+g)).x = ((f+g)|M).x by P11
.= (f+g).x by X1,FUNCT_1:49
.= f.x1 + g.x1 by DUALSP01:29
.= (T.f).x + gm.x by P11,F2
.= (T.f).x + (T.g).x by P11
.= (T.f + T.g).x by DUALSP01:29;
end;
hence T.(f+g) = T.f + T.g by E1,FUNCT_2:def 8;
end;
T is homogeneous
proof
let f be Point of DualSp X, r be Real;
E3: T.(r*f) is Function of M0,REAL
& r*(T.f) is Function of M0,REAL by DUALSP01:def 10;
for x be Point of M0 holds (T.(r*f)).x = (r*(T.f)).x
proof
let x be Point of M0;
reconsider x1=x as Point of X by X2;
T.f = f|M by P11; then
reconsider fm=f|M as Point of DualSp M0;
F4: fm.x = f.x by X1,FUNCT_1:49;
thus (T.(r*f)).x = ((r*f)|M).x by P11
.= (r*f).x by X1,FUNCT_1:49
.= r*(f.x1) by DUALSP01:30
.= r*((T.f).x) by P11,F4
.= (r*(T.f)).x by DUALSP01:30;
end;
hence T.(r*f) = r*(T.f) by E3,FUNCT_2:def 8;
end; then
reconsider T as LinearOperator of DualSp X, DualSp M0 by D1;
for v be Point of DualSp X holds ||. T.v .|| <= 1*||.v.||
proof
let v be Point of DualSp X;
reconsider v1=v as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
B0: T.v = v|M by P11; then
reconsider vm=v|M as Point of DualSp M0;
reconsider vm1=vm as Lipschitzian linear-Functional of M0
by DUALSP01:def 10;
now let r be Real;
assume r in PreNorms(vm1); then
consider t be VECTOR of M0 such that
B1: r = |. vm1.t .| & ||. t .|| <= 1;
reconsider t1=t as Point of X by X2;
B2: |. vm.t .| = |. v.t1 .| by X1,FUNCT_1:49;
||. t1 .|| = ||. t .|| by NORMSP_3:28;
hence r in PreNorms(v1) by B1,B2;
end; then
PreNorms(vm1) c= PreNorms(v1); then
upper_bound PreNorms(vm1)
<= upper_bound PreNorms(v1) by SEQ_4:48; then
||. vm .|| <= upper_bound PreNorms(v1) by DUALSP01:24;
hence ||. T.v .|| <= 1*||. v .|| by B0,DUALSP01:24;
end; then
reconsider T as Lipschitzian LinearOperator of DualSp X, DualSp M0
by LOPBAN_1:def 8;
P2: for f be Point of DualSp X, x be Point of X
st x in M holds (T.f).x = f.x
proof
let f be Point of DualSp X, x be Point of X;
assume x in M; then
(f|M).x = f.x by FUNCT_1:49;
hence thesis by P11;
end;
deffunc F(Element of DualSp X) = y.(T.$1);
consider z be Function of the carrier of DualSp X, REAL such that
Q10: for f be Element of the carrier of DualSp X holds z.f = F(f)
from FUNCT_2:sch 4;
Q11:z is additive
proof
let s,t be Point of DualSp X;
thus z.(s+t) = y.(T.(s+t)) by Q10
.= y.(T.s + T.t) by VECTSP_1:def 20
.= y1.(T.s) + y1.(T.t) by HAHNBAN:def 2
.= z.s + y.(T.t) by Q10
.= z.s + z.t by Q10;
end;
Q12:z is homogeneous
proof
let s be Point of DualSp X, r be Real;
thus z.(r*s) = y.(T.(r*s)) by Q10
.= y.(r*(T.s)) by LOPBAN_1:def 5
.= r*y1.(T.s) by HAHNBAN:def 3
.= r*(z.s) by Q10;
end;
R_NormSpace_of_BoundedLinearOperators(DualSp X,DualSp M0)
= NORMSTR (# BoundedLinearOperators(DualSp X,DualSp M0),
Zero_(BoundedLinearOperators(DualSp X,DualSp M0),
R_VectorSpace_of_LinearOperators(DualSp X,DualSp M0)),
Add_(BoundedLinearOperators(DualSp X,DualSp M0),
R_VectorSpace_of_LinearOperators(DualSp X,DualSp M0)),
Mult_(BoundedLinearOperators(DualSp X,DualSp M0),
R_VectorSpace_of_LinearOperators(DualSp X,DualSp M0)),
BoundedLinearOperatorsNorm(DualSp X,DualSp M0) #)
by LOPBAN_1:def 14; then
reconsider T1=T as Point of
R_NormSpace_of_BoundedLinearOperators(DualSp X,DualSp M0)
by LOPBAN_1:def 9;
for s be Point of DualSp X holds
|. z.s .| <= ||. y .|| * ||. T1 .|| * ||. s .||
proof
let s be Point of DualSp X;
B1: |. z.s .| = |. y.(T.s) .| by Q10;
B2: |. y1.(T.s) .| <= ||. y .||*||. T.s .|| by DUALSP01:26;
||. y .|| * ||. T.s .|| <= ||. y .|| * (||. T1 .|| * ||. s .||)
by XREAL_1:64,LOPBAN_1:32;
hence thesis by B1,B2,XXREAL_0:2;
end; then
z is Lipschitzian; then
reconsider z as Point of DualSp DualSp X by Q11,Q12,DUALSP01:def 10;
consider x be Point of X such that
Q2: for f be Point of DualSp X holds z.f = f.x by A2,REFF1;
Q3: for f be Point of DualSp X holds y.(T.f) = f.x
proof
let f be Point of DualSp X;
thus y.(T.f) = z.f by Q10
.= f.x by Q2;
end;
AX: x in the carrier of M0
proof
assume not x in the carrier of M0; then
consider f be Point of DualSp X such that
B1: (for x be Point of X st x in M holds (Bound2Lipschitz(f,X)).x = 0) and
B2: (Bound2Lipschitz(f,X)).x = 1 by A3,A4,X1,Lm64;
reconsider f1=f as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
B3: f1 = (Bound2Lipschitz(f,X)) by DUALSP01:23;
B4: for x be Point of X st x in M holds (T.f).x = 0
proof
let x be Point of X;
assume C1: x in M; then
f.x = 0 by B1,B3;
hence thesis by C1,P2;
end;
B8: T.f is Function of M0,REAL by DUALSP01:def 10;
for x be Point of M0 holds (T.f).x = (M --> 0).x
proof
let x be Point of M0;
x in M by X1; then
reconsider x1=x as Point of X;
(T.f).x1 = 0 by X1,B4;
hence thesis by X1,FUNCOP_1:7;
end; then
B9: T.f = M --> 0 by X1,B8,FUNCT_2:def 8
.= 0.(DualSp M0) by X1,DUALSP01:25;
f.x = y1.(0.(DualSp M0)) by B9,Q3
.= 0 by HAHNBAN:20;
hence contradiction by B2,B3;
end;
Q4: for f be Point of DualSp X holds y.(T.f) = (T.f).x
proof
let f be Point of DualSp X;
y.(T.f) = f.x by Q3;
hence thesis by P2,X1,AX;
end;
Q5: for f be Point of DualSp X holds y.(f|M) = (f|M).x
proof
let f be Point of DualSp X;
T.f = f|M by P11;
hence thesis by Q4;
end;
for g be Point of DualSp M0 holds y.g = g.x
proof
let g be Point of DualSp M0;
reconsider g1=g as Lipschitzian linear-Functional of M0
by DUALSP01:def 10;
ex f1 be Lipschitzian linear-Functional of X,
f be Point of DualSp X st
f1 = f & f1|(the carrier of M0) = g1 & ||.f.||=||.g.|| by DUALSP01:36;
hence thesis by X1,Q5;
end;
hence thesis by AX;
end;
hence thesis by REFF1;
end;
theorem NISOM08:
for X,Y be RealNormSpace,
L be Lipschitzian LinearOperator of X,Y,
y be Lipschitzian linear-Functional of Y
holds y*L is Lipschitzian linear-Functional of X
proof
let X,Y be RealNormSpace,
L be Lipschitzian LinearOperator of X,Y,
y be Lipschitzian linear-Functional of Y;
consider M being Real such that
AS1: 0 <= M &
for x being VECTOR of X holds
||. L.x .|| <= M * ||. x .|| by LOPBAN_1:def 8;
D1:dom L = the carrier of X by FUNCT_2:def 1;
set x = y * L;
P6:for v,w be VECTOR of X holds x.(v+w) = x.v + x.w
proof
let v,w be VECTOR of X;
thus x.(v+w) = y.(L.(v+w)) by D1,FUNCT_1:13
.= y.(L.v+L.w) by VECTSP_1:def 20
.= y.(L.v) + y.(L.w) by HAHNBAN:def 2
.= x.v + y.(L.w) by D1,FUNCT_1:13
.= x.v + x.w by D1,FUNCT_1:13;
end;
for v being VECTOR of X, r being Real holds x.(r*v) = r*x.v
proof
let v be VECTOR of X, r be Real;
thus x.(r*v) = y.(L.(r*v)) by D1,FUNCT_1:13
.= y.(r*L.v) by LOPBAN_1:def 5
.= r*y.(L.v) by HAHNBAN:def 3
.= r*x.v by D1,FUNCT_1:13;
end; then
reconsider x as linear-Functional of X by P6,HAHNBAN:def 2,def 3;
consider N be Real such that
P7: 0 <= N &
for v be VECTOR of Y holds |. y.v .| <= N * ||. v .||
by DUALSP01:def 9;
for v be VECTOR of X holds |. x.v .| <= (M*N) * ||. v .||
proof
let v be VECTOR of X;
P8: |.x.v.| = |. y.(L.v) .| by D1,FUNCT_1:13;
P9: |. y.(L.v) .| <= N * ||. (L.v) .|| by P7;
N*||. (L.v) .|| <= N*(M* ||. v .|| ) by AS1,P7,XREAL_1:64;
hence thesis by P8,P9,XXREAL_0:2;
end;
hence thesis by DUALSP01:def 9,AS1,P7;
end;
theorem NISOM09:
for X,Y be RealNormSpace,
L be Lipschitzian LinearOperator of X,Y
st L is isomorphism holds
ex T be Lipschitzian LinearOperator of DualSp X,DualSp Y st
T is isomorphism
& for x be Point of DualSp X holds T.x = x*(L")
proof
let X,Y be RealNormSpace,
L be Lipschitzian LinearOperator of X,Y;
assume AS: L is isomorphism; then
AS1: L is one-to-one & L is onto
& for x be Point of X holds ||.x.|| = ||. L.x .||;
consider K be Lipschitzian LinearOperator of Y,X such that
AS2: K = L" & K is isomorphism by AS,NORMSP_3:37;
D1:dom K = the carrier of Y by FUNCT_2:def 1;
defpred P[Function,Function] means $2=$1 * K;
P0:for x being Element of DualSp X ex y being Element of DualSp Y st P[x,y]
proof
let x being Element of DualSp X;
x is Lipschitzian linear-Functional of X by DUALSP01:def 10; then
x * K is Lipschitzian linear-Functional of Y by NISOM08; then
reconsider y=x*K as Element of DualSp Y by DUALSP01:def 10;
take y;
thus y = x* K;
end;
consider T be Function of DualSp X, DualSp Y such that
P1: for x being Element of DualSp X holds P[x,T.x]
from FUNCT_2:sch 3(P0);
for v,w be Point of DualSp X holds T.(v+w) = T.v + T.w
proof
let v,w be Point of DualSp X;
P21:T.v = v*K & T.w = w*K & T.(v+w) = (v+w)*K by P1;
for t be VECTOR of Y holds (T.(v+w)).t = (T.v).t + (T.w).t
proof
let t be VECTOR of Y;
thus (T.(v+w)).t = (v+w).(K.t) by P21,D1,FUNCT_1:13
.= v.(K.t) + w.(K.t) by DUALSP01:29
.= (T.v).t + w.(K.t) by P21,D1,FUNCT_1:13
.= (T.v).t + (T.w).t by P21,D1,FUNCT_1:13;
end;
hence thesis by DUALSP01:29;
end; then
P3:T is additive;
for v be Point of DualSp X, r be Real holds T.(r*v) = r*T.v
proof
let v be Point of DualSp X,r be Real;
P21:T.v = v*K & T.(r*v) = (r*v)*K by P1;
for t be VECTOR of Y holds (T.(r*v)).t = r*(T.v).t
proof
let t be VECTOR of Y;
thus (T.(r*v)).t = (r*v).(K.t) by P21,D1,FUNCT_1:13
.= r*(v.(K.t)) by DUALSP01:30
.= r*(T.v).t by P21,D1,FUNCT_1:13;
end;
hence thesis by DUALSP01:30;
end; then
reconsider T as LinearOperator of DualSp X, DualSp Y by P3,LOPBAN_1:def 5;
for v being object st v in the carrier of DualSp Y
ex s being object st s in the carrier of DualSp X & v = T.s
proof
let v be object;
assume v in the carrier of DualSp Y; then
reconsider y = v as Lipschitzian linear-Functional of Y
by DUALSP01:def 10;
y * L is Lipschitzian linear-Functional of X by NISOM08; then
reconsider s=y*L as Point of DualSp X by DUALSP01:def 10;
take s;
G6: dom y = the carrier of Y by FUNCT_2:def 1;
T.s = s*K by P1
.= y*(L*K) by RELAT_1:36
.= y *(id rng L) by AS2,AS,FUNCT_1:39
.= v by G6,AS1,RELAT_1:51;
hence thesis;
end; then
XX:T is onto by FUNCT_2:10;
P5:for v be Point of DualSp X holds ||. T.v .|| = ||.v.||
proof
let v be Point of DualSp X;
P21:T.v = v * K by P1;
reconsider y=T.v as Lipschitzian linear-Functional of Y
by DUALSP01:def 10;
reconsider x=v as Lipschitzian linear-Functional of X
by DUALSP01:def 10;
for z be object holds z in PreNorms(x) iff z in PreNorms(y)
proof
let z be object;
hereby assume z in PreNorms(x); then
consider t be VECTOR of X such that
B2: z=|.x.t.| & ||.t.|| <= 1;
D1: dom L = the carrier of X by FUNCT_2:def 1;
D2: dom K = the carrier of Y by FUNCT_2:def 1;
set s = L.t;
K.s = t by AS,AS2,D1,FUNCT_1:34; then
A81: z = |.y.s.| by P21,D2,B2,FUNCT_1:13;
||. s .|| = ||. t .|| by AS;
hence z in PreNorms(y) by A81,B2;
end;
assume z in PreNorms(y); then
consider s be VECTOR of Y such that
B2: z=|.y.s.| & ||.s.|| <= 1;
set t = K.s;
dom K = the carrier of Y by FUNCT_2:def 1; then
A81: z = |. x.t .| by B2,P21,FUNCT_1:13;
||. s .|| = ||. t .|| by AS2;
hence z in PreNorms(x) by A81,B2;
end; then
A9: PreNorms(x) = PreNorms(y);
thus ||. v .||
= upper_bound PreNorms(Bound2Lipschitz(v,X)) by DUALSP01:def 14
.= upper_bound PreNorms(y) by A9,DUALSP01:23
.= upper_bound PreNorms(Bound2Lipschitz(y,Y)) by DUALSP01:23
.= ||. T.v .|| by DUALSP01:def 14;
end; then
for v be Point of DualSp X holds ||. T.v .|| <= 1*||. v .||; then
reconsider T as
Lipschitzian LinearOperator of DualSp X, DualSp Y by LOPBAN_1:def 8;
take T;
for x1,x2 being object st x1 in the carrier of DualSp X
& x2 in the carrier of DualSp X
& T.x1 = T.x2 holds x1 = x2
proof
let x1,x2 be object;
assume A1: x1 in the carrier of DualSp X
& x2 in the carrier of DualSp X & T.x1 = T.x2; then
reconsider v1=x1, v2=x2 as Point of DualSp X;
T.(v1-v2) = T.(v1+(-1)*v2) by RLVECT_1:16
.= T.(v1)+T.((-1)*v2) by VECTSP_1:def 20
.= T.(v1)+(-1)*T.v2 by LOPBAN_1:def 5
.= T.v1 + -T.v2 by RLVECT_1:16
.= 0.(DualSp Y) by RLVECT_1:5,A1; then
||. T.(v1-v2) .|| = 0; then
||. v1-v2 .|| = 0 by P5;
hence thesis by NORMSP_1:6;
end;
hence thesis by P5,XX,P1,AS2,FUNCT_2:19;
end;
NISOM11:
for X,Y be RealNormSpace
st ex L be Lipschitzian LinearOperator of X,Y st L is isomorphism holds
(X is Reflexive implies Y is Reflexive)
proof
let X,Y be RealNormSpace;
assume ex L be Lipschitzian LinearOperator of X,Y
st L is isomorphism; then
consider L be Lipschitzian LinearOperator of X,Y such that
AS: L is isomorphism;
AS2:L is one-to-one onto
& for x be Point of X holds ||. x .|| = ||. L.x .|| by AS;
consider T be Lipschitzian LinearOperator of DualSp X, DualSp Y such that
AS1: T is isomorphism
& for x be Point of DualSp X holds T.x = x*(L") by NISOM09,AS;
DT:dom T = the carrier of DualSp X by FUNCT_2:def 1;
assume X is Reflexive; then
P1:BidualFunc X is onto;
for y being object st y in the carrier of DualSp DualSp Y
ex x being object st x in the carrier of Y & y = (BidualFunc Y).x
proof
let y being object;
assume y in the carrier of DualSp DualSp Y; then
reconsider v = y as Point of DualSp DualSp Y;
reconsider v as Lipschitzian linear-Functional of DualSp Y
by DUALSP01:def 10;
v * T is Lipschitzian linear-Functional of DualSp X by NISOM08; then
reconsider s=v*T as Point of DualSp DualSp X by DUALSP01:def 10;
consider t being object such that
P2: t in the carrier of X & (BidualFunc X).t = s by P1,FUNCT_2:11;
reconsider t as Point of X by P2;
set u = L.t;
take u;
for z be Point of DualSp Y holds v.z = z.u
proof
let z be Point of DualSp Y;
reconsider z0=z as Lipschitzian linear-Functional of Y
by DUALSP01:def 10;
z0*L is Lipschitzian linear-Functional of X by NISOM08; then
reconsider q=z0*L as Point of DualSp X by DUALSP01:def 10;
R1: (BiDual t) = s by P2,Def2;
G4: dom L = the carrier of X by FUNCT_2:def 1;
z is Lipschitzian linear-Functional of Y by DUALSP01:def 10; then
G6: dom z = the carrier of Y by FUNCT_2:def 1;
G7: s.q = v.(T.q) by DT, FUNCT_1:13
.= v.(q*L") by AS1
.= v.(z0*(L*L")) by RELAT_1:36
.= v.(z0*(id rng L)) by AS,FUNCT_1:39
.= v.z by G6,AS2,RELAT_1:51;
s.q = (z0*L).t by R1,Def1
.= z.u by G4,FUNCT_1:13;
hence thesis by G7;
end; then
y = BiDual u by Def1;
hence thesis by Def2;
end; then
BidualFunc Y is onto by FUNCT_2:10;
hence Y is Reflexive;
end;
theorem
for X,Y be RealNormSpace,
L be Lipschitzian LinearOperator of X,Y,
T be Lipschitzian LinearOperator of DualSp X, DualSp Y st
L is isomorphism & T is isomorphism
& for x be Point of DualSp X holds T.x = x*(L") holds
ex S be Lipschitzian LinearOperator of DualSp Y, DualSp X
st S is isomorphism
& S = T"
& for y be Point of DualSp Y holds S.y = y*L
proof
let X,Y be RealNormSpace,
L be Lipschitzian LinearOperator of X,Y,
T be Lipschitzian LinearOperator of DualSp X, DualSp Y;
assume AS1: L is isomorphism & T is isomorphism
& for x be Point of DualSp X holds T.x = x*(L"); then
AS2: L is one-to-one onto
& for x be Point of X holds ||.x.|| = ||. L.x .||;
consider K be Lipschitzian LinearOperator of Y,X such that
AS3: K = L" & K is isomorphism by AS1,NORMSP_3:37;
AS4: T is one-to-one & T is onto
& for x be Point of DualSp X holds ||.x.|| = ||. T.x .|| by AS1;
consider S be Lipschitzian LinearOperator of DualSp Y, DualSp X such that
AS5: S is isomorphism
& for y be Point of DualSp Y holds S.y = y*(K") by NISOM09,AS3;
take S;
P2:K" = L by FUNCT_1:43,AS1,AS3;
for y,x being object holds
y in the carrier of DualSp Y & S.y = x
iff x in the carrier of DualSp X & T.x = y
proof
let y,x be object;
hereby assume P31: y in the carrier of DualSp Y & S.y = x;
hence x in the carrier of DualSp X by FUNCT_2:5;
reconsider yp=y as Point of DualSp Y by P31;
reconsider xp=x as Point of DualSp X by P31,FUNCT_2:5;
yp is linear-Functional of Y by DUALSP01:def 10; then
G6: dom yp = the carrier of Y by FUNCT_2:def 1;
thus T.x = xp*(L") by AS1
.= (yp*L)*(L") by P2,AS5,P31
.= yp*(L*L") by RELAT_1:36
.= yp *(id rng L) by AS1,FUNCT_1:39
.= y by G6,AS2,RELAT_1:51;
end;
assume P32: x in the carrier of DualSp X & T.x = y;
hence y in the carrier of DualSp Y by FUNCT_2:5;
reconsider yp=y as Point of DualSp Y by P32,FUNCT_2:5;
reconsider xp=x as Point of DualSp X by P32;
G5: dom L = the carrier of X by FUNCT_2:def 1;
xp is linear-Functional of X by DUALSP01:def 10; then
G6: dom xp = the carrier of X by FUNCT_2:def 1;
thus S.y = yp*L by P2,AS5
.= (xp*(L)")*L by AS1,P32
.= xp*(L"*L) by RELAT_1:36
.= xp *(id dom L) by AS1,FUNCT_1:39
.= x by G6,G5,RELAT_1:51;
end;
hence thesis by AS5,P2,FUNCT_2:28,AS4;
end;
theorem NISOM12:
for X,Y be RealNormSpace
st ex L be Lipschitzian LinearOperator of X,Y
st L is isomorphism holds
(X is Reflexive iff Y is Reflexive)
proof
let X,Y be RealNormSpace;
given L be Lipschitzian LinearOperator of X,Y such that
AS: L is isomorphism;
ex K be Lipschitzian LinearOperator of Y,X st
K = L" & K is isomorphism by AS,NORMSP_3:37;
hence thesis by AS,NISOM11;
end;
theorem Th74A:
for X be RealNormSpace st X is non trivial holds
ex L be Lipschitzian LinearOperator of X, Im(BidualFunc X)
st L is isomorphism
proof
let X be RealNormSpace;
assume X is non trivial; then
consider DuX be SubRealNormSpace of DualSp DualSp X,
L be Lipschitzian LinearOperator of X, DuX such that
A1: L is bijective & DuX = Im(BidualFunc X)
& (for x be Point of X holds L.x = BiDual x)
& for x be Point of X holds ||.x.|| = ||. L.x .|| by IMDDX;
L is isomorphism by A1;
hence thesis by A1;
end;
Lm77R:
for X be RealBanachSpace st X is non trivial holds
X is Reflexive implies DualSp X is Reflexive
proof
let X be RealBanachSpace;
assume AS: X is non trivial;
thus X is Reflexive implies DualSp X is Reflexive
proof
assume AS1: X is Reflexive;
for f be Point of DualSp DualSp DualSp X
ex h be Point of DualSp X st
for g be Point of DualSp DualSp X holds f.g = g.h
proof
let f be Point of DualSp DualSp DualSp X;
reconsider f1=f as Lipschitzian linear-Functional of DualSp DualSp X
by DUALSP01:def 10;
deffunc F(Element of X) = f.(BiDual $1);
P0: ex h be Function of the carrier of X,REAL st
for x be Element of X holds h.x = F(x) from FUNCT_2:sch 4;
consider h be Function of the carrier of X,REAL such that
P1: for x be Point of X holds h.x = f.(BiDual x) by P0;
P2: h is additive
proof
let x,y be Point of X;
set g0 = BidualFunc X;
C2: g0 is additive homogeneous;
thus h.(x+y) = f.(BiDual(x+y)) by P1
.= f.(g0.(x+y)) by Def2
.= f.(g0.x + g0.y) by C2
.= f1.(g0.x) + f1.(g0.y) by HAHNBAN:def 2
.= f.(BiDual x) + f.(g0.y) by Def2
.= f.(BiDual x) + f.(BiDual y) by Def2
.= h.x + f.(BiDual y) by P1
.= h.x + h.y by P1;
end;
P3: h is homogeneous
proof
let x be Point of X, r be Real;
set g0 = BidualFunc X;
thus h.(r*x) = f.(BiDual(r*x)) by P1
.= f.(g0.(r*x)) by Def2
.= f.(r*g0.x) by LOPBAN_1:def 5
.= r*f1.(g0.x) by HAHNBAN:def 3
.= r*f.(BiDual x) by Def2
.= r*h.x by P1;
end;
for x be Point of X holds |. h.x .| <= ||. f .|| * ||. x .||
proof
let x be Point of X;
set g0 = BidualFunc X;
P5: h.x = f.(BiDual x) by P1
.= f.(g0.x) by Def2;
|. f1.(g0.x) .| <= ||. f .|| * ||. g0.x .|| by DUALSP01:26;
hence thesis by P5,AS,LMNORM;
end; then
h is Lipschitzian; then
h is Point of DualSp X by P2,P3,DUALSP01:def 10; then
consider h be Point of DualSp X such that
B1: for x be Point of X holds h.x = f.(BiDual x) by P1;
B2: BidualFunc X is onto by AS1;
set g0 = BidualFunc X;
BX: for g be Point of DualSp DualSp X holds f.g = g.h
proof
let g be Point of DualSp DualSp X;
consider x be object such that
C1: x in dom g0 & g = g0.x by B2,FUNCT_1:def 3;
reconsider x as Point of X by C1;
f.(BiDual x) = h.x by B1
.= (BiDual x).h by Def1;
hence f.g = (BiDual x).h by C1,Def2
.= g.h by C1,Def2;
end;
take h;
thus thesis by BX;
end;
hence DualSp X is Reflexive by REFF1;
end;
end;
theorem
for X be RealBanachSpace st X is non trivial holds
X is Reflexive iff DualSp X is Reflexive
proof
let X be RealBanachSpace;
assume AS: X is non trivial;
hence X is Reflexive implies DualSp X is Reflexive by Lm77R;
assume AS2: DualSp X is Reflexive;
DualSp X is non trivial by AS,Lm65A1; then
C2: DualSp DualSp X is Reflexive by AS2,Lm77R;
consider L be Lipschitzian LinearOperator of X, Im(BidualFunc X)
such that
C3: L is isomorphism by AS,Th74A;
set f = BidualFunc X;
set V = DualSp DualSp X;
D0: rng f is linearly-closed by NORMSP_3:35;
D1: rng f <> {}
proof
assume rng f = {}; then
dom f = {} by RELAT_1:42;
hence thesis by FUNCT_2:def 1;
end; then
C4: the carrier of Im(f) = rng f by NORMSP_3:31,D0;
Im(f) is complete by C3,NORMSP_3:44; then
rng f is closed by C4,NORMSP_3:48; then
Im(f) is Reflexive by C2,D0,Th76,D1;
hence X is Reflexive by C3,NISOM12;
end;