:: Invertible Operators on Banach Spaces
:: by Kazuhisa Nakasho
::
:: Received May 27, 2019
:: Copyright (c) 2019-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies LOPBAN13, NUMBERS, REAL_1, ZFMISC_1, NORMSP_1, PRE_TOPC,
PARTFUN1, FUNCT_1, NAT_1, SUBSET_1, RELAT_1, LOPBAN_1, RCOMP_1, MSSUBFAM,
TARSKI, ARYTM_3, VALUED_1, CARD_3, PREPOWER, SERIES_1, FUNCT_2, ARYTM_1,
SEQ_2, ORDINAL2, SUPINF_2, FCONT_1, STRUCT_0, CARD_1, METRIC_1, ALGSTR_0,
XXREAL_0, XBOOLE_0, CFCONT_1, COMPLEX1, LOPBAN_2, LOPBAN_3, MESFUNC1,
LOPBAN_8, PRALG_1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1,
ORDINAL1, RELSET_1, PARTFUN1,
FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, COMPLEX1, SEQ_2,
SERIES_1, PREPOWER, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, VECTSP_1,
VFUNCT_1, NORMSP_0, NORMSP_1, BHSP_4, LOPBAN_1, NDIFF_2, LOPBAN_2,
LOPBAN_3, LOPBAN_5, NFCONT_1, PRVECT_3, LOPBAN_8;
constructors SEQ_2, NFCONT_1, VFUNCT_1, COMSEQ_2, RELSET_1, NAT_D, SERIES_1,
RSSPACE3, LOPBAN_3, NDIFF_5, NDIFF_2, DOMAIN_1, PREPOWER, BHSP_4,
LOPBAN_5, LOPBAN_8;
registrations RELSET_1, STRUCT_0, XREAL_0, FUNCT_1, VALUED_0, FUNCT_2,
NUMBERS, XBOOLE_0, RELAT_1, ORDINAL1, LOPBAN_1, PRVECT_3, XXREAL_0,
LOPBAN_2, NORMSP_1, NORMSP_3, LOPBAN_3;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities RLVECT_1, LOPBAN_1, NDIFF_2, NORMSP_0, BINOP_1, STRUCT_0, LOPBAN_2,
SERIES_1, ALGSTR_0, LOPBAN_3;
expansions VECTSP_1, LOPBAN_3, SERIES_1, FUNCT_2;
theorems TARSKI, XBOOLE_0, RLVECT_1, RELAT_1, FUNCT_1, VFUNCT_1, FUNCT_2,
LOPBAN_1, PARTFUN1, NFCONT_1, SEQ_2, XXREAL_0, PREPOWER, BHSP_4,
XCMPLX_1, ABSVALUE, NORMSP_0, PRVECT_3, SERIES_1, LOPBAN_3, RLVECT_4,
NDIFF_8, XTUPLE_0, NORMSP_1, XREAL_1, LOPBAN_2, LOPBAN_8;
schemes FUNCT_2, NAT_1;
begin :: Neumann series and invertible operator
reserve X,Y,Z for non trivial RealBanachSpace;
definition
let X,Y be RealNormSpace;
let u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
attr u is invertible means
u is one-to-one & rng u = the carrier of Y
& u" is Point of R_NormSpace_of_BoundedLinearOperators(Y,X);
end;
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:
u";
correctness by A1;
end;
theorem LOPBAN410:
for X be RealNormSpace, seq be sequence of X, k be Nat
holds ||.Partial_Sums(seq).k.|| <= Partial_Sums(||.seq.||).k
proof
let X be RealNormSpace, seq be sequence of X;
defpred P[Nat] means
||. Partial_Sums(seq).$1 .|| <= Partial_Sums(||.seq.||).$1;
A1: now
let k be Nat;
assume P[k]; then
A2: ||.Partial_Sums(seq).k.|| + ||.(seq).(k+1).||
<= Partial_Sums(||.seq.|| ).k + ||.(seq).(k+1).|| by XREAL_1:6;
A3: ||. Partial_Sums(seq).k + (seq).(k+1) .||
<= ||. Partial_Sums(seq).k .|| + ||. (seq).(k+1) .|| by NORMSP_1:def 1;
||. Partial_Sums(seq).(k+1) .||
= ||. Partial_Sums(seq).k + (seq).(k+1) .|| by BHSP_4:def 1; then
||. Partial_Sums(seq).(k+1) .||
<= Partial_Sums(||.seq.||).k + ||.seq.(k+1).|| by A3,A2,XXREAL_0:2; then
||. Partial_Sums(seq).(k+1) .||
<= Partial_Sums(||.seq.||).k+||.seq.||.(k+1) by NORMSP_0:def 4;
hence P[k+1] by SERIES_1:def 1;
end;
Partial_Sums(||.seq.||).0 = (||.seq.||).0 by SERIES_1:def 1
.= ||. seq.0 .|| by NORMSP_0:def 4; then
A4: P[0] by BHSP_4:def 1;
for k be Nat holds P[k] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
theorem LM0:
for X be RealBanachSpace, s be sequence of X st s is norm_summable
holds ||. Sum s .|| <= Sum ||.s.||
proof
let X be RealBanachSpace, s be sequence of X;
assume
A1: s is norm_summable; then
A3: ||.s.|| is summable;
A5: now let k be Nat;
||. Partial_Sums s .|| . k = ||.((Partial_Sums s) . k).||
by NORMSP_0:def 4;
hence ||. Partial_Sums s .|| . k <= (Partial_Sums ||.s.||) . k
by LOPBAN410;
end;
A6: s is summable by A1; then
A8: ||. Partial_Sums s .|| is convergent by NORMSP_1:23;
lim ||. Partial_Sums s .|| = ||. Sum s .|| by A6,LOPBAN_1:20;
hence ||. Sum s .|| <= Sum ||.s.|| by A3,A5,A8,SEQ_2:18;
end;
theorem LM1:
for X be Banach_Algebra, z be Point of X st ||.z.|| < 1 holds
z GeoSeq is norm_summable
& ||.Sum ( z GeoSeq ).|| <= 1 / ( 1 - ||.z.|| )
proof
let X be Banach_Algebra;
let z be Element of X;
A1: for n being Nat holds
( 0 <= ||.(z GeoSeq).|| . n
& ||.(z GeoSeq).|| . n <= (||.z.|| GeoSeq) . n )
proof
defpred S1[Nat] means
( 0 <= ||.(z GeoSeq).|| . $1
& ||.(z GeoSeq).|| . $1 <= (||.z.|| GeoSeq) . $1 );
A3: for k being Nat st S1[k] holds S1[k + 1]
proof
let k be Nat;
||.(((z GeoSeq) . k) * z).|| <= ||.((z GeoSeq) . k).|| * ||.z.||
by LOPBAN_2:def 9; then
A4: ||.(((z GeoSeq) . k) * z).|| <= (||.(z GeoSeq).|| . k) * ||.z.||
by NORMSP_0:def 4;
assume S1[k]; then
(||.(z GeoSeq).|| . k) * ||.z.|| <= ((||.z.|| GeoSeq) . k) * ||.z.||
by XREAL_1:64; then
A5: ||.(((z GeoSeq) . k) * z).|| <= ((||.z.|| GeoSeq) . k) * ||.z.||
by A4,XXREAL_0:2;
||.(z GeoSeq).|| . (k + 1)
= ||.((z GeoSeq) . (k + 1)).|| by NORMSP_0:def 4
.= ||.(((z GeoSeq) . k) * z).|| by LOPBAN_3:def 9;
hence S1[k + 1] by A5,PREPOWER:3;
end;
||.((z GeoSeq) . 0).|| = ||.(1. X).|| by LOPBAN_3:def 9
.= 1 by LOPBAN_2:def 10
.= (||.z.|| GeoSeq) . 0 by PREPOWER:3; then
A6: S1[ 0 ] by NORMSP_0:def 4;
for n being Nat holds S1[n] from NAT_1:sch 2(A6,A3);
hence for n being Nat holds
( 0 <= ||.(z GeoSeq).|| . n
& ||.(z GeoSeq).|| . n <= (||.z.|| GeoSeq) . n );
end;
assume ||.z.|| < 1; then
|.||.z.||.| < 1 by ABSVALUE:def 1; then
A7: ||.z.|| GeoSeq is summable
& Sum (||.z.|| GeoSeq) = 1 / (1 - ||.z.||) by SERIES_1:24; then
A8: ||.(z GeoSeq).|| is summable
& Sum ||.(z GeoSeq).|| <= Sum (||.z.|| GeoSeq) by A1,SERIES_1:20;
z GeoSeq is norm_summable by A1,A7,SERIES_1:20; then
||.Sum (z GeoSeq ).|| <= Sum ||.(z GeoSeq).|| by LM0;
hence thesis by A7,A8,XXREAL_0:2;
end;
theorem LM2:
for S be Banach_Algebra, w be 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
let S be Banach_Algebra,
w be Point of S;
assume
A1: ||.w.|| < 1;
set x = 1.S + w;
A2: ||.(1. S) - x.|| = ||.x -1.S .|| by NORMSP_1:7
.= ||.w.|| by RLVECT_4:1; then
A3: x is invertible & x" = Sum ( (1. S - x) GeoSeq ) by A1,LOPBAN_3:42;
1.S - x = 1.S - 1.S - w by RLVECT_1:27
.= 0.S - w by RLVECT_1:15
.= -w by RLVECT_1:14;
hence thesis by A1,A2,A3,LM1;
end;
theorem
for X be non trivial RealBanachSpace,
v1,v2 be Lipschitzian LinearOperator of X,X,
w1,w2 be Point of R_Normed_Algebra_of_BoundedLinearOperators X,
a be Real
st v1 = w1 & v2 = w2
holds
v1 * v2 = w1 * w2
& v1 + v2 = w1 + w2
& a (#) v1 =a * w1
proof
let X be non trivial RealBanachSpace,
v1,v2 be Lipschitzian LinearOperator of X,X,
w1,w2 be Point of R_Normed_Algebra_of_BoundedLinearOperators X,
a be Real;
set S = R_Normed_Algebra_of_BoundedLinearOperators X;
assume
A1: v1 = w1 & v2 = w2;
reconsider zw1 = w1, zw2 = w2 as
Element of BoundedLinearOperators (X,X);
v1 = modetrans(v1,X,X) & v2 = modetrans(v2,X,X) by LOPBAN_1:29;
hence v1 * v2 = zw1 * zw2 by A1
.= w1 * w2 by LOPBAN_2:def 4;
reconsider zw1 = w1,zw2 = w2 as
Point of R_NormSpace_of_BoundedLinearOperators(X,X);
reconsider zw12 = zw1 + zw2 as
Point of R_NormSpace_of_BoundedLinearOperators(X,X);
zw12 is Lipschitzian LinearOperator of X,X by LOPBAN_1:def 9; then
A4: dom zw12 = the carrier of X by FUNCT_2:def 1;
A5: dom (v1 + v2)
= dom v1 /\ dom v2 by VFUNCT_1:def 1
.= (the carrier of X) /\ dom v2 by FUNCT_2:def 1
.= (the carrier of X) /\ the carrier of X by FUNCT_2:def 1
.= the carrier of X;
for s being object st s in dom (v1 + v2) holds (v1 + v2).s = zw12.s
proof
let s be object;
assume
A6: s in dom (v1+v2); then
reconsider d = s as Point of X;
thus (v1 + v2).s = (v1 + v2)/.d by A5,PARTFUN1:def 6
.= v1/.d + v2/.d by A6,VFUNCT_1:def 1
.= zw12.s by A1,LOPBAN_1:35;
end;
hence v1 + v2 = w1 + w2 by A4,A5,FUNCT_1:2;
reconsider zw12 = a * zw1 as
Point of R_NormSpace_of_BoundedLinearOperators(X,X);
zw12 is Lipschitzian LinearOperator of X,X by LOPBAN_1:def 9; then
A8: dom zw12 = the carrier of X by FUNCT_2:def 1;
A9: dom (a(#)v1)
= dom v1 by VFUNCT_1:def 4
.= the carrier of X by FUNCT_2:def 1;
for s being object st s in dom (a(#)v1) holds (a(#)v1) . s = zw12 . s
proof
let s be object;
assume
A10: s in dom (a(#)v1); then
reconsider d = s as Point of X;
thus (a(#)v1) . s = (a(#)v1)/.d by A9,PARTFUN1:def 6
.= a * v1/.d by A10,VFUNCT_1:def 4
.= zw12.s by A1,LOPBAN_1:36;
end;
hence a(#)v1 = a * w1 by A8,A9,FUNCT_1:2;
end;
theorem
for X be non trivial RealBanachSpace,
v1,v2 be Point of R_NormSpace_of_BoundedLinearOperators(X,X),
w1,w2 be Point of R_Normed_Algebra_of_BoundedLinearOperators X,
a be Real
st v1 = w1 & v2 = w2
holds v1 + v2 = w1 + w2
& a * v1 = a * w1;
theorem
for X be non trivial RealBanachSpace,
v1,v2 be Point of R_NormSpace_of_BoundedLinearOperators(X,X),
w1,w2 be Point of R_Normed_Algebra_of_BoundedLinearOperators X
st v1 = w1 & v2 = w2
holds v1 * v2 = w1 * w2
proof
let X be non trivial RealBanachSpace,
v1,v2 be Point of R_NormSpace_of_BoundedLinearOperators(X,X),
w1,w2 be Point of R_Normed_Algebra_of_BoundedLinearOperators X;
set S = R_Normed_Algebra_of_BoundedLinearOperators X;
assume
A1: v1= w1 & v2= w2;
reconsider zw1 = w1,zw2 = w2 as Element of BoundedLinearOperators (X,X);
thus v1*v2 = zw1 * zw2 by A1
.= w1 * w2 by LOPBAN_2:def 4;
end;
theorem LM4:
for X be non trivial RealBanachSpace,
v be Point of R_NormSpace_of_BoundedLinearOperators(X,X),
w be Point of R_Normed_Algebra_of_BoundedLinearOperators X
st v = w
holds
( v is invertible iff w is invertible )
& ( w is invertible implies v" = w" )
proof
let X be non trivial RealBanachSpace,
v be Point of R_NormSpace_of_BoundedLinearOperators(X,X),
w be Point of R_Normed_Algebra_of_BoundedLinearOperators X;
set S = R_Normed_Algebra_of_BoundedLinearOperators X;
assume
A1: v = w;
A2: v is Lipschitzian LinearOperator of X,X by LOPBAN_1:def 9;
A4: v is invertible implies w is invertible
proof
assume
A5: v is invertible; then
reconsider x = v" as Point of S;
A7: v" is Lipschitzian LinearOperator of X,X by A5,LOPBAN_1:def 9;
reconsider zx = x, zv = v as
Element of BoundedLinearOperators (X,X);
dom v = the carrier of X & rng v = the carrier of X
by A2,A5,FUNCT_2:def 1; then
A9: v" * v = id X
& v * v" = id X by A5,FUNCT_1:39;
A10: v" = modetrans(v",X,X)
& v = modetrans(v,X,X) by A2,A7,LOPBAN_1:29; then
A11: v" * v = zx * zv
.= x * w by A1,LOPBAN_2:def 4;
v * v" = zv * zx by A10
.= w * x by A1,LOPBAN_2:def 4;
hence w is invertible by A9,A11;
end;
w is invertible implies v is invertible & v" = w"
proof
assume
A13: w is invertible;
A14: v is Lipschitzian LinearOperator of X,X by LOPBAN_1:def 9;
reconsider y = w" as
Lipschitzian LinearOperator of X,X by LOPBAN_1:def 9;
reconsider zy = y, zw = w as
Element of BoundedLinearOperators(X,X);
A15: y = modetrans(y,X,X) & v = modetrans(v,X,X)
by A14,LOPBAN_1:29; then
A16: y * v = zy * zw by A1
.= w" * w by LOPBAN_2:def 4
.= id X by A13,LOPBAN_3:def 8;
A17: v * y = zw * zy by A1,A15
.= w * w" by LOPBAN_2:def 4
.= id X by A13,LOPBAN_3:def 8;
reconsider y0 = y, v0 = v as
Function of the carrier of X,the carrier of X by LOPBAN_1:def 9;
A18: dom v = the carrier of X by A14,FUNCT_2:def 1;
A19: v0 is one-to-one & v0 is onto by A16,A17,FUNCT_2:23; then
dom y = rng v by FUNCT_2:def 1;
hence thesis by A16,A18,A19,FUNCT_1:41;
end;
hence thesis by A4;
end;
theorem Th1:
for v,I be 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 be Point of R_Normed_Algebra_of_BoundedLinearOperators X
st w = v
& (-w) GeoSeq is norm_summable
& Inv(I+v) = Sum( (-w) GeoSeq )
proof
let v,I be Point of R_NormSpace_of_BoundedLinearOperators(X,X);
assume that
A1: I = id X and
A2: ||.v.|| < 1;
set S = R_Normed_Algebra_of_BoundedLinearOperators X;
reconsider w = v as Point of S;
set x = 1.S + w;
||.w.|| < 1 by A2; then
A3: x is invertible
& (-w) GeoSeq is norm_summable
& x" = Sum ( (-w) GeoSeq )
& ||.x".|| <= 1 / ( 1 - ||.w.|| ) by LM2;
hence
A6: I+v is invertible by A1,LM4;
A7: (I+v)" = x" by A1,A3,LM4;
hence ||.Inv (I+v).|| <= 1 / ( 1 - ||.v.|| ) by A3,A6,Def1;
thus thesis by A3,A6,A7,Def1;
end;
theorem RELAT136:
for X,Y,Z,W be RealNormSpace,
f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
g be Point of R_NormSpace_of_BoundedLinearOperators(Y,Z),
h be Point of R_NormSpace_of_BoundedLinearOperators(Z,W)
holds h*(g*f) = (h*g)*f
proof
let X,Y,Z,W be RealNormSpace,
f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
g be Point of R_NormSpace_of_BoundedLinearOperators(Y,Z),
h be Point of R_NormSpace_of_BoundedLinearOperators(Z,W);
A2: h*g is Lipschitzian LinearOperator of Y,W by LOPBAN_2:2;
g*f is Lipschitzian LinearOperator of X,Z by LOPBAN_2:2;
hence h*(g*f)
= modetrans(h,Z,W) * (modetrans(g,Y,Z) * modetrans(f,X,Y))
by LOPBAN_1:29
.= (modetrans(h,Z,W) * modetrans(g,Y,Z)) * modetrans(f,X,Y) by RELAT_1:36
.= (h*g)*f by A2,LOPBAN_1:29;
end;
theorem FUNCT229:
for X,Y be RealNormSpace,
f be 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
let X,Y be RealNormSpace,
f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
assume
A1: f is one-to-one & rng f = the carrier of Y;
A2: f is Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
hence f" * f = id X by A1,FUNCT_2:29;
thus f * f" = id Y by A1,A2,FUNCT_2:29;
end;
theorem LM50:
for u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
st u is invertible
holds 0 < ||.u.|| & 0 < ||.Inv u.||
proof
let u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
assume
A1: u is invertible;
set S = R_Normed_Algebra_of_BoundedLinearOperators X;
reconsider Lu = u 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;
A8: BoundedLinearOperatorsNorm(X,X).(LInvu*Lu)
<= (BoundedLinearOperatorsNorm(Y,X).LInvu)
* (BoundedLinearOperatorsNorm(X,Y).Lu) by LOPBAN_2:2;
LInvu = u" by A1,Def1; then
BoundedLinearOperatorsNorm(X,X).(LInvu*Lu)
= ||.1.S.|| by A1,FUNCT_2:29
.= 1 by LOPBAN_2:def 10;
then ||.Inv u.|| <> 0 & ||.u.|| <> 0 by A8;
hence 0 < ||.u.|| & 0 < ||.Inv u.||;
end;
theorem Th2:
for u,v be 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 be Point of R_Normed_Algebra_of_BoundedLinearOperators X,
s,I be 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
let u,v be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
assume that
A1: u is invertible and
A2: ||.v.|| < 1 / ||.Inv u .||;
set S = R_Normed_Algebra_of_BoundedLinearOperators X;
1.S = id X; then
reconsider I = id X
as Point of R_NormSpace_of_BoundedLinearOperators(X,X);
reconsider Is = I as Point of S;
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 S;
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.S.|| by A1,FUNCT_2:29
.= 1 by LOPBAN_2:def 10;
A18: ||.Inv u.|| <> 0
proof
assume ||.Inv u.|| = 0; then
1 <= 0 * (BoundedLinearOperatorsNorm(X,Y).u) by A17,LOPBAN_2:2;
hence contradiction;
end; 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 be 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 be Element of the carrier of X
holds (u+v).x = (u*(I+udv)).x
proof
let x be Element of the carrier of 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 thesis by A33,A37,LOPBAN_1:35;
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);
Iuv is Lipschitzian LinearOperator of Y,X by LOPBAN_2:2; then
A48: modetrans(Iuv,Y,X) = Iuv 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(Iuv,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(Iuv,Y,X)
by A24,A43,A46,FUNCT_2:30;
thus
A58: u+v is invertible by A24,A43,A46,A48,A56,FUNCT_2:30;
reconsider Iuvp = Iuv
as Point of R_NormSpace_of_BoundedLinearOperators(Y,X);
A59: BoundedLinearOperatorsNorm(Y,X).(Iuv)
<= (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;
consider w be 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,udv,I;
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;
thus Inv (u+v) = Inv (I+udv) * (Inv u) by A24,A48,A57,A58,Def1;
end;
theorem Th3:
for S be 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
let S be Subset of R_NormSpace_of_BoundedLinearOperators(X,Y);
assume
A1: S = {v where v is Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
: v is invertible};
set P = R_NormSpace_of_BoundedLinearOperators(X,Y);
for u be Point of P st u in S holds
ex r be Real st r > 0 & Ball(u,r) c= S
proof
let u be Point of P;
assume u in S; then
A2: ex v be Point of P
st u = v & v is invertible by A1; then
A3: 0 < ||.Inv u .|| by LM50;
set r = 1 / ||.Inv u .||;
take r;
thus 0 < r by A3,XREAL_1:139;
now
let x be object;
assume x in Ball(u,r); then
x in {y where y is Point of P: ||.y - u.|| < r} by NDIFF_8:17; then
consider v be Point of P such that
A4: x = v & ||.v - u.|| < r;
v = u + (v-u) by RLVECT_4:1; then
v is invertible by A2,A4,Th2;
hence x in S by A1,A4;
end;
hence Ball(u,r) c= S by TARSKI:def 3;
end;
hence S is open by NDIFF_8:20;
end;
definition
let X,Y;
func InvertibleOperators(X,Y)
-> open Subset of R_NormSpace_of_BoundedLinearOperators(X,Y)
equals
{ v where v is Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
: v is invertible };
correctness
proof
set S = { v where v is Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
: v is invertible };
now
let x be object;
assume x in S; then
ex v be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
st x = v & v is invertible;
hence x in the carrier of R_NormSpace_of_BoundedLinearOperators(X,Y);
end; then
reconsider S
as Subset of R_NormSpace_of_BoundedLinearOperators(X,Y) by TARSKI:def 3;
S is open by Th3;
hence thesis;
end;
end;
theorem LM60:
for u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
st u is invertible
holds Inv u is invertible & Inv Inv u = u
proof
let u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
assume
A1: u is invertible;
then A3: Inv u = u" by Def1;
reconsider Lu = u as Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
A5: rng Inv u = dom Lu by A1,A3,FUNCT_1:33
.= the carrier of X by FUNCT_2:def 1;
A6: (Inv u) " = u by A1,A3,FUNCT_1:43;
thus Inv u is invertible by A1,A3,A5,FUNCT_1:43;
hence Inv Inv u = u by A6,Def1;
end;
theorem LM70:
ex I be Function of InvertibleOperators(X,Y),InvertibleOperators(Y,X)
st I is one-to-one
& I is onto
& for u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
st u in InvertibleOperators(X,Y)
holds I.u = Inv u
proof
set S = R_NormSpace_of_BoundedLinearOperators(X,Y);
defpred P1[object,object] means
ex u be Point of S
st $1 = u & $2 = Inv u;
A1: for x being object st x in InvertibleOperators(X,Y) holds
ex y being object st y in InvertibleOperators(Y,X) & P1[x,y]
proof
let x be object;
assume x in InvertibleOperators(X,Y); then
consider u be Point of S such that
A2: x = u & u is invertible;
take y = Inv u;
y is invertible by A2,LM60;
hence y in InvertibleOperators(Y,X);
thus P1[x,y] by A2;
end;
consider I be Function of InvertibleOperators(X,Y),InvertibleOperators(Y,X)
such that
A3: for x being object st x in InvertibleOperators(X,Y)
holds P1[x,I . x] from FUNCT_2:sch 1(A1);
take I;
A4: for u be Point of S
st u in InvertibleOperators(X,Y)
holds I.u = Inv u
proof
let u be Point of S;
assume u in InvertibleOperators(X,Y); then
P1[u,I . u] by A3;
hence I.u = Inv u;
end;
A5: InvertibleOperators(X,Y) <> {}
implies InvertibleOperators(Y,X) <> {}
proof
assume InvertibleOperators(X,Y) <> {}; then
consider x be object such that
A6: x in InvertibleOperators(X,Y) by XBOOLE_0:def 1;
consider u be Point of S such that
A7: x = u & u is invertible by A6;
Inv u is invertible by A7,LM60; then
Inv u in InvertibleOperators(Y,X);
hence InvertibleOperators(Y,X) <> {};
end;
B7: for x1, x2 being object
st x1 in InvertibleOperators(X,Y)
& x2 in InvertibleOperators(X,Y)
& I . x1 = I . x2
holds x1 = x2
proof
let x1, x2 be object;
assume that
A8: x1 in InvertibleOperators(X,Y)
& x2 in InvertibleOperators(X,Y) and
A9: I . x1 = I . x2;
reconsider u1 = x1, u2 = x2 as Point of S by A8;
A10: ( ex v1 be Point of S st u1=v1 & v1 is invertible )
& ( ex v2 be Point of S st u2=v2 & v2 is invertible ) by A8;
A11: I.u1 = Inv u1 by A4,A8;
u1 = Inv Inv u1 by A10,LM60
.= Inv Inv u2 by A4,A8,A9,A11
.= u2 by A10,LM60;
hence x1 = x2;
end;
now
let y be object;
assume y in InvertibleOperators(Y,X); then
consider v be Point of R_NormSpace_of_BoundedLinearOperators(Y,X)
such that
A15: y = v & v is invertible;
Inv v is invertible by A15,LM60; then
A16: Inv v in InvertibleOperators(X,Y);
Inv Inv v = v by A15,LM60;
then y = I.(Inv v) by A4,A15,A16;
hence y in rng I by A5,A16,FUNCT_2:4;
end; then
InvertibleOperators(Y,X) c= rng I by TARSKI:def 3;
hence thesis by A4,A5,B7,FUNCT_2:19,XBOOLE_0:def 10;
end;
theorem LMTh2:
for u,v be 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 be Point of R_Normed_Algebra_of_BoundedLinearOperators X,
s,I be 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
let u,v be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
assume
A1: u is invertible & ||.v-u.|| < 1 / ||.Inv u .||;
set vu = v-u;
v = u + vu by RLVECT_4:1;
hence thesis by A1,Th2;
end;
begin :: Isomorphic Mapping to Inverse Operators
theorem NRM:
for X,Y,Z be RealNormSpace,
u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
v be Point of R_NormSpace_of_BoundedLinearOperators(Y,Z),
w be Point of R_NormSpace_of_BoundedLinearOperators(X,Z)
st w = v*u
holds ||.w.|| <= ||.v.|| * ||.u.||
proof
let X,Y,Z be RealNormSpace,
u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
v be Point of R_NormSpace_of_BoundedLinearOperators(Y,Z),
w be Point of R_NormSpace_of_BoundedLinearOperators(X,Z);
assume
A2: w = v*u;
modetrans(v,Y,Z) = v & modetrans(u,X,Y) = u by LOPBAN_1:def 11;
hence ||.w.|| <= ||.v.|| * ||.u.|| by A2,LOPBAN_2:2;
end;
theorem LM100:
for X,Y,Z be RealNormSpace,
u,v be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
w be Point of R_NormSpace_of_BoundedLinearOperators(Y,Z)
holds w*(u-v) = w*u-w*v & w*(u+v) = w*u+w*v
proof
let X,Y,Z be RealNormSpace,
u,v be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
w be Point of R_NormSpace_of_BoundedLinearOperators(Y,Z);
A2: modetrans(u,X,Y)=u by LOPBAN_1:def 11;
for x be Point of X holds (w*(u-v)).x =(w*u).x-(w*v).x
proof
let x be Point of X;
A6: modetrans(w,Y,Z) is additive;
thus (w*(u-v)).x
= modetrans(w,Y,Z).(modetrans(u-v,X,Y).x) by FUNCT_2:15
.= modetrans(w,Y,Z). ((u-v).x) by LOPBAN_1:def 11
.= modetrans(w,Y,Z).(u.x-v.x) by LOPBAN_1:40
.= modetrans(w,Y,Z).(u.x)+modetrans(w,Y,Z).(-v.x) by A6
.= modetrans(w,Y,Z).(u.x)+modetrans(w,Y,Z).((-1)*v.x) by RLVECT_1:16
.= modetrans(w,Y,Z).(u.x)+(-1) * modetrans(w,Y,Z).(v.x) by LOPBAN_1:def 5
.= modetrans(w,Y,Z).(u.x) -modetrans(w,Y,Z).(v.x) by RLVECT_1:16
.= modetrans(w,Y,Z).(modetrans(u,X,Y).x)
-modetrans(w,Y,Z).(modetrans(v,X,Y).x) by A2,LOPBAN_1:def 11
.= (modetrans(w,Y,Z)*modetrans(u,X,Y)).x
-modetrans(w,Y,Z).(modetrans(v,X,Y).x) by FUNCT_2:15
.= (w*u).x- (w*v).x by FUNCT_2:15;
end;
hence w*(u-v) = w*u-w*v by LOPBAN_1:40;
for x be Point of X holds (w*(u+v)).x = (w*u).x+(w*v).x
proof
let x be Point of X;
A7: modetrans(w,Y,Z) is additive;
thus (w*(u+v)).x
= modetrans(w,Y,Z).(modetrans(u+v,X,Y).x) by FUNCT_2:15
.= modetrans(w,Y,Z). ((u+v).x) by LOPBAN_1:def 11
.= modetrans(w,Y,Z).(u.x+v.x) by LOPBAN_1:35
.= modetrans(w,Y,Z).(u.x)+modetrans(w,Y,Z).(v.x) by A7
.= modetrans(w,Y,Z).(modetrans(u,X,Y).x)
+modetrans(w,Y,Z).(modetrans(v,X,Y).x) by A2,LOPBAN_1:def 11
.= (modetrans(w,Y,Z)*modetrans(u,X,Y)).x
+modetrans(w,Y,Z).(modetrans(v,X,Y).x) by FUNCT_2:15
.= (w*u).x + (w*v).x by FUNCT_2:15;
end;
hence w*(u+v) = w*u+w*v by LOPBAN_1:35;
end;
theorem LM200:
for X,Y,Z be RealNormSpace,
w be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
u,v be Point of R_NormSpace_of_BoundedLinearOperators(Y,Z)
holds (u-v)*w = u*w-v*w & (u+v)*w = u*w+v*w
proof
let X,Y,Z be RealNormSpace,
w be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
u,v be Point of R_NormSpace_of_BoundedLinearOperators(Y,Z);
A1: modetrans(w,X,Y)=w by LOPBAN_1:def 11;
A2: modetrans(u,Y,Z)=u by LOPBAN_1:def 11;
for x be Point of X holds ((u-v)*w).x =(u*w).x-(v*w).x
proof
let x be Point of X;
thus ((u-v)*w).x
= modetrans((u-v),Y,Z).(modetrans(w,X,Y).x) by FUNCT_2:15
.= modetrans((u-v),Y,Z). (w.x) by LOPBAN_1:def 11
.= (u-v).(w.x) by LOPBAN_1:def 11
.= u.(w.x)-v.(w.x) by LOPBAN_1:40
.= modetrans(u,Y,Z).(modetrans(w,X,Y).x)
-modetrans(v,Y,Z).(modetrans(w,X,Y).x) by A1,A2,LOPBAN_1:def 11
.= (modetrans(u,Y,Z)*modetrans(w,X,Y)).x
-modetrans(v,Y,Z).(modetrans(w,X,Y).x) by FUNCT_2:15
.= (u*w).x- (v*w).x by FUNCT_2:15;
end;
hence (u-v)*w = u*w-v*w by LOPBAN_1:40;
for x be Point of X holds ((u+v)*w).x = (u*w).x+(v*w).x
proof
let x be Point of X;
thus ((u+v)*w).x
= modetrans((u+v),Y,Z).(modetrans(w,X,Y).x) by FUNCT_2:15
.= modetrans((u+v),Y,Z). (w.x) by LOPBAN_1:def 11
.= (u+v).(w.x) by LOPBAN_1:def 11
.= u.(w.x)+v.(w.x) by LOPBAN_1:35
.= modetrans(u,Y,Z).(modetrans(w,X,Y).x)
+modetrans(v,Y,Z).(modetrans(w,X,Y).x) by A1,A2,LOPBAN_1:def 11
.= (modetrans(u,Y,Z)*modetrans(w,X,Y)).x
+modetrans(v,Y,Z).(modetrans(w,X,Y).x) by FUNCT_2:15
.= (u*w).x+ (v*w).x by FUNCT_2:15;
end;
hence (u+v)*w = u*w+v*w by LOPBAN_1:35;
end;
theorem LM300:
for X,Y be RealNormSpace,
u,v be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
holds u - (u+v) = -v
proof
let X,Y be RealNormSpace,
u,v be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
thus u - (u+v) = (u-u) -v by RLVECT_1:27
.= 0.R_NormSpace_of_BoundedLinearOperators(X,Y) -v by RLVECT_1:15
.= -v by RLVECT_1:14;
end;
theorem LM400:
for X,Y be RealNormSpace,
u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
st u is invertible
holds (Inv u) * u = id X
& u * (Inv u) = id Y
proof
let X,Y be RealNormSpace,
v be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
assume
A1: v is invertible;
v is Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
then A7: dom v = the carrier of X & rng v = the carrier of Y
by A1,FUNCT_2:def 1;
Inv v = v" by A1,Def1;
then A9: modetrans((Inv v),Y,X) = v" by LOPBAN_1:def 11;
then A11: (Inv v) * v = v" * v by LOPBAN_1:def 11;
v * (Inv v) = v * v" by A9,LOPBAN_1:def 11;
hence thesis by A1,A7,A11,FUNCT_1:39;
end;
theorem LMTh3:
for u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
st u is invertible holds
for r be Real st 0 < r
ex s be Real
st 0 < s
& for v be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
st ||.v-u.|| < s
holds ||.Inv v - Inv u .|| < r
proof
let u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
assume
A1: u is invertible;
let r be Real;
assume
A2: 0 < r;
set r0 = r/2;
A3: 0 < r0 & r0 < r by A2,XREAL_1:215,216;
set s1 = 1 / ||.Inv u .||;
set AG = R_Normed_Algebra_of_BoundedLinearOperators X;
A5: 0 < ||. Inv u .|| by A1,LM50; then
A6: 0 < s1 by XREAL_1:139;
set s2 = (1/2) / ||. Inv u .||;
A7: 0 < s2 by A5,XREAL_1:139;
A8: 0 < ||. Inv u .|| * ||. Inv u .|| by A5,XREAL_1:129;
A9: 0 < r0/2 by A3,XREAL_1:215;
set s3 = (r0/2) / (||. Inv u .|| * ||. Inv u .||);
A10: 0 < s3 by A8,A9,XREAL_1:139;
set s4 = min(s1,s2);
A11: 0 < s4 & s4 <= s1 & s4 <= s2 by A6,A7,XXREAL_0:15,17;
set s = min(s4,s3);
B11: 0 < s & s <= s4 & s <= s3 by A10,A11,XXREAL_0:15,17; then
A12: 0 < s & s <= s1 & s <= s2 & s <= s3 by A11,XXREAL_0:2;
take s;
thus 0 < s by A10,A11,XXREAL_0:15;
let v be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
assume
A13: ||.v-u.|| < s; then
||.v-u.|| < s1 by A12,XXREAL_0:2; then
consider w be Point of R_Normed_Algebra_of_BoundedLinearOperators X,
s,I be Point of R_NormSpace_of_BoundedLinearOperators(X,X)
such that
A14: 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) by A1,LMTh2;
reconsider sA = s as Point of AG;
A16: I * (Inv u) = (id X)*modetrans(Inv u,Y,X) by A14,LOPBAN_1:def 11
.= modetrans(Inv u,Y,X) by FUNCT_2:17
.= Inv u by LOPBAN_1:def 11;
reconsider IIu = I * (Inv u)
as Point of R_NormSpace_of_BoundedLinearOperators(Y,X);
Inv v - Inv u = (Inv(I+s) - I) * (Inv u) by A14,A16,LM200; then
A18: ||. Inv v - Inv u.|| <= ||. Inv(I+s) -I .|| * ||. Inv u .|| by NRM;
A19: Inv(I+s)*(I+s) = I by A14,LM400;
Inv(I+s)*I = modetrans(Inv(I+s),X,X) * (id X)
by A14,LOPBAN_1:def 11
.= modetrans(Inv(I+s),X,X) by FUNCT_2:17
.= Inv(I+s) by LOPBAN_1:def 11;
then Inv(I+s) - I = Inv(I+s) * (I - (I+s)) by A19,LM100
.= Inv(I+s) * (-s) by LM300; then
||. Inv(I+s) -I .|| <= ||.Inv(I+s) .|| * ||.-s.|| by NRM; then
A23: ||. Inv(I+s) -I .|| <= ||.Inv(I+s) .|| * ||.s.|| by NORMSP_1:2;
A24: ||.s.|| <= ||. Inv u .|| * ||.v-u.|| by A14,NRM;
||.Inv(I+s) .|| * ||.s.||
<= ||.Inv(I+s) .|| * (||. Inv u .|| * ||.v-u.|| )
by A14,NRM,XREAL_1:64; then
A25: ||. Inv(I+s) -I .||
<= ||.Inv(I+s) .|| * ||. Inv u .|| * ||.v-u.|| by A23,XXREAL_0:2;
||.Inv(I+s) .|| * ( ||. Inv u .|| * ||.v-u.|| )
<= ( 1 / ( 1 - ||.s.|| )) * ( ||. Inv u .|| * ||.v-u.|| )
by A14,XREAL_1:64; then
||. Inv(I+s) -I .||
<= ( 1 / ( 1 - ||.s.|| )) * ||. Inv u .|| * ||.v-u.||
by A25,XXREAL_0:2; then
||. Inv(I+s) -I .|| * ||. Inv u .||
<= (( 1 / ( 1 - ||.s.|| )) * ||. Inv u .|| * ||.v-u.||)
* ||. Inv u .|| by XREAL_1:64; then
A29: ||. Inv v - Inv u.||
<= (( 1 / ( 1 - ||.s.|| )) * ||. Inv u .|| * ||.v-u.||)
* ||. Inv u .|| by A18,XXREAL_0:2;
||.v-u.|| < s2 by A12,A13,XXREAL_0:2; then
||. Inv u .|| * ||.v-u.||
<= ||. Inv u .|| * ( (1/2) / ||. Inv u .|| ) by XREAL_1:64; then
||. Inv u .|| * ||.v-u.|| <= 1/2 by A5,XCMPLX_1:87; then
||.s.|| <= 1/2 by A24,XXREAL_0:2; then
1-1/2 <= 1-||.s.|| by XREAL_1:10; then
1 / (1-||.s.||) <= 1/(1/2) by XREAL_1:118; then
A32: ( 1/ ( 1 - ||.s.|| )) * (||. Inv u .|| * ||. Inv u .|| * ||.v-u.|| )
<= 2 * ( ||. Inv u .|| * ||. Inv u .|| * ||.v-u.|| ) by XREAL_1:64;
||.v-u.|| < s3 by B11,A13,XXREAL_0:2; then
||.v-u.|| * ( ||. Inv u .|| * ||. Inv u .|| )
<= s3 * ( ||. Inv u .|| * ||. Inv u .|| ) by XREAL_1:64; then
||.v-u.|| * ( ||. Inv u .|| * ||. Inv u .|| )
<= r0/2 by A8,XCMPLX_1:87; then
2 * ( ||. Inv u .|| * ( ||. Inv u .|| * ||.v-u.|| ) )
<= r0/2 * 2 by XREAL_1:64; then
( 1 / ( 1 - ||.s.|| )) * ( ||. Inv u .|| * ||. Inv u .|| * ||.v-u.|| )
<= r0 by A32,XXREAL_0:2; then
||. Inv v - Inv u.|| <= r0 by A29,XXREAL_0:2;
hence ||. Inv v - Inv u.|| < r by A3,XXREAL_0:2;
end;
theorem LM80:
for I be PartFunc of
R_NormSpace_of_BoundedLinearOperators(X,Y),
R_NormSpace_of_BoundedLinearOperators(Y,X)
st dom I = InvertibleOperators(X,Y)
& for u be 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
let I be PartFunc of
R_NormSpace_of_BoundedLinearOperators(X,Y),
R_NormSpace_of_BoundedLinearOperators(Y,X);
assume
A1: dom I = InvertibleOperators(X,Y)
& for u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
st u in InvertibleOperators(X,Y)
holds I.u = Inv u;
set S = R_NormSpace_of_BoundedLinearOperators(X,Y);
set T = InvertibleOperators(X,Y);
for x0 being Point of S
for r being Real st x0 in T & 0 < r holds
ex s being Real
st 0 < s
& for x1 being Point of S st x1 in T & ||.x1 - x0.|| < s
holds ||.(I /. x1) - (I /. x0).|| < r
proof
let x0 be Point of S;
let r be Real;
assume
A2: x0 in T & 0 < r; then
ex u be Point of S st x0 = u & u is invertible;
then consider s be Real such that
A4: 0 < s
& for v be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
st ||.v-x0.|| < s
holds ||.Inv v - Inv x0 .|| < r by A2,LMTh3;
take s;
thus 0 < s by A4;
let x1 be Point of S;
assume
A5: x1 in T & ||.x1 - x0.|| < s;
A7: I/.x0 = I.x0 by A1,A2,PARTFUN1:def 6
.= Inv x0 by A1,A2;
I/.x1 = I.x1 by A1,A5,PARTFUN1:def 6
.= Inv x1 by A1,A5;
hence thesis by A4,A5,A7;
end;
hence I is_continuous_on InvertibleOperators(X,Y) by A1,NFCONT_1:19;
end;
theorem
ex I be 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 be 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 be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
st u in InvertibleOperators(X,Y)
holds I.u = Inv u
proof
set S = R_NormSpace_of_BoundedLinearOperators(X,Y);
set K = R_NormSpace_of_BoundedLinearOperators(Y,X);
consider J be Function of InvertibleOperators(X,Y),InvertibleOperators(Y,X)
such that
A1: J is one-to-one
& J is onto
& for u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
st u in InvertibleOperators(X,Y)
holds J.u = Inv u by LM70;
A2: InvertibleOperators(X,Y) <> {} implies
InvertibleOperators(Y,X) <> {}
proof
assume InvertibleOperators(X,Y) <> {}; then
consider x be object such that
A3: x in InvertibleOperators(X,Y) by XBOOLE_0:def 1;
consider u be Point of S such that
A4: x=u & u is invertible by A3;
Inv u is invertible by A4,LM60; then
Inv u in InvertibleOperators(Y,X);
hence InvertibleOperators(Y,X) <> {};
end;
then dom J = InvertibleOperators(X,Y) by FUNCT_2:def 1; then
J in PFuncs (the carrier of R_NormSpace_of_BoundedLinearOperators(X,Y),
the carrier of R_NormSpace_of_BoundedLinearOperators(Y,X))
by A1,PARTFUN1:def 3; then
reconsider I = J
as PartFunc of the carrier of R_NormSpace_of_BoundedLinearOperators(X,Y),
the carrier of R_NormSpace_of_BoundedLinearOperators(Y,X)
by PARTFUN1:46;
take I;
thus
A9: dom I = InvertibleOperators(X,Y) by A2,FUNCT_2:def 1;
thus rng I = InvertibleOperators(Y,X) by A1;
thus I is one-to-one by A1;
reconsider L = J"
as Function of InvertibleOperators(Y,X), InvertibleOperators(X,Y)
by A1,FUNCT_2:25;
A14: dom (J") = InvertibleOperators(Y,X) by A1,FUNCT_1:33;
A16: rng (J") = dom J by A1,FUNCT_1:33
.= InvertibleOperators(X,Y) by A2,FUNCT_2:def 1; then
L in PFuncs (the carrier of R_NormSpace_of_BoundedLinearOperators(Y,X),
the carrier of R_NormSpace_of_BoundedLinearOperators(X,Y))
by A14,PARTFUN1:def 3; then
reconsider L
as PartFunc of the carrier of R_NormSpace_of_BoundedLinearOperators(Y,X),
the carrier of R_NormSpace_of_BoundedLinearOperators(X,Y)
by PARTFUN1:46;
for v be Point of R_NormSpace_of_BoundedLinearOperators(Y,X)
st v in InvertibleOperators(Y,X)
holds L.v = Inv v
proof
let v be Point of R_NormSpace_of_BoundedLinearOperators(Y,X);
assume v in InvertibleOperators(Y,X); then
consider u be object such that
A23: u in InvertibleOperators(X,Y) & J.u = v by A1,FUNCT_2:11;
reconsider u
as Point of R_NormSpace_of_BoundedLinearOperators(X,Y) by A23;
A24: ex u0 be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
st u = u0 & u0 is invertible by A23;
Inv v = Inv (Inv u) by A1,A23
.= u by A24,LM60;
hence thesis by A1,A2,A23,FUNCT_2:26;
end;
hence thesis by A1,A9,A14,A16,LM80;
end;
theorem LOPBAN1623:
for X,Y,Z be RealNormSpace,
u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
w be Point of R_NormSpace_of_BoundedLinearOperators(Y,Z)
holds w*(-u) = -w*u & (-w)*u = -w*u
proof
let X,Y,Z be RealNormSpace,
u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
w be Point of R_NormSpace_of_BoundedLinearOperators(Y,Z);
for x be Point of X holds (w*(-u)).x = (-1)*(w*u).x
proof
let x be Point of X;
thus (w*(-u)).x = modetrans(w,Y,Z).(modetrans(-u,X,Y).x) by FUNCT_2:15
.= modetrans(w,Y,Z).((-u).x ) by LOPBAN_1:def 11
.= modetrans(w,Y,Z).(((-1)*u).x ) by RLVECT_1:16
.= modetrans(w,Y,Z).((-1)*(u.x)) by LOPBAN_1:36
.= (-1) * modetrans(w,Y,Z).(u.x) by LOPBAN_1:def 5
.= (-1) * modetrans(w,Y,Z).(modetrans(u,X,Y).x) by LOPBAN_1:def 11
.= (-1) * (w*u).x by FUNCT_2:15;
end;
hence w*(-u) = (-1) * (w*u) by LOPBAN_1:36
.= -w*u by RLVECT_1:16;
for x be Point of X holds ((-w)*u).x = (-1)*(w*u).x
proof
let x be Point of X;
thus ((-w)*u).x = modetrans(-w,Y,Z).(modetrans(u,X,Y).x) by FUNCT_2:15
.= (-w).(modetrans(u,X,Y).x ) by LOPBAN_1:def 11
.= ((-1)*w).(modetrans(u,X,Y).x ) by RLVECT_1:16
.= (-1)* w.(modetrans(u,X,Y).x) by LOPBAN_1:36
.= (-1) * modetrans(w,Y,Z).(modetrans(u,X,Y).x) by LOPBAN_1:def 11
.= (-1) * (w*u).x by FUNCT_2:15;
end;
hence (-w)*u = (-1) * (w*u) by LOPBAN_1:36
.= -w*u by RLVECT_1:16;
end;
theorem
for X,Y,Z be RealNormSpace,
u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
w be Point of R_NormSpace_of_BoundedLinearOperators(Y,Z)
holds (-w)*(-u) = w*u
proof
let X,Y,Z be RealNormSpace,
u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
w be Point of R_NormSpace_of_BoundedLinearOperators(Y,Z);
thus (-w)*(-u) = -w*(-u) by LOPBAN1623
.=-(-w*u) by LOPBAN1623
.= w*u by RLVECT_1:17;
end;
theorem LOPBAN1624:
for X,Y,Z be RealNormSpace,
u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
w be Point of R_NormSpace_of_BoundedLinearOperators(Y,Z),
r be Real
holds w*(r*u) = r*w*u & (r*w)*u = r*w*u & r*w*u = r*(w*u)
proof
let X,Y,Z be RealNormSpace,
u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
w be Point of R_NormSpace_of_BoundedLinearOperators(Y,Z),
r be Real;
A3: for x be Point of X holds (w*(r*u)).x = r*(w*u).x
proof
let x be Point of X;
thus (w*(r*u)).x
= modetrans(w,Y,Z).(modetrans(r*u,X,Y).x) by FUNCT_2:15
.= modetrans(w,Y,Z).((r*u).x ) by LOPBAN_1:def 11
.= modetrans(w,Y,Z).(r*(u.x)) by LOPBAN_1:36
.= r * modetrans(w,Y,Z).(u.x) by LOPBAN_1:def 5
.= r * modetrans(w,Y,Z).(modetrans(u,X,Y).x) by LOPBAN_1:def 11
.= r * (w*u).x by FUNCT_2:15;
end;
for x be Point of X holds ((r*w)*u).x = r*(w*u).x
proof
let x be Point of X;
thus ((r*w)*u).x = modetrans(r*w,Y,Z).(modetrans(u,X,Y).x) by FUNCT_2:15
.= (r*w).(modetrans(u,X,Y).x ) by LOPBAN_1:def 11
.= r * w.(modetrans(u,X,Y).x) by LOPBAN_1:36
.= r * modetrans(w,Y,Z).(modetrans(u,X,Y).x) by LOPBAN_1:def 11
.= r * (w*u).x by FUNCT_2:15;
end;
then r*w*u = r*(w*u) by LOPBAN_1:36;
hence thesis by A3,LOPBAN_1:36;
end;
theorem
for X,Y,Z be RealNormSpace holds
ex I be 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 be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
v be Point of R_NormSpace_of_BoundedLinearOperators(Y,Z)
holds I.(u,v) = v*u
proof
let X,Y,Z be RealNormSpace;
set E = R_NormSpace_of_BoundedLinearOperators(X,Y);
set F = R_NormSpace_of_BoundedLinearOperators(Y,Z);
set G = R_NormSpace_of_BoundedLinearOperators(X,Z);
defpred P1[object,object] means
ex u be Point of E,v be Point of F
st $1=[u,v] & $2 = v*u;
A1: for x being object st x in the carrier of [:E,F:] holds
ex y being object st y in the carrier of G & P1[x,y]
proof
let x be object;
assume x in the carrier of [:E,F:]; then
consider u be Point of E,v be Point of F such that
A2: x = [u,v] by PRVECT_3:18;
take y = v*u;
thus y in the carrier of G & P1[x,y] by A2;
end;
consider L being Function of the carrier of [:E,F:],the carrier of G
such that
A3: for x being object st x in the carrier of [:E,F:]
holds P1[x,L . x] from FUNCT_2:sch 1(A1);
A4: for u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
v be Point of R_NormSpace_of_BoundedLinearOperators(Y,Z)
holds L.(u,v) = v*u
proof
let u be Point of E, v be Point of F;
consider u1 be Point of E, v1 be Point of F such that
A5: [u,v] = [u1,v1] & L.[u,v] = v1*u1 by A3;
u = u1 & v = v1 by A5,XTUPLE_0:1;
hence thesis by A5;
end;
A6: for x1,x2 be Point of E, y be Point of F
holds L.(x1+x2,y) = L.(x1,y) + L.(x2,y)
proof
let x1,x2 be Point of E, y be Point of F;
thus L.(x1+x2,y) = y*(x1+x2) by A4
.= y*x1 + y*x2 by LM100
.= L.(x1,y) + y*x2 by A4
.= L.(x1,y) + L.(x2,y) by A4;
end;
A7: for x be Point of E, y be Point of F, a be Real
holds L.(a*x,y) = a*L.(x,y)
proof
let x be Point of E, y be Point of F, a be Real;
thus L.(a*x,y) = y*(a*x) by A4
.= a*y*x by LOPBAN1624
.= a*(y*x) by LOPBAN1624
.= a*L.(x,y) by A4;
end;
A8: for x be Point of E, y1,y2 be Point of F
holds L.(x,y1+y2) = L.(x,y1) + L.(x,y2)
proof
let x be Point of E, y1,y2 be Point of F;
thus L. (x,y1+y2) = (y1+y2) * x by A4
.= y1*x + y2*x by LM200
.= L.(x,y1) + y2*x by A4
.= L.(x,y1) + L.(x,y2) by A4;
end;
for x be Point of E, y be Point of F, a be Real
holds L.(x,a*y) = a*L.(x,y)
proof
let x be Point of E, y be Point of F, a be Real;
thus L. (x,a*y) = (a*y)*x by A4
.= a*(y*x) by LOPBAN1624
.= a*L.(x,y) by A4;
end; then
reconsider L as BilinearOperator of E,F,G by A6,A7,A8,LOPBAN_8:12;
take L;
set K = 1;
for x be Point of E,y be Point of F
holds ||.L. (x,y) .|| <= K * ||.x.|| * ||.y.||
proof
let x be Point of E,y be Point of F;
L.(x,y) = y*x by A4;
hence ||.L. (x,y) .|| <= K * ||.x.|| * ||.y.|| by NRM;
end;
hence thesis by A4,LOPBAN_8:13;
end;
theorem XXXX:
for X,Y be RealNormSpace,
v be Lipschitzian LinearOperator of X,Y,
w be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
a be Real
st v = w
holds a*w = a(#)v
proof
let X,Y be RealNormSpace,
v be Lipschitzian LinearOperator of X,Y,
w be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
a be Real;
set S = R_Normed_Algebra_of_BoundedLinearOperators X;
assume
A1: v = w;
a*w is Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9; then
A3: dom (a*w) = the carrier of X by FUNCT_2:def 1;
A4: dom (a(#)v) = dom v by VFUNCT_1:def 4
.= the carrier of X by FUNCT_2:def 1;
for s being object st s in dom (a(#)v)
holds (a(#)v) . s = (a*w) . s
proof
let s be object;
assume
A5: s in dom (a(#)v); then
reconsider d = s as Point of X;
thus (a(#)v) . s = (a(#)v) /.d by A4,PARTFUN1:def 6
.= a*v/.d by A5,VFUNCT_1:def 4
.= (a*w).s by A1,LOPBAN_1:36;
end;
hence a(#)v = a*w by A3,A4,FUNCT_1:2;
end;
theorem
for X,Y be RealNormSpace,
v be Lipschitzian LinearOperator of X,Y,
w be Point of R_NormSpace_of_BoundedLinearOperators (X,Y),
a be Real
st v = w
holds -w = -v
proof
let X,Y be RealNormSpace,
v be Lipschitzian LinearOperator of X,Y,
w be Point of R_NormSpace_of_BoundedLinearOperators (X,Y),
a be Real;
assume
A1: v = w;
thus -w = (-1)*w by RLVECT_1:16
.= (-1)(#)v by A1,XXXX
.= -v by VFUNCT_1:23;
end;