:: Banach's Continuous Inverse Theorem and Closed Graph Theorem
:: by Hideki Sakurai , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 6, 2012
:: Copyright (c) 2012-2017 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;
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:];
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:];
end;
theorem :: LOPBAN_7:1
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;
theorem :: LOPBAN_7:2
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;
theorem :: LOPBAN_7:3
for X,Y be RealNormSpace,
f be LinearOperator of X,Y holds 0.Y=f.(0.X);
theorem :: LOPBAN_7:4
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;
theorem :: LOPBAN_7:5
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;
theorem :: LOPBAN_7:6
for X,Y be RealNormSpace, f be LinearOperator of X,Y
holds f is Lipschitzian iff f is_continuous_on the carrier of X;
:: Banach's Continuous Inverse Theorem
theorem :: LOPBAN_7:7
for X,Y be RealBanachSpace,
T be Lipschitzian LinearOperator of X,Y
st T is bijective
holds T" is Lipschitzian LinearOperator of Y,X;
theorem :: LOPBAN_7:8
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];
definition
let X,Y be RealNormSpace;
let T be PartFunc of X, Y;
func graph(T) -> Subset of [:X,Y:] equals
:: LOPBAN_7:def 1
T;
end;
registration
let X,Y be RealNormSpace;
let T be non empty PartFunc of X, Y;
cluster graph(T) -> non empty;
end;
registration
let X,Y be RealNormSpace, T be LinearOperator of X,Y;
cluster graph(T) -> linearly-closed;
end;
definition
let X,Y be RealNormSpace;
let T be LinearOperator of X,Y;
func graphNrm(T) -> Function of graph(T),REAL equals
:: LOPBAN_7:def 2
(the normF of [:X,Y:]) | graph(T);
end;
definition
let X,Y be RealNormSpace;
let T be PartFunc of X,Y;
attr T is closed means
:: LOPBAN_7:def 3
graph(T) is closed;
end;
definition
let X,Y be RealNormSpace, T be LinearOperator of X,Y;
func graphNSP(T) -> non empty NORMSTR equals
:: LOPBAN_7:def 4
NORMSTR(# graph(T),Zero_(graph(T),[:X,Y:]), Add_(graph(T),[:X,Y:]),
Mult_(graph(T),[:X,Y:]),graphNrm(T) #);
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;
end;
theorem :: LOPBAN_7:9
for X,Y be RealNormSpace, T be LinearOperator of X,Y holds
graphNSP(T) is Subspace of [:X,Y:];
registration
let X,Y be RealNormSpace,
T be LinearOperator of X,Y;
cluster graphNSP(T) -> reflexive discerning RealNormSpace-like;
end;
theorem :: LOPBAN_7:10
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;
theorem :: LOPBAN_7:11
for X,Y be RealBanachSpace,
T be LinearOperator of X,Y st T is closed
holds graphNSP(T) is complete;
theorem :: LOPBAN_7:12
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);
theorem :: LOPBAN_7:13
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;
theorem :: LOPBAN_7:14
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;
:: The Closed Graph Theorem
theorem :: LOPBAN_7:15
for X,Y be RealNormSpace, x be Point of X, y be Point of Y holds
||.x.|| <= ||. [x,y] .|| & ||.y.|| <= ||. [x,y] .||;
registration
let X,Y be RealBanachSpace;
cluster closed -> Lipschitzian for LinearOperator of X,Y;
end;