:: Banach's Continuous Inverse Theorem and Closed Graph Theorem
:: by Hideki Sakurai , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 6, 2012
:: Copyright (c) 2012-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 NUMBERS, CARD_1, XXREAL_0, ARYTM_3, RELAT_1, ARYTM_1, XBOOLE_0,
SUBSET_1, FUNCT_1, ZFMISC_1, NORMSP_1, RLSUB_1, RSSPACE, COHSP_1,
PRE_TOPC, METRIC_1, SUPINF_2, TARSKI, REAL_1, COMPLEX1, LOPBAN_1,
STRUCT_0, NORMSP_2, RCOMP_1, NAT_1, CARD_3, ORDINAL2, SEQ_2, RSSPACE3,
FUNCT_2, UNIALG_1, PARTFUN1, FCONT_1, CFCONT_1, RLVECT_1, TMAP_1,
MSSUBFAM, RELAT_2, RLTOPSP1, REWRITE1, FINSEQ_1, NORMSP_0, ALGSTR_0,
LOPBAN_7, REALSET1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, REALSET1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0,
COMPLEX1, FUNCT_3, FINSEQ_1, FINSEQ_2, STRUCT_0, ALGSTR_0, PRE_TOPC,
RLVECT_1, RLSUB_1, VECTSP_1, NORMSP_0, NORMSP_1, T_0TOPSP, TMAP_1,
RLTOPSP1, RSSPACE, EUCLID, RSSPACE3, LOPBAN_1, NFCONT_1, NORMSP_2,
PDIFF_1, PRVECT_3;
constructors REAL_1, PCOMPS_1, RUSUB_4, NFCONT_1, FUNCT_3, NEWTON, NORMSP_2,
RSSPACE3, T_0TOPSP, RELSET_1, TMAP_1, PRVECT_3, PDIFF_1, REALSET1;
registrations XREAL_0, XXREAL_0, ORDINAL1, RELSET_1, STRUCT_0, NAT_1,
NORMSP_1, NORMSP_2, FUNCT_1, FUNCT_2, LOPBAN_1, NORMSP_0, RELAT_1,
RLTOPSP1, PRVECT_3, NUMBERS, XBOOLE_0, VALUED_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, FUNCT_2, LOPBAN_1, VECTSP_1, RLSUB_1;
equalities STRUCT_0, RLVECT_1, PCOMPS_1, NORMSP_0, NORMSP_2, PRVECT_3;
expansions TARSKI, FUNCT_2, NORMSP_0, NORMSP_1, LOPBAN_1;
theorems TARSKI, XBOOLE_1, RLVECT_1, RELAT_1, RLSUB_1, ZFMISC_1, FUNCT_2,
XREAL_1, XCMPLX_1, NORMSP_1, NFCONT_1, XXREAL_0, FUNCT_1, ORDINAL1,
PARTFUN1, VECTSP_1, RSSPACE, NORMSP_2, FUNCT_3, ABSVALUE, PDIFF_8,
PDIFF_1, FINSEQ_1, XTUPLE_0, LOPBAN_1, NORMSP_0, LOPBAN_6, T_0TOPSP,
TOPS_2, TMAP_1, PRVECT_3, RSSPACE3;
schemes FUNCT_2;
begin
definition
let X,Y be non empty NORMSTR,
x be Point of X,
y be Point of Y;
redefine func [x,y] -> Point of [:X,Y:]; :: redefines [ (TARSKI, definition)
coherence by ZFMISC_1:87;
end;
definition
let X,Y be non empty NORMSTR,
seqx be sequence of X,
seqy be sequence of Y;
redefine func <:seqx,seqy:> -> sequence of [:X,Y:]; :: redefines <: (FUNCT_3, definition)
coherence
proof
<:seqx,seqy:> is Function of NAT,[:the carrier of X,the carrier of Y:];
hence thesis;
end;
end;
theorem Th1:
for X,Y be RealLinearSpace,
T be LinearOperator of X,Y
st T is bijective
holds T" is LinearOperator of Y,X & rng(T") = the carrier of X
proof
let X,Y be RealLinearSpace,
T be LinearOperator of X,Y;
assume A1: T is bijective;
A2:rng T = the carrier of Y by A1,FUNCT_2:def 3;
A3:dom T = the carrier of X by FUNCT_2:def 1;
T" is LinearOperator of Y,X
proof
reconsider T1=T" as Function of Y,X by A1,A2,FUNCT_2:25;
A4: T1 is additive
proof
let y1,y2 be Point of Y;
consider x1,x2 be Point of X such that
A5: T1.y1=x1 & T1.y2=x2;
A6: T.x1=y1 & T.x2=y2 by A5,A1,A2,FUNCT_1:32;
x1+x2 =T1.(T.(x1+x2)) by A1,FUNCT_1:32, A3
.=T1.(y1+y2) by A6, VECTSP_1:def 20;
hence thesis by A5;
end;
T1 is homogeneous
proof
let y1 be Point of Y,r be Real;
set x1 = T1.y1;
r*x1=T1.(T.(r*x1)) by A1,FUNCT_1:32,A3
.=T1.(r*T.x1) by LOPBAN_1:def 5
.=T1.(r*y1) by A1,A2,FUNCT_1:32;
hence thesis;
end;
hence thesis by A4;
end;
hence thesis by A1,FUNCT_1:33,A3;
end;
theorem
for X,Y be non empty LinearTopSpace,
T be LinearOperator of X,Y,
S be Function of Y, X
st T is bijective open & S = T" holds
S is LinearOperator of Y,X & S is onto continuous
proof
let X,Y be non empty LinearTopSpace,
T be LinearOperator of X,Y,
S be Function of Y,X;
assume A1: T is bijective open & S = T"; then
A2: T" is LinearOperator of Y,X & T" is one-to-one
& rng(T") = the carrier of X by Th1;
A3: [#] Y<>{} & [#] X<>{};
S is continuous
proof
now let A be Subset of X;
assume A4:A is open;
S"A = S".:A by A1,FUNCT_1:85
.=T.:A by A1,FUNCT_1:43;
hence S"A is open by A4, A1,T_0TOPSP:def 2;
end;
hence thesis by A3,TOPS_2:43;
end;
hence thesis by A2,A1;
end;
theorem Th3:
for X,Y be RealNormSpace,
f be LinearOperator of X,Y holds 0.Y=f.(0.X)
proof
let X,Y be RealNormSpace,
f be LinearOperator of X,Y;
f/.(0.X)+0.Y = f/.(0.X) by RLVECT_1:4
.=f/.(0.X+0.X) by RLVECT_1:4
.=f/.(0.X) + f/.(0.X) by VECTSP_1:def 20;
hence thesis by RLVECT_1:8;
end;
theorem Th4:
for X,Y be RealNormSpace,
f be LinearOperator of X,Y,
x be Point of X holds
f is_continuous_in x iff f is_continuous_in 0.X
proof
let X,Y be RealNormSpace,
f be LinearOperator of X,Y,
x be Point of X;
A1: dom f =the carrier of X by FUNCT_2:def 1;
A2: 0.Y=f/.0.X by Th3;
hereby assume A3:f is_continuous_in x;
now let r be Real;
assume 0 < r;
then consider s be Real such that
A4: 0<s & for x1 be Point of X st x1 in dom f &
||. x1- x .|| < s holds ||. f/.x1 - f/.x .|| < r by A3,NFCONT_1:7;
take s;
thus 0 < s by A4;
let x1 be Point of X;
assume A5: x1 in dom f & ||. x1- 0.X .|| < s;
set y1= x1+x;
A6: y1- x = x1+(x- x) by RLVECT_1:28
.= x1+0.X by RLVECT_1:15
.= x1 by RLVECT_1:4; then
A7: ||. y1- x .|| < s by A5, RLVECT_1:13;
f/.y1 - f/.x =f.(y1) +(-1) * f.x by RLVECT_1:16
.=f.(y1) + f.((-1)*x) by LOPBAN_1:def 5
.= f.(y1 + (-1)*x) by VECTSP_1:def 20
.= f.(y1-x) by RLVECT_1:16
.= f/.x1 - f/.(0.X) by A6, A2,RLVECT_1:13;
hence ||. f/.x1 - f/.(0.X) .|| < r by A7,A4,A1;
end;
hence f is_continuous_in 0.X by A1,NFCONT_1:7;
end;
assume A8:f is_continuous_in 0.X;
now let r be Real;
assume 0 < r;
then consider s be Real such that
A9: 0<s & for x1 be Point of X st x1 in dom f &
||. x1- 0.X .|| < s holds ||. f/.x1 - f/.0.X .|| < r by A8,NFCONT_1:7;
take s;
thus 0 < s by A9;
thus for x1 be Point of X st x1 in dom f &
||. x1- x .|| < s holds ||. f/.x1 - f/.x .|| < r
proof
let x1 be Point of X;
assume A10: x1 in dom f & ||. x1- x .|| < s;
set y1= x1-x;
A11: ||. y1-0.X .|| <s by A10, RLVECT_1:13;
f/.y1 - f/.(0.X) = f.y1 by A2,RLVECT_1:13
.= f.(x1+(-1)*x) by RLVECT_1:16
.= f.x1+f.((-1)*x) by VECTSP_1:def 20
.= f.x1+(-1)*f.x by LOPBAN_1:def 5
.= f.x1-f.x by RLVECT_1:16;
hence ||. f/.x1 - f/.x .|| < r by A11,A9,A1;
end;
end;
hence f is_continuous_in x by A1,NFCONT_1:7;
end;
theorem Th5:
for X,Y be RealNormSpace, f be LinearOperator of X,Y holds
f is_continuous_on the carrier of X
iff
f is_continuous_in 0.X
proof
let X,Y be RealNormSpace, f be LinearOperator of X,Y;
A1: f| (the carrier of X) = f;
A2: dom f = the carrier of X by FUNCT_2:def 1;
now assume A3:f is_continuous_in 0.X;
for x be Point of X st x in the carrier of X
holds f| (the carrier of X) is_continuous_in x by A3,Th4;
hence f is_continuous_on the carrier of X by A2,NFCONT_1:def 7;
end;
hence thesis by A1,NFCONT_1:def 7;
end;
theorem Th6:
for X,Y be RealNormSpace, f be LinearOperator of X,Y
holds f is Lipschitzian iff f is_continuous_on the carrier of X
proof
let X,Y be RealNormSpace, f be LinearOperator of X,Y;
hereby assume A1:f is Lipschitzian;
A2: dom f =the carrier of X by FUNCT_2:def 1;
consider K being Real such that
A3: 0 <= K & for x being VECTOR of X holds ||. f.x .|| <= K * ||. x .||
by A1;
now
let x,y be Point of X;
assume x in the carrier of X & y in the carrier of X;
f/.x -f/.y =f.x +(-1)* f.y by RLVECT_1:16;
then f/.x -f/.y = f.x + f.((-1)*y) by LOPBAN_1:def 5;
then f/.x -f/.y = f.(x+(-1)*y) by VECTSP_1:def 20;
then
A4: f/.x -f/.y =f.(x+-y) by RLVECT_1:16;
||.f/.x -f/.y .||<=K*||. x-y .||+||. x-y .|| by A3,A4,XREAL_1:38;
hence ||. f/.x -f/.y .|| <= (K+1) * ||. x-y .||;
end;
hence
f is_continuous_on the carrier of X by NFCONT_1:45,A2,A3,NFCONT_1:def 9;
end;
assume
A5: f is_continuous_on the carrier of X;
A6: dom f =the carrier of X by FUNCT_2:def 1;
f| (the carrier of X) = f;
then f is_continuous_in 0.X by A5,NFCONT_1:def 7;
then consider s be Real such that
A7: 0<s & for x1 be Point of X st x1 in dom f &
||. x1- 0.X .|| < s holds ||. f/.x1 - f/.0.X .|| < 1 by NFCONT_1:7;
set r1=2/s;
now let x1 be VECTOR of X;
A8: 0.Y=f/.(0.X) by Th3;
per cases;
suppose x1=0.X;
hence ||. f.x1 .||<=r1*||.x1.|| by A7,A8;
end;
suppose A9: x1<>0.X;
then
A10: ||.x1.|| <> 0 by NORMSP_0:def 5;
set r3= (s/2)/||.x1.||;
0 < s/2 by A7,XREAL_1:215;
then
A11: 0 < r3 by A10,XREAL_1:139;
set x2=r3*x1;
A12: 1/r3 = ||.x1.|| /(s/2) by XCMPLX_1:57
.= ||.x1.|| *(2/s) by XCMPLX_1:79;
||.x2.||=|.r3.|*||.x1.|| by NORMSP_1:def 1
.= r3 *||.x1.|| by A7,ABSVALUE:def 1
.=s/2 by A9, NORMSP_0:def 5,XCMPLX_1:87;
then ||.x2.||<s by A7,XREAL_1:216;
then ||.x2 - 0.X .||<s by RLVECT_1:13; then
A13: ||. f/.x2 - f/.0.X .|| < 1 by A6,A7;
||. f/.x2.||= ||.r3*(f.x1).|| by LOPBAN_1:def 5
.=|.r3.|*||.f.x1.|| by NORMSP_1:def 1
.= r3* ||.f.x1.|| by A7,ABSVALUE:def 1;
then r3*||.f.x1.|| < 1 by A13, A8,RLVECT_1:13;
hence ||.f.x1.|| <= r1*||.x1.|| by A12, A11,XREAL_1:81;
end;
end;
hence f is Lipschitzian by A7;
end;
:: Banach's Continuous Inverse Theorem
theorem Th7:
for X,Y be RealBanachSpace,
T be Lipschitzian LinearOperator of X,Y
st T is bijective
holds T" is Lipschitzian LinearOperator of Y,X
proof
let X,Y be RealBanachSpace,
T be Lipschitzian LinearOperator of X,Y;
assume A1: T is bijective;
A2: the carrier of LinearTopSpaceNorm X = the carrier of X
& the carrier of LinearTopSpaceNorm Y
= the carrier of Y by NORMSP_2:def 4;
then reconsider S = T as
Function of LinearTopSpaceNorm X,LinearTopSpaceNorm Y;
reconsider T2=T" as LinearOperator of Y,X by Th1,A1;
reconsider T3=T2 as Function of
LinearTopSpaceNorm Y,LinearTopSpaceNorm X by A2;
A3: T3 is continuous
proof
A4: [#]LinearTopSpaceNorm Y<>{} & [#]LinearTopSpaceNorm X<>{};
now let A be Subset of LinearTopSpaceNorm X;
assume A5: A is open;
T3"A = T3".:A by A1,FUNCT_1:85
.= S.:A by A1,FUNCT_1:43;
hence T3"A is open by A5, A2,A1,LOPBAN_6:16,T_0TOPSP:def 2;
end;
hence thesis by A4,TOPS_2:43;
end;
A6: dom T2 =the carrier of Y by FUNCT_2:def 1;
now
let x be Point of Y;
assume x in the carrier of Y;
reconsider xt=x as Point of LinearTopSpaceNorm Y by NORMSP_2:def 4;
A7: T3 is_continuous_at xt by A3,TMAP_1:44;
reconsider x1=x as Point of TopSpaceNorm Y;
reconsider T4=T2 as Function of TopSpaceNorm Y,TopSpaceNorm X;
T4 is_continuous_at x1 by A7,NORMSP_2:35;
hence T2| (the carrier of Y) is_continuous_in x by NORMSP_2:18;
end;
hence thesis by Th6, A6,NFCONT_1:def 7;
end;
theorem Th8:
for X,Y be RealNormSpace,
seqx be sequence of X,
seqy be sequence of Y,
x be Point of X,
y be Point of Y holds
( seqx is convergent & lim seqx = x
& seqy is convergent & lim seqy = y )
iff
<:seqx,seqy:> is convergent & lim <:seqx,seqy:> = [x,y]
proof
let X,Y be RealNormSpace,
seqx be sequence of X,
seqy be sequence of Y,
x be Point of X,
y be Point of Y;
set seq = <:seqx,seqy:>;
set v = [x,y];
hereby assume A1:
seqx is convergent & lim seqx = x & seqy is convergent & lim seqy = y;
A2: for r be Real st 0 < r ex m be Nat
st for n be Nat st m <= n holds ||.(seq.n) - v.|| < r
proof
let r1 be Real;
assume A3: 0 < r1;
set r=r1/2;
A4: 0 < r & r < r1 by A3,XREAL_1:215,216;
set r2=r/2;
A5:0 < r2 & r2 < r by A4,XREAL_1:215,216;
then consider m1 be Nat such that
A6: for n be Nat
st m1 <= n holds ||.(seqx.n) - x .|| < r2 by A1,NORMSP_1:def 7;
consider m2 be Nat such that
A7: for n be Nat
st m2 <= n holds ||.(seqy.n) - y .|| < r2 by A1,A5,NORMSP_1:def 7;
reconsider m=max(m1,m2) as Nat by TARSKI:1;
take m;
let n be Nat;
assume A8: m <= n;
m1 <= m by XXREAL_0:25; then
A9: m1<= n by A8,XXREAL_0:2;
m2 <= m by XXREAL_0:25; then
A10: m2<= n by A8,XXREAL_0:2;
n in NAT by ORDINAL1:def 12; then
A11: [seqx.n,seqy.n] = seq.n by FUNCT_3:59;
A12: - v = [-x, -y] by PRVECT_3:18;
(seq.n) - v = [(seqx.n)-x,(seqy.n)-y] by A11,A12,PRVECT_3:18;
then consider w be Element of REAL 2 such that
A13: w = <* ||. (seqx.n)-x .||,||. (seqy.n)-y .|| *>
& ||. (seq.n) - v .|| = |.w.| by PRVECT_3:18;
now let i be Element of NAT;
assume 1 <= i & i <= 2; then
A14: i in Seg 2 by FINSEQ_1:1;
per cases by A14,FINSEQ_1:2,TARSKI:def 2;
suppose A15: i=1;
A16:(proj (i,2)).w = w.1 by A15,PDIFF_1:def 1
.= ||. (seqx.n)-x .|| by A13,FINSEQ_1:44;
|. (proj (i,2)).w .| = ||. (seqx.n)-x .||
by ABSVALUE:def 1, A16;
hence |. (proj (i,2)).w .| <= r2 by A9, A6;
end;
suppose i=2; then
A17:(proj (i,2)).w = w.2 by PDIFF_1:def 1
.= ||. (seqy.n)-y .|| by A13,FINSEQ_1:44;
|. (proj (i,2)).w .| = ||. (seqy.n)-y .||
by ABSVALUE:def 1, A17;
hence |. (proj (i,2)).w .| <= r2 by A10,A7;
end;
end;
then |.w.| <= 2*(r2) by PDIFF_8:17;
hence ||. (seq.n) - v .|| < r1 by A13,A4,XXREAL_0:2;
end;
hence seq is convergent;
hence lim seq = [x, y] by A2,NORMSP_1:def 7;
end;
assume
A18:seq is convergent & lim seq = [x,y];
A19: for r be Real st 0 < r ex m be Nat
st for n be Nat st m <= n holds
||.(seqx.n) - x.|| < r & ||. (seqy.n) - y.|| < r
proof
let r be Real;
assume 0 < r;
then consider m be Nat such that
A20: for n be Nat st m <= n holds ||.(seq.n) - v.|| < r by A18,NORMSP_1:def 7;
take m;
let n be Nat;
assume m <= n; then
A21: ||.(seq.n) - v .|| < r by A20;
n in NAT by ORDINAL1:def 12; then
A22: [seqx.n,seqy.n ] = seq.n by FUNCT_3:59;
A23: - v = [-x,-y] by PRVECT_3:18;
(seq.n) - v = [(seqx.n)-x,(seqy.n)-y] by A22,A23,PRVECT_3:18;
then consider w be Element of REAL 2 such that
A24: w = <* ||. (seqx.n)-x .||,||. (seqy.n)-y .|| *>
& ||. (seq.n) - v .|| = |.w.| by PRVECT_3:18;
(proj (1,2)).w = w.1 by PDIFF_1:def 1
.= ||. (seqx.n)-x .|| by A24,FINSEQ_1:44;
then |. ||. (seqx.n)-x .|| .| <= |.w.| by PDIFF_8:5;
then ||. (seqx.n)-x .|| <= |.w.| by ABSVALUE:def 1;
hence ||.(seqx.n)-x.|| < r by A24,A21,XXREAL_0:2;
(proj (2,2)).w = w.2 by PDIFF_1:def 1
.= ||. (seqy.n)-y .|| by A24,FINSEQ_1:44;
then |. ||. (seqy.n)-y .|| .| <= |.w.| by PDIFF_8:5;
then ||. (seqy.n)-y .|| <= |.w.| by ABSVALUE:def 1;
hence ||.(seqy.n)-y.|| < r by A24,A21,XXREAL_0:2;
end;
A25 :now let r be Real;
assume 0 < r;
then consider m be Nat such that
A26: for n be Nat st m <= n holds
||.(seqx.n)-x.|| < r & ||.(seqy.n)-y.|| < r by A19;
take m;
thus for n be Nat st m <= n holds
||.(seqx.n) - x.|| < r by A26;
end;
hence seqx is convergent;
hence lim seqx = x by A25,NORMSP_1:def 7;
A27: now let r be Real;
assume 0 < r;
then consider m be Nat such that
A28: for n be Nat st m <= n holds
||.(seqx.n)-x.|| < r & ||.(seqy.n)-y.|| < r by A19;
take m;
thus for n be Nat st m <= n holds
||.(seqy.n)-y.|| < r by A28;
end;
hence seqy is convergent;
hence lim seqy = y by A27,NORMSP_1:def 7;
end;
definition
let X,Y be RealNormSpace;
let T be PartFunc of X, Y;
func graph(T) -> Subset of [:X,Y:] equals
T;
correctness;
end;
registration
let X,Y be RealNormSpace;
let T be non empty PartFunc of X, Y;
cluster graph(T) -> non empty;
correctness;
end;
registration
let X,Y be RealNormSpace, T be LinearOperator of X,Y;
cluster graph(T) -> linearly-closed;
correctness
proof
set V = [:X,Y:];
set W = graph(T);
hereby
let v,u be VECTOR of V such that
A1: v in W and
A2: u in W;
consider x1,y1 be object such that
A3: v = [x1,y1] by RELAT_1:def 1;
A4: x1 in dom T & y1 = T.x1 by FUNCT_1:1,A3,A1;
reconsider x1 as VECTOR of X by A3,ZFMISC_1:87;
reconsider y1 as VECTOR of Y by A3,ZFMISC_1:87;
consider x2,y2 be object such that
A5: u = [x2,y2] by RELAT_1:def 1;
reconsider x2 as VECTOR of X by A5,ZFMISC_1:87;
reconsider y2 as VECTOR of Y by A5,ZFMISC_1:87;
x1+x2 in the carrier of X; then
A6: x1+x2 in dom T by FUNCT_2:def 1;
A7: y1+y2 = (T.x1) +(T.x2) by A4,FUNCT_1:1,A5,A2
.= T.(x1+x2) by VECTSP_1:def 20;
[x1+x2,y1+y2 ] = v + u by PRVECT_3:18,A3,A5;
hence v+u in W by A7,A6,FUNCT_1:1;
end;
let a be Real;
let v be VECTOR of V;
assume A8: v in W;
consider x,y be object such that
A9: v = [x,y] by RELAT_1:def 1;
reconsider x as VECTOR of X by A9,ZFMISC_1:87;
reconsider y as VECTOR of Y by A9,ZFMISC_1:87;
a*x in the carrier of X; then
A10: a*x in dom T by FUNCT_2:def 1;
A11: a*y = a*(T.x) by FUNCT_1:1,A9,A8
.=T.(a*x) by LOPBAN_1:def 5;
[a*x,a*y ] = a*v by PRVECT_3:18,A9;
hence a*v in W by A11,A10,FUNCT_1:1;
end;
end;
definition
let X,Y be RealNormSpace;
let T be LinearOperator of X,Y;
func graphNrm(T) -> Function of graph(T),REAL equals
(the normF of [:X,Y:]) | graph(T);
correctness;
end;
definition
let X,Y be RealNormSpace;
let T be PartFunc of X,Y;
attr T is closed means
graph(T) is closed;
correctness;
end;
definition
let X,Y be RealNormSpace, T be LinearOperator of X,Y;
func graphNSP(T) -> non empty NORMSTR equals
NORMSTR(# graph(T),Zero_(graph(T),[:X,Y:]), Add_(graph(T),[:X,Y:]),
Mult_(graph(T),[:X,Y:]),graphNrm(T) #);
correctness;
end;
registration
let X,Y be RealNormSpace, T be LinearOperator of X,Y;
cluster graphNSP(T) -> Abelian add-associative right_zeroed
right_complementable scalar-distributive vector-distributive
scalar-associative scalar-unital;
coherence
proof
the RLSStruct of graphNSP(T) is RealLinearSpace by RSSPACE:11;
hence thesis by RSSPACE3:2;
end;
end;
theorem Th9:
for X,Y be RealNormSpace, T be LinearOperator of X,Y holds
graphNSP(T) is Subspace of [:X,Y:]
proof
let X,Y be RealNormSpace,
T be LinearOperator of X,Y;
set l = graphNSP(T);
reconsider W = the RLSStruct of l as Subspace of [:X,Y:] by RSSPACE:11;
A1: 0.l = 0.W
.= 0.([:X,Y:]) by RLSUB_1:def 2;
A2: the addF of l =(the addF of ([:X,Y:]) ) || (the carrier of W)
by RLSUB_1:def 2
.= (the addF of ([:X,Y:])) || (the carrier of l);
the Mult of l =(the Mult of ([:X,Y:])) | [:REAL, the carrier of W:]
by RLSUB_1:def 2
.=(the Mult of ([:X,Y:]) ) | [:REAL, the carrier of l:];
hence l is Subspace of [:X,Y:] by A1,A2,RLSUB_1:def 2;
end;
Lm1:
for X,Y be RealNormSpace,
T be LinearOperator of X,Y,
x, y being Point of graphNSP(T),
a be Real holds ( ||.x.|| = 0 iff x = 0.(graphNSP(T))) & 0 <= ||.x.||
& ||.x+y.|| <= ||.x.|| + ||.y.||
& ||. a*x .|| = |.a.| * ||.x.||
proof
let X,Y be RealNormSpace,
T be LinearOperator of X,Y,
x, y be Point of graphNSP(T), a be Real;
x in graph(T) & y in graph(T);
then reconsider x1=x,y1=y as Point of [:X,Y:];
set W = graphNSP(T);
set V = [:X,Y:];
A1: W is Subspace of V by Th9;
A2: ||.x.|| = ||.x1.|| by FUNCT_1:49;
A3: ||.y.|| = ||.y1.|| by FUNCT_1:49;
x+y = x1+y1 by A1,RLSUB_1:13; then
A4: ||. x+y .|| = ||. x1+y1 .|| by FUNCT_1:49;
a*x = a*x1 by A1,RLSUB_1:14; then
A5: ||. a*x .|| = ||. a*x1 .|| by FUNCT_1:49;
A6: 0.([:X,Y:]) = 0.(graphNSP(T)) by A1,RLSUB_1:11;
||.x.|| = 0 iff ||.x1.|| = 0 by FUNCT_1:49;
hence ||.x.|| = 0 iff x = 0.(graphNSP(T)) by A6, NORMSP_0:def 5;
thus 0 <= ||.x.|| by A2;
thus ||.x+y.|| <= ||.x.|| + ||.y.|| by A2,A3,A4, NORMSP_1:def 1;
thus thesis by A2,A5,NORMSP_1:def 1;
end;
registration
let X,Y be RealNormSpace,
T be LinearOperator of X,Y;
cluster graphNSP(T) -> reflexive discerning RealNormSpace-like;
coherence
by Lm1;
end;
theorem Th10:
for X be RealNormSpace, Y be RealBanachSpace, X0 be Subset of Y
st X is Subspace of Y & the carrier of X = X0
& the normF of X = (the normF of Y ) | (the carrier of X) &
X0 is closed holds
X is complete
proof
let X be RealNormSpace, Y be RealBanachSpace,
X0 be Subset of Y;
assume A1: X is Subspace of Y & the carrier of X = X0 &
the normF of X = (the normF of Y ) | (the carrier of X)
& X0 is closed;
now let seq be sequence of X;
assume A2: seq is Cauchy_sequence_by_Norm;
rng seq c= the carrier of Y by A1,XBOOLE_1:1; then
reconsider yseq=seq as sequence of Y by FUNCT_2:6;
for r be Real st r > 0 ex k
be Nat st for n, m be Nat st n >= k & m >= k
holds ||.(yseq.n) - (yseq.m).|| < r
proof
let r be Real;
assume r > 0;
then consider k be Nat such that
A3: for n, m be Nat st n >= k & m >= k
holds ||.(seq.n) - (seq.m).|| < r by RSSPACE3:8,A2;
take k;
now let n, m be Nat;
assume A4: n >= k & m >= k;
(seq.n) - (seq.m) = (yseq.n) - (yseq.m) by A1,RLSUB_1:16;
then ||.(seq.n) - (seq.m).||
= ||.(yseq.n) - (yseq.m).|| by FUNCT_1:49,A1;
hence ||.(yseq.n) - (yseq.m).|| < r by A4,A3;
end;
hence thesis;
end; then
A5: yseq is convergent by LOPBAN_1:def 15, RSSPACE3:8;
rng yseq = rng seq;
then reconsider lyseq=lim yseq as Point of X by A1,A5,NFCONT_1:def 3;
for r be Real st 0 < r ex m be Nat st for n be Nat
st m <= n holds ||.(seq.n) - lyseq.|| < r
proof
let r be Real;
assume 0 < r; then
consider m be Nat such that
A6: for n be Nat
st m <= n holds ||.(yseq.n) - lim yseq.|| < r by A5,NORMSP_1:def 7;
take m;
now let n be Nat;
assume A7: m <= n;
(yseq.n) - (lim yseq) = (seq.n) - (lyseq) by A1,RLSUB_1:16;
then ||.(yseq.n) - (lim yseq).||
= ||.(seq.n) - (lyseq).|| by FUNCT_1:49,A1;
hence ||.(seq.n) - (lyseq).|| < r by A7,A6;
end;
hence thesis;
end;
hence seq is convergent;
end;
hence thesis;
end;
theorem Th11:
for X,Y be RealBanachSpace,
T be LinearOperator of X,Y st T is closed
holds graphNSP(T) is complete
proof
let X,Y be RealBanachSpace, T be LinearOperator of X,Y;
graphNSP(T) is Subspace of [:X, Y :] by Th9;
hence thesis by Th10;
end;
theorem Th12:
for X,Y be RealNormSpace, T be non empty PartFunc of X,Y holds
T is closed iff
for seq be sequence of X
st rng seq c= dom T & seq is convergent & T/*seq is convergent
holds lim seq in dom T & lim (T/*seq)= T.(lim seq)
proof
let X,Y be RealNormSpace, T be non empty PartFunc of X,Y;
hereby
assume A1: T is closed;
thus for seq be sequence of X
st rng seq c= dom T & seq is convergent & T/*seq is convergent
holds lim seq in dom T & lim (T/*seq)= T.(lim seq)
proof
let seq be sequence of X;
assume A2: rng seq c= dom T & seq is convergent & T/*seq is convergent;
set s1 = <:seq,T/*seq:>;
A3: rng s1 c= graph(T)
proof
let y be object;
assume y in rng s1;
then consider i be object
such that A4: i in NAT & s1.i = y by FUNCT_2:11;
A5: (T/*seq).i = T.(seq.i) by A4,A2,FUNCT_2:108;
seq.i in rng seq by A4,FUNCT_2:4;
then [seq.i,(T/*seq).i ] in T by A5,FUNCT_1:def 2,A2;
hence y in graph(T) by A4,FUNCT_3:59;
end;
lim seq = lim seq & lim (T/*seq) = lim (T/*seq);
then s1 is convergent
& lim s1 = [lim seq, lim (T/*seq) ] by Th8,A2;
then [lim seq, lim (T/*seq) ] in graph(T)
by A1,NFCONT_1:def 3,A3;
hence lim seq in dom T & lim (T/*seq)= T.(lim seq) by FUNCT_1:1;
end;
end;
assume
A6: for seq be sequence of X
st rng seq c= dom T & seq is convergent & T/*seq is convergent holds
lim seq in dom T & lim (T/*seq)= T.(lim seq);
for s1 be sequence of [:X,Y:] st rng s1 c= graph(T)
& s1 is convergent holds lim s1 in graph(T)
proof
let s1 be sequence of [:X,Y:];
assume A7: rng s1 c= graph(T) & s1 is convergent;
defpred Q0[set,set] means [$2,T.$2] = s1.$1;
A8: for i being Element of NAT ex x being Element of
the carrier of X st Q0[i,x]
proof
let i be Element of NAT;
A9: s1.i in rng s1 by FUNCT_2:4;
consider x be Point of X,y be Point of Y such that
A10: s1.i =[x,y] by PRVECT_3:18;
take x;
thus thesis by A10,FUNCT_1:1,A9,A7;
end;
consider seq be sequence of X such that
A11: for x being Element of NAT holds Q0[x,seq.x] from FUNCT_2:sch 3(A8);
A12: now let y be object;
assume y in rng seq; then
consider i be object such that
A13: i in dom seq & y=seq. i by FUNCT_1:def 3;
A14: [seq.i,T.(seq.i) ] = s1.i by A13,A11;
s1.i in rng s1 by A13,FUNCT_2:4;
hence y in dom T by A13,FUNCT_1:1, A14,A7;
end; then
A15:rng seq c= dom T;
consider x be Point of X,y be Point of Y such that
A16: lim s1 =[x,y] by PRVECT_3:18;
s1 = <:seq,T/*seq:>
proof
let n be Element of NAT;
(T/*seq).n = T.(seq.n) by A12,TARSKI:def 3,FUNCT_2:108;
hence s1.n = [seq.n,(T/*seq).n] by A11
.= <:seq,T/*seq:>.n by FUNCT_3:59;
end; then
A17: seq is convergent & lim seq = x
& T/*seq is convergent & lim (T/*seq) = y by A16,Th8,A7;
lim seq in dom T & lim (T/*seq)= T.(lim seq) by A15,A6,A17;
hence lim s1 in graph(T) by A16,A17,FUNCT_1:1;
end;
hence thesis by NFCONT_1:def 3;
end;
theorem
for X,Y be RealNormSpace,
T be non empty PartFunc of X,Y,T0 be LinearOperator of X,Y st
T0 is Lipschitzian & dom T is closed & T=T0
holds T is closed
proof
let X,Y be RealNormSpace,
T be non empty PartFunc of X,Y,T0 be LinearOperator of X,Y;
assume
A1:T0 is Lipschitzian & dom T is closed & T=T0; then
A2:T is_continuous_in 0.X by Th5,Th6;
for seq be sequence of X
st rng seq c= dom T & seq is convergent & T/*seq is convergent
holds lim seq in dom T & lim (T/*seq)= T.(lim seq)
proof
let seq be sequence of X;
assume
A3: rng seq c= dom T & seq is convergent & T/*seq is convergent;
A4:T is_continuous_in lim seq by A1,A2,Th4;
T/.(lim seq)=T.(lim seq) by A1,A3,NFCONT_1:def 3,PARTFUN1:def 6;
hence thesis by A3,A4, NFCONT_1:def 5;
end;
hence thesis by Th12;
end;
theorem
for X,Y be RealNormSpace,T be non empty PartFunc of X,Y,
S be non empty PartFunc of Y,X st
T is closed & T is one-to-one & S=T"
holds S is closed
proof
let X,Y be RealNormSpace,T be non empty PartFunc of X,Y,
S be non empty PartFunc of Y,X;
assume
A1:T is closed & T is one-to-one & S=T";
A2: rng T = dom S & dom T = rng S by A1, FUNCT_1:33;
for seq be sequence of Y
st rng seq c= dom S & seq is convergent & S/*seq is convergent
holds lim seq in dom S & lim (S/*seq)= S.(lim seq)
proof
let seq be sequence of Y;
assume
A3: rng seq c= dom S & seq is convergent & S/*seq is convergent;
set seq1=S/*seq;
A4: rng seq1 c= dom T
proof
let x be object;
assume x in rng seq1;
then consider i be object such that
A5: i in dom seq1 & x=seq1.i by FUNCT_1:def 3;
reconsider i as Nat by A5;
S.(seq.i) in rng S by FUNCT_1:3, A3,NFCONT_1:5;
hence x in dom T by A5, A2, A3,FUNCT_2:108;
end;
A6:T/*seq1=seq
proof
now
let n be Element of NAT;
thus (T/*seq1).n = seq.n
proof
A7: seq.n in rng T by A3,NFCONT_1:5,A2;
(T/*seq1).n= T.(seq1.n) by A4,FUNCT_2:108
.= T.(S.(seq.n)) by A3,FUNCT_2:108
.= seq.n by A1,A7,FUNCT_1:35;
hence thesis;
end;
end;
hence thesis;
end;
lim seq1 in dom T & lim (T/*seq1)=T.(lim S/*seq)
by A1,A3,A4,A6,Th12;
hence thesis by A2,A6,FUNCT_1:3,A1,FUNCT_1:34;
end;
hence thesis by Th12;
end;
:: The Closed Graph Theorem
theorem Th15:
for X,Y be RealNormSpace, x be Point of X, y be Point of Y holds
||.x.|| <= ||. [x,y] .|| & ||.y.|| <= ||. [x,y] .||
proof
let X,Y be RealNormSpace, x be Point of X, y be Point of Y;
consider w be Element of REAL 2 such that
A1: w=<* ||.x.||,||.y.|| *> & ||.[x,y].|| = |.w.| by PRVECT_3:18;
(proj (1,2)).w = w.1 by PDIFF_1:def 1
.= ||.x.|| by A1,FINSEQ_1:44;
then |. ||.x.|| .| <= |.w.| by PDIFF_8:5;
hence ||.x.|| <= ||.[x,y].|| by A1, ABSVALUE:def 1;
(proj (2,2)).w = w.2 by PDIFF_1:def 1
.= ||.y.|| by A1,FINSEQ_1:44;
then |. ||.y.|| .| <= |.w.| by PDIFF_8:5;
hence ||.y.|| <= ||.[x,y].|| by A1, ABSVALUE:def 1;
end;
registration
let X,Y be RealBanachSpace;
cluster closed -> Lipschitzian for LinearOperator of X,Y;
coherence
proof
let T be LinearOperator of X,Y;
assume
A1: T is closed;
defpred Q0[object,object] means $1=[$2,T.$2];
A2: for z be object st z in the carrier of graphNSP(T) ex x be object
st x in the carrier of X & Q0[z,x]
proof
let z be object;
assume
A3:z in the carrier of graphNSP(T);
then consider x,y be object such that
A4: z = [x,y] by RELAT_1:def 1;
x in dom T & y = T.x by FUNCT_1:1,A4,A3;
hence thesis by A4;
end;
consider J be Function of graphNSP(T), X such that
A5: for z be object st z in the carrier of graphNSP(T) holds Q0[z,J.z]
from FUNCT_2:sch 1(A2);
A6: graphNSP(T) is complete by Th11, A1;
A7: graphNSP(T) is Subspace of [:X,Y:]
& the normF of graphNSP(T) = (the normF of [:X,Y:] )
| (the carrier of graphNSP(T)) by Th9;
A8: for x being VECTOR of graphNSP(T),
r being Real holds J.(r*x) = r*J.x
proof
let x be VECTOR of graphNSP(T), r be Real;
A9: x = [J.x,T.(J.x)] by A5;
A10: r*x = [J.(r*x),T.(J.(r*x)) ] by A5;
x in graph(T); then
reconsider x1=x as Point of [:X,Y:];
r*x1=r*x by A7, RLSUB_1:14; then
r*x = [r*(J.x),r*(T.(J.x))] by PRVECT_3:18,A9;
hence J.(r*x) = r*(J.x) by A10,XTUPLE_0:1;
end;
for x,y being VECTOR of graphNSP(T) holds J.(x+y) = J.x + J.y
proof
let x,y be VECTOR of graphNSP(T);
A11: x = [J.x,T.(J.x)] by A5;
A12: y = [J.y,T.(J.y)] by A5;
A13: x+y = [J.(x+y),T.(J.(x+y)) ] by A5;
x in graph(T) & y in graph(T); then
reconsider x1=x,y1=y as Point of [:X,Y:];
x1+y1=x+y by A7, RLSUB_1:13;
then x+y = [(J.x)+(J.y),(T.(J.x)) + (T.(J.y)) ] by PRVECT_3:18,A11,A12;
hence J.(x+y) = (J.x) + (J.y) by A13,XTUPLE_0:1;
end;
then reconsider
J as LinearOperator of graphNSP(T),X by A8, LOPBAN_1:def 5, VECTSP_1:def 20;
J is Lipschitzian
proof
A14: now
let x be Point of graphNSP(T);
x in graph(T); then
reconsider x1=x as Point of [:X,Y:];
A15: x1= [J.x,T.(J.x)] by A5;
||.J.x.|| <= ||.x1.|| by A15,Th15;
hence ||.J.x.|| <= 1 * ||.x.|| by FUNCT_1:49;
end;
take 1;
thus thesis by A14;
end;
then reconsider J as Lipschitzian LinearOperator of graphNSP(T),X;
now let x,y be object;
assume A16: x in the carrier of graphNSP(T)
& y in the carrier of graphNSP(T) & J.x = J.y;
then reconsider x1=x as Point of graphNSP(T);
x1 = [J.x1,T.(J.x1)] by A5;
hence x=y by A5,A16;
end; then
A17: J is one-to-one by FUNCT_2:19;
for y be object holds y in rng J iff y in the carrier of X
proof
let y be object;
now assume A18: y in the carrier of X;
then reconsider y1=y as Point of X;
y1 in dom T by A18,FUNCT_2:def 1;
then reconsider x= [y1,T.y1] as Point of graphNSP(T) by FUNCT_1:1;
x = [J.x,T.(J.x)] by A5;
then y1=J.x by XTUPLE_0:1;
hence y in rng J by FUNCT_2:112;
end;
hence thesis;
end;
then J is onto by TARSKI:2;
then reconsider L=J" as
Lipschitzian LinearOperator of X,graphNSP(T) by A17,Th7,A6;
consider K being Real such that
A19: 0 <= K &
for x being VECTOR of X holds ||. L.x .|| <= K * ||. x .||
by LOPBAN_1:def 8;
now
let y be Point of X;
y in the carrier of X; then
y in dom T by FUNCT_2:def 1; then
reconsider x= [y,T.y] as Point of graphNSP(T) by FUNCT_1:1;
A20: x = [J.x,T.(J.x)] by A5;
A21: ||. L.y .|| <= K * ||. y .|| by A19;
x in the carrier of graphNSP(T); then
A22: x in dom J by FUNCT_2:def 1;
A23: L.y = L.(J.x) by XTUPLE_0:1,A20
.= x by FUNCT_1:34,A17,A22;
reconsider x1=x as Point of [:X,Y:];
||.x1.|| = ||.x.|| by FUNCT_1:49;
then ||.T.y.|| <= ||. L.y .|| by A23, Th15;
hence ||.T.y.|| <= K * ||. y .|| by A21,XXREAL_0:2;
end;
hence T is Lipschitzian by A19;
end;
end;