let X, Y be 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) ) )
let u, v be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ( u is invertible & ||.v.|| < 1 / ||.(Inv u).|| implies ( 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) ) ) )
assume that
A1:
u is invertible
and
A2:
||.v.|| < 1 / ||.(Inv u).||
; ( 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) ) )
set S = R_Normed_Algebra_of_BoundedLinearOperators X;
1. (R_Normed_Algebra_of_BoundedLinearOperators X) = id X
;
then reconsider I = id X as Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) ;
reconsider Is = I as Point of (R_Normed_Algebra_of_BoundedLinearOperators X) ;
A6:
u is Lipschitzian LinearOperator of X,Y
by LOPBAN_1:def 9;
A7:
v is Lipschitzian LinearOperator of X,Y
by LOPBAN_1:def 9;
reconsider udv = (Inv u) * v as Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) ;
reconsider udv2 = udv as Point of (R_Normed_Algebra_of_BoundedLinearOperators X) ;
reconsider Lu = u, Lv = v as Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
reconsider LInvu = Inv u as Lipschitzian LinearOperator of Y,X by LOPBAN_1:def 9;
A14:
( modetrans (LInvu,Y,X) = LInvu & modetrans (Lv,X,Y) = Lv )
by LOPBAN_1:29;
then A15:
||.udv.|| <= ||.(Inv u).|| * ||.v.||
by LOPBAN_2:2;
LInvu = u "
by A1, Def1;
then A17: (BoundedLinearOperatorsNorm (X,X)) . (LInvu * Lu) =
||.(1. (R_Normed_Algebra_of_BoundedLinearOperators X)).||
by A1, FUNCT_2:29
.=
1
by LOPBAN_2:def 10
;
A18:
||.(Inv u).|| <> 0
then
||.(Inv u).|| * ||.v.|| < ||.(Inv u).|| * (1 / ||.(Inv u).||)
by A2, XREAL_1:68;
then A20:
||.(Inv u).|| * ||.v.|| < 1
by A18, XCMPLX_1:106;
then A21:
||.udv.|| < 1
by A15, XXREAL_0:2;
then A22:
( I + udv is invertible & ||.(Inv (I + udv)).|| <= 1 / (1 - ||.udv.||) & ex w being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) st
( w = udv & (- w) GeoSeq is norm_summable & Inv (I + udv) = Sum ((- w) GeoSeq) ) )
by Th1;
A23:
u + v is Lipschitzian LinearOperator of X,Y
by LOPBAN_1:def 9;
then A24:
modetrans ((u + v),X,Y) = u + v
by LOPBAN_1:29;
A25:
I + udv is Lipschitzian LinearOperator of X,X
by LOPBAN_1:def 9;
then A26:
modetrans ((I + udv),X,X) = I + udv
by LOPBAN_1:29;
A27:
modetrans (u,X,Y) = u
by A6, LOPBAN_1:29;
A28:
for x being Element of the carrier of X holds (u + v) . x = (u * (I + udv)) . x
proof
let x be
Element of the
carrier of
X;
(u + v) . x = (u * (I + udv)) . x
A33:
(u * (I + udv)) . x =
(modetrans (u,X,Y)) . ((modetrans ((I + udv),X,X)) . x)
by FUNCT_2:15
.=
u . ((I + udv) . x)
by A25, A27, LOPBAN_1:29
;
A35:
(I + udv) . x =
((id X) . x) + (udv . x)
by LOPBAN_1:35
.=
x + (udv . x)
;
Lu is
additive
;
then A37:
Lu . ((I + udv) . x) = (Lu . x) + (Lu . (udv . x))
by A35;
A39:
Inv u is
Lipschitzian LinearOperator of
Y,
X
by LOPBAN_1:def 9;
A40:
modetrans (
v,
X,
Y)
= v
by A7, LOPBAN_1:29;
u . (udv . x) =
u . ((modetrans ((Inv u),Y,X)) . ((modetrans (v,X,Y)) . x))
by FUNCT_2:15
.=
u . ((Inv u) . (v . x))
by A39, A40, LOPBAN_1:29
.=
u . ((u ") . (v . x))
by A1, Def1
.=
v . x
by A1, FUNCT_1:35
;
hence
(u + v) . x = (u * (I + udv)) . x
by A33, A37, LOPBAN_1:35;
verum
end;
then A43:
u + v is one-to-one
by A1, A22, A23, A26, A27, FUNCT_2:def 7;
A44:
modetrans (u,X,Y) is onto
by A1, A6, LOPBAN_1:29;
modetrans ((I + udv),X,X) is onto
by A22, A25, LOPBAN_1:29;
then
(modetrans (u,X,Y)) * (modetrans ((I + udv),X,X)) is onto
by A44, FUNCT_2:27;
then A46:
rng (u + v) = the carrier of Y
by A23, A28, FUNCT_2:def 7;
set Iuv = (Inv (I + udv)) * (Inv u);
(Inv (I + udv)) * (Inv u) is Lipschitzian LinearOperator of Y,X
by LOPBAN_2:2;
then A48:
modetrans (((Inv (I + udv)) * (Inv u)),Y,X) = (Inv (I + udv)) * (Inv u)
by LOPBAN_1:29;
Inv u is Lipschitzian LinearOperator of Y,X
by LOPBAN_1:def 9;
then A49:
modetrans ((Inv u),Y,X) = Inv u
by LOPBAN_1:29;
B49:
Inv (I + udv) is Lipschitzian LinearOperator of X,X
by LOPBAN_1:def 9;
then A50:
modetrans ((Inv (I + udv)),X,X) = Inv (I + udv)
by LOPBAN_1:29;
A51: modetrans (((I + udv) "),X,X) =
modetrans ((Inv (I + udv)),X,X)
by A21, Def1, Th1
.=
Inv (I + udv)
by B49, LOPBAN_1:29
.=
(I + udv) "
by A21, Def1, Th1
;
modetrans ((Inv u),Y,X) = u "
by A1, A49, Def1;
then A53: (Inv u) * u =
(u ") * u
by A6, LOPBAN_1:29
.=
id X
by A1, FUNCT229
;
(Inv u) * u is Lipschitzian LinearOperator of X,X
by LOPBAN_2:2;
then
modetrans (((Inv u) * u),X,X) = id X
by A53, LOPBAN_1:29;
then A55: ((Inv u) * u) * (I + udv) =
(id X) * (I + udv)
by A25, LOPBAN_1:29
.=
I + udv
by A25, FUNCT_2:17
;
A56: (modetrans (((Inv (I + udv)) * (Inv u)),Y,X)) * (modetrans ((u + v),X,Y)) =
((Inv (I + udv)) * (Inv u)) * (u + v)
.=
(Inv (I + udv)) * ((Inv u) * (u + v))
by RELAT136
.=
(Inv (I + udv)) * ((Inv u) * (u * (I + udv)))
by A23, A28, FUNCT_2:def 7
.=
(Inv (I + udv)) * (I + udv)
by A55, RELAT136
.=
(modetrans (((I + udv) "),X,X)) * (modetrans ((I + udv),X,X))
by A21, Def1, Th1
.=
((I + udv) ") * (I + udv)
by A25, A51, LOPBAN_1:29
.=
id X
by A22, FUNCT229
;
then A57:
(modetrans ((u + v),X,Y)) " = modetrans (((Inv (I + udv)) * (Inv u)),Y,X)
by A24, A43, A46, FUNCT_2:30;
thus A58:
u + v is invertible
by A24, A43, A46, A48, A56, FUNCT_2:30; ( ||.(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) ) )
reconsider Iuvp = (Inv (I + udv)) * (Inv u) as Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) ;
A59:
(BoundedLinearOperatorsNorm (Y,X)) . ((Inv (I + udv)) * (Inv u)) <= ((BoundedLinearOperatorsNorm (X,X)) . (modetrans ((Inv (I + udv)),X,X))) * ((BoundedLinearOperatorsNorm (Y,X)) . (modetrans ((Inv u),Y,X)))
by LOPBAN_2:2;
((BoundedLinearOperatorsNorm (X,X)) . (Inv (I + udv))) * ((BoundedLinearOperatorsNorm (Y,X)) . (Inv u)) <= (1 / (1 - ||.udv.||)) * ||.(Inv u).||
by A22, XREAL_1:64;
then A64:
||.Iuvp.|| <= (1 / (1 - ||.udv.||)) * ||.(Inv u).||
by A49, A50, A59, XXREAL_0:2;
A65:
1 - (||.(Inv u).|| * ||.v.||) <= 1 - ||.udv.||
by A14, LOPBAN_2:2, XREAL_1:10;
0 < 1 - (||.(Inv u).|| * ||.v.||)
by A20, XREAL_1:50;
then
1 / (1 - ||.udv.||) <= 1 / (1 - (||.(Inv u).|| * ||.v.||))
by A65, XREAL_1:118;
then
(1 / (1 - ||.udv.||)) * ||.(Inv u).|| <= (1 / (1 - (||.(Inv u).|| * ||.v.||))) * ||.(Inv u).||
by XREAL_1:64;
then A67:
(1 / (1 - ||.udv.||)) * ||.(Inv u).|| <= ||.(Inv u).|| / (1 - (||.(Inv u).|| * ||.v.||))
by XCMPLX_1:99;
(1 - (||.(Inv u).|| * ||.v.||)) / ||.(Inv u).|| =
(1 / ||.(Inv u).||) - ((||.(Inv u).|| * ||.v.||) / ||.(Inv u).||)
by XCMPLX_1:120
.=
(1 / ||.(Inv u).||) - ||.v.||
by A18, XCMPLX_1:89
;
then
1 / ((1 / ||.(Inv u).||) - ||.v.||) = ||.(Inv u).|| / (1 - (||.(Inv u).|| * ||.v.||))
by XCMPLX_1:57;
then
||.Iuvp.|| <= 1 / ((1 / ||.(Inv u).||) - ||.v.||)
by A64, A67, XXREAL_0:2;
hence
||.(Inv (u + v)).|| <= 1 / ((1 / ||.(Inv u).||) - ||.v.||)
by A24, A48, A57, A58, Def1; 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) )
consider w being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) such that
A70:
( w = udv & (- w) GeoSeq is norm_summable & Inv (I + udv) = Sum ((- w) GeoSeq) )
by A21, Th1;
reconsider S = Sum ((- w) GeoSeq) as Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) ;
take
w
; 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) )
take
udv
; ex I being Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) st
( w = (Inv u) * v & udv = w & I = id X & ||.udv.|| < 1 & (- w) GeoSeq is norm_summable & I + udv is invertible & ||.(Inv (I + udv)).|| <= 1 / (1 - ||.udv.||) & Inv (I + udv) = Sum ((- w) GeoSeq) & Inv (u + v) = (Inv (I + udv)) * (Inv u) )
take
I
; ( w = (Inv u) * v & udv = w & I = id X & ||.udv.|| < 1 & (- w) GeoSeq is norm_summable & I + udv is invertible & ||.(Inv (I + udv)).|| <= 1 / (1 - ||.udv.||) & Inv (I + udv) = Sum ((- w) GeoSeq) & Inv (u + v) = (Inv (I + udv)) * (Inv u) )
thus
( w = (Inv u) * v & udv = w & I = id X & ||.udv.|| < 1 & (- w) GeoSeq is norm_summable & I + udv is invertible & ||.(Inv (I + udv)).|| <= 1 / (1 - ||.udv.||) & Inv (I + udv) = Sum ((- w) GeoSeq) )
by A21, A70, Th1; Inv (u + v) = (Inv (I + udv)) * (Inv u)
thus
Inv (u + v) = (Inv (I + udv)) * (Inv u)
by A24, A48, A57, A58, Def1; verum