:: Banach's Continuous Inverse Theorem and Closed Graph Theorem
:: by Hideki Sakurai , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 6, 2012
:: Copyright (c) 2012-2021 Association of Mizar Users

definition

let X, Y be non empty NORMSTR ;
let x be Point of X;
let y be Point of Y;
:: original: [
redefine func [x,y] -> Point of [:X,Y:];
coherence
[x,y] is Point of [:X,Y:] by ZFMISC_1:87;

end;

definition

let X, Y be non empty NORMSTR ;
let seqx be sequence of X;
let seqy be sequence of Y;
:: original: <:
redefine func <:seqx,seqy:> -> sequence of [:X,Y:];
coherence
<:seqx,seqy:> is sequence of [:X,Y:]

proof end;

end;

theorem Th1: :: LOPBAN_7:1

for X, Y being RealLinearSpace
for T being LinearOperator of X,Y st T is bijective holds
( T " is LinearOperator of Y,X & rng (T ") = the carrier of X )

proof end;

theorem :: LOPBAN_7:2

for X, Y being LinearTopSpace
for T being LinearOperator of X,Y
for S being Function of Y,X st T is bijective & T is open & S = T " holds
( S is LinearOperator of Y,X & S is onto & S is continuous )

proof end;

theorem Th3: :: LOPBAN_7:3

for X, Y being RealNormSpace
for f being LinearOperator of X,Y holds 0. Y = f . (0. X)

proof end;

theorem Th4: :: LOPBAN_7:4

for X, Y being RealNormSpace
for f being LinearOperator of X,Y
for x being Point of X holds
( f is_continuous_in x iff f is_continuous_in 0. X )

proof end;

theorem Th5: :: LOPBAN_7:5

for X, Y being RealNormSpace
for f being LinearOperator of X,Y holds
( f is_continuous_on the carrier of X iff f is_continuous_in 0. X )

proof end;

theorem Th6: :: LOPBAN_7:6

for X, Y being RealNormSpace
for f being LinearOperator of X,Y holds
( f is Lipschitzian iff f is_continuous_on the carrier of X )

proof end;

:: Banach's Continuous Inverse Theorem

theorem Th7: :: LOPBAN_7:7

for X, Y being RealBanachSpace
for T being Lipschitzian LinearOperator of X,Y st T is bijective holds
T " is Lipschitzian LinearOperator of Y,X

proof end;

theorem Th8: :: LOPBAN_7:8

for X, Y being RealNormSpace
for seqx being sequence of X
for seqy being sequence of Y
for x being Point of X
for y being 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 end;

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;

correctness
coherence
T is Subset of [:X,Y:];
;

end;

:: deftheorem defines graph LOPBAN_7:def 1 :
for X, Y being RealNormSpace
for T being PartFunc of X,Y holds graph T = T;

registration

let X, Y be RealNormSpace;
let T be non empty PartFunc of X,Y;

cluster graph T -> non empty ;

correctness
coherence
not graph T is empty ;
;

end;

registration

let X, Y be RealNormSpace;
let T be LinearOperator of X,Y;

cluster graph T -> linearly-closed ;

correctness
coherence
graph T is linearly-closed ;

proof end;

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);

correctness
coherence
the normF of [:X,Y:] | (graph T) is Function of (graph T),REAL;
;

end;

:: deftheorem defines graphNrm LOPBAN_7:def 2 :
for X, Y being RealNormSpace
for T being LinearOperator of X,Y holds graphNrm T = the normF of [:X,Y:] | (graph T);

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 ;

correctness
;

end;

:: deftheorem defines closed LOPBAN_7:def 3 :
for X, Y being RealNormSpace
for T being PartFunc of X,Y holds
( T is closed iff graph T is closed );

definition

let X, Y be RealNormSpace;
let 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) #);

correctness
coherence
NORMSTR(# (graph T),(Zero_ ((graph T),[:X,Y:])),(Add_ ((graph T),[:X,Y:])),(Mult_ ((graph T),[:X,Y:])),(graphNrm T) #) is non empty NORMSTR ;
;

end;

:: deftheorem defines graphNSP LOPBAN_7:def 4 :
for X, Y being RealNormSpace
for T being LinearOperator of X,Y holds graphNSP T = NORMSTR(# (graph T),(Zero_ ((graph T),[:X,Y:])),(Add_ ((graph T),[:X,Y:])),(Mult_ ((graph T),[:X,Y:])),(graphNrm T) #);

registration

let X, Y be RealNormSpace;
let T be LinearOperator of X,Y;

cluster graphNSP T -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence
( graphNSP T is Abelian & graphNSP T is add-associative & graphNSP T is right_zeroed & graphNSP T is right_complementable & graphNSP T is scalar-distributive & graphNSP T is vector-distributive & graphNSP T is scalar-associative & graphNSP T is scalar-unital )

proof end;

end;

theorem Th9: :: LOPBAN_7:9

for X, Y being RealNormSpace
for T being LinearOperator of X,Y holds graphNSP T is Subspace of [:X,Y:]

proof end;

Lm1: for X, Y being RealNormSpace
for T being LinearOperator of X,Y
for x, y being Point of (graphNSP T)
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (graphNSP T) ) & ( x = 0. (graphNSP T) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )

proof end;

registration

let X, Y be RealNormSpace;
let T be LinearOperator of X,Y;

cluster graphNSP T -> non empty discerning reflexive RealNormSpace-like ;

coherence
( graphNSP T is reflexive & graphNSP T is discerning & graphNSP T is RealNormSpace-like ) by Lm1;

end;

theorem Th10: :: LOPBAN_7:10

for X being RealNormSpace
for Y being RealBanachSpace
for X0 being 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 end;

theorem Th11: :: LOPBAN_7:11

for X, Y being RealBanachSpace
for T being LinearOperator of X,Y st T is closed holds
graphNSP T is complete

proof end;

theorem Th12: :: LOPBAN_7:12

for X, Y being RealNormSpace
for T being non empty PartFunc of X,Y holds
( T is closed iff for seq being 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 end;

theorem :: LOPBAN_7:13

for X, Y being RealNormSpace
for T being non empty PartFunc of X,Y
for T0 being LinearOperator of X,Y st T0 is Lipschitzian & dom T is closed & T = T0 holds
T is closed

proof end;

theorem :: LOPBAN_7:14

for X, Y being RealNormSpace
for T being non empty PartFunc of X,Y
for S being non empty PartFunc of Y,X st T is closed & T is one-to-one & S = T " holds
S is closed

proof end;

:: The Closed Graph Theorem

theorem Th15: :: LOPBAN_7:15

for X, Y being RealNormSpace
for x being Point of X
for y being Point of Y holds
( ||.x.|| <= ||.[x,y].|| & ||.y.|| <= ||.[x,y].|| )

proof end;

registration

let X, Y be RealBanachSpace;

cluster Function-like quasi_total additive homogeneous closed -> Lipschitzian for Element of bool [: the carrier of X, the carrier of Y:];

coherence
for b₁ being LinearOperator of X,Y st b₁ is closed holds
b₁ is Lipschitzian

proof end;

end;