:: 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 b1 being LinearOperator of X,Y st b1 is closed holds
b1 is Lipschitzian
proof end;
end;