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

definition

let X, Y be RealNormSpace;
let u be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y));

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

end;

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

definition

let X, Y be RealNormSpace;
let u be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y));
assume A1: u is invertible ;

func Inv u -> Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) equals :Def1: :: LOPBAN13:def 2
u " ;

correctness
coherence
u " is Point of (R_NormSpace_of_BoundedLinearOperators (Y,X));
by A1;

end;

:: deftheorem Def1 defines Inv LOPBAN13:def 2 :
for X, Y being RealNormSpace
for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) 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).|| <= (Partial_Sums ||.seq.||) . 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 ||.s.||

proof end;

theorem LM1: :: LOPBAN13:3

for X being Banach_Algebra
for z being Point of X st ||.z.|| < 1 holds
( z GeoSeq is norm_summable & ||.(Sum (z GeoSeq)).|| <= 1 / (1 - ||.z.||) )

proof end;

theorem LM2: :: LOPBAN13:4

for S being Banach_Algebra
for w being Point of S st ||.w.|| < 1 holds
( (1. S) + w is invertible & (- w) GeoSeq is norm_summable & ((1. S) + w) " = Sum ((- w) GeoSeq) & ||.(((1. S) + w) ").|| <= 1 / (1 - ||.w.||) )

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 (R_Normed_Algebra_of_BoundedLinearOperators X)
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 (R_NormSpace_of_BoundedLinearOperators (X,X))
for w1, w2 being Point of (R_Normed_Algebra_of_BoundedLinearOperators X)
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 (R_NormSpace_of_BoundedLinearOperators (X,X))
for w1, w2 being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) 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 (R_NormSpace_of_BoundedLinearOperators (X,X))
for w being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) 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 (R_NormSpace_of_BoundedLinearOperators (X,X)) st I = id X & ||.v.|| < 1 holds
( I + v is invertible & ||.(Inv (I + v)).|| <= 1 / (1 - ||.v.||) & ex w being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) 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 (R_NormSpace_of_BoundedLinearOperators (X,Y))
for g being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z))
for h being Point of (R_NormSpace_of_BoundedLinearOperators (Z,W)) holds h * (g * f) = (h * g) * f

proof end;

theorem FUNCT229: :: LOPBAN13:11

for X, Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) 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 (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds
( 0 < ||.u.|| & 0 < ||.(Inv u).|| )

proof end;

theorem Th2: :: LOPBAN13:13

for X, Y being non trivial RealBanachSpace
for u, v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible & ||.v.|| < 1 / ||.(Inv u).|| holds
( u + v is invertible & ||.(Inv (u + v)).|| <= 1 / ((1 / ||.(Inv u).||) - ||.v.||) & ex w being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) ex s, I being Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) st
( w = (Inv u) * v & s = w & I = id X & ||.s.|| < 1 & (- w) GeoSeq is norm_summable & I + s is invertible & ||.(Inv (I + s)).|| <= 1 / (1 - ||.s.||) & 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 (R_NormSpace_of_BoundedLinearOperators (X,Y)) st S = { v where v is Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible } holds
S is open

proof end;

definition

let X, Y be non trivial RealBanachSpace;

func InvertibleOperators (X,Y) -> open Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)) equals :: LOPBAN13:def 3
{ v where v is Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible } ;

correctness
coherence
{ v where v is Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible } is open Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y));

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 (R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible } ;

theorem LM60: :: LOPBAN13:15

for X, Y being non trivial RealBanachSpace
for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) 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 (R_NormSpace_of_BoundedLinearOperators (X,Y)) 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 (R_NormSpace_of_BoundedLinearOperators (X,Y)) 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 (R_Normed_Algebra_of_BoundedLinearOperators X) ex s, I being Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) st
( w = (Inv u) * (v - u) & s = w & I = id X & ||.s.|| < 1 & (- w) GeoSeq is norm_summable & I + s is invertible & ||.(Inv (I + s)).|| <= 1 / (1 - ||.s.||) & 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 (R_NormSpace_of_BoundedLinearOperators (X,Y))
for v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z))
for w being Point of (R_NormSpace_of_BoundedLinearOperators (X,Z)) st w = v * u holds
||.w.|| <= ||.v.|| * ||.u.||

proof end;

theorem LM100: :: LOPBAN13:19

for X, Y, Z being RealNormSpace
for u, v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for w being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) 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 (R_NormSpace_of_BoundedLinearOperators (X,Y))
for u, v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) 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 (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds u - (u + v) = - v

proof end;

theorem LM400: :: LOPBAN13:22

for X, Y being RealNormSpace
for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) 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 (R_NormSpace_of_BoundedLinearOperators (X,Y)) 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 (R_NormSpace_of_BoundedLinearOperators (X,Y)) 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 (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,X)) st dom I = InvertibleOperators (X,Y) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) 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 (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,X)) 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 (R_NormSpace_of_BoundedLinearOperators (Y,X)),(R_NormSpace_of_BoundedLinearOperators (X,Y)) 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 (R_NormSpace_of_BoundedLinearOperators (X,Y)) 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 (R_NormSpace_of_BoundedLinearOperators (X,Y))
for w being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) 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 (R_NormSpace_of_BoundedLinearOperators (X,Y))
for w being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds (- w) * (- u) = w * u

proof end;

theorem LOPBAN1624: :: LOPBAN13:28

for X, Y, Z being RealNormSpace
for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for w being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z))
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 (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,Z)),(R_NormSpace_of_BoundedLinearOperators (X,Z)) st
( I is_continuous_on the carrier of [:(R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,Z)):] & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) 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 (R_NormSpace_of_BoundedLinearOperators (X,Y))
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 (R_NormSpace_of_BoundedLinearOperators (X,Y))
for a being Real st v = w holds
- w = - v

proof end;