:: Implicit Function Theorem -- Part {II}
:: by Kazuhisa Nakasho and Yasunari Shidama
::
:: 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 NUMBERS, REAL_1, ZFMISC_1, NORMSP_1, PRE_TOPC, PARTFUN1, FUNCT_1,
NAT_1, FDIFF_1, SUBSET_1, RELAT_1, LOPBAN_1, RCOMP_1, SQUARE_1, TARSKI,
ARYTM_3, VALUED_1, ALGSTR_0, PRALG_1, PREPOWER, FUNCT_2, ARYTM_1, SEQ_2,
ORDINAL2, SUPINF_2, FCONT_1, STRUCT_0, CARD_1, XXREAL_0, XBOOLE_0,
FINSEQ_1, RLVECT_1, CFCONT_1, NDIFF_7, MCART_1, CARD_3, METRIC_1,
LOPBAN_2, LOPBAN_3, SEQ_4, LOPBAN_8, LOPBAN13;
notations TARSKI, ZFMISC_1, SUBSET_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2,
BINOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, FINSEQ_1,
SEQ_4, STRUCT_0, PRE_TOPC, RLVECT_1, NORMSP_0, NORMSP_1, VFUNCT_1,
LOPBAN_1, LOPBAN_2, LOPBAN_3, LOPBAN_5, LOPBAN_8, NFCONT_1, PRVECT_2,
NDIFF_1, NDIFF_2, PRVECT_3, NDIFF_7, NDIFF_8, LOPBAN13;
constructors SQUARE_1, VFUNCT_1, NDIFF_1, RELSET_1, NAT_D, RSSPACE3, LOPBAN_3,
NDIFF_5, NDIFF_2, DOMAIN_1, LOPBAN_8, NDIFF_7, NDIFF_8, SEQ_4, LOPBAN_5,
LOPBAN13;
registrations RELSET_1, STRUCT_0, XREAL_0, MEMBERED, FUNCT_1, FUNCT_2,
XBOOLE_0, ORDINAL1, LOPBAN_1, LOPBAN_2, PRVECT_2, PRVECT_3, XXREAL_0,
XTUPLE_0, NDIFF_7, NDIFF_8, NORMSP_1, SQUARE_1, FINSEQ_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, NFCONT_1;
equalities RLVECT_1, LOPBAN_1, NDIFF_2, NORMSP_0, BINOP_1, SQUARE_1, PRVECT_3,
STRUCT_0, LOPBAN_2, XCMPLX_0, LOPBAN_5, NDIFF_7, LOPBAN13;
expansions NDIFF_7, LOPBAN13;
theorems TARSKI, XBOOLE_0, XBOOLE_1, RLVECT_1, ZFMISC_1, RELAT_1, FUNCT_1,
SQUARE_1, VFUNCT_1, FUNCT_2, LOPBAN_1, PARTFUN1, NFCONT_1, NDIFF_1,
VECTSP_1, XXREAL_0, XCMPLX_1, NORMSP_0, PRVECT_3, NDIFF_5, RLVECT_4,
NDIFF_7, NDIFF_8, SEQ_4, XTUPLE_0, NORMSP_1, PARTFUN2, VALUED_0, XREAL_1,
LOPBAN_2, LOPBAN_7, LOPBAN13;
schemes FUNCT_2;
begin :: Properties of Lipschitz continuous linear operators
reserve S,T,W,Y for RealNormSpace;
reserve f,f1,f2 for PartFunc of S,T;
reserve Z for Subset of S;
reserve i,n for Nat;
theorem LMDIFF:
for E,F be RealNormSpace,
f be PartFunc of E,F,
Z be Subset of E,
z be Point of E
st Z is open
& z in Z
& Z c= dom f
& f is_differentiable_in z
holds
f|Z is_differentiable_in z
& diff(f,z) = diff(f|Z,z)
proof
let E,F be RealNormSpace,
f be PartFunc of E,F,
Z be Subset of E,
z be Point of E;
assume
A1: Z is open & z in Z & Z c= dom f
& f is_differentiable_in z; then
consider N being Neighbourhood of z such that
A2: N c= dom f
& ex R being RestFunc of E,F
st for x being Point of E st x in N holds
(f /. x) - (f /. z) = diff(f,z).(x - z) + R /. (x - z)
by NDIFF_1:def 7;
consider r be Real such that
A3: r > 0 & Ball(z,r) c= Z by A1,NDIFF_8:20;
Ball(z,r) = {y where y is Point of E: ||.y - z.|| < r} by NDIFF_8:17; then
Z is Neighbourhood of z by A3,NFCONT_1:def 1; then
reconsider NZ = N /\ Z as Neighbourhood of z by NDIFF_5:8;
A4: dom (f|Z) = (dom f) /\ Z by RELAT_1:61;
A5: N /\ Z c= (dom f) /\ Z by A2,XBOOLE_1:26;
consider R being RestFunc of E,F such that
A6: for x being Point of E st x in N holds
(f /. x) - (f /. z) = diff(f,z).(x - z) + R /. (x - z) by A2;
A7: for x being Point of E st x in NZ holds
( f|Z /. x) - ( f|Z /. z) = diff(f,z).(x - z) + R /. (x - z)
proof
let x be Point of E;
assume
A8: x in NZ; then
A9: x in N & x in Z by XBOOLE_0:def 4; then
A15: f /. x = f.x by A2,PARTFUN1:def 6
.= (f|Z).x by A9,FUNCT_1:49
.= (f|Z) /. x by A4,A5,A8,PARTFUN1:def 6;
A14: z in NZ by NFCONT_1:4;
f /. z = f.z by A1,PARTFUN1:def 6
.= (f|Z).z by A1,FUNCT_1:49
.= (f|Z) /. z by A4,A5,A14,PARTFUN1:def 6;
hence thesis by A6,A9,A15;
end;
hence (f|Z) is_differentiable_in z by A2,A4,NDIFF_1:def 6,XBOOLE_1:26;
hence diff(f,z) = diff(f|Z,z) by A4,A5,A7,NDIFF_1:def 7;
end;
theorem LMPDIFF:
for E,F,G be RealNormSpace,
f be PartFunc of [:E,F:],G,
Z be Subset of [:E,F:],
z be Point of [:E,F:]
st Z is open & z in Z & Z c= dom f
holds
( f is_partial_differentiable_in`1 z
implies
( f|Z is_partial_differentiable_in`1 z
& partdiff`1(f,z) = partdiff`1(f|Z,z) ) )
&
( f is_partial_differentiable_in`2 z
implies
( f|Z is_partial_differentiable_in`2 z
& partdiff`2(f,z) = partdiff`2(f|Z,z) ) )
proof
let E,F,G be RealNormSpace,
f be PartFunc of [:E,F:],G,
Z be Subset of [:E,F:],
z be Point of [:E,F:];
assume
A1: Z is open & z in Z & Z c= dom f;
A2: ex x1 be Point of E, x2 being Point of F
st z = [x1,x2] by PRVECT_3:18;
thus f is_partial_differentiable_in`1 z implies
( f|Z is_partial_differentiable_in`1 z
& partdiff`1(f,z) = partdiff`1(f|Z,z) )
proof
assume
A4: f is_partial_differentiable_in`1 z;
set g = f * (reproj1 z);
consider N being Neighbourhood of (z `1) such that
A6: N c= dom g
& ex R being RestFunc of E,G
st for x being Point of E st x in N holds
(g /. x) - (g /. (z `1))
= partdiff`1(f,z) . (x - (z `1)) + R /. (x - (z `1))
by A4,NDIFF_1:def 7;
consider R being RestFunc of E,G such that
A7: for x being Point of E st x in N holds
(g /. x) - (g /. (z `1))
= partdiff`1(f,z) . (x - (z `1)) + R /. (x - (z `1)) by A6;
set h = (f|Z) * (reproj1 z);
A9: (reproj1 z).(z `1) = [z `1,z `2] by NDIFF_7:def 1
.= z by A2;
consider r1 be Real such that
A10: r1 > 0 & Ball(z,r1) c= Z by A1,NDIFF_8:20;
A11: Ball(z,r1) = {y where y is Point of [:E,F:] : ||.y - z.|| < r1}
by NDIFF_8:17;
consider r2 be Real such that
A13: r2 > 0
& {y where y is Point of E: ||.y - z `1.|| < r2} c= N
by NFCONT_1:def 1;
set r = min(r1,r2);
A14: 0 < r & r <= r1 & r <= r2 by A10,A13,XXREAL_0:15,17;
set M = Ball(z `1,r);
A15: M = {y where y is Point of E: ||.y - z `1.|| < r} by NDIFF_8:17;
then reconsider M as Neighbourhood of z `1 by A14,NFCONT_1:def 1;
A17: {y where y is Point of E: ||.y - z `1.|| < r2}
= Ball(z `1,r2) by NDIFF_8:17;
A18: M c= Ball(z `1,r2) by A14,NDIFF_8:15;
A19: M c= N & for x be Point of E st x in M holds (reproj1 z).x in Z
proof
thus M c= N by A13,A17,A18,XBOOLE_1:1;
let x be Point of E;
assume x in M; then
A20: ex y be Point of E st x=y & ||.y - z `1.|| < r by A15;
A21: (reproj1 z).x = [x,z `2] by NDIFF_7:def 1;
-z = [-z `1,-z `2] by A2,PRVECT_3:18; then
(reproj1 z).x - z = [x-z `1,z `2-z `2] by A21,PRVECT_3:18
.= [x-z `1,0.F] by RLVECT_1:15; then
||. (reproj1 z).x - z .|| = ||.x - z `1.|| by NDIFF_8:2; then
||. (reproj1 z).x - z .|| < r1 by A14,A20,XXREAL_0:2; then
(reproj1 z).x in {y where y is Point of [:E,F:] : ||.y - z.|| < r1};
hence (reproj1 z).x in Z by A10,A11;
end;
A22: dom (reproj1 z) = the carrier of E by FUNCT_2:def 1;
A23: dom (f|Z) = Z by A1,RELAT_1:62;
A24: M c= dom h
proof
let x be object;
assume
A25: x in M; then
(reproj1 z).x in Z by A19;
hence x in dom h by A22,A23,A25,FUNCT_1:11;
end;
A27: for x being Point of E st x in M holds
(h /. x) - (h /. (z `1))
= partdiff`1(f,z) . (x - (z `1)) + R /. (x - (z `1))
proof
let x be Point of E;
assume
A28: x in M; then
A29: x in N by A19;
A30: (z `1) in N by NFCONT_1:4;
A31: (z `1) in M by NFCONT_1:4;
A33: h /. x = h.x by A24,A28,PARTFUN1:def 6
.= (f|Z).((reproj1 z).x) by A22,FUNCT_1:13
.= f.((reproj1 z).x) by A19,A28,FUNCT_1:49
.= (f*(reproj1 z)).x by A22,FUNCT_1:13
.= g/.x by A6,A29,PARTFUN1:def 6;
h /. (z `1) = h.(z `1) by A24,A31,PARTFUN1:def 6
.= (f|Z).((reproj1 z).(z `1)) by A22,FUNCT_1:13
.= f.((reproj1 z).(z `1)) by A1,A9,FUNCT_1:49
.= (f*(reproj1 z)).(z `1) by A22,FUNCT_1:13
.= g/.(z `1) by A6,A30,PARTFUN1:def 6;
hence thesis by A7,A19,A28,A33;
end;
then A35: h is_differentiable_in z `1 by A24,NDIFF_1:def 6;
thus (f|Z) is_partial_differentiable_in`1 z
by A24,A27,NDIFF_1:def 6;
thus partdiff`1((f|Z),z) = partdiff`1(f,z) by A35,A24,A27,NDIFF_1:def 7;
end;
assume
A38: f is_partial_differentiable_in`2 z;
set g = f * (reproj2 z);
consider N being Neighbourhood of (z `2) such that
A40: N c= dom g
& ex R being RestFunc of F,G
st for x being Point of F st x in N holds
(g /. x) - (g /. (z `2))
= partdiff`2(f,z) . (x - (z `2)) + R /. (x - (z `2))
by A38,NDIFF_1:def 7;
consider R being RestFunc of F,G such that
A41: for x being Point of F st x in N holds
(g /. x) - (g /. (z `2))
= partdiff`2(f,z) . (x - (z `2)) + R /. (x - (z `2)) by A40;
set h = (f|Z) * (reproj2 z);
A43: (reproj2 z).(z `2) = [z `1,z `2] by NDIFF_7:def 2
.= z by A2;
consider r1 be Real such that
A44: r1 > 0 & Ball(z,r1) c= Z by A1,NDIFF_8:20;
A45: Ball(z,r1) = {y where y is Point of [:E,F:] : ||.y - z.|| < r1}
by NDIFF_8:17;
consider r2 be Real such that
A47: r2 > 0
& {y where y is Point of F: ||.y - z `2.|| < r2} c= N
by NFCONT_1:def 1;
set r = min(r1,r2);
A48: 0 < r & r <= r1 & r <= r2 by A44,A47,XXREAL_0:15,17;
set M = Ball(z `2,r);
A49: M = {y where y is Point of F: ||.y - z `2.|| < r}
by NDIFF_8:17; then
reconsider M as Neighbourhood of z `2 by A48,NFCONT_1:def 1;
A51: {y where y is Point of F: ||.y - z `2.|| < r2} = Ball(z `2,r2)
by NDIFF_8:17;
A52: M c= Ball(z `2,r2) by A48,NDIFF_8:15;
A53: M c= N
& for x be Point of F st x in M holds (reproj2 z).x in Z
proof
thus M c= N by A47,A51,A52,XBOOLE_1:1;
let x be Point of F;
assume x in M; then
A54: ex y be Point of F st x = y & ||.y - z `2.|| < r by A49;
A55: (reproj2 z).x = [z `1,x] by NDIFF_7:def 2;
-z = [-z `1,-z `2] by A2,PRVECT_3:18; then
(reproj2 z).x - z = [z `1- z `1, x-z `2] by A55,PRVECT_3:18
.= [0.E,x-z `2] by RLVECT_1:15; then
||. (reproj2 z).x - z .|| = ||.x - z `2.|| by NDIFF_8:3; then
||. (reproj2 z).x - z .|| < r1 by A48,A54,XXREAL_0:2; then
(reproj2 z).x in {y where y is Point of [:E,F:] : ||.y - z.|| < r1};
hence (reproj2 z).x in Z by A44,A45;
end;
A56: dom (reproj2 z) = the carrier of F by FUNCT_2:def 1;
A57: dom (f|Z) = Z by A1,RELAT_1:62;
A58: M c= dom h
proof
let x be object;
assume
A59: x in M; then
(reproj2 z).x in Z by A53;
hence x in dom h by A56,A57,A59,FUNCT_1:11;
end;
A61: for x being Point of F st x in M holds
(h /. x) - (h /. (z `2))
= partdiff`2(f,z) . (x - (z `2)) + R /. (x - (z `2))
proof
let x be Point of F;
assume
A62: x in M; then
A63: x in N by A53;
A64: (z `2) in N by NFCONT_1:4;
A65: (z `2) in M by NFCONT_1:4;
A67: h /. x = h.x by A58,A62,PARTFUN1:def 6
.= (f|Z).((reproj2 z).x) by A56,FUNCT_1:13
.= f.((reproj2 z).x) by A53,A62,FUNCT_1:49
.= (f*(reproj2 z)).x by A56,FUNCT_1:13
.= g/.x by A40,A63,PARTFUN1:def 6;
h /. (z `2) = h.(z `2) by A58,A65,PARTFUN1:def 6
.= (f|Z).((reproj2 z).(z `2)) by A56,FUNCT_1:13
.= f.((reproj2 z).(z `2)) by A1,A43,FUNCT_1:49
.= (f*(reproj2 z)).(z `2) by A56,FUNCT_1:13
.= g/.(z `2) by A40,A64,PARTFUN1:def 6;
hence thesis by A41,A53,A62,A67;
end;
thus then (f|Z) is_partial_differentiable_in`2 z
by A58,NDIFF_1:def 6;
h is_differentiable_in z `2 by A58,A61,NDIFF_1:def 6;
hence partdiff`2((f|Z),z) = partdiff`2(f,z) by A58,A61,NDIFF_1:def 7;
end;
theorem LmTh47:
for X,E,G,F be RealNormSpace,
BL be BilinearOperator of E,F,G,
f be PartFunc of X,E,
g be PartFunc of X,F,
S be Subset of X
st BL is_continuous_on the carrier of [:E,F:]
& S c= dom f & S c= dom g
& ( for s be Point of X st s in S holds f is_continuous_in s )
& ( for s be Point of X st s in S holds g is_continuous_in s )
holds
ex H be PartFunc of X,G
st dom H = S
& ( for s be Point of X st s in S holds H.s = BL. (f.s,g.s) )
& H is_continuous_on S
proof
let X,E,G,F be RealNormSpace,
BL be BilinearOperator of E,F,G,
f be PartFunc of X,E,
g be PartFunc of X,F,
S be Subset of X;
assume that
A1: BL is_continuous_on the carrier of [:E,F:] and
A2: S c= dom f & S c= dom g and
A3: ( for s be Point of X st s in S holds f is_continuous_in s ) and
A4: ( for s be Point of X st s in S holds g is_continuous_in s );
defpred P1[object,object] means
ex t be Point of X
st t = $1
& $2= BL.(f.t,g.t);
A5: for x being object st x in S holds
ex y being object st y in the carrier of G & P1[x,y]
proof
let x be object;
assume
A6: x in S; then
reconsider t = x as Point of X;
take y = BL.(f.t,g.t);
A7: f.t in rng f & g.t in rng g by A2,A6,FUNCT_1:3; then
reconsider p = f.t as Point of E;
reconsider q = g.t as Point of F by A7;
[p,q] is Point of [:E,F:];
hence y in the carrier of G & P1[x,y] by FUNCT_2:5;
end;
consider H being Function of S,G such that
A8: for z being object st z in S
holds P1[z,H.z] from FUNCT_2:sch 1(A5);
A9: dom H = S by FUNCT_2:def 1;
rng H c= the carrier of G;
then H in PFuncs(the carrier of X,the carrier of G)
by A9,PARTFUN1:def 3; then
reconsider H as PartFunc of X,G by PARTFUN1:46;
take H;
thus
A12: dom H = S by FUNCT_2:def 1;
thus
A13: for s be Point of X st s in S holds H.s = BL. (f.s,g.s)
proof
let s be Point of X;
assume s in S; then
ex t be Point of X st t = s & H.s = BL.(f.t,g.t) by A8;
hence thesis;
end;
for x0 being Point of X
for r being Real st x0 in S & 0 < r
holds
ex pq being Real
st 0 < pq
& for x1 being Point of X
st x1 in S
& ||.x1 - x0.|| < pq
holds ||.H /. x1 - H /. x0.|| < r
proof
let x0 be Point of X;
let r be Real;
assume
A16: x0 in S & 0 < r; then
A17: f is_continuous_in x0 by A3;
A18: g is_continuous_in x0 by A4,A16;
A20: f.x0 in rng f & g.x0 in rng g by A2,A16,FUNCT_1:3;
[f.x0,g.x0] is set by TARSKI:1; then
reconsider z0 = [f.x0,g.x0] as Point of [:E,F:] by A20,PRVECT_3:18;
consider s being Real such that
A21: 0 < s
& for z1 being Point of [:E,F:]
st z1 in the carrier of [:E,F:]
& ||.z1 - z0.|| < s
holds ||.BL /. z1 - BL /. z0.|| < r by A1,A16,NFCONT_1:19;
set s1 = s/2;
consider p being Real such that
A23: 0 < p
& for x1 being Point of X
st x1 in dom f & ||. x1 - x0.|| < p
holds ||. f /. x1 - f /. x0.|| < s1
by A17,A21,NFCONT_1:7,XREAL_1:215;
consider q being Real such that
A24: 0 < q
& for x1 being Point of X
st x1 in dom g & ||. x1 - x0.|| < q
holds ||. g /. x1 - g /. x0.|| < s1
by A18,A21,NFCONT_1:7,XREAL_1:215;
set pq = min(p,q);
A25: 0 < pq & pq <= p & pq <= q by A23,A24,XXREAL_0:15,17;
take pq;
thus 0 < pq by A23,A24,XXREAL_0:15;
thus for x1 being Point of X
st x1 in S & ||.x1 - x0.|| < pq
holds ||.H /. x1 - H /. x0.|| < r
proof
let x1 be Point of X;
assume
A26: x1 in S & ||.x1 - x0.|| < pq; then
A27: ||.x1 - x0.|| < p & ||.x1 - x0.|| < q by A25,XXREAL_0:2; then
A29: ||. f /. x1 - f /. x0.|| < s1 by A2,A23,A26;
A30: ||. g /. x1 - g /. x0.|| < s1 by A2,A24,A26,A27;
A32: f.x1 in rng f & g.x1 in rng g by A2,A26,FUNCT_1:3;
[f.x1,g.x1] is set by TARSKI:1; then
reconsider z1=[f.x1,g.x1] as Point of [:E,F:] by A32,PRVECT_3:18;
A33: z1 = [f/.x1,g.x1] by A2,A26,PARTFUN1:def 6
.= [f/.x1,g/.x1] by A2,A26,PARTFUN1:def 6;
z0 = [f/.x0,g.x0] by A2,A16,PARTFUN1:def 6
.= [f/.x0,g/.x0] by A2,A16,PARTFUN1:def 6; then
-z0 = [-f/.x0,-g/.x0] by PRVECT_3:18; then
z1 -z0 = [f/.x1-f/.x0,g/.x1-g/.x0] by A33,PRVECT_3:18; then
A35: ||.z1-z0.|| = sqrt( ||.f/.x1-f/.x0.|| ^2 + ||.g/.x1-g/.x0.|| ^2 )
by NDIFF_8:1;
A36: ||.f/.x1-f/.x0.|| ^2 <= s1^2 by A29,SQUARE_1:15;
||.g/.x1-g/.x0.|| ^2 <= s1^2 by A30,SQUARE_1:15; then
A38: ||.f/.x1-f/.x0.|| ^2 + ||.g/.x1-g/.x0.|| ^2
<= s^2/4 + s^2/4 by A36,XREAL_1:7;
s^2/2 < s^2 by A21,XREAL_1:129,216; then
||.f/.x1-f/.x0.|| ^2 + ||.g/.x1-g/.x0.|| ^2 < s^2
by A38,XXREAL_0:2; then
sqrt( ||.f/.x1-f/.x0.|| ^2 + ||.g/.x1-g/.x0.|| ^2 )
< sqrt s^2 by SQUARE_1:27; then
A40: ||.z1-z0.|| < s by A21,A35,SQUARE_1:22;
A41: H /. x1 = H.x1 by A12,A26,PARTFUN1:def 6
.= BL.(f.x1,g.x1) by A13,A26
.= BL/.z1;
H /. x0 = H.x0 by A12,A16,PARTFUN1:def 6
.= BL.(f.x0,g.x0) by A13,A16
.= BL/.z0;
hence ||.H /. x1 - H /. x0.|| < r by A21,A40,A41;
end;
end;
hence H is_continuous_on S by A12,NFCONT_1:19;
end;
theorem LmTh471:
for E,F be RealNormSpace,
g be PartFunc of E,F,
A be Subset of E
st g is_continuous_on A
& dom g = A
holds
ex xg be PartFunc of E,[:E,F:]
st dom xg = A
& ( for x be Point of E st x in A
holds xg.x = [x,g.x] )
& xg is_continuous_on A
proof
let E,F be RealNormSpace,
g be PartFunc of E,F,
S be Subset of E;
assume that
A1: g is_continuous_on S and
A2: dom g = S;
defpred P1[object,object] means
ex t be Point of E
st t = $1 & $2 = [t,g.t];
A3: for x being object st x in S holds
ex y being object
st y in the carrier of [:E,F:] & P1[x,y]
proof
let x be object;
assume
A4: x in S; then
reconsider t = x as Point of E;
take y = [t,g.t];
g.t in rng g by A2,A4,FUNCT_1:3; then
reconsider q = g.t as Point of F;
[t,q] is Point of [:E,F:];
hence y in the carrier of [:E,F:] & P1[x,y];
end;
consider H being Function of S,[:E,F:] such that
A6: for z being object st z in S
holds P1[z,H.z] from FUNCT_2:sch 1(A3);
A7: dom H = S by FUNCT_2:def 1;
rng H c= the carrier of [:E,F:]; then
H in PFuncs(the carrier of E,the carrier of [:E,F:])
by A7,PARTFUN1:def 3; then
reconsider H as PartFunc of E,[:E,F:] by PARTFUN1:46;
take H;
thus dom H = S by FUNCT_2:def 1;
thus
A11: for s be Point of E st s in S holds H.s =[s,g.s]
proof
let s be Point of E;
assume s in S; then
ex t be Point of E st t = s & H.s = [t,g.t] by A6;
hence thesis;
end;
for x0 being Point of E
for r being Real st x0 in S & 0 < r
holds
ex pq being Real
st 0 < pq
& for x1 being Point of E
st x1 in S & ||.x1 - x0.|| < pq
holds ||.H /. x1 - H /. x0.|| < r
proof
let x0 be Point of E;
let r be Real;
assume
A12: x0 in S & 0 < r; then
A14: g.x0 in rng g by A2,FUNCT_1:3;
[x0,g.x0] is set by TARSKI:1; then
reconsider z0 = [x0,g.x0] as Point of [:E,F:] by A14,PRVECT_3:18;
A15: 0 < r/2 & r/2 < r by A12,XREAL_1:215,216;
consider q being Real such that
A16: 0 < q
& for x1 being Point of E st x1 in S & ||.x1 - x0.|| < q
holds ||.g /. x1 - g /. x0.|| < r/2
by A1,A12,NFCONT_1:19,XREAL_1:215;
set pq= min (q,r/2);
A17: 0 < pq & pq <= q & pq <= r/2 by A15,A16,XXREAL_0:15,17;
take pq;
thus 0 < pq by A15,A16,XXREAL_0:15;
thus for x1 being Point of E
st x1 in S & ||.x1 - x0.|| < pq
holds ||.H /. x1 - H /. x0.|| < r
proof
let x1 be Point of E;
assume
A18: x1 in S & ||.x1 - x0.|| < pq; then
||.x1 - x0.|| < q by A17,XXREAL_0:2; then
A21: ||. g /. x1 - g /. x0.|| < r/2 by A16,A18;
A23: g.x1 in rng g by A2,A18,FUNCT_1:3;
[x1,g.x1] is set by TARSKI:1; then
reconsider z1 = [x1,g.x1] as Point of [:E,F:] by A23,PRVECT_3:18;
A24: z1 = [x1,g/.x1] by A2,A18,PARTFUN1:def 6;
z0 = [x0,g/.x0] by A2,A12,PARTFUN1:def 6; then
-z0 = [-x0,-g/.x0] by PRVECT_3:18; then
z1 -z0 = [x1-x0,g/.x1-g/.x0] by A24,PRVECT_3:18; then
A26: ||.z1-z0.|| = sqrt( ||.x1-x0.|| ^2 + ||.g/.x1-g/.x0.|| ^2 )
by NDIFF_8:1;
||.x1 - x0.|| < (r/2) by A17,A18,XXREAL_0:2; then
A27: ||.x1-x0.|| ^2 < (r/2)^2 by SQUARE_1:16;
||.g/.x1-g/.x0.|| ^2 <= (r/2)^2 by A21,SQUARE_1:15; then
A29: ||.x1-x0.|| ^2 + ||.g/.x1-g/.x0.|| ^2
<= r^2/4 + r^2/4 by A27,XREAL_1:7;
r^2/2 < r^2 by A12,XREAL_1:129,216; then
||.x1-x0.|| ^2 + ||.g/.x1-g/.x0.|| ^2
< r^2 by A29,XXREAL_0:2; then
A31: sqrt( ||.x1-x0.|| ^2 + ||.g/.x1-g/.x0.|| ^2 )
< sqrt r^2 by SQUARE_1:27;
A32: H /. x1 = H.x1 by A7,A18,PARTFUN1:def 6
.= z1 by A11,A18;
H /. x0 = H.x0 by A7,A12,PARTFUN1:def 6
.= z0 by A11,A12;
hence ||.H /. x1 - H /. x0.|| < r by A12,A26,A31,A32,SQUARE_1:22;
end;
end;
hence H is_continuous_on S by A7,NFCONT_1:19;
end;
theorem NFCONT112:
for S, T, V being RealNormSpace
for x0 being Point of V
for f1 being PartFunc of the carrier of V, the carrier of S
for f2 being PartFunc of the carrier of S, the carrier of T
st x0 in dom (f2 * f1)
& f1 is_continuous_in x0
& f2 is_continuous_in f1 /. x0
holds f2 * f1 is_continuous_in x0
proof
let S, T, V be RealNormSpace;
let x0 be Point of V;
let f1 be PartFunc of the carrier of V, the carrier of S;
let f2 be PartFunc of the carrier of S, the carrier of T;
assume
A1: x0 in dom (f2 * f1);
assume that
A2: f1 is_continuous_in x0 and
A3: f2 is_continuous_in f1 /. x0;
thus x0 in dom (f2 * f1) by A1;
let s1 be sequence of V;
assume that
A4: rng s1 c= dom (f2 * f1) and
A5: s1 is convergent & lim s1 = x0;
A6: dom (f2 * f1) c= dom f1 by RELAT_1:25;
B6: rng (f1 /* s1) c= dom f2
proof
let x be object;
assume x in rng (f1 /* s1); then
consider n being Element of NAT such that
A7: x = (f1 /* s1) . n by FUNCT_2:113;
s1 . n in rng s1 by VALUED_0:28; then
f1 . (s1 . n) in dom f2 by A4,FUNCT_1:11;
hence x in dom f2 by A4,A6,A7,FUNCT_2:108,XBOOLE_1:1;
end;
A9: now
let n be Element of NAT;
s1 . n in rng s1 by VALUED_0:28;
then A10: s1 . n in dom f1 by A4,FUNCT_1:11;
thus ((f2 * f1) /* s1) . n
= (f2 * f1) . (s1 . n) by A4,FUNCT_2:108
.= f2 . (f1 . (s1 . n)) by A10,FUNCT_1:13
.= f2 . ((f1 /* s1) . n) by A4,A6,FUNCT_2:108,XBOOLE_1:1
.= (f2 /* (f1 /* s1)) . n by B6,FUNCT_2:108;
end; then
A10: f2 /* (f1 /* s1) = (f2 * f1) /* s1 by FUNCT_2:63;
rng s1 c= dom f1 by A4,A6,XBOOLE_1:1; then
A11: ( f1 /* s1 is convergent & f1 /. x0 = lim (f1 /* s1) )
by A2,A5,NFCONT_1:def 5;
(f2 * f1) /. x0 = f2 /. (f1 /. x0) by A1,PARTFUN2:3
.= lim (f2 /* (f1 /* s1)) by A3,B6,A11,NFCONT_1:def 5
.= lim ((f2 * f1) /* s1) by A9,FUNCT_2:63;
hence ( (f2 * f1) /* s1 is convergent
& (f2 * f1) /. x0 = lim ((f2 * f1) /* s1) )
by A3,B6,A10,A11,NFCONT_1:def 5;
end;
theorem LM0:
for E,F be RealNormSpace,
z be Point of [:E,F:],
x be Point of E,
y be Point of F
st z = [x,y]
holds ||.z.|| <= ||.x.|| + ||.y.||
proof
let E,F be RealNormSpace,
z be Point of [:E,F:],
x be Point of E,
y be Point of F;
assume z = [x,y]; then
A2: ||.z.|| =sqrt (||.x.|| ^2 + ||.y.|| ^2) by NDIFF_8:1;
||.x.|| ^2 + ||.y.|| ^2 + 0
<= ( ||.x.|| ^2 + ||.y.|| ^2 ) + ( 2 * ||.x.||) * ||.y.||
by XREAL_1:7; then
sqrt (||.x.|| ^2 + ||.y.|| ^2 )
<= sqrt (( ||.x.|| + ||.y.|| ) ^2 ) by SQUARE_1:26;
hence thesis by A2,SQUARE_1:22;
end;
theorem Th0:
for E,F,G be RealNormSpace,
L be LinearOperator of [:E,F:],G
holds
ex L1 be LinearOperator of E,G,
L2 be LinearOperator of F,G
st ( for x be Point of E,
y be Point of F
holds L. [x,y] = L1.x + L2.y )
& ( for x be Point of E holds L1.x = L/. [x,0.F] )
& ( for y be Point of F holds L2.y = L/. [0.E,y] )
proof
let E,F,G be RealNormSpace,
L be LinearOperator of [:E,F:],G;
deffunc FH1(Point of E) = L/. [$1,0.F];
consider L1 being Function of the carrier of E,the carrier of G
such that
A1: for x being Point of E holds L1.x = FH1(x) from FUNCT_2:sch 4;
A4: for s, t being Element of E holds
L1 . (s + t) = (L1 . s) + (L1 . t)
proof
let s, t be Element of E;
reconsider z = [s,0.F], w = [t,0.F] as Point of [:E,F:];
z+w = [s+t,0.F+0.F] by PRVECT_3:18
.= [s+t,0.F] by RLVECT_1:4;
hence L1. (s+t) = L/.(z+w) by A1
.= L/.z +L/.w by VECTSP_1:def 20
.= L1.s +L/.[t,0.F] by A1
.= L1.s +L1.t by A1;
end;
for s being Element of E
for r being Real holds L1 . (r * s) = r * (L1 . s)
proof
let s be Element of E,
r be Real;
reconsider z = [s,0.F] as Point of [:E,F:];
r*z = [r*s,r*0.F] by PRVECT_3:18
.= [r*s,0.F] by RLVECT_1:10;
hence L1. (r*s) = L/.(r*z) by A1
.= r * ( L/.z ) by LOPBAN_1:def 5
.= r * L1.s by A1;
end; then
reconsider L1 as LinearOperator of E,G
by A4,LOPBAN_1:def 5,VECTSP_1:def 20;
deffunc FH2(Point of F) = L/. [0.E,$1];
consider L2 being Function of the carrier of F,the carrier of G such that
A7: for x being Point of F holds L2.x = FH2(x) from FUNCT_2:sch 4;
A10: for s, t being Element of F holds
L2 . (s + t) = (L2 . s) + (L2 . t)
proof
let s, t be Element of F;
reconsider z = [0.E,s], w = [0.E,t] as Point of [:E,F:];
z+w = [0.E+0.E,s+t] by PRVECT_3:18
.= [0.E,s+t] by RLVECT_1:4;
hence L2. (s+t) = L/.(z+w) by A7
.= L/.z +L/.w by VECTSP_1:def 20
.= L2.s +L/.[0.E,t] by A7
.= L2.s +L2.t by A7;
end;
for s being Element of F
for r being Real holds L2 . (r * s) = r * (L2 . s)
proof
let s be Element of F,
r be Real;
reconsider z = [0.E,s] as Point of [:E,F:];
r*z = [r*0.E,r*s] by PRVECT_3:18
.= [0.E,r*s] by RLVECT_1:10;
hence L2. (r*s) = L/.(r*z) by A7
.= r*( L/.z ) by LOPBAN_1:def 5
.= r * L2.s by A7;
end; then
reconsider L2 as LinearOperator of F,G
by A10,LOPBAN_1:def 5,VECTSP_1:def 20;
for x be Point of E, y be Point of F
holds L. [x,y] = L1.x + L2.y
proof
let x be Point of E, y be Point of F;
reconsider z = [x,y], z1 = [x,0.F], z2 = [0.E,y]
as Point of [:E,F:];
z1+z2 = [x+0.E,0.F+y] by PRVECT_3:18
.= [x,0.F+y] by RLVECT_1:4
.= z by RLVECT_1:4;
hence L. [x,y] = L/.z1 + L/.z2 by VECTSP_1:def 20
.= L1.x + L/.z2 by A1
.= L1.x + L2.y by A7;
end;
hence ex L1 be LinearOperator of E,G,
L2 be LinearOperator of F,G
st ( for x be Point of E, y be Point of F
holds L. [x,y] = L1.x + L2.y )
& ( for x be Point of E holds L1.x = L/. [x,0.F] )
& ( for y be Point of F holds L2.y = L/. [0.E,y] ) by A1,A7;
end;
theorem Th0X:
for E,F,G be RealNormSpace,
L be LinearOperator of [:E,F:],G,
L11 be LinearOperator of E,G,
L12 be LinearOperator of F,G,
L21 be LinearOperator of E,G,
L22 be LinearOperator of F,G
st ( for x be Point of E,
y be Point of F
holds L. [x,y] = L11.x + L12.y )
& ( for x be Point of E,
y be Point of F
holds L. [x,y] = L21.x + L22.y )
holds L11 = L21 & L12 = L22
proof
let E,F,G be RealNormSpace,
L be LinearOperator of [:E,F:],G;
let L11 be LinearOperator of E,G,
L12 be LinearOperator of F,G,
L21 be LinearOperator of E,G,
L22 be LinearOperator of F,G;
assume that
A1: ( for x be Point of E, y be Point of F
holds L. [x,y] = L11.x + L12.y ) and
A2: ( for x be Point of E, y be Point of F
holds L. [x,y] = L21.x + L22.y );
now
let x be Point of E;
A4: L22. (0.F) = 0.G by LOPBAN_7:3;
L12. (0.F) = 0.G by LOPBAN_7:3;
hence L11.x = L11.x + L12. (0.F) by RLVECT_1:4
.= L. [x,0.F] by A1
.= L21.x + L22. 0.F by A2
.= L21.x by A4,RLVECT_1:4;
end;
hence L11 = L21 by FUNCT_2:def 8;
now
let y be Point of F;
A6: L21.(0.E) = 0.G by LOPBAN_7:3;
L11.(0.E) = 0.G by LOPBAN_7:3;
hence L12.y = L11.(0.E) + L12.y by RLVECT_1:4
.= L. [0.E,y] by A1
.= L21. 0.E + L22. y by A2
.= L22.y by A6,RLVECT_1:4;
end;
hence L12 = L22 by FUNCT_2:def 8;
end;
theorem Th1:
for E,F,G be RealNormSpace,
L1 be LinearOperator of E,G,
L2 be LinearOperator of F,G
holds
ex L be LinearOperator of [:E,F:],G
st ( for x be Point of E,
y be Point of F
holds L. [x,y] = L1.x + L2.y )
& ( for x be Point of E holds L1.x = L/. [x,0.F] )
& ( for y be Point of F holds L2.y = L/. [0.E,y] )
proof
let E,F,G be RealNormSpace,
L1 be LinearOperator of E,G,
L2 be LinearOperator of F,G;
defpred P1[object,object] means
ex x be Point of E,y be Point of F
st $1 = [x,y] & $2 = L1.x + L2.y;
A1: for z being Element of [:E,F:]
ex y being Element of G st P1[z,y]
proof
let z be Element of [:E,F:];
consider x be Point of E,y be Point of F such that
A2: z = [x,y] by PRVECT_3:18;
take w = L1.x + L2.y;
thus P1[z,w] by A2;
end;
consider L being Function of [:E,F:],G such that
A3: for z being Element of [:E,F:]
holds P1[z,L.z] from FUNCT_2:sch 3(A1);
A4: for z,w be Point of [:E,F:]
holds L. (z+w) = L.z + L.w
proof
let z,w be Point of [:E,F:];
consider x1 be Point of E,y1 be Point of F such that
A5: z = [x1,y1] & L.z = L1.x1 + L2.y1 by A3;
consider x2 be Point of E,y2 be Point of F such that
A6: w = [x2,y2] & L.w = L1.x2 + L2.y2 by A3;
A7: z+w = [x1+x2,y1+y2] by A5,A6,PRVECT_3:18;
consider x3 be Point of E,y3 be Point of F such that
A8: z+w = [x3,y3] & L. (z+w) = L1.x3 + L2.y3 by A3;
A9: x3=x1+x2 & y3=y1+y2 by A7,A8,XTUPLE_0:1;
L.z + L.w = (L1.x1 + L2.y1 + L1.x2) + L2.y2 by A5,A6,RLVECT_1:def 3
.= (L1.x1 + L1.x2 + L2.y1) + L2.y2 by RLVECT_1:def 3
.= (L1.x1 + L1.x2 ) + ( L2.y1 + L2.y2 ) by RLVECT_1:def 3
.= L1.(x1+x2) + ( L2.y1 + L2.y2 ) by VECTSP_1:def 20
.= L. (z+w) by A8,A9,VECTSP_1:def 20;
hence thesis;
end;
for z being Element of [:E,F:]
for r being Real holds L . (r * z) = r * (L . z)
proof
let z be Element of [:E,F:],
r be Real;
consider x1 be Point of E,y1 be Point of F such that
A10: z = [x1,y1] & L.z = L1.x1 + L2.y1 by A3;
A11: r*z = [r*x1,r*y1] by A10,PRVECT_3:18;
consider x2 be Point of E,y2 be Point of F such that
A12: r*z = [x2,y2] & L. (r*z) = L1.x2 + L2.y2 by A3;
x2=r*x1 & y2 =r*y1 by A11,A12,XTUPLE_0:1;
hence L. (r*z) = r * (L1.x1) + L2.(r*y1) by A12,LOPBAN_1:def 5
.= r * (L1.x1) + r * (L2.y1) by LOPBAN_1:def 5
.= r * L.z by A10,RLVECT_1:def 5;
end; then
reconsider L as LinearOperator of [:E,F:],G
by A4,LOPBAN_1:def 5,VECTSP_1:def 20;
take L;
thus
A14: for x be Point of E,
y be Point of F
holds L. [x,y] = L1.x + L2.y
proof
let x be Point of E,
y be Point of F;
reconsider z = [x,y] as Point of [:E,F:];
consider x1 be Point of E,y1 be Point of F such that
A15: z = [x1,y1] & L.z = L1.x1 + L2.y1 by A3;
x = x1 & y1 = y by A15,XTUPLE_0:1;
hence L. [x,y] = L1.x + L2.y by A15;
end;
thus for x be Point of E holds L1.x = L/. [x,0.F]
proof
let x be Point of E;
thus L1.x = L1.x + 0.G by RLVECT_1:4
.= L1.x + L2. (0.F) by LOPBAN_7:3
.= L/. [x,0.F] by A14;
end;
thus for y be Point of F holds L2.y = L/. [0.E,y]
proof
let y be Point of F;
thus L2.y = 0.G + L2.y by RLVECT_1:4
.= L1.(0.E) + L2. y by LOPBAN_7:3
.= L/. [0.E,y] by A14;
end;
end;
theorem Th2:
for E,F,G be RealNormSpace,
L be Lipschitzian LinearOperator of [:E,F:],G
holds
ex L1 be Lipschitzian LinearOperator of E,G,
L2 be Lipschitzian LinearOperator of F,G
st ( for x be Point of E,
y be Point of F
holds L. [x,y] = L1.x + L2.y )
& ( for x be Point of E holds L1.x = L/. [x,0.F] )
& ( for y be Point of F holds L2.y = L/. [0.E,y] )
proof
let E,F,G be RealNormSpace,
L be Lipschitzian LinearOperator of [:E,F:],G;
consider L1 be LinearOperator of E,G,
L2 be LinearOperator of F,G such that
A1: ( for x be Point of E,
y be Point of F
holds L. [x,y] = L1.x + L2.y )
& ( for x be Point of E holds L1.x = L/. [x,0.F] )
& ( for y be Point of F holds L2.y = L/. [0.E,y] ) by Th0;
consider K being Real such that
A2: 0 <= K
& for z being VECTOR of [:E,F:]
holds ||. L.z .|| <= K * ||.z.|| by LOPBAN_1:def 8;
now
let x be Point of E;
reconsider z=[x,0.F] as Point of [:E,F:];
A4: L1.x = L/. [x,0.F] by A1
.= L.z;
||.z.|| = ||.x.|| by NDIFF_8:2;
hence ||. L1.x .|| <= K * ||.x.|| by A2,A4;
end; then
A5: L1 is Lipschitzian by A2,LOPBAN_1:def 8;
now
let y be Point of F;
reconsider z = [0.E,y] as Point of [:E,F:];
A7: L2.y = L /. [0.E,y] by A1
.= L.z;
||.z.|| = ||.y.|| by NDIFF_8:3;
hence ||. L2.y .|| <= K * ||.y.|| by A2,A7;
end; then
L2 is Lipschitzian by A2,LOPBAN_1:def 8;
hence thesis by A1,A5;
end;
theorem
for E,F,G be RealNormSpace,
L1 be Lipschitzian LinearOperator of E,G,
L2 be Lipschitzian LinearOperator of F,G
holds
ex L be Lipschitzian LinearOperator of [:E,F:],G
st ( for x be Point of E,
y be Point of F
holds L. [x,y] = L1.x + L2.y )
& ( for x be Point of E holds L1.x = L/. [x,0.F] )
& ( for y be Point of F holds L2.y = L/. [0.E,y] )
proof
let E,F,G be RealNormSpace,
L1 be Lipschitzian LinearOperator of E,G,
L2 be Lipschitzian LinearOperator of F,G;
consider L be LinearOperator of [:E,F:],G such that
A1: ( for x be Point of E,
y be Point of F
holds L. [x,y] = L1.x + L2.y )
& ( for x be Point of E holds L1.x = L/. [x,0.F] )
& ( for y be Point of F holds L2.y = L/. [0.E,y] ) by Th1;
consider K1 being Real such that
A2: 0 <= K1
& for x being VECTOR of E
holds ||. L1.x .|| <= K1 * ||.x.|| by LOPBAN_1:def 8;
consider K2 being Real such that
A3: 0 <= K2
& for y being VECTOR of F
holds ||. L2.y .|| <= K2 * ||.y.|| by LOPBAN_1:def 8;
now
let z be Point of [:E,F:];
consider x be Point of E,y be Point of F such that
A5: z = [x,y] by PRVECT_3:18;
L.z = L1.x + L2.y by A1,A5; then
A7: ||. L.z .|| <= ||. L1.x .|| + ||. L2.y .|| by NORMSP_1:def 1;
A8: ||. L1.x .|| <= K1* ||.x.||
& ||. L2.y .|| <= K2* ||.y.|| by A2,A3;
A9: K1 * ||.x.|| <= K1 * ||.z.|| by A2,A5,NDIFF_8:21,XREAL_1:64;
K2 * ||.y.|| <= K2 * ||.z.|| by A3,A5,NDIFF_8:21,XREAL_1:64; then
||. L1.x .|| <= K1 * ||.z.||
& ||. L2.y .|| <= K2 * ||.z.|| by A8,A9,XXREAL_0:2;
then ||. L1.x .|| + ||. L2.y .||
<= K1* ||.z.|| + K2* ||.z.|| by XREAL_1:7;
hence ||. L.z .|| <= (K1 + K2) * ||.z.|| by A7,XXREAL_0:2;
end; then
L is Lipschitzian by A2,A3,LOPBAN_1:def 8;
hence thesis by A1;
end;
theorem
for E,F,G be RealNormSpace,
L be Point of R_NormSpace_of_BoundedLinearOperators([:E,F:],G)
holds
ex L1 be Point of R_NormSpace_of_BoundedLinearOperators(E,G),
L2 be Point of R_NormSpace_of_BoundedLinearOperators(F,G)
st ( for x be Point of E,
y be Point of F
holds L. [x,y] = L1.x + L2.y )
& ( for x be Point of E holds L1.x = L. [x,0.F] )
& ( for y be Point of F holds L2.y = L. [0.E,y] )
& ||.L.|| <= ||.L1.|| + ||.L2.||
& ||.L1.|| <= ||.L.|| & ||.L2.|| <= ||.L.||
proof
let E,F,G be RealNormSpace,
LP be Point of R_NormSpace_of_BoundedLinearOperators([:E,F:],G);
reconsider L = LP as Lipschitzian LinearOperator of [:E,F:],G
by LOPBAN_1:def 9;
consider L1 be Lipschitzian LinearOperator of E,G,
L2 be Lipschitzian LinearOperator of F,G such that
A1: ( for x be Point of E,
y be Point of F
holds L. [x,y] = L1.x + L2.y ) and
A2: ( for x be Point of E holds L1.x = L/. [x,0.F] ) and
A3: ( for y be Point of F holds L2.y = L/. [0.E,y] ) by Th2;
reconsider LP1=L1 as Point of R_NormSpace_of_BoundedLinearOperators(E,G)
by LOPBAN_1:def 9;
reconsider LP2=L2 as Point of R_NormSpace_of_BoundedLinearOperators(F,G)
by LOPBAN_1:def 9;
take LP1,LP2;
thus for x be Point of E, y be Point of F
holds LP. [x,y] = LP1.x + LP2.y by A1;
thus for x be Point of E holds LP1.x = LP. [x,0.F]
proof
let x be Point of E;
thus LP1. x = L/.[x,0.F] by A2
.= LP. [x,0.F];
end;
thus for y be Point of F holds LP2.y = LP. [0.E,y]
proof
let y be Point of F;
thus LP2. y = L/.[0.E,y] by A3
.= LP. [0.E,y];
end;
A7: ||.LP.||
= upper_bound (PreNorms(modetrans(LP,[:E,F:],G))) by LOPBAN_1:def 13
.= upper_bound PreNorms(L) by LOPBAN_1:29;
for t be Real st t in PreNorms(L) holds t <= ||.LP1.|| + ||.LP2.||
proof
let t be Real;
assume t in PreNorms(L); then
consider w be Point of [:E,F:] such that
A8: t = ||. L.w .|| & ||.w.|| <= 1;
consider x be Point of E,y be Point of F such that
A9: w =[x,y] by PRVECT_3:18;
||.x.|| <= ||.w.|| by A9,NDIFF_8:21; then
A10: ||.x.|| <= 1 by A8,XXREAL_0:2;
||.y.|| <= ||.w.|| by A9,NDIFF_8:21; then
A11: ||.y.|| <= 1 by A8,XXREAL_0:2;
L. w = L1.x + L2.y by A1,A9; then
A12: ||. L.w .|| <= ||.L1.x.|| + ||.L2.y.|| by NORMSP_1:def 1;
A13: ||.L1.x.|| <= ||.LP1.|| * ||.x.|| by LOPBAN_1:32;
||.LP1.|| * ||.x.|| <= ||.LP1.|| * 1 by A10,XREAL_1:64; then
A14: ||.L1.x.|| <= ||.LP1.|| by A13,XXREAL_0:2;
A15: ||.L2.y.|| <= ||.LP2.|| * ||.y.|| by LOPBAN_1:32;
||.LP2.|| * ||.y.|| <= ||.LP2.|| * 1 by A11,XREAL_1:64; then
||.L2.y.|| <= ||.LP2.|| by A15,XXREAL_0:2; then
||.L1.x.|| + ||.L2.y.|| <= ||.LP1.|| + ||.LP2.|| by A14,XREAL_1:7;
hence thesis by A8,A12,XXREAL_0:2;
end;
hence ||.LP.|| <= ||.LP1.|| + ||.LP2.|| by A7,SEQ_4:45;
A17: ||.LP1.||
= upper_bound (PreNorms(modetrans(LP1,E,G))) by LOPBAN_1:def 13
.= upper_bound PreNorms(L1) by LOPBAN_1:29;
for t be Real st t in PreNorms(L1) holds t <= ||.LP.||
proof
let t be Real;
assume t in PreNorms(L1); then
consider x be Point of E such that
A18: t = ||. L1.x .|| & ||.x.|| <= 1;
reconsider w = [x,0.F] as Point of [:E,F:];
A19: ||.w.|| <= 1 by A18,NDIFF_8:2;
A20: L. w = L1.x + L2. (0.F) by A1
.= L1.x + 0.G by LOPBAN_7:3
.= L1.x by RLVECT_1:def 4;
A21: ||. L.w .|| <= ||.LP.|| * ||.w.|| by LOPBAN_1:32;
||.LP.|| * ||.w.|| <= ||.LP.|| * 1 by A19,XREAL_1:64;
hence t <= ||.LP.|| by A18,A20,A21,XXREAL_0:2;
end;
hence ||.LP1.|| <= ||.LP.|| by A17,SEQ_4:45;
A23: ||.LP2.||
= upper_bound (PreNorms(modetrans(LP2,F,G))) by LOPBAN_1:def 13
.= upper_bound PreNorms(L2) by LOPBAN_1:29;
for t be Real st t in PreNorms(L2) holds t <= ||.LP.||
proof
let t be Real;
assume t in PreNorms(L2); then
consider x be Point of F such that
A24: t = ||. L2.x .|| & ||.x.|| <= 1;
reconsider w = [0.E,x] as Point of [:E,F:];
A25: ||.x.|| = ||.w.|| by NDIFF_8:3;
A26: L. w = L1.(0.E) + L2.x by A1
.= 0.G + L2.x by LOPBAN_7:3
.= L2.x by RLVECT_1:def 4;
A27: ||. L.w .|| <= ||.LP.|| * ||.w.|| by LOPBAN_1:32;
||.LP.|| * ||.w.|| <= ||.LP.|| * 1 by A24,A25,XREAL_1:64;
hence t <= ||.LP.|| by A24,A26,A27,XXREAL_0:2;
end;
hence ||.LP2.|| <= ||.LP.|| by A23,SEQ_4:45;
end;
theorem
for E,F,G be RealNormSpace,
L be Point of R_NormSpace_of_BoundedLinearOperators([:E,F:],G),
L11,L12 be Point of R_NormSpace_of_BoundedLinearOperators(E,G),
L21,L22 be Point of R_NormSpace_of_BoundedLinearOperators(F,G)
st ( for x be Point of E,
y be Point of F
holds L. [x,y] = L11.x + L21.y )
& ( for x be Point of E,
y be Point of F
holds L. [x,y] = L12.x + L22.y )
holds L11 = L12 & L21 = L22
proof
let E,F,G be RealNormSpace,
L be Point of R_NormSpace_of_BoundedLinearOperators([:E,F:],G),
L11,L12 be Point of R_NormSpace_of_BoundedLinearOperators(E,G),
L21,L22 be Point of R_NormSpace_of_BoundedLinearOperators(F,G);
assume
A1: for x be Point of E,
y be Point of F
holds L. [x,y] = L11.x + L21.y;
assume
A2: for x be Point of E,
y be Point of F
holds L. [x,y] = L12.x + L22.y;
reconsider LP = L
as Lipschitzian LinearOperator of [:E,F:],G by LOPBAN_1:def 9;
reconsider LP11 = L11, LP12 = L12
as Lipschitzian LinearOperator of E,G by LOPBAN_1:def 9;
reconsider LP21 = L21, LP22 = L22
as Lipschitzian LinearOperator of F,G by LOPBAN_1:def 9;
A3: for x be Point of E, y be Point of F
holds LP. [x,y] = LP11.x + LP21.y by A1;
for x be Point of E, y be Point of F
holds LP. [x,y] = LP12.x + LP22.y by A2;
hence L11 = L12 & L21 = L22 by A3,Th0X;
end;
begin :: Differentiability of implicit function
theorem Th4:
for E,G,F be RealNormSpace,
Z be Subset of [:E,F:],
f be PartFunc of [:E,F:], G,
z be Point of [:E,F:]
st f is_differentiable_in z
holds
f is_partial_differentiable_in`1 z
& f is_partial_differentiable_in`2 z
& for dx be Point of E,dy be Point of F holds
diff(f,z) . [dx,dy] = partdiff`1(f,z).dx + partdiff`2(f,z).dy
proof
let E,G,F be RealNormSpace,
Z be Subset of [:E,F:],
f be PartFunc of [:E,F:], G,
z be Point of [:E,F:];
assume
A1: f is_differentiable_in z;
reconsider y = (IsoCPNrSP (E,F)).z as Point of product <*E,F*>;
(IsoCPNrSP (E,F))" .( (IsoCPNrSP (E,F)).z) = z by FUNCT_2:26; then
A3: f * ((IsoCPNrSP (E,F)) ") is_differentiable_in y
by A1,NDIFF_7:28; then
A4: f is_partial_differentiable_in`1 z
& f is_partial_differentiable_in`2 z by NDIFF_5:41,NDIFF_7:34;
consider N being Neighbourhood of z such that
A5: N c= dom f
& ex R be RestFunc of [:E,F:],G
st for w be Point of [:E,F:] st w in N
holds f/.w-f/.z = diff(f,z).(w-z) + R/.(w-z) by A1,NDIFF_1:def 7;
consider R be RestFunc of [:E,F:],G such that
A6: for w be Point of [:E,F:] st w in N
holds f/.w-f/.z = diff(f,z).(w-z) + R/.(w-z) by A5;
reconsider L = diff(f,z)
as Lipschitzian LinearOperator of [:E,F:],G by LOPBAN_1:def 9;
consider L1 be Lipschitzian LinearOperator of E,G,
L2 be Lipschitzian LinearOperator of F,G such that
A7: ( for dx be Point of E,
dy be Point of F
holds L. [dx,dy] = L1.dx + L2.dy ) and
( for dx be Point of E holds L1.dx = L/. [dx,0.F] ) and
( for dy be Point of F holds L2.dy = L/. [0.E,dy] ) by Th2;
reconsider LL1 = L1
as Point of R_NormSpace_of_BoundedLinearOperators(E,G)
by LOPBAN_1:def 9;
reconsider LL2 = L2
as Point of R_NormSpace_of_BoundedLinearOperators(F,G)
by LOPBAN_1:def 9;
set g1 = f*reproj1(z);
set g2 = f*reproj2(z);
reconsider x = z`1 as Point of E;
reconsider y = z`2 as Point of F;
A9: ex x1 being Point of E, x2 being Point of F
st z = [x1,x2] by PRVECT_3:18; then
A10: z = [x,y];
consider r0 be Real such that
A14: 0 < r0
& { y where y is Point of [:E,F:] : ||.y-z .|| < r0} c= N
by NFCONT_1:def 1;
A15: { y where y is Point of [:E,F:] : ||.y-z .|| < r0}
= Ball(z,r0) by NDIFF_8:17;
consider r be Real such that
A16: 0 < r & r < r0
& [:Ball(x,r),Ball(y,r):] c= Ball(z,r0) by A9,A14,NDIFF_8:22;
A17: [:Ball(x,r),Ball(y,r):] c= N by A14,A15,A16,XBOOLE_1:1;
deffunc FP1(Point of E) = R/. [$1,0.F];
consider R1 being Function of the carrier of E,the carrier of G
such that
A18: for p being Point of E holds R1.p = FP1(p)
from FUNCT_2:sch 4;
A20: for dx be Point of E
holds R1/.dx = R/. [dx,0.F] by A18;
deffunc FP2(Point of F) = R/. [0.E,$1];
consider R2 being Function of the carrier of F,the carrier of G
such that
A21: for p being Point of F holds R2.p = FP2(p)
from FUNCT_2:sch 4;
A23: for dy be Point of F holds R2/.dy = R/. [0.E,dy] by A21;
for r being Real st r > 0 holds
ex d being Real
st d > 0
& for z being Point of E st z <> 0. E & ||.z.|| < d holds
(||.z.|| ") * ||.(R1 /. z).|| < r
proof
let r be Real;
assume
A25: r > 0;
R is total by NDIFF_1:def 5; then
consider d being Real such that
A26: d > 0
& for z being Point of [:E,F:]
st z <> 0. [:E,F:] & ||.z.|| < d
holds (||.z.|| ") * ||.(R /. z).|| < r by A25,NDIFF_1:23;
take d;
thus d > 0 by A26;
let x1 be Point of E;
assume
A27: x1 <> 0. E & ||.x1.|| < d;
reconsider z=[x1,0.F] as Point of [:E,F:];
A28: z <> 0. [:E,F:] by A27,XTUPLE_0:1;
A29: R /. z = R1/.x1 by A18;
||.z.|| = ||.x1.|| by NDIFF_8:2;
hence (||.x1.|| ") * ||.(R1 /. x1).|| < r by A26,A27,A28,A29;
end; then
reconsider R1 as RestFunc of E,G by NDIFF_1:23;
for r being Real st r > 0 holds
ex d being Real
st d > 0
& for z being Point of F st z <> 0. F & ||.z.|| < d holds
(||.z.|| ") * ||.(R2 /. z).|| < r
proof
let r be Real;
assume
A32: r > 0;
R is total by NDIFF_1:def 5; then
consider d being Real such that
A33: d > 0
& for z being Point of [:E,F:]
st z <> 0. [:E,F:] & ||.z.|| < d
holds (||.z.|| ") * ||.(R /. z).|| < r by A32,NDIFF_1:23;
take d;
thus d > 0 by A33;
let y1 be Point of F;
assume
A34: y1 <> 0. F & ||.y1.|| < d;
reconsider z=[0.E,y1] as Point of [:E,F:];
A35: z <> 0. [:E,F:] by A34,XTUPLE_0:1;
A36: R /. z = R2/.y1 by A21;
||.z.|| = ||.y1.|| by NDIFF_8:3;
hence (||.y1.|| ") * ||.(R2 /. y1).|| < r by A33,A34,A35,A36;
end; then
reconsider R2 as RestFunc of F,G by NDIFF_1:23;
reconsider N1 = Ball(x,r) as Neighbourhood of x by A16,NDIFF_8:19;
reconsider N2 = Ball(y,r) as Neighbourhood of y by A16,NDIFF_8:19;
A37: N1 c= dom g1
proof
let s be object;
assume
A39: s in N1; then
reconsider t = s as Point of E;
A40: dom(reproj1 z) = the carrier of E by FUNCT_2:def 1;
A41: (reproj1 z).t = [t,y] by NDIFF_7:def 1;
t in Ball(x,r) & y in Ball(y,r) by A16,A39,NDIFF_8:13; then
[t,y] in [:Ball(x,r),Ball(y,r):] by ZFMISC_1:87; then
(reproj1 z).t in N by A17,A41;
hence s in dom g1 by A5,A40,FUNCT_1:11;
end;
B42: N2 c= dom g2
proof
let s be object;
assume
A43: s in N2; then
reconsider t = s as Point of F;
A44: dom(reproj2 z) = the carrier of F by FUNCT_2:def 1;
A45: (reproj2 z).t = [x,t] by NDIFF_7:def 2;
t in Ball(y,r) & x in Ball(x,r) by A16,A43,NDIFF_8:13; then
[x,t] in [:Ball(x,r),Ball(y,r):] by ZFMISC_1:87; then
(reproj2 z).t in N by A17,A45;
hence s in dom g2 by A5,A44,FUNCT_1:11;
end;
for x1 be Point of E st x1 in N1
holds g1/.x1-g1/.x = LL1.(x1-x) + R1/.(x1-x)
proof
let x1 be Point of E;
assume
A48: x1 in N1; then
A50: (reproj1 z).x1 in dom f by A37,FUNCT_1:11;
A51: (reproj1 z).x1 =[x1,y] by NDIFF_7:def 1;
x1 in Ball(x,r) & y in Ball(y,r) by A16,A48,NDIFF_8:13; then
A52: [x1,y] in [:Ball(x,r),Ball(y,r):] by ZFMISC_1:87;
A53: x in N1 by A16,NDIFF_8:13; then
A54: (reproj1 z).x in dom f by A37,FUNCT_1:11;
-z = [-x,-y] by A9,PRVECT_3:18; then
A56: (reproj1 z).x1 - z = [x1-x,y-y] by A51,PRVECT_3:18
.= [x1-x,0.F] by RLVECT_1:15;
A57: g1/.x1 = g1.x1 by A37,A48,PARTFUN1:def 6
.= f.((reproj1 z).x1) by A37,A48,FUNCT_1:12
.= f/.((reproj1 z).x1) by A50,PARTFUN1:def 6;
g1/.x = g1.x by A37,A53,PARTFUN1:def 6
.= f.((reproj1 z).x) by A37,A53,FUNCT_1:12
.= f/.((reproj1 z).x) by A54,PARTFUN1:def 6
.= f/.z by A10,NDIFF_7:def 1;
hence g1/.x1-g1/.x
= diff(f,z).((reproj1 z).x1-z) + R/.((reproj1 z).x1-z)
by A6,A17,A51,A52,A57
.= L1. (x1-x) + L2. 0.F + R/.( [x1-x,0.F] ) by A7,A56
.= L1. (x1-x) + 0.G + R/.( [x1-x,0.F] ) by LOPBAN_7:3
.= L1. (x1-x) + R/.( [x1-x,0.F] ) by RLVECT_1:4
.= LL1. (x1-x) + R1/.( x1-x ) by A20;
end; then
A59: LL1 = partdiff`1(f,z) by A4,A37,NDIFF_1:def 7;
for y1 be Point of F st y1 in N2
holds g2/.y1-g2/.y = LL2.(y1-y) + R2/.(y1-y)
proof
let y1 be Point of F;
assume
A61: y1 in N2; then
A63: (reproj2 z).y1 in dom f by B42,FUNCT_1:11;
A64: (reproj2 z).y1 = [x,y1] by NDIFF_7:def 2;
x in Ball(x,r) & y1 in Ball(y,r) by A16,A61,NDIFF_8:13; then
A65: [x,y1] in [:Ball(x,r),Ball(y,r):] by ZFMISC_1:87;
A66: y in N2 by A16,NDIFF_8:13; then
A67: (reproj2 z).y in dom f by B42,FUNCT_1:11;
-z = [-x,-y] by A9,PRVECT_3:18; then
A69: (reproj2 z).y1 -z = [x-x,y1-y] by A64,PRVECT_3:18
.= [0.E,y1-y] by RLVECT_1:15;
A70: g2/.y1 = g2.y1 by B42,A61,PARTFUN1:def 6
.= f.((reproj2 z).y1) by B42,A61,FUNCT_1:12
.= f/.((reproj2 z).y1) by A63,PARTFUN1:def 6;
g2/.y = g2.y by B42,A66,PARTFUN1:def 6
.= f.((reproj2 z).y) by B42,A66,FUNCT_1:12
.= f/.((reproj2 z).y) by A67,PARTFUN1:def 6
.= f/.z by A10,NDIFF_7:def 2;
hence g2/.y1-g2/.y
= diff(f,z).((reproj2 z).y1-z) + R/.((reproj2 z).y1-z)
by A6,A17,A64,A65,A70
.= L1. 0.E + L2. (y1-y) + R/.( [0.E,y1-y] ) by A7,A69
.= 0.G + L2. (y1-y) + R/.( [0.E,y1-y] ) by LOPBAN_7:3
.= L2. (y1-y) + R/.( [0.E,y1-y] ) by RLVECT_1:4
.= LL2. (y1-y) + R2/.( y1-y ) by A23;
end; then
LL2 = partdiff`2(f,z) by A4,B42,NDIFF_1:def 7;
hence thesis by A3,A7,A59,NDIFF_5:41,NDIFF_7:34;
end;
theorem Th5:
for E,G,F be RealNormSpace,
Z be Subset of [:E,F:],
f be PartFunc of [:E,F:], G,
a be Point of E,
b be Point of F,
c be Point of G,
z be Point of [:E,F:],
r1,r2 be Real,
g be PartFunc of E,F,
P be Lipschitzian LinearOperator of E,G,
Q be Lipschitzian LinearOperator of G,F
st Z is open & dom f = Z
& z = [a,b] & z in Z
& f.(a,b) = c
& f is_differentiable_in z
& 0 < r1 & 0 < r2
& dom g = Ball(a,r1) & rng g c= Ball(b,r2)
& g.a = b
& g is_continuous_in a
& ( for x be Point of E st x in Ball(a,r1) holds f.(x,g.x) = c )
& partdiff`2(f,z) is one-to-one
& Q = partdiff`2(f,z)"
& P = partdiff`1(f,z)
holds
g is_differentiable_in a
& diff(g,a) = - Q*P
proof
let E,G,F be RealNormSpace,
Z be Subset of [:E,F:],
f be PartFunc of [:E,F:], G,
a be Point of E,
b be Point of F,
c be Point of G,
z be Point of [:E,F:],
r1,r2 be Real,
g be PartFunc of E,F,
P be Lipschitzian LinearOperator of E,G,
Q be Lipschitzian LinearOperator of G,F;
assume
A1: Z is open & dom f = Z
& z = [a,b] & z in Z
& f.(a,b) = c
& f is_differentiable_in z
& 0 <r1 & 0 < r2
& dom g = Ball(a,r1) & rng g c= Ball(b,r2)
& g.a = b
& g is_continuous_in a
& ( for x be Point of E st x in Ball(a,r1) holds f.(x,g.x) = c )
& partdiff`2(f,z) is one-to-one
& Q= partdiff`2(f,z)"
& P = partdiff`1(f,z);
then A5: g/.a = b by NDIFF_8:13,PARTFUN1:def 6;
reconsider S = partdiff`2(f,z)
as Lipschitzian LinearOperator of F,G by LOPBAN_1:def 9;
A8: Q*P is Lipschitzian LinearOperator of E,F by LOPBAN_2:2; then
reconsider L = Q*P
as Point of R_NormSpace_of_BoundedLinearOperators(E,F) by LOPBAN_1:def 9;
A9: (-1)*L is Lipschitzian LinearOperator of E,F by LOPBAN_1:def 9;
reconsider NL = (-1)*L as PartFunc of E,F by LOPBAN_1:def 9;
A10: dom NL = the carrier of E by A9,FUNCT_2:def 1
.= dom (Q*P) by FUNCT_2:def 1;
A11: now
let x be VECTOR of E;
assume x in dom NL;
hence NL /. x = ((-1)*L). x by PARTFUN1:def 6
.= (-1) * ( (Q*P) /. x ) by LOPBAN_1:36;
end;
A15: -L = (-1)*L by RLVECT_1:16
.= (-1) (#) (Q*P) by A10,A11,VFUNCT_1:def 4
.= -Q*P by VFUNCT_1:23;
consider N0 being Neighbourhood of z such that
A16: N0 c= dom f
& ex R be RestFunc of [:E,F:],G
st for w be Point of [:E,F:] st w in N0
holds f/.w - f/.z = diff(f,z).(w-z) + R/.(w-z) by A1,NDIFF_1:def 7;
consider R be RestFunc of [:E,F:],G such that
A17: for w be Point of [:E,F:] st w in N0
holds f/.w-f/.z = diff(f,z).(w-z) + R/.(w-z) by A16;
consider r0 be Real such that
A20: 0 < r0
& {y where y is Point of [:E,F:] : ||.y-z .|| < r0} c= N0
by NFCONT_1:def 1;
A21: {y where y is Point of [:E,F:] : ||.y-z .|| < r0} = Ball(z,r0)
by NDIFF_8:17;
consider r3 be Real such that
A22: 0 < r3 & r3 < r0
& [:Ball(a,r3),Ball(b,r3):] c= Ball(z,r0) by A1,A20,NDIFF_8:22;
A23: [:Ball(a,r3),Ball(b,r3):] c= N0 by A20,A21,A22,XBOOLE_1:1;
reconsider r4 = min(r1,r3) as Real;
A24: 0 < r4 by A1,A22,XXREAL_0:15;
r4 <= r1 & r4 <= r3 by XXREAL_0:17; then
A26: Ball(a,r4) c= Ball(a,r1)
& Ball(a,r4) c= Ball(a,r3) by NDIFF_8:15;
consider r5 being Real such that
A27: 0 < r5
& for x1 being Point of E
st x1 in dom g & ||.(x1 - a).|| < r5
holds ||.((g /. x1) - (g /. a)).|| < r3 by A1,A22,NFCONT_1:7;
reconsider r6 = min(r4,r5) as Real;
A28: 0 < r6 by A24,A27,XXREAL_0:15;
r6 <= r4 & r6 <= r5 by XXREAL_0:17; then
A30: Ball(a,r6) c= Ball(a,r4)
& Ball(a,r6) c= Ball(a,r5) by NDIFF_8:15;
reconsider N = Ball(a,r6) as Neighbourhood of a by A28,NDIFF_8:19;
deffunc FR1(Point of E) = -Q.(R/.( [$1,g/.(a+$1)-g/.a] ) );
consider R1 being Function of the carrier of E,the carrier of F
such that
A31: for p being Point of E holds R1.p = FR1(p) from FUNCT_2:sch 4;
A33: N c= dom g by A1,A26,A30,XBOOLE_1:1;
A34: for x be Point of E st x in N
holds g/.x-g/.a = (-L).(x-a) + R1 /.(x-a)
proof
let x be Point of E;
assume x in N; then
A36: x in Ball(a,r4) & x in Ball(a,r5) by A30;
then
x in {y where y is Point of E: ||.y - a.|| < r5} by NDIFF_8:17; then
ex q be Element of E st x=q & ||.q-a.|| < r5; then
||.((g /. x) - (g /. a)).|| < r3 by A1,A26,A27,A36; then
g/.x in {y where y is Point of F: ||.y - b.|| < r3} by A5; then
A39: g /. x in Ball(b,r3) by NDIFF_8:17;
A41: f.(x,g.x) = c by A1,A26,A36;
A42: [x,g/.x ] in [:Ball(a,r3),Ball(b,r3):]
by A26,A36,A39,ZFMISC_1:87; then
A45: [x,g/.x] in N0 by A23;
reconsider w=[x,g/.x] as Point of [:E,F:];
A47: f/.w-f/.z = diff(f,z).(w-z) + R/.(w-z) by A17,A23,A42;
A48: f/.z = c by A1,PARTFUN1:def 6;
A50: f/.w = f. [x,g/.x] by A16,A45,PARTFUN1:def 6
.= c by A1,A26,A36,A41,PARTFUN1:def 6;
-z = [-a,-b] by A1,PRVECT_3:18; then
A52: w-z = [x-a,g/.x-b] by PRVECT_3:18
.= [x-a,g/.x-g/.a] by A1,NDIFF_8:13,PARTFUN1:def 6; then
diff(f,z).(w-z) = partdiff`1(f,z) . (x-a) + partdiff`2(f,z) .(g/.x-g/.a)
by A1,Th4; then
0.G = P.(x-a) + S. (g/.x-g/.a) + R/.(w-z)
by A1,A47,A48,A50,RLVECT_1:15; then
0.F = Q.(P.(x-a) + S. (g/.x-g/.a) + R/.(w-z)) by LOPBAN_7:3; then
0.F = Q.(P.(x-a) + S. (g/.x-g/.a)) + Q.(R/.(w-z)) by VECTSP_1:def 20
.= Q.(P.(x-a)) + Q.( S. (g/.x-g/.a)) + Q.(R/.(w-z)) by VECTSP_1:def 20
.= (Q*P).(x-a) + Q.( S. (g/.x-g/.a)) + Q.(R/.(w-z)) by FUNCT_2:15
.= (Q*P).(x-a) + (g/.x-g/.a) + Q.(R/.(w-z)) by A1,FUNCT_2:26; then
0.F - Q.(R/.(w-z)) = (Q*P).(x-a) + (g/.x-g/.a) by RLVECT_4:1; then
A53: -Q.(R/.(w-z)) - (Q*P).(x-a)
= (g/.x-g/.a) + (Q*P).(x-a) - (Q*P).(x-a) by RLVECT_1:14
.= g/.x-g/.a by RLVECT_4:1;
A54: dom (-Q*P) = dom (Q*P) by VFUNCT_1:def 5
.= the carrier of E by FUNCT_2:def 1;
A55: - (Q*P).(x-a) = - (Q*P)/.(x-a)
.= (- (Q*P))/.(x-a) by A54,VFUNCT_1:def 5
.= (-L).(x-a) by A15,A54,PARTFUN1:def 6;
R1/.(x-a) = -Q.(R/.( [x-a,g/. (x-a + a)- g/.a] ) ) by A31
.= -Q.(R/.(w-z)) by A52,RLVECT_4:1;
hence g/.x-g/.a = (-L).(x-a) + R1/.(x-a) by A53,A55;
end;
defpred FP[Point of E,object] means $2 = [$1,g/.(a+$1)-g/.a];
A59: for dx being Element of the carrier of E
ex dy being Element of the carrier of [:E,F:]
st FP[dx,dy];
consider V being Function of the carrier of E,the carrier of [:E,F:]
such that
A60: for dx being Element of the carrier of E holds FP[dx,V.dx]
from FUNCT_2:sch 3(A59);
A62: R is total by NDIFF_1:def 5;
reconsider Q1 = Q
as Point of R_NormSpace_of_BoundedLinearOperators(G,F) by LOPBAN_1:def 9;
set BLQ = ||.Q1.||;
0 *(BLQ + 1) < 2*(BLQ + 1) by XREAL_1:68; then
consider dr be Real such that
A65: dr > 0
& for dz be Point of [:E,F:]
st dz <> 0. [:E,F:] & ||.dz.|| < dr
holds ( ||.dz.||" * ||. R/.dz .||) < 1/(2 * ( BLQ + 1))
by A62,NDIFF_1:23;
consider dr1 be Real such that
A66: 0 < dr1 & dr1 < dr
& [: Ball(a,dr1),Ball(g/.a,dr1):] c= Ball(z,dr)
by A1,A5,A65,NDIFF_8:22;
consider dr2 being Real such that
A67: 0 < dr2
& for x1 being Point of E st x1 in dom g & ||.(x1 - a).|| < dr2
holds ||.((g /. x1) - (g /. a)).|| < dr1 by A1,A66,NFCONT_1:7;
reconsider dr3 = min(dr1,dr2) as Real;
A69: dr3 <= dr1 & dr3 <= dr2 by XXREAL_0:17;
reconsider dr4 = min(dr3,r1) as Real;
0 < dr3 by A66,A67,XXREAL_0:15; then
A71: 0 < dr4 by A1,XXREAL_0:15;
A72: dr4 <= dr3 & dr4 <= r1 by XXREAL_0:17;
A74: for dx be Point of E st dx <> 0.E & ||.dx.|| < dr4
holds ||. R/. (V.dx) .||
<= (1/(2 * ( BLQ + 1))) * ( ||.dx.|| + ||. g/.(a+dx)-g/.a .|| )
proof
let dx be Point of E;
set x1 = a + dx;
assume
A75: dx <> 0.E & ||.dx.|| < dr4; then
A76: ||.x1-a.|| < dr4 by RLVECT_4:1; then
||.x1-a.|| < dr3 by A72,XXREAL_0:2; then
A78: ||.x1-a.|| < dr1 & ||.x1-a.|| < dr2 by A69,XXREAL_0:2; then
||.a-x1.|| < dr1 by NORMSP_1:7; then
A79: x1 in Ball(a,dr1);
||.a-x1.|| < dr4 by A76,NORMSP_1:7; then
||.a-x1.|| < r1 & ||.a-x1.|| < dr3 by A72,XXREAL_0:2; then
x1 in Ball(a,r1); then
||.((g /. x1) - (g /. a)).|| < dr1 by A1,A67,A78; then
||. (g /. a) - (g /. x1) .|| < dr1 by NORMSP_1:7; then
g /. x1 in Ball(g /. a,dr1); then
[x1,g /. x1] in [:Ball(a,dr1),Ball(g /. a,dr1) :]
by A79,ZFMISC_1:87; then
[x1,g /. x1] in Ball(z,dr) by A66; then
consider w be Point of [:E,F:] such that
A84: w = [x1,g /. x1] & ||.z - w.|| < dr;
-z = [-a,-g /. a ] by A1,A5,PRVECT_3:18; then
A86: w - z = [x1-a,g/.x1 - g/.a] by A84,PRVECT_3:18;
A87: ||.w -z.|| < dr by A84,NORMSP_1:7;
x1-a = dx by RLVECT_4:1; then
A88: w -z <> 0.[:E,F:] by A75,A86,XTUPLE_0:1; then
||.w -z.|| <> 0 by NORMSP_0:def 5; then
( ||.w -z.||"* ||. R/. (w -z) .||) * ||.w -z.||
< (1/(2 * ( BLQ + 1))) * ||.w -z.||
by A65,A87,A88,XREAL_1:68; then
||.w -z.||"* ( ||. R/. (w -z) .|| * ||.w -z.|| )
< (1/(2 * ( BLQ + 1))) * ||.w -z.||; then
A91: ||. R/. (w -z) .|| < (1/(2 * ( BLQ + 1))) * ||.w -z.||
by A88,NORMSP_0:def 5,XCMPLX_1:203;
A92: V.dx = [ dx,g/.(a+dx)-g/.a ] by A60
.= [x1-a,g/.x1-g/.a] by RLVECT_4:1; then
A94: (1/(2 * ( BLQ + 1))) * ||.V.dx.||
<= (1/(2 * ( BLQ + 1))) * (||.x1-a.|| + ||. g/.x1-g/.a .|| )
by LM0,XREAL_1:64;
g/.x1 = g/.(a+dx) & x1-a =dx by RLVECT_4:1;
hence ||. R/. (V.dx) .||
<= (1/(2 * ( BLQ + 1))) * ( ||.dx.|| + ||. g/.(a+dx)-g/.a .|| )
by A86,A91,A92,A94,XXREAL_0:2;
end;
A95: for dx be Point of E st dx <> 0.E & ||.dx.|| < dr4
holds ||. R1/.dx .|| <= (1/2) * ( ||.dx.|| + ||. g/.(a+dx)-g/.a .|| )
proof
let dx be Point of E;
assume dx <> 0.E & ||.dx.|| < dr4; then
A97: ||. R/. (V.dx) .||
<= (1/(2 *( BLQ + 1))) * ( ||.dx.|| + ||. g/.(a+dx)-g/.a .|| ) by A74;
A98: ||. Q.(R/. (V.dx)).|| <= BLQ * ||. R/. (V.dx) .|| by LOPBAN_1:32;
A99: BLQ * ||. R/. (V.dx) .||
<= BLQ* ( (1/(2 *( BLQ + 1))) * ( ||.dx.|| + ||. g/.(a+dx)-g/.a .|| ))
by A97,XREAL_1:64;
A101: BLQ * ( (1/(2 *( BLQ + 1)))) = (1*BLQ) /(2 *( BLQ + 1))
.= (1/2)* ( BLQ/(BLQ+1)) by XCMPLX_1:103;
BLQ + 0 <= BLQ+1 by XREAL_1:7; then
BLQ/(BLQ+1) <= 1 by XREAL_1:183; then
(1/2) * ( BLQ/(BLQ+1)) <= (1/2)*1 by XREAL_1:64; then
( BLQ * ( (1/(2 *( BLQ + 1)))) * ( ||.dx.|| + ||. g/.(a+dx)-g/.a .|| ))
<= (1/2)*( ||.dx.|| + ||. g/.(a+dx)-g/.a .|| ) by A101,XREAL_1:64; then
BLQ * ||. R/. (V.dx) .||
<= (1/2)*( ||.dx.|| + ||. g/.(a+dx)-g/.a .|| ) by A99,XXREAL_0:2; then
A102: ||. Q.(R/. (V.dx)).||
<= (1/2) *( ||.dx.|| + ||. g/.(a+dx)-g/.a .|| ) by A98,XXREAL_0:2;
-Q.(R/. (V.dx)) = -Q.(R/. [dx,g/.(a+dx)-g/.a]) by A60
.= R1/.dx by A31;
hence thesis by A102,NORMSP_1:2;
end;
set LQ = ||.L.||;
reconsider dr5 = min(r6,dr4) as Real;
A104: 0 < dr5 by A28,A71,XXREAL_0:15;
A105: dr5 <= r6 & dr5 <= dr4 by XXREAL_0:17;
A107: for dx be Point of E
st dx <> 0.E & ||.dx.|| < dr5
holds ||. g/.(a+dx)-g/.a .|| <= (2*LQ+1) * ||.dx.||
proof
let dx be Point of E;
assume
A108: dx <> 0.E & ||.dx.|| < dr5; then
A109: ||.dx.|| < dr4 by A105,XXREAL_0:2;
A111: ||.dx.|| < r6 by A105,A108,XXREAL_0:2;
set x1=a+dx;
A112: x1-a = dx by RLVECT_4:1; then
||.a-x1.|| < r6 by A111,NORMSP_1:7; then
x1 in N; then
g/.x1-g/.a = (-L).(x1-a) + R1 /.(x1-a) by A34; then
A114: ||.g/.x1-g/.a.|| <= ||. (-L).(x1-a) .|| + ||. R1 /.(x1-a).||
by NORMSP_1:def 1;
(-L).(x1-a) = ((-1)*L ).(x1-a) by RLVECT_1:16
.= (-1) * ((Q*P) . (x1-a)) by LOPBAN_1:36
.= - ((Q*P) . (x1-a)) by RLVECT_1:16; then
||. (-L).(x1-a) .|| = ||. (Q*P) . (x1-a) .|| by NORMSP_1:2; then
A115: ||. (-L).(x1-a) .|| <= LQ* ||. x1-a .|| by A8,LOPBAN_1:32;
||. R1 /.(x1-a).|| <= (1/2) *( ||.x1-a.|| + ||. g/.x1-g/.a .|| )
by A95,A108,A109,A112; then
||. (-L).(x1-a) .|| + ||. R1 /.(x1-a).||
<= LQ * ||. x1-a .||
+ ( (1/2) * ( ||.x1-a.|| ) + (1/2) * ( ||. g/.x1-g/.a .|| ))
by A115,XREAL_1:7; then
||.g/.x1-g/.a.|| <= LQ * ||. x1-a .||
+ (1/2) *( ||.x1-a.|| ) + (1/2) *( ||. g/.x1-g/.a .|| )
by A114,XXREAL_0:2; then
||.g/.x1-g/.a.|| - (1/2) *( ||. g/.x1-g/.a .|| )
<= LQ * ||. x1-a .||
+ (1/2) * ( ||.x1-a.|| ) + (1/2) * ( ||. g/.x1-g/.a .|| )
- (1/2) * ( ||. g/.x1-g/.a .|| ) by XREAL_1:9; then
2 * ((1/2) * ( ||. g/.x1-g/.a .|| ) )
<= 2 *( LQ* ||. x1-a .|| + (1/2) *( ||.x1-a.|| ) ) by XREAL_1:64;
hence ||. g/.(a+dx)-g/.a .|| <= (2*LQ+1) * ||.dx.|| by A112;
end;
for r be Real st r > 0 ex d be Real st d > 0 &
for dx be Point of E st dx <> 0.E &
||.dx.|| < d holds ( ||.dx.||" * ||. R1/.dx .||) < r
proof
let r be Real;
assume
A117: r > 0;
A120: 0 < ((BLQ+1)*(2*LQ+2)) by XREAL_1:129; then
0 < r / ((BLQ+1)*(2*LQ+2)) by A117,XREAL_1:139; then
consider d1 be Real such that
A122: d1 > 0 &
for dz be Point of [:E,F:]
st dz <> 0. [:E,F:] & ||.dz.|| < d1
holds ( ||.dz.||"* ||. R/.dz .||)
< r / ((BLQ+1)*(2*LQ+2)) by A62,NDIFF_1:23;
consider r3 be Real such that
A123: 0 < r3 & r3 < d1
& [:Ball(a,r3),Ball(b,r3):] c= Ball(z,d1)
by A1,A122,NDIFF_8:22;
reconsider r4 = min(r1,r3) as Real;
A124: 0 < r4 by A1,A123,XXREAL_0:15;
A125: r4 <= r1 & r4 <= r3 by XXREAL_0:17;
consider r5 being Real such that
A127: 0 < r5
& for x1 being Point of E
st x1 in dom g & ||.(x1 - a).|| < r5
holds ||.((g /. x1) - (g /. a)).|| < r3 by A1,A123,NFCONT_1:7;
reconsider r6 = min(r4,r5) as Real;
A128: 0 < r6 by A124,A127,XXREAL_0:15;
A129: r6 <= r4 & r6 <= r5 by XXREAL_0:17;
reconsider d = min(r6,dr5) as Real;
A132: d <= r6 & d <= dr5 by XXREAL_0:17;
take d;
thus 0 < d by A104,A128,XXREAL_0:15;
let dx be Point of E;
assume
A133: dx <> 0.E & ||.dx.|| < d;
set x1 = a+dx;
reconsider dz = [dx,g/.(a+dx)-g/.a] as Point of [:E,F:];
A134: dz <> 0. [:E,F:] by A133,XTUPLE_0:1;
A137: ||.dx.|| < dr5 by A132,A133,XXREAL_0:2;
A138: ||.dx.|| < r6 by A132,A133,XXREAL_0:2; then
A139: ||.dx.|| < r5 by A129,XXREAL_0:2;
||.dx.|| < r4 by A129,A138,XXREAL_0:2; then
A140: ||.dx.|| < r1 & ||.dx.|| < r3 by A125,XXREAL_0:2; then
||.x1 - a .|| < r1 by RLVECT_4:1; then
||.a -x1 .|| < r1 by NORMSP_1:7; then
A141: x1 in dom g by A1;
||.(x1 - a).|| < r5 by A139,RLVECT_4:1; then
||.((g /. x1) - (g /. a)).|| < r3 by A127,A141; then
||.(g /. a) - (g /. x1) .|| < r3 by NORMSP_1:7; then
A142: g/.x1 in Ball(b,r3) by A5;
||.x1 - a .|| < r3 by A140,RLVECT_4:1; then
||. a - x1 .|| < r3 by NORMSP_1:7; then
x1 in Ball(a,r3); then
[x1,g /. x1] in [:Ball(a,r3),Ball(b,r3) :] by A142,ZFMISC_1:87; then
[x1,g /. x1] in Ball(z,d1) by A123; then
consider w be Point of [:E,F:] such that
A145: w = [x1,g /. x1] & ||.z - w.|| < d1;
-z = [-a,-g /. a ] by A1,A5,PRVECT_3:18; then
w - z = [x1-a,g/.x1 - g/.a ] by A145,PRVECT_3:18
.= dz by RLVECT_4:1; then
A148: ||.dz.|| < d1 by A145,NORMSP_1:7;
R1/.dx = -Q.(R/.( [dx,g/.(a+dx)-g/.a] ) ) by A31; then
||. R1/.dx .||
= ||. Q.(R/.( [dx,g/.(a+dx)-g/.a] ) ) .|| by NORMSP_1:2; then
A150: ||. R1/.dx .||
<= BLQ * ||. R/.( [dx,g/.(a+dx)-g/.a] ) .|| by LOPBAN_1:32;
0 + BLQ < BLQ +1 by XREAL_1:8; then
BLQ * ||. R/.( [dx,g/.(a+dx)-g/.a] ) .||
<= (BLQ+1) * ||. R/.( [dx,g/.(a+dx)-g/.a] ) .||
by XREAL_1:64; then
||. R1/.dx .|| <= (BLQ+1) * ||. R/.( [dx,g/.(a+dx)-g/.a] ) .||
by A150,XXREAL_0:2; then
||.dx.||" * ||. R1/.dx .||
<= ||.dx.||" * ( (BLQ+1)* ||. R/.( [dx,g/.(a+dx)-g/.a] ) .|| )
by XREAL_1:64; then
||.dx.||" * ||. R1/.dx .||
<= ||.dx.||" * (BLQ+1) * ||. R/.( dz ) .||; then
A152: ||.dx.||" * ||. R1/.dx .||
<= ||.dx.||" * (BLQ+1)*( ||.dz.||" * ( ||. R/.( dz ) .|| * ||.dz.|| ))
by A134,NORMSP_0:def 5,XCMPLX_1:203;
A153: ||.dz.|| <= ||.dx.|| + ||.g/.(a+dx)-g/.a.|| by LM0;
||. g/.(a+dx)-g/.a .|| <= (2*LQ+1) * ||.dx.||
by A107,A133,A137; then
||.dx.|| + ||.g/.(a+dx)-g/.a.||
<= ||.dx.|| + (2*LQ+1) * ||.dx.|| by XREAL_1:7; then
||.dz.|| <= ||.dx.|| + (2*LQ+1) * ||.dx.|| by A153,XXREAL_0:2; then
||.dx.||" * ||.dz.|| <= ||.dx.||" * ( ||.dx.|| + (2*LQ+1) * ||.dx.||)
by XREAL_1:64; then
||.dx.||" * ||.dz.|| <= ( ||.dx.||" * ( ||.dx.||*1 ) )
+ ( ||.dx.||" * ( (2*LQ+1) * ||.dx.|| ) ); then
||.dx.||" * ||.dz.|| <= 1 + ||.dx.||" * ( (2*LQ+1) * ||.dx.|| )
by A133,NORMSP_0:def 5,XCMPLX_1:203; then
||.dx.||" * ||.dz.|| <= 1 + (2*LQ+1)
by A133,NORMSP_0:def 5,XCMPLX_1:203;
then (BLQ+1)*( ||.dz.||" * ||. R/.( dz ) .|| ) * ( ||.dx.||" * ||.dz.|| )
<= (BLQ+1)*( ||.dz.||" * ||. R/.( dz ) .|| ) * (2*LQ+2)
by XREAL_1:64; then
A159: ||.dx.||" * ||. R1/.dx .||
<= ((BLQ+1)* (2*LQ+2)) *( ||.dz.||" * ||. R/. dz .|| )
by A152,XXREAL_0:2;
((BLQ+1)* (2*LQ+2)) * (||.dz.||" * ||. R/. dz .||)
< ((BLQ+1)* (2*LQ+2)) * (r / ((BLQ+1)*(2*LQ+2)))
by A120,A122,A134,A148,XREAL_1:68;
then ((BLQ+1)* (2*LQ+2)) * (||.dz.||" * ||. R/. dz .||) < r
by A120,XCMPLX_1:87;
hence ||.dx.||" * ||. R1/.dx .|| < r by A159,XXREAL_0:2;
end; then
A162: R1 is RestFunc of E,F by NDIFF_1:23;
hence g is_differentiable_in a by A1,A26,A30,A34,NDIFF_1:def 6,XBOOLE_1:1;
hence diff(g,a) = - Q*P by A15,A33,A34,A162,NDIFF_1:def 7;
end;
reserve X,Y,Z for non trivial RealBanachSpace;
theorem LMTh3:
for u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
st u is invertible
holds
ex K,s be Real
st 0 <= K & 0 < s
& for du be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
st ||.du.|| < s
holds
u+du is invertible
& ||.Inv(u+du) - Inv u - (- (Inv u)*du*(Inv u) ) .||
<= K * (||.du.|| * ||.du.||)
proof
let u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
assume
A1: u is invertible;
set s1 = 1 / ||.Inv u .||;
set AG = R_Normed_Algebra_of_BoundedLinearOperators X;
A3: 0 < ||. Inv u .|| by A1,LOPBAN13:12;
set s2 = (1/2) / ||. Inv u .||;
A5: 0 < s2 by A3,XREAL_1:139;
set s12 = min(s1,s2);
A7: 0 < s12 & s12 <= s1 & s12 <= s2 by A3,A5,XXREAL_0:15,17;
set K = 2 * ||. (Inv u) .|| * ||. (Inv u) .|| * ||. (Inv u) .||;
take K,s12;
thus 0 <= K & 0 < s12 by A3,A5,XXREAL_0:15;
let du be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
assume
A8: ||.du.|| < s12; then
A9: ||.du.|| < s1 by A7,XXREAL_0:2;
hence u+du is invertible by A1,LOPBAN13:13;
consider w be Point of R_Normed_Algebra_of_BoundedLinearOperators X,
s,I be Point of R_NormSpace_of_BoundedLinearOperators(X,X)
such that
A11: w = (Inv u) * du
& 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 + du) = Inv(I+s) * (Inv u) by A1,A9,LOPBAN13:13;
reconsider sA = s as Point of AG;
A13: I * (Inv u)
= (id the carrier of X) * modetrans(Inv u,Y,X) by A11,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);
set L = ( Inv u ) * du * ( Inv u );
A14: Inv (u+du) - Inv u -( -( Inv u) * du * (Inv u) )
= Inv(I+s) * (Inv u) - IIu + L by A11,A13,RLVECT_1:17
.= ( Inv(I+s) -I) * (Inv u) + L by LOPBAN13:20;
A15: Inv(I+s)*(I+s) = I by A11,LOPBAN13:22;
Inv(I+s)*I = modetrans(Inv(I+s),X,X) * (id the carrier of X)
by A11,LOPBAN_1:def 11
.= modetrans(Inv(I+s),X,X) by FUNCT_2:17
.= Inv(I+s) by LOPBAN_1:def 11; then
A17: Inv(I+s) - I = Inv(I+s) * (I - (I+s) ) by A15,LOPBAN13:19
.= Inv(I+s) * (- ((Inv u) * du)) by A11,LOPBAN13:21; then
A19: (Inv(I+s) -I) * (Inv u)
= ( - Inv(I+s) * ((Inv u) * du)) * Inv u by LOPBAN13:26
.= - ( Inv(I+s) * ((Inv u) * du) * Inv u) by LOPBAN13:26
.= - Inv(I+s) * L by LOPBAN13:10;
I * L = (id the carrier of X) * modetrans(L,Y,X) by A11,LOPBAN_1:def 11
.= modetrans(L,Y,X) by FUNCT_2:17
.= L by LOPBAN_1:def 11;
then - Inv(I+s) * L + L = I * L - Inv(I+s) * L
.= (I - Inv(I+s)) * L by LOPBAN13:20
.= (- (Inv(I+s)-I) ) * L by RLVECT_1:33
.= - Inv(I+s) * ( - ((Inv u) * du) ) * ((Inv u) * du * (Inv u))
by A17,LOPBAN13:26; then
Inv (u+du) - Inv u -( -(Inv u) * du * (Inv u) )
= - ((- ( Inv(I+s) *((Inv u) * du)))*((Inv u)*du*(Inv u)))
by A14,A19,LOPBAN13:26
.= - - (Inv(I+s)*((Inv u) * du)) * ((Inv u)*du*(Inv u)) by LOPBAN13:26
.= (Inv(I+s) * ((Inv u) * du))*((Inv u)*du*(Inv u)) by RLVECT_1:17;
then
A22: ||. Inv(u+du) - Inv u -(-(Inv u)*du*(Inv u)) .||
<= ||. Inv(I+s) * ((Inv u) * du) .|| * ||. (Inv u)*du*(Inv u) .||
by LOPBAN13:18;
A23: ||. Inv(I+s) * ((Inv u) * du) .||
<= ||. Inv(I+s) .|| * ||. (Inv u) * du .|| by LOPBAN13:18;
||. Inv(I+s) .|| * ||. (Inv u) * du .||
<= ||. Inv(I+s) .|| * (||. (Inv u).|| * ||.du .||)
by LOPBAN13:18,XREAL_1:64; then
A25: ||. Inv(I+s) * ((Inv u) * du) .||
<= ||. Inv(I+s) .|| * ( ||. (Inv u).|| * ||.du .|| ) by A23,XXREAL_0:2;
A26: ||. (Inv u) * du .|| * ||.Inv u .||
<= ||. (Inv u).|| * ||.du .|| * ||.Inv u .|| by LOPBAN13:18,XREAL_1:64;
||. (Inv u)*du*(Inv u) .||
<= ||. (Inv u)*du .|| * ||.Inv u .|| by LOPBAN13:18; then
||. (Inv u)*du*(Inv u) .||
<= ||. (Inv u).|| * ||.du .|| * ||.Inv u .|| by A26,XXREAL_0:2; then
||. Inv(I+s) *( (Inv u) * du ) .|| * ||. ( Inv u )*du*(Inv u ) .||
<= ||. Inv(I+s) .|| * ( ||. (Inv u).|| * ||.du .|| )
* (||. (Inv u).|| * ||.du .|| * ||.Inv u .|| )
by A25,XREAL_1:66; then
A28: ||. Inv(u+du) - Inv u -( -(Inv u)*du*(Inv u) ) .||
<= ||. Inv(I+s) .|| * ( ||. (Inv u).|| * ||.du .|| )
* (||. (Inv u).|| * ||.du .|| * ||.Inv u .||) by A22,XXREAL_0:2;
A29: ||.s.|| <= ||. Inv u .|| * ||.du.|| by A11,LOPBAN13:18;
||.du.|| < s2 by A7,A8,XXREAL_0:2; then
||. Inv u .|| * ||.du.||
<= ||. Inv u .|| * ((1/2) / ||. Inv u .||) by XREAL_1:64; then
||. Inv u .|| * ||.du.|| <= 1/2 by A3,XCMPLX_1:87; then
||.s.|| <= 1/2 by A29,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
||.Inv (I+s).|| <=2 by A11,XXREAL_0:2; then
||. Inv(I+s) .|| * ((||. (Inv u).|| * ||.du .||)
* (||. (Inv u).|| * ||.du .|| * ||.Inv u .||))
<= 2 * ((||. (Inv u).|| * ||.du .||)
* (||. (Inv u).|| * ||.du .|| * ||.Inv u .||)) by XREAL_1:64;
hence ||. Inv (u+du) - Inv u -( -(Inv u)*du*(Inv u) ) .||
<= K * (||.du .|| * ||.du .||) by A28,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
for u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
st u in InvertibleOperators(X,Y)
holds I is_differentiable_in u
& for du be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
holds diff(I,u).du = - (Inv u) * du * (Inv u)
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 W = R_NormSpace_of_BoundedLinearOperators(Y,X);
set N = InvertibleOperators(X,Y);
set P = InvertibleOperators(Y,X);
let u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
assume
A2: u in N;
deffunc FL(Point of S) = - (Inv u) * $1 * (Inv u);
consider L being Function of the carrier of S,the carrier of W
such that
A3: for x being Point of S holds L.x = FL(x) from FUNCT_2:sch 4;
A6: for s, t being Element of S holds
L . (s + t) = (L . s) + (L . t)
proof
let s, t be Element of S;
thus L . (s + t) = - (Inv u) * (s + t) * Inv u by A3
.= - ((Inv u) * s + (Inv u) * t ) * (Inv u) by LOPBAN13:19
.= - ((Inv u) * s * (Inv u) + (Inv u) * t * (Inv u)) by LOPBAN13:20
.= - (Inv u) * s * (Inv u) - (Inv u) * t * (Inv u) by RLVECT_1:31
.= L.s + - (Inv u) * t * (Inv u) by A3
.= L.s + L.t by A3;
end;
for s being Element of S
for r being Real holds L . (r * s) = r * (L . s)
proof
let s be Element of S,
r be Real;
thus L . (r*s) = - (Inv u) * (r*s) * Inv u by A3
.= -(r * (Inv u) * s) * Inv u by LOPBAN13:28
.= - r * ((Inv u) * s) * (Inv u) by LOPBAN13:28
.= - r * (((Inv u) * s) * (Inv u)) by LOPBAN13:28
.= r * (- (Inv u) * s * Inv u) by RLVECT_1:25
.= r * L.s by A3;
end; then
reconsider L as LinearOperator of S,W
by A6,LOPBAN_1:def 5,VECTSP_1:def 20;
now
let x be VECTOR of S;
L.x = - (Inv u) * x * Inv u by A3; then
A8: ||.L . x.|| = ||. (Inv u) * x * Inv u .|| by NORMSP_1:2;
A9: ||. (Inv u) * x * Inv u .|| <= ||. (Inv u) * x .|| * ||.Inv u .||
by LOPBAN13:18;
||. (Inv u) * x .|| * ||. Inv u .||
<= ||. (Inv u) .|| * ||. x .|| * ||. Inv u .||
by LOPBAN13:18,XREAL_1:64;
hence ||. L.x .|| <= ( ||. (Inv u) .|| * ||. Inv u .||) * ||. x .||
by A8,A9,XXREAL_0:2;
end; then
reconsider L as Lipschitzian LinearOperator of S,W by LOPBAN_1:def 8;
deffunc FR(Point of S) = Inv (u+$1) - Inv u - L.$1;
consider R being Function of the carrier of S,the carrier of W
such that
A11: for x being Point of S holds R.x = FR(x) from FUNCT_2:sch 4;
A12: dom R = the carrier of S by FUNCT_2:def 1;
A13: for x be Point of S
holds R.x = Inv (u+x) - Inv u -(- Inv u * x * Inv u)
proof
let x be Point of S;
thus R.x = Inv(u+x) - Inv u -L.x by A11
.= Inv(u+x) - Inv u -(- Inv u * x * Inv u) by A3;
end;
reconsider L0 = L
as Point of R_NormSpace_of_BoundedLinearOperators(S,W) by LOPBAN_1:def 9;
for r being Real st r > 0 holds
ex d being Real
st d > 0
& for z being Point of S st z <> 0. S & ||.z.|| < d
holds (||.z.|| ") * ||.(R/. z).|| < r
proof
let r0 be Real;
assume
A15: r0 > 0;
set r = r0/2;
A16: 0 < r & r < r0 by A15,XREAL_1:215,216;
ex v be Point of S st u = v & v is invertible by A2; then
consider K,s be Real such that
A17: 0 <= K & 0 < s
& for du be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
st ||.du.|| < s
holds u+du is invertible
& ||.Inv (u+du) - Inv u -(-(Inv u)*du*(Inv u)) .||
<= K* ( ||.du.|| * ||.du.|| ) by LMTh3;
set s1 = r / ( K+1 );
A18: K + 0 < K + 1 by XREAL_1:8;
A20: 0 < s1 by A16,A17,XREAL_1:139;
set s2 = min(s1,1);
A21: 0 < s2 & s2 <=s1 & s2 <=1 by A20,XXREAL_0:15,17;
set d = min(s,s2);
A22: 0 < d & d <= s & d <= s2 by A17,A21,XXREAL_0:15,17; then
A23: d <= s & d <= s1 & d <= 1 by A21,XXREAL_0:2;
take d;
thus d > 0 by A17,A21,XXREAL_0:15;
let z be Point of S;
assume
A24: z <> 0. S & ||.z.|| < d; then
A25: ||.z.|| < s by A22,XXREAL_0:2;
||.(R/. z).|| = ||.Inv (u+z) - Inv u -( - Inv u * z * Inv u ) .||
by A13; then
||.(R/. z).|| <= K* ( ||.z.|| * ||.z.|| ) by A17,A25; then
||.(R/. z).|| / ||.z.|| <=( ( K * ||.z.||) * ||.z.|| ) / ||.z.||
by XREAL_1:72; then
A27: ||.(R/. z).|| / ||.z.|| <= K * ||.z.||
by A24,NORMSP_0:def 5,XCMPLX_1:89;
||.z.|| <= s1 by A23,A24,XXREAL_0:2; then
A28: K * ||.z.|| <= K*(r / ( K+1 )) by A17,XREAL_1:64;
K / (K+1) <=1 by A17,A18,XREAL_1:183; then
r * ( K / (K+1) ) <= 1*r by A15,XREAL_1:64; then
K * ||.z.|| <= r by A28,XXREAL_0:2; then
||.(R/. z).|| / ||.z.|| <= r by A27,XXREAL_0:2;
hence (||.z.|| ") * ||.(R/. z).|| < r0 by A16,XXREAL_0:2;
end; then
reconsider R0 = R as RestFunc of S,W by NDIFF_1:23;
ex g being Real
st 0 < g & { y where y is Point of S : ||.(y - u).|| < g } c= N
by A2,NDIFF_1:3; then
A29: N is Neighbourhood of u by NFCONT_1:def 1;
A30: for v being Point of S st v in N holds
I /. v - I /. u = L0 . (v - u) + R0 /. (v - u)
proof
let v be Point of S;
assume
A31: v in N; then
A32: I /. v = I.v by A1,PARTFUN1:def 6
.= Inv v by A1,A31;
I /. u = I.u by A1,A2,PARTFUN1:def 6
.= Inv u by A1,A2;
hence I /. v - I /. u = Inv (u+(v-u)) - Inv u by A32,RLVECT_4:1
.= L0.(v-u) + (Inv (u+(v-u)) - Inv u - L.(v-u)) by RLVECT_4:1
.= L0.(v-u) + (Inv (u+(v-u)) - Inv u - (- Inv u * (v-u) * Inv u)) by A3
.= L0.(v-u) + R.(v-u) by A13
.= L0.(v-u) + R0/.(v-u) by A12,PARTFUN1:def 6;
end;
hence
A34: I is_differentiable_in u by A1,A29,NDIFF_1:def 6;
let du be Point of S;
thus diff(I,u).du = L0.du by A1,A29,A30,A34,NDIFF_1:def 7
.= -(Inv u) *du * (Inv u) by A3;
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_differentiable_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_differentiable_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 )
& for u,du be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
st u in InvertibleOperators(X,Y)
holds diff(I,u).du =- (Inv u) * du * (Inv u)
proof
set S = R_NormSpace_of_BoundedLinearOperators(X,Y);
set K = R_NormSpace_of_BoundedLinearOperators(Y,X);
consider I be PartFunc of
R_NormSpace_of_BoundedLinearOperators(X,Y),
R_NormSpace_of_BoundedLinearOperators(Y,X) such that
A1: 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 by LOPBAN13:25;
consider J be PartFunc of
R_NormSpace_of_BoundedLinearOperators(Y,X),
R_NormSpace_of_BoundedLinearOperators(X,Y) such that
A2: J = I"
& J is one-to-one
& dom J = InvertibleOperators(Y,X)
& rng J = InvertibleOperators(X,Y)
& J is_continuous_on InvertibleOperators(Y,X) by A1;
take I;
A4: for u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
st u in InvertibleOperators(X,Y)
holds I is_differentiable_in u by A1,LM80;
for v be Point of R_NormSpace_of_BoundedLinearOperators(Y,X)
st v in InvertibleOperators(Y,X)
holds J.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
A5: u in dom I & v=I.u by A1,FUNCT_1:def 3;
reconsider u
as Point of R_NormSpace_of_BoundedLinearOperators(X,Y) by A5;
A7: ex u0 be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
st u = u0 & u0 is invertible by A1,A5;
thus J.v = u by A1,A2,A5,FUNCT_1:34
.= Inv Inv u by A7,LOPBAN13:15
.= Inv v by A1,A5;
end; then
for v be Point of R_NormSpace_of_BoundedLinearOperators(Y,X)
st v in InvertibleOperators(Y,X)
holds J is_differentiable_in v by A2,LM80; then
J is_differentiable_on InvertibleOperators(Y,X) by A2,NDIFF_1:31;
hence thesis by A1,A2,A4,LM80,NDIFF_1:31;
end;
theorem Th45:
for E,G,F be RealNormSpace,
Z be Subset of [:E,F:],
f be PartFunc of [:E,F:], G,
a be Point of E,
b be Point of F,
c be Point of G,
z be Point of [:E,F:],
A be Subset of E,
B be Subset of F,
g be PartFunc of E,F
st Z is open & dom f = Z
& A is open & B is open & [:A,B:] c= Z
& z = [a,b] & f.(a,b) = c
& f is_differentiable_in z
& dom g = A & rng g c= B & a in A
& g.a = b
& g is_continuous_in a
& ( for x be Point of E st x in A holds f.(x,g.x) = c )
& partdiff`2(f,z) is invertible
holds
g is_differentiable_in a
& diff(g,a) = - ( Inv partdiff`2(f,z)) * partdiff`1(f,z)
proof
let E,G,F be RealNormSpace,
Z be Subset of [:E,F:],
f be PartFunc of [:E,F:], G,
a be Point of E,
b be Point of F,
c be Point of G,
z be Point of [:E,F:],
A be Subset of E,
B be Subset of F,
g be PartFunc of E,F;
assume
A1: Z is open & dom f = Z
& A is open & B is open & [:A,B:] c= Z
& z = [a,b] & f.(a,b) = c
& f is_differentiable_in z
& dom g = A & rng g c= B & a in A
& g.a = b
& g is_continuous_in a
& ( for x be Point of E st x in A holds f.(x,g.x) = c )
& partdiff`2(f,z) is invertible;
then b in rng g by FUNCT_1:def 3; then
consider r2 be Real such that
A3: 0 < r2 & Ball(b,r2) c= B by A1,NDIFF_8:20;
consider r3 being Real such that
A4: 0 < r3
& for x1 being Point of E
st x1 in dom g & ||.(x1 - a).|| < r3
holds ||.((g /. x1) - (g /. a)).|| < r2 by A1,A3,NFCONT_1:7;
consider r4 be Real such that
A5: 0 < r4 & Ball(a,r4) c= A by A1,NDIFF_8:20;
set r1 = min(r3,r4);
A6: 0 < r1 & r1 <= r3 & r1 <= r4 by A4,A5,XXREAL_0:17,21;
set g1 = g| Ball(a,r1);
B6: Ball(a,r1) c= Ball(a,r4) by A6,NDIFF_8:15; then
A7: Ball(a,r1) c= A by A5,XBOOLE_1:1;
A8: dom g1 = Ball(a,r1) by A1,A5,B6,RELAT_1:62,XBOOLE_1:1;
B8: now
let y be object;
assume
A9: y in rng g1; then
consider x be object such that
A10: x in dom g1 & y = g1.x by FUNCT_1:def 3;
reconsider xp = x as Point of E by A10;
A12: x in Ball(a,r4) by A6,A8,A10,NDIFF_8:15,TARSKI:def 3;
reconsider yp = y as Point of F by A9;
xp in {xx where xx is Point of E: ||.xx - a.|| < r1}
by A8,A10,NDIFF_8:17; then
ex z be Point of E st z = xp & ||.z - a.|| < r1; then
||.xp - a.|| < r3 by A6,XXREAL_0:2; then
A13: ||.((g /. xp) - (g /. a)).|| < r2 by A1,A4,A5,A12;
A14: y = g.xp by A8,A10,FUNCT_1:49
.= g/.xp by A1,A5,A12,PARTFUN1:def 6;
b = g/.a by A1,PARTFUN1:def 6; then
yp in {z where z is Point of F: ||.z - b.|| < r2} by A13,A14;
hence y in Ball(b,r2) by NDIFF_8:17;
end;
A17: a in Ball(a,r1) by A6,NDIFF_8:13;
A26: for r being Real st 0 < r holds
ex s being Real
st 0 < s
& for x1 being Point of E
st x1 in dom g1
& ||.(x1 - a).|| < s
holds ||.((g1 /. x1) - (g1 /. a)).|| < r
proof
let r be Real;
assume 0 < r; then
consider s being Real such that
A20: 0 < s
& for x1 being Point of E
st x1 in dom g
& ||.(x1 - a).|| < s
holds ||.((g /. x1) - (g /. a)).|| < r by A1,NFCONT_1:7;
take s;
thus 0 < s by A20;
let x1 be Point of E;
assume
A21: x1 in dom g1 & ||.(x1 - a).|| < s;
then A25: g /. x1 = g.x1 by A1,A7,A8,PARTFUN1:def 6
.= g1.x1 by A8,A21,FUNCT_1:49
.= g1/.x1 by A21,PARTFUN1:def 6;
g /. a = g.a by A1,PARTFUN1:def 6
.= g1.a by A6,FUNCT_1:49,NDIFF_8:13
.= g1/.a by A6,A8,NDIFF_8:13,PARTFUN1:def 6;
hence ||.((g1 /. x1) - (g1 /. a)).|| < r by A1,A7,A8,A20,A21,A25;
end;
A28: for x be Point of E st x in Ball(a,r1) holds f.(x,g1.x) = c
proof
let x be Point of E;
assume
A29: x in Ball(a,r1); then
f.(x,g.x) = c by A1,A7;
hence thesis by A29,FUNCT_1:49;
end;
b in Ball(b,r2) by A3,NDIFF_8:13; then
A31: [a,b] in [:Ball(a,r1),Ball(b,r2):] by A17,ZFMISC_1:87;
A32: [:Ball(a,r1),Ball(b,r2):] c= [:A,B:] by A3,A7,ZFMISC_1:96;
reconsider Q = partdiff`2(f,z)"
as Lipschitzian LinearOperator of G,F by A1,LOPBAN_1:def 9;
reconsider P = partdiff`1(f,z)
as Lipschitzian LinearOperator of E,G by LOPBAN_1:def 9;
Z is open & dom f = Z
& z = [a,b] & z in Z
& f.(a,b) = c
& f is_differentiable_in z
& 0 <r1 & 0 < r2
& dom g1 = Ball(a,r1)
& rng g1 c= Ball(b,r2)
& g1.a = b
& g1 is_continuous_in a
& ( for x be Point of E st x in Ball(a,r1) holds f.(x,g1.x) = c )
& partdiff`2(f,z) is one-to-one
& Q = partdiff`2(f,z)"
& P = partdiff`1(f,z) by A1,A3,A6,A8,B8,A26,A28,A31,A32,FUNCT_1:49,
NDIFF_8:13,NFCONT_1:7,TARSKI:def 3; then
A33: g1 is_differentiable_in a
& diff(g1,a) = - Q*P by Th5;
then consider N being Neighbourhood of a such that
A34: N c= dom g1
& ex R being RestFunc of E,F
st for x being Point of E st x in N holds
g1 /. x - g1 /. a = diff(g1,a) . (x - a) + R /. (x - a)
by NDIFF_1:def 7;
consider R being RestFunc of E,F such that
A35: for x being Point of E st x in N holds
g1 /. x - g1 /. a = diff(g1,a) . (x - a) + R /. (x - a) by A34;
A37: N c= A by A7,A8,A34,XBOOLE_1:1;
A38: N c= dom g by A1,A7,A8,A34,XBOOLE_1:1;
A39: for x being Point of E st x in N holds
g /. x - g /. a = diff(g1,a) . (x - a) + R /. (x - a)
proof
let x be Point of E;
assume
A40: x in N; then
A46: g /. x = g.x by A1,A37,PARTFUN1:def 6
.= g1.x by A8,A34,A40,FUNCT_1:49
.= g1/.x by A34,A40,PARTFUN1:def 6;
g /. a = g.a by A1,PARTFUN1:def 6
.= g1.a by A6,FUNCT_1:49,NDIFF_8:13
.= g1/.a by A6,A8,NDIFF_8:13,PARTFUN1:def 6;
hence g /. x - g /. a = diff(g1,a) . (x - a) + R /. (x - a)
by A35,A40,A46;
end;
hence g is_differentiable_in a
by A1,A7,A8,A34,NDIFF_1:def 6,XBOOLE_1:1; then
A48: diff(g,a)= diff(g1,a) by A38,A39,NDIFF_1:def 7;
Q = Inv partdiff`2(f,z) by A1,LOPBAN13:def 2; then
modetrans(( Inv partdiff`2(f,z) ),G,F) = Q by LOPBAN_1:def 11;
then A51: ( Inv partdiff`2(f,z) ) * partdiff`1(f,z) = Q*P
by LOPBAN_1:def 11; then
Q*P is Lipschitzian LinearOperator of E,F by LOPBAN_1:def 9;
hence thesis by A33,A48,A51,LOPBAN13:31;
end;
theorem Th47:
for E be RealNormSpace,
G,F be non trivial RealBanachSpace,
Z be Subset of [:E,F:],
f be PartFunc of [:E,F:], G,
c be Point of G,
A be Subset of E,
B be Subset of F,
g be PartFunc of E,F
st Z is open & dom f = Z
& A is open & B is open & [:A,B:] c= Z
& f is_differentiable_on Z
& f `| Z is_continuous_on Z
& dom g = A & rng g c= B
& g is_continuous_on A
& ( for x be Point of E st x in A holds f.(x,g.x) = c )
& ( for x be Point of E, z be Point of [:E,F:]
st x in A & z =[x,g.x]
holds partdiff`2(f,z) is invertible )
holds
g is_differentiable_on A
& g `| A is_continuous_on A
& for x be Point of E,
z be Point of [:E,F:]
st x in A & z =[x,g.x]
holds diff(g,x) = - (Inv partdiff`2(f,z)) * partdiff`1(f,z)
proof
let E be RealNormSpace,
G,F be non trivial RealBanachSpace,
Z be Subset of [:E,F:],
f be PartFunc of [:E,F:], G,
c be Point of G,
A be Subset of E,
B be Subset of F,
g be PartFunc of E,F;
assume
A1: Z is open & dom f = Z
& A is open & B is open & [:A,B:] c= Z
& f is_differentiable_on Z
& f `| Z is_continuous_on Z
& dom g = A & rng g c= B
& g is_continuous_on A
& ( for x be Point of E st x in A holds f.(x,g.x) = c )
& ( for x be Point of E,
z be Point of [:E,F:]
st x in A & z =[x,g.x]
holds partdiff`2(f,z) is invertible );
then A2: f is_partial_differentiable_on`1 Z
& f is_partial_differentiable_on`2 Z
& f `partial`1| Z is_continuous_on Z
& f `partial`2| Z is_continuous_on Z by NDIFF_7:52;
A3: for x being Point of E,
z be Point of [:E,F:]
st x in A & z = [x,g.x]
holds
g is_differentiable_in x
& diff(g,x) = - (Inv partdiff`2(f,z)) * partdiff`1(f,z)
proof
let a be Point of E,
z be Point of [:E,F:];
assume
A4: a in A & z=[a,g.a]; then
A5: g.a in rng g by A1,FUNCT_1:def 3; then
reconsider b = g.a as Point of F;
A6: f.(a,b) = c by A1,A4;
z in [:A,B:] by A1,A4,A5,ZFMISC_1:87; then
A9: f is_differentiable_in z by A1,NDIFF_1:31;
A10: g|A is_continuous_in a by A1,A4,NFCONT_1:def 7;
A11: g | A = g by A1,RELAT_1:68;
partdiff`2(f,z) is invertible by A1,A4;
hence g is_differentiable_in a
& diff(g,a) = - ( Inv partdiff`2(f,z)) * partdiff`1(f,z)
by A1,A4,A6,A9,A10,A11,Th45;
end;
for x being Point of E st x in A holds g is_differentiable_in x
proof
let x be Point of E;
assume
A13: x in A; then
g.x in rng g by A1,FUNCT_1:def 3; then
reconsider y = g.x as Point of F;
[x,y] = [x,g.x];
hence thesis by A3,A13;
end;
hence
A15: g is_differentiable_on A by A1,NDIFF_1:31; then
A16: dom ( g `| A ) = A by NDIFF_1:def 9;
consider xg be PartFunc of E,[:E,F:] such that
A17: dom xg = A
& for x be Point of E st x in A
holds xg.x = [x,g.x] and
A18: xg is_continuous_on A by A1,LmTh471;
consider BL be BilinearOperator of
R_NormSpace_of_BoundedLinearOperators(E,G),
R_NormSpace_of_BoundedLinearOperators(G,F),
R_NormSpace_of_BoundedLinearOperators(E,F) such that
A19: BL is_continuous_on the carrier of
[: R_NormSpace_of_BoundedLinearOperators(E,G),
R_NormSpace_of_BoundedLinearOperators(G,F):]
& for u be Point of R_NormSpace_of_BoundedLinearOperators(E,G),
v be Point of R_NormSpace_of_BoundedLinearOperators(G,F)
holds BL.(u,v) = v*u by LOPBAN13:29;
consider I be PartFunc of
R_NormSpace_of_BoundedLinearOperators(F,G),
R_NormSpace_of_BoundedLinearOperators(G,F) such that
A20: dom I = InvertibleOperators(F,G)
& rng I = InvertibleOperators(G,F)
& I is one-to-one
& I is_continuous_on InvertibleOperators(F,G)
& ( ex J be PartFunc of
R_NormSpace_of_BoundedLinearOperators(G,F),
R_NormSpace_of_BoundedLinearOperators(F,G)
st J = I"
& J is one-to-one
& dom J = InvertibleOperators(G,F)
& rng J = InvertibleOperators(F,G)
& J is_continuous_on InvertibleOperators(G,F))
& for u be Point of R_NormSpace_of_BoundedLinearOperators(F,G)
st u in InvertibleOperators(F,G)
holds I.u = Inv u by LOPBAN13:25;
A21: dom (f `partial`1| Z) = Z by A2,NDIFF_7:def 10;
A22: dom (f `partial`2| Z) = Z by A2,NDIFF_7:def 11;
A23: for x being Point of E st x in A
holds ( g `| A )/.x = - BL/.[ ((f `partial`1| Z)*xg).x,
(I*(f `partial`2| Z)*xg).x]
proof
let x be Point of E;
assume
A24: x in A; then
A25: ( g `| A )/.x = diff (g,x) by A15,NDIFF_1:def 9;
xg/.x = xg.x by A17,A24,PARTFUN1:def 6
.= [x,g.x] by A17,A24; then
partdiff`2(f,xg/.x) is invertible by A1,A24; then
partdiff`2(f,xg/.x) in InvertibleOperators(F,G); then
A27: I. partdiff`2(f,xg/.x) = Inv partdiff`2(f,xg/.x) by A20;
[partdiff`1(f,xg/.x),(I. partdiff`2(f,xg/.x))] is set by TARSKI:1; then
[partdiff`1(f,xg/.x),(I. partdiff`2(f,xg/.x))] is Point of
[: R_NormSpace_of_BoundedLinearOperators(E,G),
R_NormSpace_of_BoundedLinearOperators(G,F) :]
by A27,PRVECT_3:18; then
[partdiff`1(f,xg/.x),(I. partdiff`2(f,xg/.x))] in the carrier of
[: R_NormSpace_of_BoundedLinearOperators(E,G),
R_NormSpace_of_BoundedLinearOperators(G,F):];
then
A28: [partdiff`1(f,xg/.x),(I. partdiff`2(f,xg/.x)) ] in dom BL
by FUNCT_2:def 1;
A29: ( Inv partdiff`2(f,xg/.x)) * partdiff`1(f,xg/.x)
= BL.( partdiff`1(f,xg/.x),(I. partdiff`2(f,xg/.x))) by A19,A27
.= BL/. [partdiff`1(f,xg/.x),(I. partdiff`2(f,xg/.x))]
by A28,PARTFUN1:def 6;
A30: g.x in rng g by A1,A24,FUNCT_1:def 3; then
reconsider y = g.x as Point of F;
reconsider z = [x,y] as Point of [:E,F:];
A33: z = xg.x & xg.x = xg/.x by A17,A24,PARTFUN1:def 6;
A34: z in [:A,B:] by A1,A24,A30,ZFMISC_1:87;
A35: ((f `partial`1| Z)*xg).x
= (f `partial`1| Z).(xg.x) by A17,A24,FUNCT_1:13
.= (f `partial`1| Z)/.(xg.x) by A1,A21,A33,A34,PARTFUN1:def 6
.= partdiff`1(f,xg/.x) by A1,A2,A33,A34,NDIFF_7:def 10;
(I*(f `partial`2| Z)*xg).x
= (I*(f `partial`2| Z)).(xg.x) by A17,A24,FUNCT_1:13
.= I. ((f `partial`2| Z).(xg.x) ) by A1,A22,A33,A34,FUNCT_1:13
.= I. ((f `partial`2| Z)/.(xg.x) ) by A1,A22,A33,A34,PARTFUN1:def 6
.= I. (partdiff`2(f,xg/.x)) by A1,A2,A33,A34,NDIFF_7:def 11;
hence thesis by A3,A24,A25,A29,A33,A35;
end;
A39: for x be Point of E st x in A
holds x in dom ((f `partial`1| Z)*xg)
& ((f `partial`1| Z)*xg) is_continuous_in x
proof
let x be Point of E;
assume
A40: x in A; then
A41: g.x in rng g by A1,FUNCT_1:def 3;
[x,g.x] is set by TARSKI:1; then
reconsider z = [x,g.x] as Point of [:E,F:] by A41,PRVECT_3:18;
A44: z in [:A,B:] by A1,A40,A41,ZFMISC_1:87;
A46: xg.x = [x,g.x] & xg.x = xg/.x by A17,A40,PARTFUN1:def 6;
hence
A47: x in dom ((f `partial`1| Z)*xg) by A1,A17,A40,A21,A44,FUNCT_1:11;
xg | A is_continuous_in x by A18,A40,NFCONT_1:def 7; then
A48: xg is_continuous_in x by A17,RELAT_1:69;
(f `partial`1| Z) | Z is_continuous_in xg/.x
by A1,A2,A44,A46,NFCONT_1:def 7; then
(f `partial`1| Z) is_continuous_in xg/.x by A21,RELAT_1:69;
hence thesis by A47,A48,NFCONT112;
end;
A49: for x be Point of E st x in A
holds x in dom (I*(f `partial`2| Z)*xg)
& I*(f `partial`2| Z)*xg is_continuous_in x
proof
let x be Point of E;
assume
A50: x in A; then
A51: g.x in rng g by A1,FUNCT_1:def 3;
[x,g.x] is set by TARSKI:1; then
reconsider z = [x,g.x] as Point of [:E,F:] by A51,PRVECT_3:18;
A54: z in [:A,B:] by A1,A50,A51,ZFMISC_1:87;
A56: xg.x = [x,g.x] & xg.x = xg/.x by A17,A50,PARTFUN1:def 6;
xg | A is_continuous_in x by A18,A50,NFCONT_1:def 7; then
A58: xg is_continuous_in x by A17,RELAT_1:69;
(f `partial`2| Z) | Z is_continuous_in xg/.x
by A1,A2,A54,A56,NFCONT_1:def 7; then
A61: (f `partial`2| Z) is_continuous_in xg/.x by A22,RELAT_1:69;
A62: partdiff`2(f,xg/.x) is invertible by A1,A50,A56; then
A63: partdiff`2(f,xg/.x) in InvertibleOperators(F,G);
A64: partdiff`2(f,xg/.x) in dom I by A20,A62;
A65: (f `partial`2| Z)/. (xg/.x)
= partdiff`2(f,xg/.x) by A1,A2,A54,A56,NDIFF_7:def 11; then
(f `partial`2| Z). (xg/.x) in dom I
by A1,A22,A54,A56,A64,PARTFUN1:def 6;
then A68: xg/.x in dom (I*(f `partial`2| Z))
by A1,A22,A54,A56,FUNCT_1:11;
hence
A70: x in dom (I*(f `partial`2| Z)*xg) by A17,A50,A56,FUNCT_1:11;
I| InvertibleOperators(F,G) is_continuous_in (f `partial`2| Z)/. (xg/.x)
by A20,A63,A65,NFCONT_1:def 7; then
I is_continuous_in (f `partial`2| Z)/. (xg/.x) by A20,RELAT_1:69; then
I*(f `partial`2| Z) is_continuous_in xg/.x by A61,A68,NFCONT112;
hence thesis by A58,A70,NFCONT112;
end;
for x be object st x in A
holds x in dom ((f `partial`1| Z)*xg) by A39; then
A72: A c= dom ((f `partial`1| Z)*xg) by TARSKI:def 3;
for x be object st x in A
holds x in dom (I*(f `partial`2| Z)*xg) by A49; then
A74: A c= dom (I*(f `partial`2| Z)*xg) by TARSKI:def 3;
A75: for x be Point of E st x in A
holds ((f `partial`1| Z)*xg) is_continuous_in x by A39;
for x be Point of E st x in A
holds (I*(f `partial`2| Z)*xg) is_continuous_in x by A49;
then consider H be PartFunc of E,R_NormSpace_of_BoundedLinearOperators(E,F)
such that
A77: dom H = A
& ( for x be Point of E st x in A
holds H.x = BL.(((f `partial`1| Z)*xg).x,(I*(f `partial`2| Z)*xg).x))
& H is_continuous_on A by A19,A72,A74,A75,LmTh47;
A78: for x0 being Point of E st x0 in A holds
BL. [ ((f `partial`1| Z)*xg).x0, (I*(f `partial`2| Z)*xg).x0]
= BL/.[ ((f `partial`1| Z)*xg).x0,(I*(f `partial`2| Z)*xg).x0]
proof
let x0 be Point of E;
assume x0 in A; then
A82: ((f `partial`1| Z)*xg).x0 in rng ((f `partial`1| Z)*xg)
& (I*(f `partial`2| Z)*xg).x0 in rng (I*(f `partial`2| Z)*xg)
by A39,A49,FUNCT_1:3;
[((f `partial`1| Z)*xg).x0,(I*(f `partial`2| Z)*xg).x0] is set
by TARSKI:1; then
[((f `partial`1| Z)*xg).x0,(I*(f `partial`2| Z)*xg).x0 ] is Point of
[: R_NormSpace_of_BoundedLinearOperators(E,G),
R_NormSpace_of_BoundedLinearOperators(G,F):]
by A82,PRVECT_3:18; then
[((f `partial`1| Z)*xg).x0,(I*(f `partial`2| Z)*xg).x0 ]
in the carrier of [: R_NormSpace_of_BoundedLinearOperators(E,G),
R_NormSpace_of_BoundedLinearOperators(G,F):]; then
[((f `partial`1| Z)*xg).x0,(I*(f `partial`2| Z)*xg).x0 ] in dom BL
by FUNCT_2:def 1;
hence BL.[((f `partial`1| Z)*xg).x0,(I*(f `partial`2| Z)*xg).x0]
= BL/.[ ((f `partial`1| Z)*xg).x0,(I*(f `partial`2| Z)*xg).x0]
by PARTFUN1:def 6;
end;
for x0 being Point of E st x0 in A holds
( g `| A ) | A is_continuous_in x0
proof
let x0 be Point of E;
assume
A83: x0 in A; then
A85: x0 in dom (( g `| A ) | A ) by A16,RELAT_1:69;
set F = ( g `| A ) | A;
for r being Real st 0 < r holds
ex s being Real
st 0 < s
& for x1 being Point of E
st x1 in dom F & ||. x1 - x0.|| < s
holds ||. F /. x1 - F /. x0 .|| < r
proof
let r be Real;
assume 0 < r;
then consider s being Real such that
A88: 0 < s
& for x1 being Point of E
st x1 in A & ||.x1 - x0.|| < s
holds ||.H/. x1 - H /. x0.|| < r by A77,A83,NFCONT_1:19;
take s;
thus 0 < s by A88;
let x1 be Point of E;
assume
A89: x1 in dom F & ||. x1 - x0.|| < s; then
A90: x1 in A by A16,RELAT_1:69; then
A91: ||.H/. x1 - H /. x0.|| < r by A88,A89;
A92: H/.x1 = H.x1 by A77,A90,PARTFUN1:def 6
.= BL. ( ((f `partial`1| Z)*xg).x1, (I*(f `partial`2| Z)*xg).x1 )
by A77,A90
.= BL/.[ ((f `partial`1| Z)*xg).x1,(I*(f `partial`2| Z)*xg).x1]
by A78,A90;
A93: F /. x1 = ( g `| A ) /.x1 by A16,RELAT_1:69
.= -H/.x1 by A23,A90,A92;
A94: H/.x0 = H.x0 by A77,A83,PARTFUN1:def 6
.= BL.(((f `partial`1| Z)*xg).x0,(I*(f `partial`2| Z)*xg).x0)
by A77,A83
.= BL/.[ ((f `partial`1| Z)*xg).x0,(I*(f `partial`2| Z)*xg).x0]
by A78,A83;
F /. x0 = ( g `| A ) /.x0 by A16,RELAT_1:69
.= -H/.x0 by A23,A83,A94; then
F /. x1 - F /. x0 = -H/.x1 + H/.x0 by A93,RLVECT_1:17
.= -( H/.x1 - H/.x0 ) by RLVECT_1:33;
hence ||. F /. x1 - F /. x0 .|| < r by A91,NORMSP_1:2;
end;
hence thesis by A85,NFCONT_1:7;
end;
hence g `| A is_continuous_on A by A16,NFCONT_1:def 7;
thus for x be Point of E, z be Point of [:E,F:]
st x in A & z = [x,g.x]
holds diff(g,x) = - ( Inv partdiff`2(f,z)) * partdiff`1(f,z) by A3;
end;
theorem
for E be RealNormSpace,
G,F be non trivial RealBanachSpace,
Z be Subset of [:E,F:],
f be PartFunc of [:E,F:], G,
a be Point of E,
b be Point of F,
c be Point of G,
z be Point of [:E,F:]
st Z is open & dom f = Z
& f is_differentiable_on Z
& f `| Z is_continuous_on Z
& [a,b] in Z & f.(a,b) = c
& z = [a,b]
& partdiff`2(f,z) is invertible
holds
ex r1,r2 be Real
st 0 < r1 & 0 < r2
& [:Ball(a,r1),cl_Ball(b,r2):] c= Z
& ( for x be Point of E st x in Ball(a,r1) holds
ex y be Point of F
st y in Ball(b,r2) & f.(x,y) = c )
& ( for x be Point of E st x in Ball(a,r1) holds
for y1,y2 be Point of F
st y1 in Ball(b,r2) & y2 in Ball(b,r2)
& f.(x,y1) =c & f.(x,y2)= c
holds y1=y2 )
& ( ex g be PartFunc of E,F
st dom g = Ball(a,r1) & rng g c= Ball(b,r2)
& g is_continuous_on Ball(a,r1)
& g.a = b
& ( for x be Point of E st x in Ball(a,r1)
holds f.(x,g.x) = c )
& g is_differentiable_on Ball(a,r1)
& g `| Ball(a,r1) is_continuous_on Ball(a,r1)
& ( for x be Point of E, z be Point of [:E,F:]
st x in Ball(a,r1) & z = [x,g.x]
holds diff(g,x) = - ( Inv partdiff`2(f,z)) * partdiff`1(f,z) )
& ( for x be Point of E, z be Point of [:E,F:]
st x in Ball(a,r1) & z =[x,g.x]
holds partdiff`2(f,z) is invertible ) )
& ( for g1,g2 be PartFunc of E,F
st dom g1 = Ball(a,r1)
& rng g1 c= Ball(b,r2)
& ( for x be Point of E st x in Ball(a,r1)
holds f.(x,g1.x) = c )
& dom g2 = Ball(a,r1)
& rng g2 c= Ball(b,r2)
& ( for x be Point of E st x in Ball(a,r1)
holds f.(x,g2.x) = c )
holds g1 = g2)
proof
let E be RealNormSpace,
G,F be non trivial RealBanachSpace,
Z0 be Subset of [:E,F:],
f0 be PartFunc of [:E,F:], G,
a be Point of E,
b be Point of F,
c be Point of G,
z be Point of [:E,F:];
assume
A1: Z0 is open & dom f0 = Z0
& f0 is_differentiable_on Z0
& f0 `| Z0 is_continuous_on Z0
& [a,b] in Z0 & f0.(a,b) = c
& z = [a,b]
& partdiff`2(f0,z) is invertible;
then A2: f0 is_partial_differentiable_on`1 Z0
& f0 is_partial_differentiable_on`2 Z0
& f0 `partial`1| Z0 is_continuous_on Z0
& f0 `partial`2| Z0 is_continuous_on Z0 by NDIFF_7:52;
set DF0 = f0 `| Z0;
set PDF2 = f0 `partial`2| Z0;
A3: dom (PDF2) = Z0 by A2,NDIFF_7:def 11;
A4: partdiff`2(f0,z) in InvertibleOperators(F,G) by A1;
A5: PDF2.z = PDF2/. z by A1,A3,PARTFUN1:def 6; then
PDF2.z = partdiff`2(f0,z) by A1,A2,NDIFF_7:def 11; then
consider p1 be Real such that
A8: 0 < p1 & Ball(PDF2/.z,p1)
c= InvertibleOperators(F,G) by A4,A5,NDIFF_8:20;
consider s1 being Real such that
A9: 0 < s1
& for z1 being Point of [:E,F:]
st z1 in Z0 & ||.z1 - z.|| < s1
holds ||.PDF2/. z1 - PDF2 /. z.|| < p1 by A1,A2,A8,NFCONT_1:19;
consider s2 be Real such that
A10: 0 < s2 & Ball(z,s2) c= Z0 by A1,NDIFF_8:20;
set s = min(s1,s2);
A11: 0 < s & s <= s1 & s <= s2 by A9,A10,XXREAL_0:17,21;
set Z = Ball(z,s);
set f = f0| Z;
A12: z in Z by A11,NDIFF_8:13;
A15: f.(a,b) = c by A1,A11,FUNCT_1:49,NDIFF_8:13;
A16: Z c= Ball(z,s2) by A11,NDIFF_8:15; then
A18: Z c= Z0 by A10,XBOOLE_1:1;
A19: dom f = Z by A1,A10,A16,RELAT_1:62,XBOOLE_1:1;
f0 is_differentiable_on Z by A1,A10,A16,XBOOLE_1:1,NDIFF_1:46; then
A20: for x being Point of [:E,F:] st x in Z holds
f0 | Z is_differentiable_in x by NDIFF_1:def 8;
A21: f|Z = f0|Z by RELAT_1:72; then
A22: f is_differentiable_on Z by A19,A20,NDIFF_1:def 8;
set DF = f `| Z;
A23: dom DF = Z by A22,NDIFF_1:def 9;
A24: for z be Point of [:E,F:] st z in Z
holds diff(f0,z) = diff(f,z)
proof
let z be Point of [:E,F:];
assume
A25: z in Z; then
f0 is_differentiable_in z by A1,A18,NDIFF_1:31;
hence diff(f0,z) = diff(f,z) by A1,A18,A25,LMDIFF;
end;
for x0 being Point of [:E,F:]
for r being Real st x0 in Z & 0 < r
holds
ex s being Real
st 0 < s
& for x1 being Point of [:E,F:]
st x1 in Z & ||. x1 - x0.|| < s
holds ||. DF /. x1 - DF /. x0 .|| < r
proof
let x0 be Point of [:E,F:];
let r be Real;
assume
A26: x0 in Z & 0 < r;
then consider s being Real such that
A28: 0 < s
& for x1 being Point of [:E,F:]
st x1 in Z0 & ||.x1 - x0.|| < s
holds ||.DF0/. x1 - DF0 /. x0.|| < r by A1,A18,NFCONT_1:19;
take s;
thus 0 < s by A28;
let x1 be Point of [:E,F:];
assume
A29: x1 in Z & ||. x1 - x0.|| < s; then
A32: DF/.x1 = diff (f,x1) by A22,NDIFF_1:def 9
.= diff (f0,x1) by A24,A29
.= DF0/.x1 by A1,A18,A29,NDIFF_1:def 9;
DF/.x0 = diff (f,x0) by A22,A26,NDIFF_1:def 9
.= diff (f0,x0) by A24,A26
.= DF0/.x0 by A1,A18,A26,NDIFF_1:def 9;
hence ||. DF /. x1 - DF /. x0 .|| < r by A18,A28,A29,A32;
end; then
A34: f `| Z is_continuous_on Z by A23,NFCONT_1:19;
A35: f is_continuous_on Z by A19,A20,A21,NDIFF_1:45,def 8;
A36: f is_partial_differentiable_on`1 Z
& f is_partial_differentiable_on`2 Z
& f `partial`1| Z is_continuous_on Z
& f `partial`2| Z is_continuous_on Z by A22,A34,NDIFF_7:52;
A37: for z be Point of [:E,F:] st z in Z
holds partdiff`1(f0,z) = partdiff`1(f,z)
& partdiff`2(f0,z) = partdiff`2(f,z)
proof
let z be Point of [:E,F:];
assume
A38: z in Z; then
f0 | Z0 is_partial_differentiable_in`1 z by A2,A18; then
f0 is_partial_differentiable_in`1 z by A1,RELAT_1:69;
hence partdiff`1(f0,z) = partdiff`1(f,z) by A1,A18,A38,LMPDIFF;
f0 | Z0 is_partial_differentiable_in`2 z by A2,A18,A38; then
f0 is_partial_differentiable_in`2 z by A1,RELAT_1:69;
hence partdiff`2(f0,z) = partdiff`2(f,z) by A1,A18,A38,LMPDIFF;
end;
then partdiff`2(f,z) in { v where v is Point of
R_NormSpace_of_BoundedLinearOperators(F,G) : v is invertible }
by A4,A12; then
A44: ex v be Point of R_NormSpace_of_BoundedLinearOperators(F,G)
st partdiff`2(f,z) = v & v is invertible; then
partdiff`2(f,z)" is Lipschitzian LinearOperator of G,F
by LOPBAN_1:def 9; then
consider r1,r2 be Real such that
A47: 0 < r1 & 0 < r2
& [:Ball(a,r1),cl_Ball(b,r2):] c= Z
& ( for x be Point of E st x in Ball(a,r1) holds
ex y be Point of F st y in Ball(b,r2) & f.(x,y) = c )
& ( for x be Point of E st x in Ball(a,r1) holds
( for y1,y2 be Point of F
st y1 in Ball(b,r2) & y2 in Ball(b,r2)
& f.(x,y1) = c & f.(x,y2) = c
holds y1=y2 ))
& ( ex g be PartFunc of E,F
st g is_continuous_on Ball(a,r1)
& dom g = Ball(a,r1)
& rng g c= Ball(b,r2)
& g.a = b
& for x be Point of E st x in Ball(a,r1)
holds f.(x,g.x) = c )
& ( for g1,g2 be PartFunc of E,F
st dom g1 = Ball(a,r1)
& rng g1 c= Ball(b,r2)
& ( for x be Point of E st x in Ball(a,r1)
holds f.(x,g1.x) = c)
& dom g2 = Ball(a,r1)
& rng g2 c= Ball(b,r2)
& ( for x be Point of E st x in Ball(a,r1)
holds f.(x,g2.x) = c)
holds g1 = g2) by A1,A11,A15,A19,A35,A36,A44,NDIFF_8:13,36;
Ball(b,r2) c= cl_Ball(b,r2) by NDIFF_8:15; then
[: Ball(a,r1), Ball(b,r2):]
c= [: Ball(a,r1), cl_Ball(b,r2):] by ZFMISC_1:95; then
A48: [: Ball(a,r1), Ball(b,r2):] c= Z by A47,XBOOLE_1:1;
A49: for x be Point of E, y be Point of F
st x in Ball(a,r1) & y in Ball(b,r2)
holds f0.(x,y) = f.(x,y)
proof
let x be Point of E, y be Point of F;
assume x in Ball(a,r1) & y in Ball(b,r2); then
[x,y] in [: Ball(a,r1), Ball(b,r2):] by ZFMISC_1:87;
hence thesis by A48,FUNCT_1:49;
end;
take r1,r2;
thus 0 < r1 & 0 < r2 by A47;
thus [:Ball(a,r1),cl_Ball(b,r2):] c= Z0 by A18,A47,XBOOLE_1:1;
thus for x be Point of E st x in Ball(a,r1)
holds ex y be Point of F
st y in Ball(b,r2) & f0.(x,y) = c
proof
let x be Point of E;
assume
A52: x in Ball(a,r1); then
consider y be Point of F such that
A53: y in Ball(b,r2) & f.(x,y) = c by A47;
take y;
thus y in Ball(b,r2) by A53;
thus f0.(x,y) = c by A49,A52,A53;
end;
thus for x be Point of E st x in Ball(a,r1)
holds for y1,y2 be Point of F
st y1 in Ball(b,r2) & y2 in Ball(b,r2)
& f0.(x,y1) = c & f0.(x,y2) = c holds y1 = y2
proof
let x be Point of E;
assume
A54: x in Ball(a,r1);
let y1,y2 be Point of F such that
A55: y1 in Ball(b,r2) & y2 in Ball(b,r2)
& f0.(x,y1) = c & f0.(x,y2) = c;
A56: f.(x,y1) = c by A49,A54,A55;
f.(x,y2) = c by A49,A54,A55;
hence y1 = y2 by A47,A54,A55,A56;
end;
consider g be PartFunc of E,F such that
A57: g is_continuous_on Ball(a,r1)
& dom g = Ball(a,r1)
& rng g c= Ball(b,r2)
& g.a = b
& for x be Point of E st x in Ball(a,r1)
holds f.(x,g.x) = c by A47;
A58: for x be Point of E,
w be Point of [:E,F:]
st x in Ball(a,r1) & w = [x,g.x]
holds partdiff`2(f0,w) is invertible
proof
let x be Point of E,
w be Point of [:E,F:];
assume
A59: x in Ball(a,r1) & w = [x,g.x]; then
g.x in rng g by A57,FUNCT_1:3; then
w in [:Ball(a,r1),Ball(b,r2):] by A57,A59,ZFMISC_1:87; then
A60: w in Z by A48;
then w in {y where y is Point of [:E,F:] : ||.y - z.|| < s}
by NDIFF_8:17; then
ex y be Point of [:E,F:] st w = y & ||.y - z.|| < s; then
||.w - z.|| < s1 by A11,XXREAL_0:2; then
||.PDF2/. w - PDF2 /. z.|| < p1 by A9,A18,A60; then
PDF2/. w in { y where y is Point of
R_NormSpace_of_BoundedLinearOperators(F,G)
: ||.y - PDF2 /. z.|| < p1}; then
PDF2/. w in Ball(PDF2/.z,p1) by NDIFF_8:17; then
PDF2/. w in InvertibleOperators(F,G) by A8; then
partdiff`2(f0,w) in InvertibleOperators(F,G)
by A2,A18,A60,NDIFF_7:def 11; then
ex v be Point of R_NormSpace_of_BoundedLinearOperators(F,G)
st partdiff`2(f0,w) = v & v is invertible;
hence partdiff`2(f0,w) is invertible;
end;
A63: for x be Point of E,
w be Point of [:E,F:]
st x in Ball(a,r1) & w = [x,g.x]
holds partdiff`2(f,w) is invertible
proof
let x be Point of E,
w be Point of [:E,F:];
assume
A64: x in Ball(a,r1) & w =[x,g.x]; then
g.x in rng g by A57,FUNCT_1:3; then
w in [:Ball(a,r1),Ball(b,r2):] by A57,A64,ZFMISC_1:87; then
partdiff`2(f,w) = partdiff`2(f0,w)
& partdiff`1(f,w) = partdiff`1(f0,w) by A37,A48;
hence thesis by A58,A64;
end;
A68: for x be Point of E st x in Ball(a,r1)
holds f0.(x,g.x) = c
proof
let x be Point of E;
assume
A69: x in Ball(a,r1); then
g.x in rng g by A57,FUNCT_1:3; then
f0.(x,g.x) = f.(x,g.x) by A49,A57,A69;
hence f0.(x,g.x) = c by A57,A69;
end;
A70: g is_differentiable_on Ball(a,r1)
& g `| Ball(a,r1) is_continuous_on Ball(a,r1)
& for x be Point of E,
z be Point of [:E,F:]
st x in Ball(a,r1) & z = [x,g.x]
holds diff(g,x) = - (Inv partdiff`2(f0,z)) * partdiff`1(f0,z)
proof
for x be Point of E, z be Point of [:E,F:]
st x in Ball(a,r1) & z =[x,g.x]
holds diff(g,x) = -( Inv partdiff`2(f0,z)) * partdiff`1(f0,z)
proof
let x be Point of E,
z be Point of [:E,F:];
assume
A73: x in Ball(a,r1) & z =[x,g.x]; then
g.x in rng g by A57,FUNCT_1:3; then
z in [:Ball(a,r1),Ball(b,r2):] by A57,A73,ZFMISC_1:87; then
partdiff`2(f,z) = partdiff`2(f0,z)
& partdiff`1(f,z) = partdiff`1(f0,z) by A37,A48;
hence thesis by A19,A22,A34,A48,A57,A63,A73,Th47;
end;
hence thesis by A19,A22,A34,A48,A57,A63,Th47;
end;
for g1,g2 be PartFunc of E,F
st dom g1 = Ball(a,r1)
& rng g1 c= Ball(b,r2)
& ( for x be Point of E st x in Ball(a,r1)
holds f0.(x,g1.x) = c )
& dom g2 = Ball(a,r1)
& rng g2 c= Ball(b,r2)
& ( for x be Point of E st x in Ball(a,r1)
holds f0.(x,g2.x) = c )
holds g1 = g2
proof
let g1,g2 be PartFunc of E,F;
assume
A75: dom g1 = Ball(a,r1)
& rng g1 c= Ball(b,r2)
& ( for x be Point of E st x in Ball(a,r1)
holds f0.(x,g1.x) = c )
& dom g2 = Ball(a,r1)
& rng g2 c= Ball(b,r2)
& ( for x be Point of E st x in Ball(a,r1)
holds f0.(x,g2.x) = c );
A76: now
let x be Point of E;
assume
A77: x in Ball(a,r1); then
g1.x in rng g1 by A75,FUNCT_1:3; then
f0.(x,g1.x) = f.(x,g1.x) by A49,A75,A77;
hence f.(x,g1.x) = c by A75,A77;
end;
now
let x be Point of E;
assume
A78: x in Ball(a,r1); then
g2.x in rng g2 by A75,FUNCT_1:3; then
f0.(x,g2.x) = f.(x,g2.x) by A49,A75,A78;
hence f.(x,g2.x) = c by A75,A78;
end;
hence g1 = g2 by A47,A75,A76;
end;
hence thesis by A57,A58,A68,A70;
end;