:: Invertible Operators on Banach Spaces
:: by Kazuhisa Nakasho
::
:: Received May 27, 2019
:: Copyright (c) 2019 Association of Mizar Users

definition
let X, Y be RealNormSpace;
let u be Point of ;
attr u is invertible means :: LOPBAN13:def 1
( u is one-to-one & rng u = the carrier of Y & u " is Point of );
end;

:: deftheorem defines invertible LOPBAN13:def 1 :
for X, Y being RealNormSpace
for u being Point of holds
( u is invertible iff ( u is one-to-one & rng u = the carrier of Y & u " is Point of ) );

definition
let X, Y be RealNormSpace;
let u be Point of ;
assume A1: u is invertible ;
func Inv u -> Point of equals :Def1: :: LOPBAN13:def 2
u " ;
correctness
coherence
u " is Point of
;
by A1;
end;

:: deftheorem Def1 defines Inv LOPBAN13:def 2 :
for X, Y being RealNormSpace
for u being Point of st u is invertible holds
Inv u = u " ;

theorem LOPBAN410: :: LOPBAN13:1
for X being RealNormSpace
for seq being sequence of X
for k being Nat holds ||.((Partial_Sums seq) . k).|| <= () . k
proof end;

theorem LM0: :: LOPBAN13:2
for X being RealBanachSpace
for s being sequence of X st s is norm_summable holds
||.(Sum s).|| <= Sum
proof end;

theorem LM1: :: LOPBAN13:3
for X being Banach_Algebra
for z being Point of X st < 1 holds
( z GeoSeq is norm_summable & ||.(Sum ()).|| <= 1 / (1 - ) )
proof end;

theorem LM2: :: LOPBAN13:4
for S being Banach_Algebra
for w being Point of S st < 1 holds
( (1. S) + w is invertible & (- w) GeoSeq is norm_summable & ((1. S) + w) " = Sum ((- w) GeoSeq) & ||.(((1. S) + w) ").|| <= 1 / (1 - ) )
proof end;

theorem :: LOPBAN13:5
for X being non trivial RealBanachSpace
for v1, v2 being Lipschitzian LinearOperator of X,X
for w1, w2 being Point of
for a being Real st v1 = w1 & v2 = w2 holds
( v1 * v2 = w1 * w2 & v1 + v2 = w1 + w2 & a (#) v1 = a * w1 )
proof end;

theorem :: LOPBAN13:6
for X being non trivial RealBanachSpace
for v1, v2 being Point of
for w1, w2 being Point of
for a being Real st v1 = w1 & v2 = w2 holds
( v1 + v2 = w1 + w2 & a * v1 = a * w1 ) ;

theorem :: LOPBAN13:7
for X being non trivial RealBanachSpace
for v1, v2 being Point of
for w1, w2 being Point of st v1 = w1 & v2 = w2 holds
v1 * v2 = w1 * w2
proof end;

theorem LM4: :: LOPBAN13:8
for X being non trivial RealBanachSpace
for v being Point of
for w being Point of st v = w holds
( ( v is invertible implies w is invertible ) & ( w is invertible implies v is invertible ) & ( w is invertible implies v " = w " ) )
proof end;

theorem Th1: :: LOPBAN13:9
for X being non trivial RealBanachSpace
for v, I being Point of st I = id X & < 1 holds
( I + v is invertible & ||.(Inv (I + v)).|| <= 1 / (1 - ) & ex w being Point of st
( w = v & (- w) GeoSeq is norm_summable & Inv (I + v) = Sum ((- w) GeoSeq) ) )
proof end;

theorem RELAT136: :: LOPBAN13:10
for X, Y, Z, W being RealNormSpace
for f being Point of
for g being Point of
for h being Point of holds h * (g * f) = (h * g) * f
proof end;

theorem FUNCT229: :: LOPBAN13:11
for X, Y being RealNormSpace
for f being Point of st f is one-to-one & rng f = the carrier of Y holds
( (f ") * f = id X & f * (f ") = id Y )
proof end;

theorem LM50: :: LOPBAN13:12
for X, Y being non trivial RealBanachSpace
for u being Point of st u is invertible holds
( 0 < & 0 < ||.(Inv u).|| )
proof end;

theorem Th2: :: LOPBAN13:13
for X, Y being non trivial RealBanachSpace
for u, v being Point of st u is invertible & < 1 / ||.(Inv u).|| holds
( u + v is invertible & ||.(Inv (u + v)).|| <= 1 / ((1 / ||.(Inv u).||) - ) & ex w being Point of ex s, I being Point of st
( w = (Inv u) * v & s = w & I = id X & < 1 & (- w) GeoSeq is norm_summable & I + s is invertible & ||.(Inv (I + s)).|| <= 1 / (1 - ) & Inv (I + s) = Sum ((- w) GeoSeq) & Inv (u + v) = (Inv (I + s)) * (Inv u) ) )
proof end;

theorem Th3: :: LOPBAN13:14
for X, Y being non trivial RealBanachSpace
for S being Subset of st S = { v where v is Point of : v is invertible } holds
S is open
proof end;

definition
let X, Y be non trivial RealBanachSpace;
func InvertibleOperators (X,Y) -> open Subset of equals :: LOPBAN13:def 3
{ v where v is Point of : v is invertible } ;
correctness
coherence
{ v where v is Point of : v is invertible } is open Subset of
;
proof end;
end;

:: deftheorem defines InvertibleOperators LOPBAN13:def 3 :
for X, Y being non trivial RealBanachSpace holds InvertibleOperators (X,Y) = { v where v is Point of : v is invertible } ;

theorem LM60: :: LOPBAN13:15
for X, Y being non trivial RealBanachSpace
for u being Point of st u is invertible holds
( Inv u is invertible & Inv (Inv u) = u )
proof end;

theorem LM70: :: LOPBAN13:16
for X, Y being non trivial RealBanachSpace ex I being Function of (InvertibleOperators (X,Y)),(InvertibleOperators (Y,X)) st
( I is one-to-one & I is onto & ( for u being Point of st u in InvertibleOperators (X,Y) holds
I . u = Inv u ) )
proof end;

theorem LMTh2: :: LOPBAN13:17
for X, Y being non trivial RealBanachSpace
for u, v being Point of st u is invertible & ||.(v - u).|| < 1 / ||.(Inv u).|| holds
( v is invertible & ||.(Inv v).|| <= 1 / ((1 / ||.(Inv u).||) - ||.(v - u).||) & ex w being Point of ex s, I being Point of st
( w = (Inv u) * (v - u) & s = w & I = id X & < 1 & (- w) GeoSeq is norm_summable & I + s is invertible & ||.(Inv (I + s)).|| <= 1 / (1 - ) & Inv (I + s) = Sum ((- w) GeoSeq) & Inv v = (Inv (I + s)) * (Inv u) ) )
proof end;

theorem NRM: :: LOPBAN13:18
for X, Y, Z being RealNormSpace
for u being Point of
for v being Point of
for w being Point of st w = v * u holds
<= *
proof end;

theorem LM100: :: LOPBAN13:19
for X, Y, Z being RealNormSpace
for u, v being Point of
for w being Point of holds
( w * (u - v) = (w * u) - (w * v) & w * (u + v) = (w * u) + (w * v) )
proof end;

theorem LM200: :: LOPBAN13:20
for X, Y, Z being RealNormSpace
for w being Point of
for u, v being Point of holds
( (u - v) * w = (u * w) - (v * w) & (u + v) * w = (u * w) + (v * w) )
proof end;

theorem LM300: :: LOPBAN13:21
for X, Y being RealNormSpace
for u, v being Point of holds u - (u + v) = - v
proof end;

theorem LM400: :: LOPBAN13:22
for X, Y being RealNormSpace
for u being Point of st u is invertible holds
( (Inv u) * u = id X & u * (Inv u) = id Y )
proof end;

theorem LMTh3: :: LOPBAN13:23
for X, Y being non trivial RealBanachSpace
for u being Point of st u is invertible holds
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for v being Point of st ||.(v - u).|| < s holds
||.((Inv v) - (Inv u)).|| < r ) )
proof end;

theorem LM80: :: LOPBAN13:24
for X, Y being non trivial RealBanachSpace
for I being PartFunc of , st dom I = InvertibleOperators (X,Y) & ( for u being Point of st u in InvertibleOperators (X,Y) holds
I . u = Inv u ) holds
I is_continuous_on InvertibleOperators (X,Y)
proof end;

theorem :: LOPBAN13:25
for X, Y being non trivial RealBanachSpace ex I being PartFunc of , st
( dom I = InvertibleOperators (X,Y) & rng I = InvertibleOperators (Y,X) & I is one-to-one & I is_continuous_on InvertibleOperators (X,Y) & ex J being PartFunc of , st
( J = I " & J is one-to-one & dom J = InvertibleOperators (Y,X) & rng J = InvertibleOperators (X,Y) & J is_continuous_on InvertibleOperators (Y,X) ) & ( for u being Point of st u in InvertibleOperators (X,Y) holds
I . u = Inv u ) )
proof end;

theorem LOPBAN1623: :: LOPBAN13:26
for X, Y, Z being RealNormSpace
for u being Point of
for w being Point of holds
( w * (- u) = - (w * u) & (- w) * u = - (w * u) )
proof end;

theorem :: LOPBAN13:27
for X, Y, Z being RealNormSpace
for u being Point of
for w being Point of holds (- w) * (- u) = w * u
proof end;

theorem LOPBAN1624: :: LOPBAN13:28
for X, Y, Z being RealNormSpace
for u being Point of
for w being Point of
for r being Real holds
( w * (r * u) = (r * w) * u & (r * w) * u = (r * w) * u & (r * w) * u = r * (w * u) )
proof end;

theorem :: LOPBAN13:29
for X, Y, Z being RealNormSpace ex I being BilinearOperator of ,, st
( I is_continuous_on the carrier of & ( for u being Point of
for v being Point of holds I . (u,v) = v * u ) )
proof end;

theorem XXXX: :: LOPBAN13:30
for X, Y being RealNormSpace
for v being Lipschitzian LinearOperator of X,Y
for w being Point of
for a being Real st v = w holds
a * w = a (#) v
proof end;

theorem :: LOPBAN13:31
for X, Y being RealNormSpace
for v being Lipschitzian LinearOperator of X,Y
for w being Point of
for a being Real st v = w holds
- w = - v
proof end;