:: Isometric Differentiable Functions on Real Normed Space
:: by Yuichi Futa , Noboru Endou and Yasunari Shidama
::
:: Received December 31, 2013
:: Copyright (c) 2013-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,
FUNCT_4, NAT_1, FDIFF_1, SUBSET_1, SEQ_4, RELAT_1, LOPBAN_1, RCOMP_1,
TARSKI, ARYTM_3, FUNCT_7, VALUED_1, FUNCT_2, ARYTM_1, SEQ_2, ORDINAL2,
SUPINF_2, FCONT_1, STRUCT_0, CARD_1, VALUED_0, XXREAL_0, GROUP_2,
FUNCOP_1, XBOOLE_0, CARD_3, FINSEQ_1, RLVECT_1, PDIFF_1, PRVECT_1,
PRVECT_2, CFCONT_1, VECTMETR, NDIFF_7, MCART_1;
notations TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, MCART_1, RELAT_1,
FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1,
FUNCT_4, CARD_1, CARD_3, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1,
NAT_1, MEMBERED, VALUED_0, COMPLEX1, NAT_D, XXREAL_2, FINSEQ_1, FINSEQ_2,
VALUED_1, SEQ_2, RVSUM_1, RFINSEQ, SEQ_4, RCOMP_1, FCONT_1, FDIFF_1,
RFINSEQ2, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, NORMSP_0, NORMSP_1,
VFUNCT_1, MONOID_0, RLTOPSP1, EUCLID, LOPBAN_1, PRVECT_1, NFCONT_1,
NDIFF_1, MAZURULM, NDIFF_2, PRVECT_2, NFCONT_3, PRVECT_3, NDIFF_3,
FUNCT_7, NDIFF_5;
constructors REAL_1, SQUARE_1, SEQ_2, FDIFF_1, NFCONT_1, RSSPACE, VFUNCT_1,
NDIFF_1, RELSET_1, FINSEQ_7, NAT_D, RFINSEQ2, SEQ_4, FCONT_1, NFCONT_3,
NDIFF_3, FUNCT_4, NDIFF_5, PRVECT_3, NDIFF_2, MAZURULM, LOPBAN_1,
DOMAIN_1, RCOMP_1;
registrations RELSET_1, STRUCT_0, XREAL_0, MEMBERED, FUNCT_1, NDIFF_1,
FUNCT_2, NUMBERS, XBOOLE_0, PRVECT_2, FINSEQ_1, RELAT_1, LOPBAN_1,
PRVECT_3, FUNCOP_1, VALUED_1, XTUPLE_0, FUNCT_7, PRVECT_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities RLVECT_1, LOPBAN_1, FINSEQ_1, NDIFF_2, NORMSP_0, BINOP_1, PRVECT_3,
NDIFF_5;
expansions MAZURULM, TARSKI, FUNCT_2, LOPBAN_1, NDIFF_1, NDIFF_5;
theorems TARSKI, XBOOLE_0, XBOOLE_1, RLVECT_1, ZFMISC_1, RELAT_1, FUNCT_1,
VFUNCT_1, FUNCT_2, ORDINAL1, FINSEQ_1, FUNCT_4, LOPBAN_1, PARTFUN1,
PARTFUN2, NFCONT_1, NDIFF_1, FUNCOP_1, VALUED_0, VECTSP_1, XREAL_0,
BINOP_1, PRVECT_2, NDIFF_2, PRVECT_3, FUNCT_7, NDIFF_5, SUBSET_1;
schemes FUNCT_2, SEQ_1;
begin :: Preliminaries
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;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
theorem FX1:
for X be set,
I,f be Function holds
(f|X)*I = (f*I) | I"X
proof
let X be set,
I,f be Function;
P1: dom ((f|X)*I) = I"(dom (f|X)) by RELAT_1:147;
P2:I"( dom (f|X)) = I" ((dom f) /\ X) by RELAT_1:61
.= I"(dom f ) /\ I"X by FUNCT_1:68
.= dom (f*I) /\ I"X by RELAT_1:147
.= dom ((f*I) | I"X) by RELAT_1:61;
now
let x be object;
assume Q1: x in dom ((f|X)*I); then
x in I"(dom (f|X)) by RELAT_1:147; then
Q3: x in dom I & I.x in dom (f|X) by FUNCT_1:def 7;
thus ((f|X)*I ).x = (f|X).(I.x) by FUNCT_1:12,Q1
.= f.(I.x) by FUNCT_1:47,Q3
.= (f*I).x by FUNCT_1:13,Q3
.= ((f*I) | I"X).x by FUNCT_1:47,Q1,P1,P2;
end;
hence thesis by P2,FUNCT_1:2,RELAT_1:147;
end;
theorem LM001:
for S, T be RealNormSpace,
L be LinearOperator of S, T,
x, y be Point of S holds
L.x - L.y = L.(x-y)
proof
let S, T be RealNormSpace,
L be LinearOperator of S, T,
x, x0 be Point of S;
thus L.x - L.x0 = L.x+(-1)*(L.x0) by RLVECT_1:16
.= L.x+L.((-1)*x0) by LOPBAN_1:def 5
.= L.(x+((-1)*x0)) by VECTSP_1:def 20
.= L.(x-x0) by RLVECT_1:16;
end;
theorem Th26:
for X, Y, W be RealNormSpace,
I be Function of X, Y,
f1, f2 be PartFunc of Y, W holds
(f1+f2)*I = f1*I+f2*I & (f1-f2)*I = f1*I-f2*I
proof
let X, Y, W be RealNormSpace,
I be Function of X, Y,
f1, f2 be PartFunc of Y, W;
set DI = the carrier of X;
A1: dom(I) = DI by FUNCT_2:def 1;
A2: dom(f1+f2) = dom f1 /\ dom f2 by VFUNCT_1:def 1;
A3b: for s be Element of DI holds s in dom((f1+f2)*I)
iff s in dom(f1*I+f2*I)
proof
let s be Element of DI;
s in dom((f1+f2)*I) iff I.s in dom f1 /\ dom f2 by A2,A1,FUNCT_1:11;
then s in dom((f1+f2)*I)
iff I.s in dom f1 & I.s in dom f2 by XBOOLE_0:def 4;
then s in dom((f1+f2)*I)
iff s in dom(f1*I) & s in dom(f2*I) by A1,FUNCT_1:11;
then s in dom((f1+f2)*I)
iff s in dom(f1*I) /\ dom(f2*I) by XBOOLE_0:def 4;
hence thesis by VFUNCT_1:def 1;
end; then
A3: for s be object holds s in dom((f1+f2)*I)
iff s in dom(f1*I + f2*I); then
A3a: dom((f1+f2)*I) = dom(f1*I+f2*I) by TARSKI:2;
A4: for z being Element of DI st z in dom((f1+f2)*I) holds
((f1+f2)*I).z = (f1*I+f2*I).z
proof
let z be Element of DI;
assume A5: z in dom((f1+f2)*I); then
A6: I.z in dom(f1+f2) by FUNCT_1:11;
z in dom(f1*I) /\ dom(f2*I) by A3a,A5,VFUNCT_1:def 1; then
A7: z in dom(f1*I) & z in dom(f2*I) by XBOOLE_0:def 4;
A8: I.z in dom f1 /\ dom f2 by A2,A5,FUNCT_1:11;
then I.z in dom f1 by XBOOLE_0:def 4; then
A9: f1/.(I.z) = f1.(I.z) by PARTFUN1:def 6
.= (f1*I).z by A7,FUNCT_1:12
.= (f1*I)/.z by A7,PARTFUN1:def 6;
I.z in dom f2 by A8,XBOOLE_0:def 4; then
A10: f2/.(I.z) = f2.(I.z) by PARTFUN1:def 6
.= (f2*I).z by A7,FUNCT_1:12
.= (f2*I)/.z by A7,PARTFUN1:def 6;
((f1+f2)*I).z = (f1+f2).(I.z) by A5,FUNCT_1:12
.= (f1+f2)/.(I.z) by A6,PARTFUN1:def 6
.= f1/.(I.z) +f2/.(I.z) by A6,VFUNCT_1:def 1
.= (f1*I+ f2*I)/.z by A3b,A5,A9,A10,VFUNCT_1:def 1;
hence thesis by A3b,A5,PARTFUN1:def 6;
end;
A11: dom(f1-f2) = dom f1 /\ dom f2 by VFUNCT_1:def 2;
A12b: for s be Element of DI holds s in dom((f1-f2)*I)
iff s in dom(f1*I-f2*I)
proof
let s be Element of DI;
s in dom((f1-f2)*I) iff I.s in dom f1 /\ dom f2 by A11,A1,FUNCT_1:11;
then s in dom((f1-f2)*I)
iff I.s in dom f1 & I.s in dom f2 by XBOOLE_0:def 4;
then s in dom((f1-f2)*I)
iff s in dom(f1*I) & s in dom(f2*I) by A1,FUNCT_1:11;
then s in dom((f1-f2)*I)
iff s in dom(f1*I) /\ dom(f2*I) by XBOOLE_0:def 4;
hence thesis by VFUNCT_1:def 2;
end;
then
A12: for s be object holds s in dom((f1-f2)*I)
iff s in dom(f1*I - f2*I); then
A12a: dom((f1-f2)*I) = dom(f1*I-f2*I) by TARSKI:2;
for z being Element of DI st z in dom((f1-f2)*I) holds
((f1-f2)*I).z = (f1*I-f2*I).z
proof
let z be Element of DI;
assume A13: z in dom((f1-f2)*I); then
A14: I.z in dom (f1-f2) by FUNCT_1:11;
z in dom(f1*I) /\ dom(f2*I) by A12a,A13,VFUNCT_1:def 2; then
A15: z in dom(f1*I) & z in dom(f2*I) by XBOOLE_0:def 4;
A16: I.z in dom f1 /\ dom f2 by A11,A13,FUNCT_1:11; then
I.z in dom f1 by XBOOLE_0:def 4; then
A17:f1/.(I.z) = f1.(I.z) by PARTFUN1:def 6
.= (f1*I).z by A15,FUNCT_1:12
.= (f1*I)/.z by A15,PARTFUN1:def 6;
I.z in dom f2 by A16,XBOOLE_0:def 4; then
A18: f2/.(I.z) = f2.(I.z) by PARTFUN1:def 6
.= (f2*I).z by A15,FUNCT_1:12
.= (f2*I)/.z by A15,PARTFUN1:def 6;
thus ((f1-f2)*I).z =(f1-f2).(I.z) by A13,FUNCT_1:12
.= (f1-f2)/.(I.z) by A14,PARTFUN1:def 6
.= f1/.(I.z) - f2/.(I.z) by A14,VFUNCT_1:def 2
.= (f1*I- f2*I)/.z by A12b,A13,A17,A18,VFUNCT_1:def 2
.= (f1*I- f2*I).z by A12b,A13,PARTFUN1:def 6;
end;
hence thesis by A3,A12,A4,TARSKI:2,PARTFUN1:5;
end;
theorem Th27:
for X, Y, W be RealNormSpace,
I be Function of X, Y,
f be PartFunc of Y, W,
r be Real holds
r(#)(f*I) = (r(#)f)*I
proof
let X, Y, W be RealNormSpace,
I be Function of X, Y,
f be PartFunc of Y, W,
r be Real;
set DI = the carrier of X;
A1: dom(r(#)f) = dom f by VFUNCT_1:def 4;
A2: dom(r(#)(f*I)) = dom(f*I) by VFUNCT_1:def 4;
A3: dom(I) = DI by FUNCT_2:def 1;
A4b: for s be Element of DI holds s in dom((r(#)f)*I) iff s in dom(f*I)
proof
let s be Element of DI;
s in dom((r(#)f)*I) iff I.s in dom(r(#)f) by A3,FUNCT_1:11;
hence thesis by A1,A3,FUNCT_1:11;
end; then
A4: for s be object holds s in dom(r(#)(f*I))
iff s in dom((r(#)f)*I) by A2; then
A4a: dom(r(#)(f*I)) = dom((r(#)f)*I) by TARSKI:2;
A5: for s be Element of DI holds s in dom((r(#)f)*I) iff I.s in dom(r(#)f)
proof
let s be Element of DI;
dom(I)= DI by FUNCT_2:def 1;
hence thesis by FUNCT_1:11;
end;
for z being Element of DI st z in dom(r(#)(f*I)) holds
(r(#)(f*I)).z = ((r(#)f)*I).z
proof
let z be Element of DI;
assume A6: z in dom(r(#)(f*I)); then
A7: z in dom(f*I) by VFUNCT_1:def 4;
A9: f/.(I.z) = f.(I.z) by A1,A5,A4a,A6,PARTFUN1:def 6
.= (f*I).z by A7,FUNCT_1:12
.= (f*I)/.z by A7,PARTFUN1:def 6;
A10: (r(#)(f*I)).z =(r(#)(f*I))/.z by A6,PARTFUN1:def 6
.= r * f/.(I.z) by A6,A9,VFUNCT_1:def 4;
((r(#)f)*I).z = (r(#)f).(I.z) by A2,A4b,A6,FUNCT_1:12
.= (r(#)f)/.(I.z) by A5,A4a,A6,PARTFUN1:def 6
.= r * f/.(I.z) by A5,A4a,A6,VFUNCT_1:def 4;
hence thesis by A10;
end;
hence thesis by A4,TARSKI:2,PARTFUN1:5;
end;
theorem LM030:
for f be PartFunc of T, W,
g be Function of S, T,
x be Point of S
st x in dom g &
g/.x in dom f &
g is_continuous_in x &
f is_continuous_in g/.x holds
f*g is_continuous_in x
proof
let f be PartFunc of T, W,
g be Function of S, T,
x be Point of S;
assume that
AS1: x in dom g and
AS2: g/.x in dom f and
AS3: g is_continuous_in x and
AS4: f is_continuous_in g/.x;
set h = f*g;
P1: x in dom h by AS1,AS2,PARTFUN2:3;
for r be Real st 0<r ex s be Real st
0 < s & for x1 be Point of S st x1 in dom h & ||. x1- x .|| < s
holds ||. h/.x1-h/.x.|| < r
proof
let r be Real;
assume 0 < r;
then consider t be Real such that
P2: 0 < t &
for y1 be Point of T
st y1 in dom f & ||. y1- (g/.x) .|| < t
holds ||. f/.y1-f/.(g/.x).|| < r by AS4,NFCONT_1:7;
consider s be Real such that
P3: 0 < s &
for x1 be Point of S st x1 in dom g & ||. x1- x .|| < s holds
||. g/.x1- g/.x .|| < t by P2,AS3,NFCONT_1:7;
take s;
thus 0 < s by P3;
let x1 be Point of S;
assume P4: x1 in dom h & ||. x1- x .|| < s; then
P7: x1 in dom g & g/.x1 in dom f by PARTFUN2:3; then
P5: ||. g/.x1- (g/.x) .|| < t by P3,P4;
h/.x1 = f/.(g/.x1) & h/.x = f/.(g/.x)
by P4,AS1,AS2,PARTFUN2:3,PARTFUN2:4;
hence ||. h/.x1-h/.x.||< r by P2,P5,P7;
end;
hence h is_continuous_in x by NFCONT_1:7,P1;
end;
definition
let X, Y be RealNormSpace;
let x be Element of [:X,Y:];
func reproj1(x) -> Function of X,[:X,Y:] means :Defrep1:
for r being Element of X holds it . r = [r,x`2];
existence
proof
reconsider x1 = x as Element of [:the carrier of X,the carrier of Y:];
defpred S1[ Element of X, Element of the carrier of [:X,Y:] ]
means $2 = [$1,x1`2];
A1: for r being Element of X
ex y being Element of the carrier of [:X,Y:] st S1[r,y]
proof
let r be Element of X;
consider p1 be Point of X, p2 be Point of Y such that
X1: x=[p1,p2] by PRVECT_3:18;
[r,x1`2] in [:the carrier of X,the carrier of Y:] by X1,ZFMISC_1:def 2;
hence ex y being Element of the carrier of [:X,Y:] st S1[r,y];
end;
ex f being Function of the carrier of X, the carrier of [:X,Y:] st
for r being Element of X holds S1[r,f . r] from FUNCT_2:sch 3(A1);
hence ex b1 being Function of X,[:X,Y:] st
for r being Element of X holds b1 . r = [r,x`2];
end;
uniqueness
proof
let f, g be Function of the carrier of X, the carrier of [:X,Y:];
assume that
A2: for r being Element of X holds f . r = [r,x`2] and
A3: for r being Element of X holds g . r = [r,x`2];
now let r be Element of X;
f . r = [r,x`2] by A2;
hence f . r = g . r by A3;
end;
hence f = g;
end;
func reproj2(x) -> Function of Y,[:X,Y:] means :Defrep2:
for r being Element of Y holds it . r = [x`1,r];
existence
proof
reconsider x1 = x as Element of [:the carrier of X,the carrier of Y:];
defpred S1[ Element of Y, Element of the carrier of [:X,Y:] ]
means $2 = [x1`1,$1];
A1: for r being Element of Y
ex y being Element of the carrier of [:X,Y:] st S1[r,y]
proof
let r be Element of Y;
consider p1 be Point of X, p2 be Point of Y such that
X1: x=[p1,p2] by PRVECT_3:18;
[x1`1,r] in [:the carrier of X,the carrier of Y:] by X1,ZFMISC_1:def 2;
hence ex y being Element of the carrier of [:X,Y:] st S1[r,y];
end;
ex f being Function of the carrier of Y, the carrier of [:X,Y:] st
for r being Element of Y holds S1[r,f . r] from FUNCT_2:sch 3(A1);
hence ex b1 being Function of Y,[:X,Y:] st
for r being Element of Y holds b1 . r = [x`1,r];
end;
uniqueness
proof
let f, g be Function of the carrier of Y, the carrier of [:X,Y:];
assume that
A2: for r being Element of Y holds f . r = [x`1,r] and
A3: for r being Element of Y holds g . r = [x`1,r];
now let r be Element of Y;
f . r = [x`1,r] by A2;
hence f . r = g . r by A3;
end;
hence f = g;
end;
end;
begin :: Isometries
theorem LM010:
for I be LinearOperator of S,T,
x be Point of S st I is isometric holds
I is_continuous_in x
proof
let I be LinearOperator of S, T,
x0 be Point of S;
assume AS1: I is isometric;
P1: dom I = the carrier of S by FUNCT_2:def 1;
for r be Real st 0<r ex s be Real st
0 < s & for x1 be Point of S st x1 in dom I & ||. x1- x0 .|| < s
holds ||. I/.x1-I/.x0 .|| < r
proof
let r be Real;
assume P2: 0 < r;
take s = r;
thus 0 < s by P2;
let x1 be Point of S;
assume P3: x1 in dom I & ||. x1- x0 .|| < s;
thus thesis by AS1,P3;
end;
hence thesis by NFCONT_1:7,P1;
end;
theorem LMMAZU:
for S, T be RealNormSpace,
f be LinearOperator of S, T holds
f is isometric
iff
for x being Element of S holds ||. f.x .|| = ||. x .||
proof
let S, T be RealNormSpace,
f be LinearOperator of S, T;
hereby assume
A1: f is isometric;
thus for x being Element of S holds ||. f.x .|| = ||. x .||
proof
let x be Element of S;
thus ||. f.x .|| = ||. f.(x -0.S) .|| by RLVECT_1:13
.= ||. f.x - f. (0.S) .|| by LM001
.= ||. x -0.S .|| by A1
.= ||. x .|| by RLVECT_1:13;
end;
end;
assume A2: for x being Element of S holds ||. f.x .|| = ||. x .||;
for a,b being Point of S holds ||. f.a - f.b .|| = ||. a - b .||
proof
let a,b be Point of S;
thus ||. f.a - f.b .|| = ||. f.(a -b) .|| by LM001
.= ||. a - b .|| by A2;
end;
hence thesis;
end;
theorem LM015:
for I be LinearOperator of S,T,
Z be Subset of S
st I is isometric holds
I is_continuous_on Z
proof
let I be LinearOperator of S,T,
Z be Subset of S;
assume AS: I is isometric;
P1: dom I = the carrier of S by FUNCT_2:def 1;
for x be Point of S st x in dom I holds
I| (dom I) is_continuous_in x by AS,LM010;
hence thesis by P1,NFCONT_1:23,NFCONT_1:def 7;
end;
theorem LM020:
for I be LinearOperator of S, T
st I is one-to-one onto isometric
holds ex J be LinearOperator of T, S
st J = I" & J is one-to-one onto isometric
proof
let I be LinearOperator of S, T;
assume that
AS0: I is one-to-one onto and
AS1: I is isometric;
P0: rng I = the carrier of T & dom I = the carrier of S
by AS0,FUNCT_2:def 1;
P1: rng I = dom(I") & dom I = rng(I") by AS0,FUNCT_1:33; then
reconsider J = I" as Function of T,S by P0,FUNCT_2:1;
X1: for v, w be Point of T holds J.(v+w) = J.v + J.w
proof
let v, w be Point of T;
consider t be Point of S such that
X1: v = I.t by AS0,FUNCT_2:113;
consider s be Point of S such that
X2: w = I.s by AS0,FUNCT_2:113;
X3: J.(v+w) = J.(I.(t+s)) by X1,X2,VECTSP_1:def 20
.= t+s by FUNCT_1:34,AS0,P0;
J.w = s by X2,FUNCT_1:34,AS0,P0;
hence thesis by AS0,P0,X1,X3,FUNCT_1:34;
end;
X2: for v be Point of T, r be Real holds J.(r*v) = r*(J.v)
proof
let v be Point of T,r be Real;
consider t be Point of S such that
X1: v = I.t by AS0,FUNCT_2:113;
J.(r*v) = J.(I.(r*t)) by X1,LOPBAN_1:def 5
.= r*t by FUNCT_1:34,AS0,P0;
hence thesis by AS0,P0,X1,FUNCT_1:34;
end;
reconsider J as LinearOperator of T,S
by X1,X2,LOPBAN_1:def 5,VECTSP_1:def 20;
take J;
thus J = I";
thus J is one-to-one onto by AS0,P1,FUNCT_2:def 1;
for v be Point of T holds ||. J.v .|| = ||.v.||
proof
let v be Point of T;
consider t be Point of S such that
X1: v = I.t by AS0,FUNCT_2:113;
thus ||. J.v .|| = ||. t .|| by X1,FUNCT_1:34,AS0,P0
.= ||. v .|| by X1,AS1,LMMAZU;
end;
hence thesis by LMMAZU;
end;
theorem LM021:
for I be LinearOperator of S, T,
s1 being sequence of S
st I is isometric &
s1 is convergent holds
I*s1 is convergent &
lim (I*s1) = I.lim s1
proof
let I be LinearOperator of S, T, s1 be sequence of S;
assume AS: I is isometric & s1 is convergent;
P1: dom I = the carrier of S by FUNCT_2:def 1;
P22: rng s1 c= dom I by P1;
I is_continuous_in lim s1 by AS,LM010; then
I/*s1 is convergent & I/.lim s1 = lim (I/*s1) by NFCONT_1:def 5,AS,P22;
hence thesis by P22,FUNCT_2:def 11;
end;
theorem LM022:
for I be LinearOperator of S, T,
s1 being sequence of S
st I is one-to-one onto isometric holds
( s1 is convergent iff I*s1 is convergent )
proof
let I be LinearOperator of S, T,
s1 being sequence of S;
assume AS: I is one-to-one onto isometric;
consider J be LinearOperator of T, S such that
P2: J = I" & J is one-to-one onto isometric by AS,LM020;
thus s1 is convergent implies I*s1 is convergent by LM021,AS;
assume P4: I*s1 is convergent;
P6: rng s1 c= the carrier of S;
J*(I*s1) = (J*I)*s1 by RELAT_1:36
.= (id (the carrier of S))*s1 by AS,P2,FUNCT_2:29
.= s1 by RELAT_1:53,P6;
hence s1 is convergent by P2,P4,LM021;
end;
LM023:
for I be LinearOperator of S, T,
Z be Subset of S st I is one-to-one onto isometric &
Z is closed holds I.:Z is closed
proof
let I be LinearOperator of S, T,
Z be Subset of S;
assume that
A1: I is one-to-one onto and
A2: I is isometric and
A3: Z is closed;
P1: dom I = the carrier of S by FUNCT_2:def 1;
consider J be LinearOperator of T, S such that
P2: J = I" & J is one-to-one onto & J is isometric by A1,A2,LM020;
now
let t1 be sequence of T;
assume
A4: rng t1 c= I.:Z &
t1 is convergent; then
A5: J*t1 is convergent by P2,LM022;
A6: rng (J*t1) = J.: rng t1 by RELAT_1:127;
J.: (I.:Z) = I"(I.:Z) by A1,P2,FUNCT_1:85
.= Z by FUNCT_1:94,P1,A1;
then lim (J*t1) in Z by A3,A4,A5,A6,NFCONT_1:def 3,RELAT_1:123;
then J.(lim t1 ) in Z by A4,P2,LM021;
then I.(J.(lim t1 )) in I.: Z by FUNCT_2:35;
hence lim t1 in I.: Z by A1,P2,FUNCT_1:35;
end;
hence I.:Z is closed by NFCONT_1:def 3;
end;
theorem LM024:
for I be LinearOperator of S, T,
Z be Subset of S
st I is one-to-one onto isometric holds
(Z is closed iff I.:Z is closed)
proof
let I be LinearOperator of S, T,
Z be Subset of S;
assume that
A1: I is one-to-one onto and
A2: I is isometric;
P1: dom I = the carrier of S by FUNCT_2:def 1;
consider J be LinearOperator of T, S such that
P2: J = I" & J is one-to-one onto isometric by A1,A2,LM020;
thus Z is closed iff I.:Z is closed
proof
thus Z is closed implies I.:Z is closed by A1,A2,LM023;
assume P3: I.:Z is closed;
J.: (I.:Z) = I"(I.:Z) by A1,P2,FUNCT_1:85
.= Z by FUNCT_1:94,P1,A1;
hence Z is closed by P2,P3,LM023;
end;
end;
theorem LM025:
for I be LinearOperator of S, T,
Z be Subset of S
st I is one-to-one onto isometric holds
(Z is open iff I.:Z is open)
proof
let I be LinearOperator of S, T,
Z be Subset of S;
assume that
A1: I is one-to-one onto and
A2: I is isometric;
consider J be LinearOperator of T, S such that
P2: J = I" & J is one-to-one onto isometric by A1,A2,LM020;
Q2: I = J" by P2,A1,FUNCT_1:43;
Q3: J"Z = (J").:Z by P2,FUNCT_1:85
.= I.:Z by A1,P2,FUNCT_1:43;
A3: I.:(Z`) = J"(Z`) by Q2,P2,FUNCT_1:85
.= (I.:Z)` by Q3,FUNCT_2:100;
thus Z is open iff I.:Z is open
proof
hereby
assume Z is open;
then Z` is closed by NFCONT_1:def 4;
then (I.:Z)` is closed by A1,A2,A3,LM024;
hence I.:Z is open by NFCONT_1:def 4;
end;
assume I.:Z is open;
then I.:(Z`) is closed by A3,NFCONT_1:def 4;
then Z` is closed by A1,A2,LM024;
hence Z is open by NFCONT_1:def 4;
end;
end;
LM026:
for I be LinearOperator of S, T,
Z being Subset of S
st I is isometric &
Z is compact holds
I.:Z is compact
proof
let I be LinearOperator of S, T,
Z be Subset of S;
assume
AS: I is isometric & Z is compact;
dom I = the carrier of S by FUNCT_2:def 1;
hence I.:Z is compact by AS,LM015,NFCONT_1:32;
end;
theorem
for I be LinearOperator of S, T,
Z be Subset of S
st I is one-to-one onto isometric holds
(Z is compact iff I.:Z is compact)
proof
let I be LinearOperator of S, T,
Z be Subset of S;
assume that
A1: I is one-to-one onto and
A2: I is isometric;
consider J be LinearOperator of T, S such that
P2: J = I" & J is one-to-one onto isometric by A1,A2,LM020;
P1: dom I = the carrier of S by FUNCT_2:def 1;
thus Z is compact implies I.:Z is compact by LM026,A2;
thus I.:Z is compact implies Z is compact
proof
assume X2: I.:Z is compact;
J.:(I.:Z) = I"(I.:Z) by A1,P2,FUNCT_1:85
.= Z by FUNCT_1:94,P1,A1;
hence Z is compact by P2,X2,LM026;
end;
end;
theorem LM040:
for f be PartFunc of T, W,
I be LinearOperator of S, T
st I is one-to-one onto isometric holds
for x be Point of S st I.x in dom f
holds f*I is_continuous_in x iff f is_continuous_in I.x
proof
let f be PartFunc of T, W,
I be LinearOperator of S, T;
assume that
AS2: I is one-to-one onto and
AS3: I is isometric;
set g = f*I;
let x be Point of S;
assume
AS6: I.x in dom f;
P0: dom I = the carrier of S by FUNCT_2:def 1;
hereby
assume P1: g is_continuous_in x;
consider J be LinearOperator of T, S such that
P2: J = I" & J is one-to-one onto isometric by LM020,AS2,AS3;
Q4: J is_continuous_in I.x by LM010,P2;
P3: J.(I.x) = x by AS2,P2,P0,FUNCT_1:34;
Q0: dom J = the carrier of T by FUNCT_2:def 1;
Q1: J.(I.x) in dom g by P1,P3,NFCONT_1:7;
Q3: g*J = f*(I*I") by P2,RELAT_1:36
.= f*id (the carrier of T) by AS2,FUNCT_2:29
.= f by FUNCT_2:17;
J.(I.x) = J/.(I.x) & I.x = I/.x;
hence f is_continuous_in I.x by Q3,LM030,P3,P1,Q0,Q1,Q4;
end;
assume
P2: f is_continuous_in I.x;
I.x = I/.x;
hence g is_continuous_in x by P0,AS3,AS6,P2,LM010,LM030;
end;
theorem LM045:
for f be PartFunc of T, W,
I be LinearOperator of S, T,
X be set st X c= the carrier of T &
I is one-to-one onto isometric holds
f is_continuous_on X
iff
f*I is_continuous_on I"X
proof
let f be PartFunc of T, W,
I be LinearOperator of S, T,
X be set;
assume that
AS1: X c= the carrier of T and
AS2: I is one-to-one onto and
AS3: I is isometric;
hereby
assume P2: f is_continuous_on X; then
I"X c= I"(dom f) by NFCONT_1:def 7,RELAT_1:143; then
P3: I"X c= dom (f*I) by RELAT_1:147;
for x be Point of S st x in I"X
holds (f*I) | I"X is_continuous_in x
proof
let x be Point of S;
assume x in I"X; then
P5: x in dom I & I.x in X by FUNCT_1:def 7; then
P6: f|X is_continuous_in (I.x) by P2,NFCONT_1:def 7;
X c= dom f &
for y be Point of T st y in X holds f|X is_continuous_in y
by P2,NFCONT_1:def 7;
then I.x in (dom f) /\ X by P5,XBOOLE_0:def 4;
then I.x in dom (f|X) by RELAT_1:61;
then (f|X)*I is_continuous_in x by AS2,AS3,P6,LM040;
hence (f*I) | I"X is_continuous_in x by FX1;
end;
hence (f*I) is_continuous_on I"X by P3,NFCONT_1:def 7;
end;
assume P2: (f*I) is_continuous_on I"X;
then
I"X c= dom (f*I) &
for x be Point of S st x in I"X holds
(f*I) | I"X is_continuous_in x by NFCONT_1:def 7;
then K1: I"X c= I"(dom f) by RELAT_1:147;
P3: X c= dom f by AS1,AS2,FUNCT_1:88,K1;
for y be Point of T st y in X holds f|X is_continuous_in y
proof
let y be Point of T;
assume P4: y in X;
consider x be Point of S such that
P5: y = I.x by AS2,FUNCT_2:113;
dom I = the carrier of S by FUNCT_2:def 1;
then x in I"X by P4,P5,FUNCT_1:def 7;
then (f*I) | I"X is_continuous_in x by P2,NFCONT_1:def 7;
then P7: (f|X)*I is_continuous_in x by FX1;
I.x in dom (f|X) by P3,P4,P5,RELAT_1:57;
hence f|X is_continuous_in y by AS2,AS3,P5,P7,LM040;
end;
hence f is_continuous_on X by AS1,AS2,K1,FUNCT_1:88,NFCONT_1:def 7;
end;
definition
let X, Y be RealNormSpace;
func IsoCPNrSP(X,Y) -> LinearOperator of [:X,Y:],product <*X,Y*> means
:defISO:
for x be Point of X, y be Point of Y holds it.(x,y) = <*x,y*>;
existence
proof
consider I be Function of [:X,Y:], product <*X,Y*> such that
I is one-to-one onto and
A2: for x be Point of X, y be Point of Y holds I.(x,y) = <*x,y*> and
A3: for v,w be Point of [:X,Y:] holds I.(v+w) = I.v + I.w and
A4: for v be Point of [:X,Y:], r be Real holds I.(r*v) = r*(I.v) and
0. product <*X,Y*> = I.(0.[:X,Y:]) and
for v be Point of [:X,Y:] holds ||. I.v .|| = ||.v.|| by PRVECT_3:15;
reconsider I as LinearOperator of [:X,Y:], product <*X,Y*>
by A3,A4,VECTSP_1:def 20,LOPBAN_1:def 5;
take I;
thus thesis by A2;
end;
uniqueness
proof
let I1, I2 be LinearOperator of [:X,Y:],product <*X,Y*>;
assume that
A1: for x be Point of X, y be Point of Y holds I1.(x,y) = <*x,y*> and
A2: for x be Point of X, y be Point of Y holds I2.(x,y) = <*x,y*>;
for x,y be set st x in the carrier of X & y in the carrier of Y
holds I1.(x,y) = I2.(x,y)
proof
let x,y be set;
assume P2: x in the carrier of X & y in the carrier of Y;
then reconsider x1 = x as Point of X;
reconsider y1 = y as Point of Y by P2;
thus I1.(x,y) = <*x1,y1*> by A1
.= I2.(x,y) by A2;
end;
hence I1 = I2 by BINOP_1:def 21;
end;
end;
theorem ZeZe:
for X, Y be RealNormSpace holds
0.product <*X,Y*> = IsoCPNrSP(X,Y).(0.[:X,Y:])
proof
let X, Y be RealNormSpace;
consider I be Function of [:X,Y:], product <*X,Y*> such that
I is one-to-one onto and
A2: for x be Point of X, y be Point of Y holds I.(x,y) = <*x,y*> and
A3: for v,w be Point of [:X,Y:] holds I.(v+w) = I.v + I.w and
A4: for v be Point of [:X,Y:], r be Real holds I.(r*v) = r*(I.v) and
A5: 0. product <*X,Y*> = I.(0.[:X,Y:]) and
for v be Point of [:X,Y:] holds ||. I.v .|| = ||.v.|| by PRVECT_3:15;
reconsider I as LinearOperator of [:X,Y:], product <*X,Y*>
by A3,A4,VECTSP_1:def 20,LOPBAN_1:def 5;
for a being Element of X,
b being Element of Y holds I.(a,b) = IsoCPNrSP(X,Y).(a,b)
by defISO,A2;
hence thesis by A5,BINOP_1:2;
end;
registration
let X, Y be RealNormSpace;
cluster IsoCPNrSP(X,Y) -> one-to-one onto isometric;
correctness
proof
consider I be Function of [:X,Y:], product <*X,Y*> such that
A1: I is one-to-one onto and
A2: for x be Point of X, y be Point of Y holds I.(x,y) = <*x,y*> and
A3: for v,w be Point of [:X,Y:] holds I.(v+w) = I.v + I.w and
A4: for v be Point of [:X,Y:], r be Real holds I.(r*v) = r*(I.v) and
0. product <*X,Y*> = I.(0.[:X,Y:]) and
A6: for v be Point of [:X,Y:] holds ||. I.v .|| = ||.v.|| by PRVECT_3:15;
reconsider I as LinearOperator of [:X,Y:], product <*X,Y*>
by A3,A4,VECTSP_1:def 20,LOPBAN_1:def 5;
for a being Element of X,
b being Element of Y holds
I.(a,b) = IsoCPNrSP(X,Y).(a,b) by defISO,A2;
then I = IsoCPNrSP(X,Y) by BINOP_1:2;
hence thesis by A1,A6,LMMAZU;
end;
end;
registration
let X, Y be RealNormSpace;
cluster one-to-one onto isometric for
LinearOperator of [:X,Y:],product <*X,Y*>;
correctness
proof
take IsoCPNrSP(X,Y);
thus thesis;
end;
end;
definition
let X, Y be RealNormSpace;
let f be one-to-one onto isometric
LinearOperator of [:X,Y:],product <*X,Y*>;
redefine func f" -> LinearOperator of product <*X,Y*>,[:X,Y:]; :: redefines " (FUNCT_1, definition)
correctness
proof
consider J be LinearOperator of product <*X,Y*>,[:X,Y:] such that
P3: J = f" and
J is one-to-one onto isometric by LM020;
thus thesis by P3;
end;
end;
registration
let X, Y be RealNormSpace;
let f be one-to-one onto isometric
LinearOperator of [:X,Y:],product <*X,Y*>;
cluster f" -> one-to-one onto isometric
for LinearOperator of product <*X,Y*>,[:X,Y:];
correctness
proof
consider J be LinearOperator of product <*X,Y*>,[:X,Y:] such that
P3: J = f" and
P4: J is one-to-one onto and
P5: J is isometric by LM020;
thus thesis by P3,P4,P5;
end;
end;
registration
let X, Y be RealNormSpace;
cluster one-to-one onto isometric
for LinearOperator of product <*X,Y*>,[:X,Y:];
correctness
proof
set J = IsoCPNrSP(X,Y)";
take J;
thus thesis;
end;
end;
theorem defISOA1:
for X, Y be RealNormSpace,
x be Point of X, y be Point of Y holds
(IsoCPNrSP(X,Y)").<*x,y*> = [x,y]
proof
let X, Y be RealNormSpace;
set I = IsoCPNrSP(X,Y);
set J = I";
P0: dom I = the carrier of [:X,Y:] by FUNCT_2:def 1;
for x be Point of X, y be Point of Y holds J.<*x,y*> = [x,y]
proof
let x be Point of X, y be Point of Y;
Q1: I.(x,y) = <*x,y*> by defISO;
reconsider z = [x,y] as Point of [:X,Y:];
J.(I.z) = z by P0,FUNCT_1:34;
hence thesis by Q1;
end;
hence thesis;
end;
theorem defISOA2:
for X, Y be RealNormSpace holds
(IsoCPNrSP(X,Y)").(0. product <*X,Y*>) = 0.[:X,Y:]
proof
let X, Y be RealNormSpace;
set I = IsoCPNrSP(X,Y);
set J = I";
P0: dom I = the carrier of [:X,Y:] by FUNCT_2:def 1;
J.(0. product <*X,Y*>) = J.(I.(0.[:X,Y:])) by ZeZe;
hence thesis by P0,FUNCT_1:34;
end;
theorem
for X, Y be RealNormSpace,
Z be Subset of [:X,Y:] holds
IsoCPNrSP(X,Y) is_continuous_on Z by LM015;
theorem
for X, Y be RealNormSpace,
Z be Subset of product <*X,Y*> holds
IsoCPNrSP(X,Y)" is_continuous_on Z by LM015;
theorem LMX00:
for S, T, W be RealNormSpace,
f be Point of R_NormSpace_of_BoundedLinearOperators(S,W),
g be Point of R_NormSpace_of_BoundedLinearOperators(T,W),
I be LinearOperator of S, T
st I is one-to-one onto isometric & f = g*I
holds ||.f.|| = ||.g.||
proof
let S, T, W be RealNormSpace,
f be Point of R_NormSpace_of_BoundedLinearOperators(S,W),
g be Point of R_NormSpace_of_BoundedLinearOperators(T,W),
I be LinearOperator of S, T;
assume
AS: I is one-to-one onto isometric & f = g*I;
P1: dom I = the carrier of S by FUNCT_2:def 1;
consider J be LinearOperator of T, S such that
P2: J = I" & J is one-to-one onto isometric by AS,LM020;
reconsider f0 = f as Lipschitzian LinearOperator of S, W
by LOPBAN_1:def 9;
reconsider g0 = g as Lipschitzian LinearOperator of T, W
by LOPBAN_1:def 9;
reconsider gI = g*I as Lipschitzian LinearOperator of S, W
by LOPBAN_1:def 9,AS;
Y1: for x be object holds
x in {||.g0.t.|| where t is VECTOR of T : ||.t.|| <= 1 } iff
x in {||.gI.w.|| where w is VECTOR of S : ||.w.|| <= 1 }
proof
let x be object;
hereby
assume x in {||.g0.t.|| where t is VECTOR of T : ||.t.|| <= 1 };
then consider t be VECTOR of T such that
B1: x = ||.g0.t.|| & ||.t.|| <= 1;
set s = J.t;
B2: gI.s = g0.(I.(J.t)) by P1,FUNCT_1:13
.= g0.t by FUNCT_1:35,AS,P2;
||.s.|| <= 1 by B1,P2,LMMAZU;
hence
x in {||.gI.w.|| where w is VECTOR of S : ||.w.|| <= 1 } by B1,B2;
end;
assume x in {||.gI.w.|| where w is VECTOR of S : ||.w.|| <= 1 };
then
consider w be VECTOR of S such that
B1: x = ||.gI.w.|| & ||.w.|| <= 1;
set t = I.w;
B2: gI.w = g0.t by P1,FUNCT_1:13;
||.t.|| <= 1 by B1,AS,LMMAZU;
hence x in {||.g0.t.|| where t is VECTOR of T : ||.t.|| <= 1 } by B1,B2;
end;
X0: PreNorms(f0) = PreNorms(g0) by AS,Y1,TARSKI:2;
X1: PreNorms(modetrans(f,S,W)) = PreNorms(f0) by LOPBAN_1:29
.= PreNorms(modetrans(g,T,W)) by X0,LOPBAN_1:29;
thus ||. f .|| = upper_bound PreNorms(modetrans(f,S,W)) by LOPBAN_1:def 13
.= ||.g.|| by X1,LOPBAN_1:def 13;
end;
registration let S, T;
cluster isometric -> Lipschitzian for LinearOperator of S, T;
coherence
proof
let g be LinearOperator of S, T;
assume
A1: g is isometric;
reconsider K = 1 as Real;
for x be VECTOR of S holds ||. g.x .|| <= K*||. x .|| by A1,LMMAZU;
hence thesis;
end;
end;
begin :: Isometric Differentiable Functions on Real Normed Space
theorem
for G be RealNormSpace-Sequence,
F be RealNormSpace,
i be set,
f,g be PartFunc of product G,F,
X be Subset of product G
st X is open & i in dom G &
f is_partial_differentiable_on X,i &
g is_partial_differentiable_on X,i holds
f+g is_partial_differentiable_on X,i &
(f+g) `partial|(X,i) = f `partial|(X,i) + g `partial|(X,i)
proof
let G be RealNormSpace-Sequence;
let F be RealNormSpace;
let i be set;
let f,g be PartFunc of product G,F;
let X be Subset of product G;
assume that
O1:X is open and
A0: i in dom G and
A1:f is_partial_differentiable_on X,i and
A2:g is_partial_differentiable_on X,i;
set h = f+g;
dom h = (dom f) /\ (dom g) by VFUNCT_1:def 1; then
D1: X c= dom h by A1,A2,XBOOLE_1:19;
X1: for x be Point of product G st x in X holds
h is_partial_differentiable_in x,i &
partdiff(h,x,i) = partdiff(f,x,i)+partdiff(g,x,i)
proof
let x be Point of product G;
assume P5: x in X; then
P6: f is_partial_differentiable_in x,i by A1,O1,NDIFF_5:24;
g is_partial_differentiable_in x,i by A2,O1,P5,NDIFF_5:24;
hence h is_partial_differentiable_in x,i &
partdiff(h,x,i) = partdiff(f,x,i)+partdiff(g,x,i) by A0,NDIFF_5:28,P6;
end; then
for x be Point of product G st x in X holds
h is_partial_differentiable_in x,i;
hence
P7: h is_partial_differentiable_on X,i by NDIFF_5:24,D1,O1;
set fp = f`partial|(X,i);
set gp = g`partial|(X,i);
P8: dom fp = X &
for x be Point of product G st x in X holds fp/.x = partdiff(f,x,i)
by A1,NDIFF_5:def 9;
P9: dom gp = X &
for x be Point of product G st x in X holds gp/.x = partdiff(g,x,i)
by A2,NDIFF_5:def 9;
P10: dom (fp+gp) = X /\ X by P8,P9,VFUNCT_1:def 1
.= X;
for x be Point of product G st x in X
holds (fp+gp)/.x = partdiff(h,x,i)
proof
let x be Point of product G;
assume P11: x in X;
Z1: fp/.x = partdiff(f,x,i) by A1,P11,NDIFF_5:def 9;
thus (fp+gp)/.x = fp/.x + gp/.x by P11,P10,VFUNCT_1:def 1
.= partdiff(f,x,i) + partdiff(g,x,i) by Z1,A2,P11,NDIFF_5:def 9
.= partdiff(f+g,x,i) by P11,X1;
end;
hence thesis by P7,P10,NDIFF_5:def 9;
end;
theorem
for G be RealNormSpace-Sequence,
F be RealNormSpace,
i be set,
f,g be PartFunc of product G,F,
X be Subset of product G
st X is open & i in dom G &
f is_partial_differentiable_on X,i &
g is_partial_differentiable_on X,i holds
f-g is_partial_differentiable_on X,i &
(f-g) `partial|(X,i) = f `partial|(X,i)- g `partial|(X,i)
proof
let G be RealNormSpace-Sequence;
let F be RealNormSpace;
let i be set;
let f,g be PartFunc of product G,F;
let X be Subset of product G;
assume that
O1:X is open and
A0: i in dom G and
A1:f is_partial_differentiable_on X,i and
A2:g is_partial_differentiable_on X,i;
set h = f-g;
dom h = (dom f) /\ (dom g) by VFUNCT_1:def 2;
then
D1: X c= dom h by A1,A2,XBOOLE_1:19;
X1: for x be Point of product G st x in X holds
h is_partial_differentiable_in x,i &
partdiff(h,x,i) = partdiff(f,x,i) - partdiff(g,x,i)
proof
let x be Point of product G;
assume P5: x in X; then
P6: f is_partial_differentiable_in x,i by A1,O1,NDIFF_5:24;
g is_partial_differentiable_in x,i by A2,O1,P5,NDIFF_5:24;
hence thesis by A0,NDIFF_5:29,P6;
end; then
for x be Point of product G st x in X holds
h is_partial_differentiable_in x,i;
hence P7:h is_partial_differentiable_on X,i by NDIFF_5:24,D1,O1;
set fp = f`partial|(X,i);
set gp = g`partial|(X,i);
P8: dom fp = X &
for x be Point of product G st x in X
holds fp/.x = partdiff(f,x,i) by A1,NDIFF_5:def 9;
P9: dom gp = X &
for x be Point of product G st x in X
holds gp/.x = partdiff(g,x,i) by A2,NDIFF_5:def 9;
P10: dom (fp-gp) = X /\ X by P8,P9,VFUNCT_1:def 2
.= X;
for x be Point of product G st x in X
holds (fp-gp)/.x = partdiff(h,x,i)
proof
let x be Point of product G;
assume P11: x in X;
Z1: fp/.x = partdiff(f,x,i) by A1,P11,NDIFF_5:def 9;
thus (fp-gp)/.x = fp/.x - gp/.x by P11,P10,VFUNCT_1:def 2
.= partdiff(f,x,i) - partdiff(g,x,i) by Z1,A2,P11,NDIFF_5:def 9
.= partdiff(f-g,x,i) by P11,X1;
end;
hence thesis by P7,P10,NDIFF_5:def 9;
end;
theorem
for G be RealNormSpace-Sequence,
F be RealNormSpace,
i be set,
f be PartFunc of product G,F,
r be Real,
X be Subset of product G
st X is open & i in dom G &
f is_partial_differentiable_on X,i holds
r(#)f is_partial_differentiable_on X,i &
(r(#)f) `partial|(X,i) = r(#)(f `partial|(X,i))
proof
let G be RealNormSpace-Sequence;
let F be RealNormSpace;
let i be set;
let f be PartFunc of product G,F;
let r be Real;
let X be Subset of product G;
assume that
O1:X is open and
A0: i in dom G and
A1: f is_partial_differentiable_on X,i;
set h = r(#)f;
D1: X c= dom h by A1,VFUNCT_1:def 4;
X1: for x be Point of product G st x in X holds
h is_partial_differentiable_in x,i &
partdiff(h,x,i) = r*partdiff(f,x,i)
proof
let x be Point of product G;
assume x in X;
then f is_partial_differentiable_in x,i by A1,O1,NDIFF_5:24;
hence thesis by A0,NDIFF_5:30;
end; then
for x be Point of product G st x in X holds
h is_partial_differentiable_in x,i;
hence
P7: h is_partial_differentiable_on X,i by NDIFF_5:24,D1,O1;
set fp = f`partial|(X,i);
P8: dom fp = X &
for x be Point of product G st x in X
holds fp/.x = partdiff(f,x,i) by A1,NDIFF_5:def 9;
P10: dom (r(#)fp) = X by P8,VFUNCT_1:def 4;
for x be Point of product G st x in X
holds (r(#)fp)/.x = partdiff(h,x,i)
proof
let x be Point of product G;
assume P11: x in X;
thus (r(#)fp)/.x = r*(fp/.x) by P11,P10,VFUNCT_1:def 4
.= r* partdiff(f,x,i) by A1,P11,NDIFF_5:def 9
.= partdiff(r(#)f,x,i) by P11,X1;
end;
hence h`partial|(X,i) = r(#)fp by P7,P10,NDIFF_5:def 9;
end;
theorem LM090:
for S, T be RealNormSpace,
L be Lipschitzian LinearOperator of S, T,
x0 be Point of S holds
L is_differentiable_in x0 & diff(L,x0) = L
proof
let S, T be RealNormSpace,
L0 be Lipschitzian LinearOperator of S, T,
x0 be Point of S;
the carrier of S c= the carrier of S; then
reconsider Z = the carrier of S as Subset of S;
reconsider E = {} as Subset of S by XBOOLE_1:2;
reconsider L = L0
as Point of R_NormSpace_of_BoundedLinearOperators(S,T) by LOPBAN_1:def 9;
reconsider R = (the carrier of S) --> 0.T as PartFunc of S, T;
A6: dom R = the carrier of S;
now
let h be (0.S)-convergent sequence of S;
assume h is non-zero;
A7: now
let n be Nat;
A8: R/.(h.n) = R.(h.n) by A6,PARTFUN1:def 6
.= 0.T;
A9: rng h c= dom R;
A10: n in NAT by ORDINAL1:def 12;
thus ((||.h.||")(#)(R/*h)).n = (||.h.||".n)*((R/*h).n)
by NDIFF_1:def 2
.= 0.T by A8,A9,A10,FUNCT_2:109,RLVECT_1:10;
end; then
A11: (||.h.||")(#)(R/*h) is constant by VALUED_0:def 18;
hence (||.h.||")(#)(R/*h) is convergent by NDIFF_1:18;
((||.h.||")(#)(R/*h)).0 = 0.T by A7;
hence lim ((||.h.||")(#)(R/*h)) = 0.T by A11,NDIFF_1:18;
end;
then reconsider R as RestFunc of S, T by NDIFF_1:def 5;
set N = the Neighbourhood of x0;
A15: for x be Point of S st x in N holds L0/.x-L0/.x0=L.(x-x0)+R/.(x-x0)
proof
let x be Point of S;
A16: R/.(x-x0) =R.(x-x0) by A6,PARTFUN1:def 6
.= 0.T;
assume x in N;
thus L0/.x-L0/.x0 = L.(x-x0) by LM001
.= L.(x-x0)+R/.(x-x0) by A16,RLVECT_1:4;
end;
A17: dom L0 = the carrier of S by FUNCT_2:def 1;
hence L0 is_differentiable_in x0 by A15;
hence thesis by A17,A15,NDIFF_1:def 7;
end;
theorem LM120:
for f be PartFunc of T, W,
I be Lipschitzian LinearOperator of S, T,
I0 be Point of R_NormSpace_of_BoundedLinearOperators(S,T)
st I0 = I holds
for x be Point of S
st f is_differentiable_in I.x holds
f*I is_differentiable_in x &
diff(f*I,x) = diff(f,I.x)*I0
proof
let f be PartFunc of T, W,
I be Lipschitzian LinearOperator of S, T,
I0 be Point of R_NormSpace_of_BoundedLinearOperators(S,T);
assume AS0: I0 = I;
let x be Point of S;
assume
AS4: f is_differentiable_in I.x;
X1: I is_differentiable_in x & diff(I,x) = I by LM090;
thus f*I is_differentiable_in x by X1,AS4,NDIFF_2:13;
thus thesis by AS0,AS4,X1,NDIFF_2:13;
end;
theorem LM150:
for f be PartFunc of T, W,
I be LinearOperator of S, T
st I is one-to-one onto &
I is isometric holds
for x be Point of S holds
f*I is_differentiable_in x iff f is_differentiable_in I.x
proof
let f be PartFunc of T, W,
I be LinearOperator of S, T;
assume that
AS2: I is one-to-one onto and
AS3: I is isometric;
P0: dom I = the carrier of S by FUNCT_2:def 1;
set g = f*I;
let x be Point of S;
hereby
assume P1: g is_differentiable_in x;
consider J be LinearOperator of T, S such that
P2: J = I" & J is one-to-one onto isometric by LM020,AS2,AS3;
Q4: J is_differentiable_in I.x by LM090,P2;
P3: J.(I.x) = x by AS2,P2,P0,FUNCT_1:34;
g*J = f*(I*I") by P2,RELAT_1:36
.= f*id (the carrier of T) by AS2,FUNCT_2:29
.= f by FUNCT_2:17;
hence f is_differentiable_in I.x by NDIFF_2:13,P3,P1,Q4;
end;
assume P2: f is_differentiable_in I.x;
I is Lipschitzian LinearOperator of S, T by AS3;
then
reconsider I0 = I as Point of R_NormSpace_of_BoundedLinearOperators(S,T)
by LOPBAN_1:def 9;
I0 = I;
hence thesis by P2,LM120,AS3;
end;
theorem LM155:
for f be PartFunc of T, W,
I be LinearOperator of S, T,
X be set st X c= the carrier of T &
I is one-to-one onto & I is isometric holds
f is_differentiable_on X iff f*I is_differentiable_on I"X
proof
let f be PartFunc of T, W,
I be LinearOperator of S, T,
X be set;
assume that
AS1: X c= the carrier of T and
AS2: I is one-to-one onto and
AS3: I is isometric;
hereby
assume P2: f is_differentiable_on X;
P3: I"X c= I"(dom f) by P2,RELAT_1:143;
for x be Point of S st x in I"X
holds (f*I) | I"X is_differentiable_in x
proof
let x be Point of S;
assume x in I"X; then
x in dom I & I.x in X by FUNCT_1:def 7; then
P6: f|X is_differentiable_in (I.x) by P2;
(f|X)*I is_differentiable_in x by AS2,AS3,P6,LM150;
hence (f*I) | I"X is_differentiable_in x by FX1;
end;
hence f*I is_differentiable_on I"X by P3,RELAT_1:147;
end;
assume P2: f*I is_differentiable_on I"X; then
K1: I"X c= I"(dom f) by RELAT_1:147;
for y be Point of T st y in X
holds f|X is_differentiable_in y
proof
let y be Point of T;
assume P4: y in X;
consider x be Point of S such that
P5: y= I.x by AS2,FUNCT_2:113;
dom I = the carrier of S by FUNCT_2:def 1;
then x in I"X by P4,P5,FUNCT_1:def 7; then
(f*I) | I"X is_differentiable_in x by P2; then
(f|X)*I is_differentiable_in x by FX1;
hence f|X is_differentiable_in y by AS2,AS3,P5,LM150;
end;
hence thesis by AS1,AS2,K1,FUNCT_1:88;
end;
theorem
for X, Y be RealNormSpace,
f be PartFunc of product <*X,Y*>, W,
D be Subset of product <*X,Y*>
st f is_differentiable_on D holds
for z be Point of product <*X,Y*>
st z in dom (f`| D ) holds
(f`| D ).z = ((f*IsoCPNrSP(X,Y) `| (IsoCPNrSP(X,Y))"D)
/.((IsoCPNrSP(X,Y)").z)) *(IsoCPNrSP(X,Y)")
proof
let X, Y be RealNormSpace,
f be PartFunc of product <*X,Y*>, W,
D be Subset of product <*X,Y*>;
assume AS2: f is_differentiable_on D;
then OP1: D is open by NDIFF_1:32;
set I = IsoCPNrSP(X,Y);
X1: I is one-to-one onto &
( for x be Point of X, y be Point of Y holds I.(x,y) = <*x,y*> ) &
0. product <*X,Y*> = I.(0.[:X,Y:]) & I is isometric by defISO,ZeZe;
set J = (IsoCPNrSP(X,Y)");
P1: dom (f`| D) = D &
for x be Point of product <*X,Y*> st x in D holds (f`| D)/.x = diff(f,x)
by NDIFF_1:def 9,AS2;
set g = f*I;
set E = I"D;
P3: g is_differentiable_on E by LM155,AS2;
for z be Point of product <*X,Y*> st z in dom (f`| D)
holds (f`| D).z = ((g`| E )/.(J.z)) *I"
proof
let z be Point of product <*X,Y*>;
assume F1: z in dom (f`| D);
then
F2: (f`| D).z = (f`| D)/.z by PARTFUN1:def 6
.= diff(f,z) by F1,P1;
F3: f is_differentiable_in z by F1,OP1,P1,AS2,NDIFF_1:31;
consider w be Point of [:X,Y:] such that
F4: z = IsoCPNrSP(X,Y).w by X1,FUNCT_2:113;
reconsider I0 = I as Point of R_NormSpace_of_BoundedLinearOperators
( [:X,Y:],product <*X,Y*> ) by LOPBAN_1:def 9;
F11: diff(f,z) * I0 * I0"
= modetrans(diff(f,z), product <*X,Y*>,W)
* ( modetrans(I0,[:X,Y:],product <*X,Y*>) * I0" ) by RELAT_1:36
.= modetrans(diff(f,z), product <*X,Y*>,W)
* ( I * I" ) by LOPBAN_1:def 11
.= modetrans(diff(f,z), product <*X,Y*>,W)
* (id rng I0) by FUNCT_1:39
.= modetrans(diff(f,z), product <*X,Y*>,W) by X1,FUNCT_2:17
.= (f`| D).z by F2,LOPBAN_1:def 11;
w in E by F1,F4,P1,FUNCT_2:38; then
F12: ((g`| E )/.w) *I0" = diff(g,w)*I0" by P3,NDIFF_1:def 9;
F13: w = J.z by F4,FUNCT_2:26;
thus (f`| D).z = ((g`| E )/.(J.z)) *I" by F3,F4,F11,F12,F13,LM120;
end;
hence thesis;
end;
theorem LM166:
for X, Y be RealNormSpace,
f be PartFunc of [:X,Y:], W,
D be Subset of [:X,Y:]
st f is_differentiable_on D holds
for z be Point of [:X,Y:] st z in dom (f`| D )
holds (f`| D ).z = ((f*(IsoCPNrSP(X,Y)") `| ((IsoCPNrSP(X,Y)"))"D)
/.(IsoCPNrSP(X,Y).z)) *(IsoCPNrSP(X,Y)")"
proof
let X, Y be RealNormSpace,
f be PartFunc of [:X,Y:], W,
D be Subset of [:X,Y:];
assume AS2: f is_differentiable_on D;
then OP1: D is open by NDIFF_1:32;
set I = (IsoCPNrSP(X,Y)");
X1: I = (IsoCPNrSP(X,Y)") & I is one-to-one onto &
( for x be Point of X, y be Point of Y holds I.<*x,y*> =[x,y] ) &
0. [:X,Y:] = I.(0.product <*X,Y*>) & I is isometric by defISOA1,defISOA2;
set J = IsoCPNrSP(X,Y);
X2: J is one-to-one onto &
( for x be Point of X, y be Point of Y holds J.(x,y) =<*x,y*> ) &
0.product <*X,Y*> = J.(0. [:X,Y:]) & J is isometric by defISO,ZeZe;
P1: dom (f`| D) = D &
for x be Point of [:X,Y:] st x in D holds (f`| D)/.x = diff(f,x)
by NDIFF_1:def 9,AS2;
set g = f*I;
set E = I"D;
P3: g is_differentiable_on E by LM155,AS2;
for z be Point of [:X,Y:] st z in dom (f`| D)
holds (f`| D ).z = ((g`| E )/.(J.z)) *I"
proof
let z be Point of [:X,Y:];
assume F1X: z in dom (f`| D );
then F1: z in D by AS2,NDIFF_1:def 9;
F2: (f`| D).z = (f`| D)/.z by F1X,PARTFUN1:def 6
.= diff(f,z) by F1X,P1;
F3: f is_differentiable_in z by F1,OP1,AS2,NDIFF_1:31;
consider w be Point of product <*X,Y*> such that
F4: z = (IsoCPNrSP(X,Y)").w by X1,FUNCT_2:113;
reconsider I0 = I as Point of R_NormSpace_of_BoundedLinearOperators
( product <*X,Y*>,[:X,Y:] ) by LOPBAN_1:def 9;
F9: diff(f,z) * I0 * I0" = diff(g,w)*I0" by F3,F4,LM120;
F11: diff(f,z) * I0 * I0" = modetrans(diff(f,z), [:X,Y:],W)
* ( modetrans(I0,product <*X,Y*>,[:X,Y:]) * I0" ) by RELAT_1:36
.= modetrans(diff(f,z), [:X,Y:],W) * ( I * I" ) by LOPBAN_1:def 11
.= modetrans(diff(f,z), [:X,Y:],W) * ( id rng I0 ) by FUNCT_1:39
.= modetrans(diff(f,z), [:X,Y:],W) by X1,FUNCT_2:17
.= (f`| D).z by F2,LOPBAN_1:def 11;
w in E by F4,F1,FUNCT_2:38; then
((g`| E )/.w) *I0" = diff(g,w)*I0" by P3,NDIFF_1:def 9;
hence thesis by F4,F9,F11,X2,FUNCT_1:35;
end;
hence thesis;
end;
theorem LM180:
for X,Y be RealNormSpace,
z be Point of [:X,Y:] holds
reproj1(z) = (IsoCPNrSP(X,Y)") * reproj(In(1,dom <*X,Y*>),IsoCPNrSP(X,Y).z) &
reproj2(z) = (IsoCPNrSP(X,Y)") * reproj(In(2,dom <*X,Y*>),IsoCPNrSP(X,Y).z)
proof
let X, Y be RealNormSpace,
z be Point of [:X,Y:];
set i1 = In(1,dom<*X,Y*>);
set i2 = In(2,dom<*X,Y*>);
D1: dom <*X,Y*> = Seg len <*X,Y*> by FINSEQ_1:def 3
.= Seg 2 by FINSEQ_1:44;
then 1 in dom <*X,Y*>;
then AS1: i1 = 1 by SUBSET_1:def 8;
2 in dom <*X,Y*> by D1;
then AS2: i2 = 2 by SUBSET_1:def 8;
set I = (IsoCPNrSP(X,Y)");
set J = IsoCPNrSP(X,Y);
set f1 = reproj1(z);
(<*X,Y*>).i1 = X by AS1;
then reconsider R = reproj(i1,IsoCPNrSP(X,Y).z)
as Function of X,product <*X,Y*>;
reconsider g1 = (IsoCPNrSP(X,Y)")*R as Function of X,[:X,Y:];
consider x be Point of X, y be Point of Y such that
P1: z=[x,y] by PRVECT_3:18;
P3: z`2 = y by P1;
P4: IsoCPNrSP(X,Y).z =IsoCPNrSP(X,Y).(x,y) by P1
.=<*x,y*> by defISO;
now
let r be Element of X;
reconsider r0 = r as Element of (<*X,Y*> .i1) by AS1;
i1 in Seg 2 by AS1;
then i1 in Seg len <*x,y*> by FINSEQ_1:44; then
X0: i1 in dom <*x,y*> by FINSEQ_1:def 3;
X1: R.r = <*x,y*> +* (i1,r0) by P4,NDIFF_5:def 4;
X3: <*x,y*> +* (i1,r0) = <*x,y*> +* (i1 .--> r0)
by FUNCT_7:def 3,X0;
X2: <*x,y*> +* (i1 .--> r0) = <*r,y*>
proof
set q = <*x,y*> +* (1 .--> r0 );
X5: q = <*x,y*> +* ( 1,r0 ) by AS1,X0,FUNCT_7:def 3;
then reconsider q as FinSequence;
K1: len q = len <*x,y*> by X5,FUNCT_7:97
.= 2 by FINSEQ_1:44;
1 in dom (1 .--> r0) by FUNCOP_1:74; then
K3: q.1 = (1 .--> r0).1 by FUNCT_4:13
.= r by FUNCOP_1:72;
not 2 in dom (1 .--> r0) by FUNCOP_1:75;
then q.2 = <*x,y*>.2 by FUNCT_4:11
.= y;
hence thesis by AS1,K1,K3,FINSEQ_1:44;
end;
g1.r = I.(R.r) by FUNCT_2:15
.= [r,y] by X1,X2,X3,defISOA1;
hence f1 . r = g1 . r by P3,Defrep1;
end;
hence f1 = g1
.= (IsoCPNrSP(X,Y)")*reproj(i1,IsoCPNrSP(X,Y).z);
set f2= reproj2(z);
(<*X,Y*>).i2 = Y by AS2; then
reconsider L = reproj(i2,IsoCPNrSP(X,Y).z)
as Function of Y,product <*X,Y*>;
reconsider g2 = (IsoCPNrSP(X,Y)")*L as Function of Y,[:X,Y:];
consider x be Point of X, y be Point of Y such that
P1: z=[x,y] by PRVECT_3:18;
P2: z`1 = x by P1;
P4: IsoCPNrSP(X,Y).z = IsoCPNrSP(X,Y).(x,y) by P1
.=<*x,y*> by defISO;
now
let r be Element of Y;
reconsider r0 = r as Element of (<*X,Y*> .i2) by AS2;
i2 in Seg 2 by AS2;
then i2 in Seg len <*x,y*> by FINSEQ_1:44;
then
X0: i2 in dom <*x,y*> by FINSEQ_1:def 3;
X1: L.r = <*x,y*> +* (i2,r0) by P4,NDIFF_5:def 4;
X3: <*x,y*> +* (i2,r0) = <*x,y*> +* (i2 .--> r0) by FUNCT_7:def 3,X0;
X2: <*x,y*> +* (i2 .--> r0) = <*x,r*>
proof
set q = <*x,y*> +* (2 .--> r0);
X5: q = <*x,y*> +* (2,r0) by AS2,X0,FUNCT_7:def 3;
then reconsider q as FinSequence;
K1: len q = len <*x,y*> by X5,FUNCT_7:97
.= 2 by FINSEQ_1:44;
2 in dom (2 .--> r0) by FUNCOP_1:74; then
K3: q.2 = (2 .--> r0 ).2 by FUNCT_4:13
.= r by FUNCOP_1:72;
not 1 in dom (2 .--> r0) by FUNCOP_1:75;
then q.1 = <*x,y*>.1 by FUNCT_4:11
.= x;
hence thesis by AS2,K1,K3,FINSEQ_1:44;
end;
g2.r = I.(L.r) by FUNCT_2:15
.= [x,r] by X1,X2,X3,defISOA1;
hence f2.r = g2.r by P2,Defrep2;
end;
hence f2 = g2
.=(IsoCPNrSP(X,Y)")*reproj(i2,IsoCPNrSP(X,Y).z);
end;
definition
let X, Y be RealNormSpace, z be Point of [:X,Y:];
redefine func z`1 -> Point of X; :: redefines `1 (XTUPLE_0, definition)
correctness
proof
consider x be Point of X, y be Point of Y such that
P1: z=[x,y] by PRVECT_3:18;
thus thesis by P1;
end;
redefine func z`2 -> Point of Y; :: redefines `2 (XTUPLE_0, definition)
correctness
proof
consider x be Point of X, y be Point of Y such that
P1: z=[x,y] by PRVECT_3:18;
thus thesis by P1;
end;
end;
definition
let X, Y, W be RealNormSpace,
z be Point of [:X,Y:],
f be PartFunc of [:X,Y:], W;
pred f is_partial_differentiable_in`1 z means
f*reproj1(z) is_differentiable_in z`1;
pred f is_partial_differentiable_in`2 z means
f*reproj2(z) is_differentiable_in z`2;
end;
theorem LM190:
for X, Y be RealNormSpace,
z be Point of [:X,Y:] holds
z`1 = proj(In(1,dom<*X,Y*>)).(IsoCPNrSP(X,Y).z) &
z`2 = proj(In(2,dom<*X,Y*>)).(IsoCPNrSP(X,Y).z)
proof
let X, Y be RealNormSpace,
z be Point of [:X,Y:];
set i1 = In(1,dom <*X,Y*>);
set i2 = In(2,dom<*X,Y*>);
D1: dom <*X,Y*> = Seg len <*X,Y*> by FINSEQ_1:def 3
.= Seg 2 by FINSEQ_1:44;
then 1 in dom <*X,Y*>;
then
AS1: i1 = 1 by SUBSET_1:def 8;
2 in dom <*X,Y*> by D1;
then
AS2:i2 = 2 by SUBSET_1:def 8;
set G = <*X,Y*>;
AS3: product G = NORMSTR(# product carr G,zeros G,[:addop G:]
,[:multop G:], productnorm G #) by PRVECT_2:6;
consider x be Point of X, y be Point of Y such that
P1: z=[x,y] by PRVECT_3:18;
P4: IsoCPNrSP(X,Y).z = IsoCPNrSP(X,Y).(x,y) by P1
.=<*x,y*> by defISO;
reconsider w = IsoCPNrSP(X,Y).z as Element of product carr G by AS3;
P5: proj(In(1,dom<*X,Y*>)).w = <*x,y*> .1 by P4,AS1,NDIFF_5:def 3
.= z`1 by P1;
proj(In(2,dom<*X,Y*>)).w = <*x,y*> .2 by P4,AS2,NDIFF_5:def 3
.= z`2 by P1;
hence thesis by P5;
end;
theorem LM200:
for X, Y, W be RealNormSpace,
z be Point of [:X,Y:],
f be PartFunc of [:X,Y:], W holds
(f is_partial_differentiable_in`1 z iff
f*(IsoCPNrSP(X,Y)") is_partial_differentiable_in IsoCPNrSP(X,Y).z,1 ) &
(f is_partial_differentiable_in`2 z iff
f*(IsoCPNrSP(X,Y)") is_partial_differentiable_in IsoCPNrSP(X,Y).z,2 )
proof
let X, Y, W be RealNormSpace,
z be Point of [:X,Y:],
f be PartFunc of [:X,Y:], W;
reconsider g = f*(IsoCPNrSP(X,Y)") as PartFunc of product <*X,Y*>, W;
reconsider w = IsoCPNrSP(X,Y).z as Element of product <*X,Y*>;
D1:dom <*X,Y*> = Seg len <*X,Y*> by FINSEQ_1:def 3
.= Seg 2 by FINSEQ_1:44;
then 1 in dom <*X,Y*>; then
AS1: In(1,dom<*X,Y*>) = 1 by SUBSET_1:def 8;
2 in dom <*X,Y*> by D1; then
AS2:In(2,dom<*X,Y*>) = 2 by SUBSET_1:def 8;
X1: f*reproj1(z) = f*((IsoCPNrSP(X,Y)")
*reproj(In(1,dom<*X,Y*>),IsoCPNrSP(X,Y).z)) by LM180
.= g * reproj(In(1,dom<*X,Y*>),w) by RELAT_1:36;
X3: X = <*X,Y*>. In(1,dom<*X,Y*>) by AS1;
Y1: f*reproj2(z) = f*((IsoCPNrSP(X,Y)")
*reproj(In(2,dom<*X,Y*>),IsoCPNrSP(X,Y).z)) by LM180
.= g * reproj(In(2,dom<*X,Y*>),w) by RELAT_1:36;
Y3: Y = <*X,Y*>. In(2,dom<*X,Y*>) by AS2;
thus f is_partial_differentiable_in`1 z iff
f*(IsoCPNrSP(X,Y)") is_partial_differentiable_in IsoCPNrSP(X,Y).z,1
by X1,X3,LM190;
thus thesis by Y1,Y3,LM190;
end;
definition
let X, Y, W be RealNormSpace,
z be Point of [:X,Y:],
f be PartFunc of [:X,Y:], W;
func partdiff`1(f,z) -> Point of R_NormSpace_of_BoundedLinearOperators(X,W)
equals
diff(f*reproj1(z),z`1);
coherence;
func partdiff`2(f,z) -> Point of R_NormSpace_of_BoundedLinearOperators(Y,W)
equals
diff(f*reproj2(z),z`2);
coherence;
end;
theorem LM210:
for X, Y, W be RealNormSpace,
z be Point of [:X,Y:],
f be PartFunc of [:X,Y:], W holds
partdiff`1(f,z) = partdiff(f*(IsoCPNrSP(X,Y)"),IsoCPNrSP(X,Y).z,1) &
partdiff`2(f,z) = partdiff(f*(IsoCPNrSP(X,Y)"),IsoCPNrSP(X,Y).z,2)
proof
let X, Y, W be RealNormSpace,
z be Point of [:X,Y:],
f be PartFunc of [:X,Y:], W;
reconsider g = f*(IsoCPNrSP(X,Y)") as PartFunc of product <*X,Y*>,W;
reconsider w = IsoCPNrSP(X,Y).z as Element of product <*X,Y*>;
D1:dom <*X,Y*> = Seg len <*X,Y*> by FINSEQ_1:def 3
.= Seg 2 by FINSEQ_1:44;
then 1 in dom <*X,Y*>; then
AS1: In(1,dom<*X,Y*>) = 1 by SUBSET_1:def 8;
2 in dom <*X,Y*> by D1; then
AS2: In(2,dom<*X,Y*>) = 2 by SUBSET_1:def 8;
X1: f*reproj1(z) = f*((IsoCPNrSP(X,Y)")
*reproj(In(1,dom<*X,Y*>),IsoCPNrSP(X,Y).z)) by LM180
.= g * reproj(In(1,dom<*X,Y*>),w) by RELAT_1:36;
X3: X = <*X,Y*>. In(1,dom<*X,Y*>) by AS1;
Y1: f*reproj2(z) = f*((IsoCPNrSP(X,Y)")
*reproj(In(2,dom<*X,Y*>),IsoCPNrSP(X,Y).z)) by LM180
.= g * reproj(In(2,dom<*X,Y*>),w ) by RELAT_1:36;
Y3: Y = <*X,Y*>. In(2,dom<*X,Y*>) by AS2;
thus partdiff`1(f,z) = partdiff(f*(IsoCPNrSP(X,Y)"),IsoCPNrSP(X,Y).z,1)
by X1,X3,LM190;
thus thesis by Y1,Y3,LM190;
end;
theorem LM215:
for X, Y, W be RealNormSpace,
z be Point of [:X,Y:],
f1, f2 be PartFunc of [:X,Y:], W
st f1 is_partial_differentiable_in`1 z &
f2 is_partial_differentiable_in`1 z holds
(f1+f2) is_partial_differentiable_in`1 z &
partdiff`1(f1+f2,z) = partdiff`1(f1,z)+partdiff`1(f2,z) &
(f1-f2) is_partial_differentiable_in`1 z &
partdiff`1(f1-f2,z) = partdiff`1(f1,z)-partdiff`1(f2,z)
proof
let X, Y, W be RealNormSpace,
z be Point of [:X,Y:],
f1,f2 be PartFunc of [:X,Y:],W;
assume
A1: f1 is_partial_differentiable_in`1 z &
f2 is_partial_differentiable_in`1 z;
f1*reproj1(z) + f2*reproj1(z) is_differentiable_in z`1 by NDIFF_1:35,A1;
hence (f1+f2) is_partial_differentiable_in`1 z by Th26;
thus partdiff`1(f1+f2,z) =
diff(f1*reproj1(z)+f2*reproj1(z),z`1) by Th26
.= partdiff`1(f1,z)+partdiff`1(f2,z) by NDIFF_1:35,A1;
f1*reproj1(z) - f2*reproj1(z) is_differentiable_in z`1 by NDIFF_1:36,A1;
hence (f1-f2) is_partial_differentiable_in`1 z by Th26;
thus partdiff`1(f1-f2,z) =
diff(f1*reproj1(z)-f2*reproj1(z),z`1) by Th26
.= partdiff`1(f1,z)-partdiff`1(f2,z) by NDIFF_1:36,A1;
end;
theorem LM216:
for X, Y, W be RealNormSpace,
z be Point of [:X,Y:],
f1, f2 be PartFunc of [:X,Y:], W
st f1 is_partial_differentiable_in`2 z &
f2 is_partial_differentiable_in`2 z holds
(f1+f2) is_partial_differentiable_in`2 z &
partdiff`2(f1+f2,z) = partdiff`2(f1,z)+partdiff`2(f2,z) &
(f1-f2) is_partial_differentiable_in`2 z &
partdiff`2(f1-f2,z) = partdiff`2(f1,z)-partdiff`2(f2,z)
proof
let X, Y, W be RealNormSpace,
z be Point of [:X,Y:],
f1,f2 be PartFunc of [:X,Y:],W;
assume
A1: f1 is_partial_differentiable_in`2 z &
f2 is_partial_differentiable_in`2 z;
f1*reproj2(z) + f2*reproj2(z) is_differentiable_in z`2 by NDIFF_1:35,A1;
hence (f1+f2) is_partial_differentiable_in`2 z by Th26;
thus partdiff`2(f1+f2,z) =
diff(f1*reproj2(z)+f2*reproj2(z),z`2) by Th26
.= partdiff`2(f1,z)+partdiff`2(f2,z) by NDIFF_1:35,A1;
f1*reproj2(z) - f2*reproj2(z) is_differentiable_in z`2
by NDIFF_1:36,A1;
hence (f1-f2) is_partial_differentiable_in`2 z by Th26;
thus partdiff`2(f1-f2,z) =
diff(f1*reproj2(z)-f2*reproj2(z),z`2) by Th26
.= partdiff`2(f1,z)-partdiff`2(f2,z) by NDIFF_1:36,A1;
end;
theorem LM217:
for X, Y, W be RealNormSpace,
z be Point of [:X,Y:],
r be Real,
f be PartFunc of [:X,Y:], W
st f is_partial_differentiable_in`1 z holds
r(#)f is_partial_differentiable_in`1 z &
partdiff`1(r(#)f,z) = r*partdiff`1(f,z)
proof
let X, Y, W be RealNormSpace,
z be Point of [:X,Y:],
r be Real,
f be PartFunc of [:X,Y:], W;
assume A1: f is_partial_differentiable_in`1 z;
dom <*X,Y*> = Seg len <*X,Y*> by FINSEQ_1:def 3
.= Seg 2 by FINSEQ_1:44; then
D2:1 in dom <*X,Y*>;
then In(1,dom<*X,Y*>) = 1 by SUBSET_1:def 8; then
BX1: <*X,Y*> .In(1,dom<*X,Y*>) = X;
P1: f*(IsoCPNrSP(X,Y)") is_partial_differentiable_in
IsoCPNrSP(X,Y).z,1 by LM200,A1;
P3: partdiff`1(r(#)f,z) = partdiff((r(#)f)*(IsoCPNrSP(X,Y)")
,IsoCPNrSP(X,Y).z,1) by LM210;
P4: partdiff`1(f,z) = partdiff(f*(IsoCPNrSP(X,Y)"),IsoCPNrSP(X,Y).z,1)
by LM210;
P6: (r(#)f)*(IsoCPNrSP(X,Y)") = r(#)(f*(IsoCPNrSP(X,Y)")) by Th27;
hence (r(#)f) is_partial_differentiable_in`1 z
by D2,P1,LM200,NDIFF_5:30;
thus thesis by BX1,D2,P1,P3,P4,P6,NDIFF_5:30;
end;
theorem LM218:
for X, Y, W be RealNormSpace,
z be Point of [:X,Y:],
r be Real,
f be PartFunc of [:X,Y:], W
st f is_partial_differentiable_in`2 z holds
r(#)f is_partial_differentiable_in`2 z &
partdiff`2(r(#)f,z) = r*partdiff`2(f,z)
proof
let X, Y, W be RealNormSpace,
z be Point of [:X,Y:],
r be Real,
f be PartFunc of [:X,Y:], W;
assume A1: f is_partial_differentiable_in`2 z;
D1:dom <*X,Y*> = Seg len <*X,Y*> by FINSEQ_1:def 3
.= Seg 2 by FINSEQ_1:44;
D3: 2 in dom <*X,Y*> by D1;
then In(2,dom<*X,Y*>) = 2 by SUBSET_1:def 8; then
BX2: <*X,Y*> .In(2,dom<*X,Y*>) = Y;
P1: f*(IsoCPNrSP(X,Y)") is_partial_differentiable_in
IsoCPNrSP(X,Y).z,2 by LM200,A1;
P3: partdiff`2(r(#)f,z) = partdiff((r(#)f)*(IsoCPNrSP(X,Y)")
,IsoCPNrSP(X,Y).z,2) by LM210;
P4: partdiff`2(f,z) = partdiff(f*(IsoCPNrSP(X,Y)"),IsoCPNrSP(X,Y).z,2)
by LM210;
P6: (r(#)f)*(IsoCPNrSP(X,Y)") = r(#)(f*(IsoCPNrSP(X,Y)")) by Th27;
r(#)(f*(IsoCPNrSP(X,Y)")) is_partial_differentiable_in IsoCPNrSP(X,Y).z,2
by NDIFF_5:30,P1,D3; then
(r(#)f)*(IsoCPNrSP(X,Y)") is_partial_differentiable_in IsoCPNrSP(X,Y).z,2
by Th27;
hence (r(#)f) is_partial_differentiable_in`2 z by LM200;
thus thesis by BX2,D3,P1,P3,P4,P6,NDIFF_5:30;
end;
definition
let X, Y, W be RealNormSpace,
Z be set,
f be PartFunc of [:X,Y:], W;
pred f is_partial_differentiable_on`1 Z means
Z c= dom f & for z be Point of [:X,Y:] st z in Z holds
f|Z is_partial_differentiable_in`1 z;
pred f is_partial_differentiable_on`2 Z means
Z c= dom f & for z be Point of [:X,Y:] st z in Z holds
f|Z is_partial_differentiable_in`2 z;
end;
theorem LM300:
for X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f be PartFunc of [:X,Y:],W holds
(f is_partial_differentiable_on`1 Z iff
f*(IsoCPNrSP(X,Y)") is_partial_differentiable_on ((IsoCPNrSP(X,Y)"))"Z,1) &
(f is_partial_differentiable_on`2 Z iff
f*(IsoCPNrSP(X,Y)") is_partial_differentiable_on ((IsoCPNrSP(X,Y)"))"Z,2)
proof
let X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f be PartFunc of [:X,Y:], W;
set I = (IsoCPNrSP(X,Y)");
set J = IsoCPNrSP(X,Y);
set g = f*I;
set E = I"Z;
X1: I = (IsoCPNrSP(X,Y)") & I is one-to-one onto &
( for x be Point of X, y be Point of Y holds I.<*x,y*> =[x,y] ) &
0. [:X,Y:] = I.(0.product <*X,Y*>) & I is isometric by defISOA1,defISOA2;
X2: J is one-to-one onto &
( for x be Point of X, y be Point of Y holds J.(x,y) =<*x,y*> ) &
0.product <*X,Y*> = J.(0. [:X,Y:]) & J is isometric by defISO,ZeZe;
A1: dom (f*I) = I"(dom f) by RELAT_1:147;
A2: dom J = the carrier of [:X,Y:] by FUNCT_2:def 1;
thus f is_partial_differentiable_on`1 Z iff
g is_partial_differentiable_on E,1
proof
hereby
assume P2: f is_partial_differentiable_on`1 Z;
for w be Point of product <*X,Y*> st w in E
holds g|E is_partial_differentiable_in w,1
proof
let w be Point of product <*X,Y*>;
assume A4: w in E;
consider z be Point of [:X,Y:] such that
F4: w = IsoCPNrSP(X,Y).z by X2,FUNCT_2:113;
I.w = z by A2,F4,FUNCT_1:34;
then z in Z by A4,FUNCT_2:38;
then (f|Z)*(IsoCPNrSP(X,Y)") is_partial_differentiable_in
IsoCPNrSP(X,Y).z,1 by P2,LM200;
hence thesis by F4,FX1;
end;
hence g is_partial_differentiable_on E,1 by A1,P2,RELAT_1:143;
end;
assume P2: g is_partial_differentiable_on E,1;
then P3: I"Z c= I" (dom f) by RELAT_1:147;
for z be Point of [:X,Y:] st z in Z holds
f|Z is_partial_differentiable_in`1 z
proof
let z be Point of [:X,Y:];
assume A4: z in Z;
set w = IsoCPNrSP(X,Y).z;
I.w = z by A2,FUNCT_1:34;
then F4: w in E by FUNCT_2:38,A4;
(f|Z)*I = g | E by FX1;
hence thesis by F4,P2,LM200;
end;
hence f is_partial_differentiable_on`1 Z by P3,X1,FUNCT_1:88;
end;
thus f is_partial_differentiable_on`2 Z iff
g is_partial_differentiable_on E,2
proof
hereby
assume P2: f is_partial_differentiable_on`2 Z;
for w be Point of product <*X,Y*> st w in E holds
g|E is_partial_differentiable_in w,2
proof
let w be Point of product <*X,Y*>;
assume A4: w in E;
consider z be Point of [:X,Y:] such that
F4: w = IsoCPNrSP(X,Y).z by X2,FUNCT_2:113;
F8: I.w = z by A2,F4,FUNCT_1:34;
I.w in Z by FUNCT_2:38,A4;
then (f|Z)*(IsoCPNrSP(X,Y)") is_partial_differentiable_in
IsoCPNrSP(X,Y).z,2 by F8,P2,LM200;
hence thesis by F4,FX1;
end;
hence g is_partial_differentiable_on E,2 by A1,P2,RELAT_1:143;
end;
assume P2: g is_partial_differentiable_on E,2;
P3: I"Z c= I" (dom f) by P2,RELAT_1:147;
for z be Point of [:X,Y:] st z in Z holds
f|Z is_partial_differentiable_in`2 z
proof
let z be Point of [:X,Y:];
assume A4: z in Z;
set w = IsoCPNrSP(X,Y).z;
I.w = z by A2,FUNCT_1:34;
then F4: w in E by FUNCT_2:38,A4;
(f|Z)*I = g | E by FX1;
hence thesis by F4,P2,LM200;
end;
hence f is_partial_differentiable_on`2 Z by P3,X1,FUNCT_1:88;
end;
end;
definition
let X, Y, W be RealNormSpace,
Z be set,
f be PartFunc of [:X,Y:], W;
assume A2: f is_partial_differentiable_on`1 Z;
func f `partial`1|Z -> PartFunc of [:X,Y:],
R_NormSpace_of_BoundedLinearOperators (X,W) means :Def91:
dom it = Z &
for z be Point of [:X,Y:] st z in Z holds it/.z =partdiff`1(f,z);
existence
proof
deffunc F(Element of [:X,Y:]) = partdiff`1(f,$1);
defpred P[set] means $1 in Z;
consider F being PartFunc of [:X,Y:],
R_NormSpace_of_BoundedLinearOperators (X,W) such that
A3: (for z be Point of [:X,Y:] holds z in dom F iff P[z]) &
for z be Point of [:X,Y:] st z in dom F holds F.z = F(z)
from SEQ_1:sch 3;
take F;
now
A4: Z is Subset of [:X,Y:] by A2,XBOOLE_1:1;
let y be object;
assume y in Z;
hence y in dom F by A3,A4;
end;
then A5: Z c= dom F;
dom F c= Z by A3;
hence dom F = Z by A5,XBOOLE_0:def 10;
hereby
let x be Point of [:X,Y:];
assume A6: x in Z;
then F.x = partdiff`1(f,x) by A3;
hence F/.x = partdiff`1(f,x) by A3,A6,PARTFUN1:def 6;
end;
end;
uniqueness
proof
let F, H be PartFunc of [:X,Y:],
R_NormSpace_of_BoundedLinearOperators (X,W);
assume that
A7: dom F = Z and
A8: for x be Point of [:X,Y:]
st x in Z holds F/.x = partdiff`1(f,x) and
A9: dom H = Z and
A10: for x be Point of [:X,Y:] st x in Z holds H/.x = partdiff`1(f,x);
now
let x be Point of [:X,Y:];
assume A11: x in dom F;
then F/.x = partdiff`1(f,x) by A7,A8;
hence F/.x=H/.x by A7,A10,A11;
end;
hence thesis by A7,A9,PARTFUN2:1;
end;
end;
definition
let X, Y, W be RealNormSpace,
Z be set,
f be PartFunc of [:X,Y:], W;
assume A2: f is_partial_differentiable_on`2 Z;
func f `partial`2|Z -> PartFunc of [:X,Y:],
R_NormSpace_of_BoundedLinearOperators (Y,W) means :Def92:
dom it = Z &
for z be Point of [:X,Y:] st z in Z holds it/.z =partdiff`2(f,z);
existence
proof
deffunc F(Element of [:X,Y:]) = partdiff`2(f,$1);
defpred P[Element of [:X,Y:]] means $1 in Z;
consider F being PartFunc of [:X,Y:],
R_NormSpace_of_BoundedLinearOperators (Y,W) such that
A3: (for z be Point of [:X,Y:] holds z in dom F iff P[z]) &
for z be Point of [:X,Y:] st z in dom F holds F.z = F(z)
from SEQ_1:sch 3;
take F;
now
A4: Z is Subset of [:X,Y:] by A2,XBOOLE_1:1;
let y be object;
assume y in Z;
hence y in dom F by A3,A4;
end;
then A5: Z c= dom F;
dom F c= Z by A3;
hence dom F = Z by A5,XBOOLE_0:def 10;
hereby
let x be Point of [:X,Y:];
assume A6: x in Z;
then F.x = partdiff`2(f,x) by A3;
hence F/.x = partdiff`2(f,x) by A3,A6,PARTFUN1:def 6;
end;
end;
uniqueness
proof
let F, H be PartFunc of [:X,Y:],
R_NormSpace_of_BoundedLinearOperators (Y,W);
assume that
A7: dom F = Z and
A8: for x be Point of [:X,Y:]
st x in Z holds F/.x = partdiff`2(f,x) and
A9: dom H = Z and
A10: for x be Point of [:X,Y:] st x in Z holds H/.x = partdiff`2(f,x);
now
let x be Point of [:X,Y:];
assume A11: x in dom F;
then F/.x = partdiff`2(f,x) by A7,A8;
hence F/.x=H/.x by A7,A10,A11;
end;
hence thesis by A7,A9,PARTFUN2:1;
end;
end;
theorem LM400:
for X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f be PartFunc of [:X,Y:], W
st f is_partial_differentiable_on`1 Z holds
f `partial`1|Z = (f*(IsoCPNrSP(X,Y)"))`partial|(((IsoCPNrSP(X,Y)"))"Z,1)
*IsoCPNrSP(X,Y)
proof
let X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f be PartFunc of [:X,Y:], W;
assume AS0: f is_partial_differentiable_on`1 Z;
set I = (IsoCPNrSP(X,Y)");
set J = IsoCPNrSP(X,Y);
set g = f*I;
set E = I"Z;
A2: dom J = the carrier of [:X,Y:] by FUNCT_2:def 1;
set fpz = f `partial`1|Z;
P1: dom fpz = Z &
for z be Point of [:X,Y:] st z in Z holds fpz/.z =partdiff`1(f,z)
by Def91,AS0;
set gpe = g `partial|(E,1);
P3X: g is_partial_differentiable_on E,1 by LM300,AS0; then
P3: dom gpe = E &
for x be Point of product <*X,Y*> st x in E holds
gpe/.x = partdiff(g,x,1) by NDIFF_5:def 9;
P4: dom (gpe*J) = J"E by P3,RELAT_1:147
.= J"(J.:Z) by FUNCT_1:84
.= Z by A2,FUNCT_1:94;
now
let x be object;
assume P40: x in dom fpz;
then reconsider z = x as Point of [:X,Y:];
P44: J.z in J.: Z by P1,P40,FUNCT_2:35;
I" = J by FUNCT_1:43; then
P42: J.z in E by P44,FUNCT_1:85;
thus fpz.x = fpz/.z by PARTFUN1:def 6,P40
.= partdiff`1(f,z) by P1,P40
.= partdiff(g,J.z,1) by LM210
.= gpe/.(J.z) by P3X,P42,NDIFF_5:def 9
.= gpe.(J.z) by P42,PARTFUN1:def 6,P3
.= (gpe*J).x by A2,FUNCT_1:13;
end;
hence thesis by P1,P4,FUNCT_1:2;
end;
theorem LM401:
for X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f be PartFunc of [:X,Y:], W
st f is_partial_differentiable_on`2 Z holds
f `partial`2|Z = (f*(IsoCPNrSP(X,Y)"))`partial|(((IsoCPNrSP(X,Y)"))"Z,2)
*IsoCPNrSP(X,Y)
proof
let X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f be PartFunc of [:X,Y:], W;
assume AS0: f is_partial_differentiable_on`2 Z;
set I = (IsoCPNrSP(X,Y)");
set J = IsoCPNrSP(X,Y);
set g = f*I;
set E = I"Z;
A2: dom J = the carrier of [:X,Y:] by FUNCT_2:def 1;
set fpz = f `partial`2|Z;
P1: dom fpz = Z &
for z be Point of [:X,Y:] st z in Z holds fpz/.z =partdiff`2(f,z)
by Def92,AS0;
set gpe = g `partial|(E,2);
P3X: g is_partial_differentiable_on E,2 by LM300,AS0; then
P3: dom gpe = E &
for x be Point of product <*X,Y*> st x in E holds
gpe/.x = partdiff(g,x,2) by NDIFF_5:def 9;
P4: dom (gpe*J) = J"E by P3,RELAT_1:147
.= J"(J.:Z) by FUNCT_1:84
.= Z by A2,FUNCT_1:94;
now
let x be object;
assume P40: x in dom fpz;
then reconsider z = x as Point of [:X,Y:];
P44: J.z in J.: Z by P1,P40,FUNCT_2:35;
I" = J by FUNCT_1:43; then
P42: J.z in E by P44,FUNCT_1:85;
thus fpz.x = fpz/.z by PARTFUN1:def 6,P40
.= partdiff`2(f,z) by P1,P40
.= partdiff(g,J.z,2) by LM210
.= gpe/.(J.z) by P3X,P42,NDIFF_5:def 9
.= gpe.(J.z) by P3,P42,PARTFUN1:def 6
.= (gpe*J).x by A2,FUNCT_1:13;
end;
hence thesis by P1,P4,FUNCT_1:2;
end;
theorem NDIFF5241:
for X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f be PartFunc of [:X,Y:], W
st Z is open holds
f is_partial_differentiable_on`1 Z iff
Z c= dom f &
for x be Point of [:X,Y:] st x in Z holds
f is_partial_differentiable_in`1 x
proof
let X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f be PartFunc of [:X,Y:], W;
assume AS: Z is open;
set I = (IsoCPNrSP(X,Y)");
set J = IsoCPNrSP(X,Y);
set g = f*I;
set E = I"Z;
X1: I = (IsoCPNrSP(X,Y)") & I is one-to-one onto &
( for x be Point of X, y be Point of Y holds I.<*x,y*> =[x,y] ) &
0. [:X,Y:] = I.(0.product <*X,Y*>) & I is isometric by defISOA1,defISOA2;
X2: J is one-to-one onto &
( for x be Point of X, y be Point of Y holds J.(x,y) =<*x,y*> ) &
0.product <*X,Y*> = J.(0. [:X,Y:]) & J is isometric by defISO,ZeZe;
A2: dom J = the carrier of [:X,Y:] by FUNCT_2:def 1;
I"Z = J.:Z by FUNCT_1:84;
then OP1: E is open by AS,LM025;
hereby
assume f is_partial_differentiable_on`1 Z;
then P2: g is_partial_differentiable_on E,1 by LM300;
then I"Z c= I" (dom f) by RELAT_1:147;
hence Z c= dom f by X1,FUNCT_1:88;
thus for x be Point of [:X,Y:] st x in Z holds
f is_partial_differentiable_in`1 x
proof
let z be Point of [:X,Y:];
assume A4: z in Z;
set w = IsoCPNrSP(X,Y).z;
I.w = z by A2,FUNCT_1:34;
then w in E by FUNCT_2:38,A4;
then g is_partial_differentiable_in w,1 by OP1,P2,NDIFF_5:24;
hence f is_partial_differentiable_in`1 z by LM200;
end;
end;
assume P1: Z c=dom f &
for x be Point of [:X,Y:] st x in Z holds
f is_partial_differentiable_in`1 x;
then I"Z c= I" (dom f) by RELAT_1:143; then
P3: E c=dom g by RELAT_1:147;
for w be Point of product <*X,Y*> st w in E holds
g is_partial_differentiable_in w,1
proof
let w be Point of product <*X,Y*>;
assume A4: w in E;
consider z be Point of [:X,Y:] such that
F4: w = IsoCPNrSP(X,Y).z by X2,FUNCT_2:113;
F8: I.w = z by A2,F4,FUNCT_1:34;
z in Z by A4,F8,FUNCT_2:38;
hence g is_partial_differentiable_in w,1 by F4,P1,LM200;
end;
then g is_partial_differentiable_on E,1 by NDIFF_5:24,P3,OP1;
hence f is_partial_differentiable_on`1 Z by LM300;
end;
theorem NDIFF5242:
for X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f be PartFunc of [:X,Y:], W
st Z is open holds
f is_partial_differentiable_on`2 Z iff
Z c= dom f &
for x be Point of [:X,Y:] st x in Z holds
f is_partial_differentiable_in`2 x
proof
let X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f be PartFunc of [:X,Y:], W;
assume AS: Z is open;
set I = (IsoCPNrSP(X,Y)");
set J = IsoCPNrSP(X,Y);
set g = f*I;
set E = I"Z;
X1: I = (IsoCPNrSP(X,Y)") & I is one-to-one onto &
( for x be Point of X, y be Point of Y holds I.<*x,y*> =[x,y] ) &
0. [:X,Y:] = I.(0.product <*X,Y*>) & I is isometric by defISOA1,defISOA2;
X2: J is one-to-one onto &
( for x be Point of X, y be Point of Y holds J.(x,y) =<*x,y*> ) &
0.product <*X,Y*> = J.(0. [:X,Y:]) & J is isometric by defISO,ZeZe;
A2: dom J = the carrier of [:X,Y:] by FUNCT_2:def 1;
I"Z = J.:Z by FUNCT_1:84;
then OP1: E is open by AS,LM025;
hereby
assume f is_partial_differentiable_on`2 Z;
then P2: g is_partial_differentiable_on E,2 by LM300;
then
I"Z c= I" (dom f) by RELAT_1:147;
hence Z c= dom f by X1,FUNCT_1:88;
thus for x be Point of [:X,Y:] st x in Z holds
f is_partial_differentiable_in`2 x
proof
let z be Point of [:X,Y:];
assume A4: z in Z;
set w = IsoCPNrSP(X,Y).z;
I.w = z by A2,FUNCT_1:34;
then w in E by FUNCT_2:38,A4;
then g is_partial_differentiable_in w,2 by OP1,P2,NDIFF_5:24;
hence f is_partial_differentiable_in`2 z by LM200;
end;
end;
assume P1: Z c=dom f &
for x be Point of [:X,Y:] st x in Z holds
f is_partial_differentiable_in`2 x;
then I"Z c= I" (dom f) by RELAT_1:143; then
P3: E c=dom g by RELAT_1:147;
for w be Point of product <*X,Y*> st w in E holds
g is_partial_differentiable_in w,2
proof
let w be Point of product <*X,Y*>;
assume A4: w in E;
consider z be Point of [:X,Y:] such that
F4: w = IsoCPNrSP(X,Y).z by X2,FUNCT_2:113;
I.w = z by A2,F4,FUNCT_1:34;
then z in Z by A4,FUNCT_2:38;
hence g is_partial_differentiable_in w,2 by F4,P1,LM200;
end;
then g is_partial_differentiable_on E,2 by NDIFF_5:24,P3,OP1;
hence f is_partial_differentiable_on`2 Z by LM300;
end;
theorem
for X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f,g be PartFunc of [:X,Y:], W
st Z is open &
f is_partial_differentiable_on`1 Z &
g is_partial_differentiable_on`1 Z holds
f+g is_partial_differentiable_on`1 Z &
(f+g) `partial`1|Z = f `partial`1|Z+ g `partial`1|Z
proof
let X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f, g be PartFunc of [:X,Y:], W;
assume that
O1: Z is open and
A1: f is_partial_differentiable_on`1 Z and
A2: g is_partial_differentiable_on`1 Z;
set h = f+g;
dom h = (dom f) /\ (dom g) by VFUNCT_1:def 1; then
D1: Z c= dom h by A1,A2,XBOOLE_1:19;
X1: for x be Point of [:X,Y:] st x in Z holds
h is_partial_differentiable_in`1 x &
partdiff`1(h,x) = partdiff`1(f,x)+partdiff`1(g,x)
proof
let x be Point of [:X,Y:];
assume P5: x in Z; then
P6: f is_partial_differentiable_in`1 x by A1,O1,NDIFF5241;
g is_partial_differentiable_in`1 x by A2,O1,P5,NDIFF5241;
hence h is_partial_differentiable_in`1 x &
partdiff`1(h,x) = partdiff`1(f,x)+partdiff`1(g,x) by LM215,P6;
end;
then
for x be Point of [:X,Y:] st x in Z holds
h is_partial_differentiable_in`1 x;
hence
P7: h is_partial_differentiable_on`1 Z by NDIFF5241,D1,O1;
set fp = f`partial`1|Z;
set gp = g`partial`1|Z;
P8: dom fp= Z &
for x be Point of [:X,Y:] st x in Z
holds fp/.x = partdiff`1(f,x) by A1,Def91;
P9: dom gp = Z &
for x be Point of [:X,Y:] st x in Z holds gp/.x = partdiff`1(g,x)
by A2,Def91;
P10: dom (fp+gp) = Z /\ Z by P8,P9,VFUNCT_1:def 1
.= Z;
for x be Point of [:X,Y:] st x in Z holds (fp+gp)/.x = partdiff`1(h,x)
proof
let x be Point of [:X,Y:];
assume P11: x in Z;
Z1: fp/.x = partdiff`1(f,x) by A1,P11,Def91;
Z2: gp/.x = partdiff`1(g,x) by A2,P11,Def91;
thus (fp+gp)/.x = fp/.x + gp/.x by P11,P10,VFUNCT_1:def 1
.= partdiff`1(f+g,x) by P11,X1,Z1,Z2;
end;
hence h`partial`1|Z = fp+gp by P7,P10,Def91;
end;
theorem
for X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f, g be PartFunc of [:X,Y:], W
st Z is open &
f is_partial_differentiable_on`1 Z &
g is_partial_differentiable_on`1 Z holds
f-g is_partial_differentiable_on`1 Z &
(f-g) `partial`1|Z = f `partial`1|Z- g `partial`1|Z
proof
let X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f,g be PartFunc of [:X,Y:], W;
assume that
O1: Z is open and
A1: f is_partial_differentiable_on`1 Z and
A2: g is_partial_differentiable_on`1 Z;
set h = f-g;
dom h = (dom f) /\ (dom g) by VFUNCT_1:def 2;
then
D1: Z c= dom h by A1,A2,XBOOLE_1:19;
X1: for x be Point of [:X,Y:] st x in Z holds
h is_partial_differentiable_in`1 x &
partdiff`1(h,x) = partdiff`1(f,x)-partdiff`1(g,x)
proof
let x be Point of [:X,Y:];
assume P5: x in Z; then
P6: f is_partial_differentiable_in`1 x by A1,O1,NDIFF5241;
g is_partial_differentiable_in`1 x by A2,O1,P5,NDIFF5241;
hence h is_partial_differentiable_in`1 x &
partdiff`1(h,x) = partdiff`1(f,x)-partdiff`1(g,x) by LM215,P6;
end; then
for x be Point of [:X,Y:] st x in Z holds
h is_partial_differentiable_in`1 x;
hence P7:h is_partial_differentiable_on`1 Z by NDIFF5241,D1,O1;
set fp = f`partial`1|Z;
set gp = g`partial`1|Z;
P8: dom fp= Z &
for x be Point of [:X,Y:] st x in Z
holds fp/.x = partdiff`1(f,x) by A1,Def91;
P9: dom gp= Z &
for x be Point of [:X,Y:] st x in Z
holds gp/.x = partdiff`1(g,x) by A2,Def91;
P10: dom (fp-gp) = Z /\ Z by P8,P9,VFUNCT_1:def 2
.= Z;
for x be Point of [:X,Y:] st x in Z
holds (fp-gp)/.x = partdiff`1(h,x)
proof
let x be Point of [:X,Y:];
assume P11: x in Z;
Z1: fp/.x = partdiff`1(f,x) by A1,P11,Def91;
Z2: gp/.x = partdiff`1(g,x) by A2,P11,Def91;
thus (fp-gp)/.x = fp/.x - gp/.x by P11,P10,VFUNCT_1:def 2
.= partdiff`1(f-g,x) by P11,X1,Z1,Z2;
end;
hence h`partial`1|Z = fp-gp by P7,P10,Def91;
end;
theorem
for X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f, g be PartFunc of [:X,Y:], W
st Z is open &
f is_partial_differentiable_on`2 Z &
g is_partial_differentiable_on`2 Z holds
f+g is_partial_differentiable_on`2 Z &
(f+g) `partial`2|Z = f `partial`2|Z+ g `partial`2|Z
proof
let X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f, g be PartFunc of [:X,Y:], W;
assume that
O1: Z is open and
A1: f is_partial_differentiable_on`2 Z and
A2: g is_partial_differentiable_on`2 Z;
set h = f+g;
dom h = (dom f) /\ (dom g) by VFUNCT_1:def 1; then
D1: Z c= dom h by A1,A2,XBOOLE_1:19;
X1: for x be Point of [:X,Y:] st x in Z holds
h is_partial_differentiable_in`2 x &
partdiff`2(h,x) = partdiff`2(f,x)+partdiff`2(g,x)
proof
let x be Point of [:X,Y:];
assume P5: x in Z; then
P6: f is_partial_differentiable_in`2 x by A1,O1,NDIFF5242;
g is_partial_differentiable_in`2 x by A2,O1,P5,NDIFF5242;
hence h is_partial_differentiable_in`2 x &
partdiff`2(h,x) = partdiff`2(f,x)+partdiff`2(g,x) by LM216,P6;
end; then
for x be Point of [:X,Y:] st x in Z holds
h is_partial_differentiable_in`2 x;
hence
P7:h is_partial_differentiable_on`2 Z by NDIFF5242,D1,O1;
set fp = f`partial`2|Z;
set gp = g`partial`2|Z;
P8: dom fp= Z &
for x be Point of [:X,Y:] st x in Z
holds fp/.x = partdiff`2(f,x) by A1,Def92;
P9: dom gp= Z &
for x be Point of [:X,Y:] st x in Z
holds gp/.x = partdiff`2(g,x) by A2,Def92;
P10: dom (fp+gp) = Z /\ Z by P8,P9,VFUNCT_1:def 1
.= Z;
for x be Point of [:X,Y:] st x in Z holds (fp+gp)/.x = partdiff`2(h,x)
proof
let x be Point of [:X,Y:];
assume P11: x in Z; then
Z1: fp/.x = partdiff`2(f,x) by A1,Def92;
Z2: gp/.x = partdiff`2(g,x) by A2,P11,Def92;
thus (fp+gp)/.x = fp/.x + gp/.x by P11,P10,VFUNCT_1:def 1
.= partdiff`2(f+g,x) by P11,X1,Z1,Z2;
end;
hence h`partial`2|Z = fp+gp by P7,P10,Def92;
end;
theorem
for X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f, g be PartFunc of [:X,Y:], W
st Z is open &
f is_partial_differentiable_on`2 Z &
g is_partial_differentiable_on`2 Z
holds
f-g is_partial_differentiable_on`2 Z &
(f-g) `partial`2|Z = f `partial`2|Z- g `partial`2|Z
proof
let X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f, g be PartFunc of [:X,Y:], W;
assume that
O1: Z is open and
A1: f is_partial_differentiable_on`2 Z and
A2: g is_partial_differentiable_on`2 Z;
set h = f-g;
dom h = (dom f) /\ (dom g) by VFUNCT_1:def 2; then
D1: Z c= dom h by A1,A2,XBOOLE_1:19;
X1: for x be Point of [:X,Y:] st x in Z holds
h is_partial_differentiable_in`2 x &
partdiff`2(h,x) = partdiff`2(f,x)-partdiff`2(g,x)
proof
let x be Point of [:X,Y:];
assume P5: x in Z; then
P6: f is_partial_differentiable_in`2 x by A1,O1,NDIFF5242;
g is_partial_differentiable_in`2 x by A2,O1,P5,NDIFF5242;
hence h is_partial_differentiable_in`2 x &
partdiff`2(h,x) = partdiff`2(f,x)-partdiff`2(g,x) by LM216,P6;
end;
then
for x be Point of [:X,Y:] st x in Z holds
h is_partial_differentiable_in`2 x;
hence
P7:h is_partial_differentiable_on`2 Z by NDIFF5242,D1,O1;
set fp = f`partial`2|Z;
set gp = g`partial`2|Z;
P8: dom fp= Z &
for x be Point of [:X,Y:] st x in Z
holds fp/.x = partdiff`2(f,x) by A1,Def92;
dom gp= Z &
for x be Point of [:X,Y:] st x in Z
holds gp/.x = partdiff`2(g,x) by A2,Def92; then
P10: dom (fp-gp) = Z /\ Z by P8,VFUNCT_1:def 2
.= Z;
for x be Point of [:X,Y:] st x in Z
holds (fp-gp)/.x = partdiff`2(h,x)
proof
let x be Point of [:X,Y:];
assume P11: x in Z; then
Z1: fp/.x = partdiff`2(f,x) by A1,Def92;
Z2: gp/.x = partdiff`2(g,x) by A2,P11,Def92;
thus (fp-gp)/.x = fp/.x - gp/.x by P11,P10,VFUNCT_1:def 2
.= partdiff`2(f-g,x) by P11,X1,Z1,Z2;
end;
hence h`partial`2|Z =fp-gp by P7,P10,Def92;
end;
theorem
for X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
r be Real,
f be PartFunc of [:X,Y:], W
st Z is open &
f is_partial_differentiable_on`1 Z holds
r(#)f is_partial_differentiable_on`1 Z &
(r(#)f) `partial`1|Z = r(#)(f `partial`1|Z)
proof
let X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
r be Real,
f be PartFunc of [:X,Y:], W;
assume that
O1: Z is open and
A1: f is_partial_differentiable_on`1 Z;
set h = r(#)f;
D1: Z c= dom h by A1,VFUNCT_1:def 4;
X1: for x be Point of [:X,Y:] st x in Z holds
h is_partial_differentiable_in`1 x &
partdiff`1(h,x) = r*partdiff`1(f,x)
proof
let x be Point of [:X,Y:];
assume x in Z;
then f is_partial_differentiable_in`1 x by A1,O1,NDIFF5241;
hence h is_partial_differentiable_in`1 x &
partdiff`1(h,x) = r*partdiff`1(f,x) by LM217;
end;
then
for x be Point of [:X,Y:] st x in Z holds
h is_partial_differentiable_in`1 x;
hence
P7:h is_partial_differentiable_on`1 Z by D1,O1,NDIFF5241;
set fp = f`partial`1|Z;
P8: dom fp= Z &
for x be Point of [:X,Y:] st x in Z
holds fp/.x = partdiff`1(f,x) by A1,Def91;
P10: dom (r(#)fp) = Z by P8,VFUNCT_1:def 4;
for x be Point of [:X,Y:] st x in Z
holds (r(#)fp)/.x = partdiff`1(h,x)
proof
let x be Point of [:X,Y:];
assume P11: x in Z;
Z1: fp/.x = partdiff`1(f,x) by A1,P11,Def91;
thus (r(#)fp)/.x = r*(fp/.x) by P11,P10,VFUNCT_1:def 4
.= partdiff`1(r(#)f,x) by P11,X1,Z1;
end;
hence h`partial`1|Z = r(#)fp by P7,P10,Def91;
end;
theorem
for X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
r be Real,
f be PartFunc of [:X,Y:], W
st Z is open &
f is_partial_differentiable_on`2 Z holds
r(#)f is_partial_differentiable_on`2 Z &
(r(#)f) `partial`2|Z = r(#)(f `partial`2|Z)
proof
let X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
r be Real,
f be PartFunc of [:X,Y:], W;
assume that
O1: Z is open and
A1: f is_partial_differentiable_on`2 Z;
set h = r(#)f;
D1: Z c= dom h by A1,VFUNCT_1:def 4;
X1: for x be Point of [:X,Y:] st x in Z holds
h is_partial_differentiable_in`2 x &
partdiff`2(h,x) = r*partdiff`2(f,x)
proof
let x be Point of [:X,Y:];
assume x in Z;
then f is_partial_differentiable_in`2 x by A1,O1,NDIFF5242;
hence h is_partial_differentiable_in`2 x &
partdiff`2(h,x) = r*partdiff`2(f,x) by LM218;
end;
then
for x be Point of [:X,Y:] st x in Z holds
h is_partial_differentiable_in`2 x;
hence
P7: h is_partial_differentiable_on`2 Z by D1,O1,NDIFF5242;
set fp = f`partial`2|Z;
P8: dom fp= Z &
for x be Point of [:X,Y:] st x in Z
holds fp/.x = partdiff`2(f,x) by A1,Def92;
P10: dom (r(#)fp) = Z by P8,VFUNCT_1:def 4;
for x be Point of [:X,Y:] st x in Z
holds (r(#)fp)/.x = partdiff`2(h,x)
proof
let x be Point of [:X,Y:];
assume P11: x in Z;
Z1: fp/.x = partdiff`2(f,x) by A1,P11,Def92;
thus (r(#)fp)/.x = r*(fp/.x) by P11,P10,VFUNCT_1:def 4
.= partdiff`2(r(#)f,x) by P11,X1,Z1;
end;
hence h`partial`2|Z =r(#)fp by P7,P10,Def92;
end;
theorem LMX1:
for X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f be PartFunc of [:X,Y:], W
st f is_differentiable_on Z holds
f`|Z is_continuous_on Z iff
(f*(IsoCPNrSP(X,Y)")) `| ((IsoCPNrSP(X,Y)")"Z) is_continuous_on
((IsoCPNrSP(X,Y)")"Z)
proof
let X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f be PartFunc of [:X,Y:], W;
assume AS1: f is_differentiable_on Z;
set I = (IsoCPNrSP(X,Y)");
X1: I = (IsoCPNrSP(X,Y)") & I is one-to-one onto &
( for x be Point of X, y be Point of Y holds I.<*x,y*> =[x,y] ) &
0. [:X,Y:] = I.(0.product <*X,Y*>) & I is isometric by defISOA1,defISOA2;
set J = IsoCPNrSP(X,Y);
X2: J is one-to-one onto &
( for x be Point of X, y be Point of Y holds J.(x,y) =<*x,y*> ) &
0.product <*X,Y*> = J.(0. [:X,Y:]) & J is isometric by defISO,ZeZe;
set g = f*I;
set E = I"(Z);
A2: dom J = the carrier of [:X,Y:] by FUNCT_2:def 1;
IJ1: I" = J by FUNCT_1:43;
AS2: g is_differentiable_on E by LM155,AS1;
P1: dom (f`|Z) = Z by AS1,NDIFF_1:def 9;
P2: dom (g`|E) = E by AS2,NDIFF_1:def 9;
set F = f`|Z;
set G = g`|E;
hereby
assume Q2: F is_continuous_on Z;
for y0 be Point of product <*X,Y*>, r be Real st y0 in E & 0<r
ex s be Real
st 0<s & for y1 be Point of product <*X,Y*>
st y1 in E & ||. y1- y0 .|| < s holds ||. G/.y1 - G/.y0 .|| < r
proof
let y0 be Point of product <*X,Y*>,
r be Real;
assume H1: y0 in E & 0<r;
consider x0 be Point of [:X,Y:] such that
F4: y0 = J.x0 by X2,FUNCT_2:113;
F8: I.y0 = x0 by A2,F4,FUNCT_1:34;
then
F9: x0 in Z by H1,FUNCT_2:38;
then consider s be Real such that
F10: 0 < s &
for x1 be Point of [:X,Y:] st x1 in Z & ||. x1- x0 .|| < s
holds ||. F/.x1 - F/.x0 .|| < r by Q2,H1,NFCONT_1:19;
take s;
thus 0 < s by F10;
thus for y1 be Point of product <*X,Y*>
st y1 in E & ||. y1- y0 .|| < s holds ||. G/.y1 - G/.y0 .|| < r
proof
let y1 be Point of product <*X,Y*>;
assume H3: y1 in E & ||. y1- y0 .|| < s;
consider x1 be Point of [:X,Y:] such that
G4: y1 = J.x1 by X2,FUNCT_2:113;
G8: I.y1 = x1 by A2,G4,FUNCT_1:34;
then G9: x1 in Z by H3,FUNCT_2:38;
||. x1- x0 .||
= ||. y1-y0 .|| by X1,F8,G8;
then
H5: ||. F/.x1 - F/.x0 .|| < r by F10,G9,H3;
H7: F/.x1 = F.x1 by G9,P1,PARTFUN1:def 6
.= (G/.y1)*J by AS1,G4,G9,P1,IJ1,LM166;
H8: F/.x0 = F.x0 by F9,P1,PARTFUN1:def 6
.= (G/.y0)*J by AS1,F4,F9,P1,IJ1,LM166;
reconsider Gy1y0 = G/.y1 - G/.y0 as Lipschitzian LinearOperator
of product <*X,Y*>,W by LOPBAN_1:def 9;
reconsider Fx1x0 = F/.x1 - F/.x0 as Lipschitzian LinearOperator
of [:X,Y:],W by LOPBAN_1:def 9;
now
let t be VECTOR of [:X,Y:];
U2: ((G/.y1 - G/.y0)*J).t= (G/.y1 - G/.y0).(J.t) by A2,FUNCT_1:13
.= (G/.y1).(J.t) - (G/.y0).(J.t) by LOPBAN_1:40;
U3: (F/.x1).t = (G/.y1).(J.t) by A2,H7,FUNCT_1:13;
(F/.x0).t = (G/.y0).(J.t) by A2,H8,FUNCT_1:13;
hence (Gy1y0*J).t = Fx1x0.t by U2,U3,LOPBAN_1:40;
end;
then Gy1y0*J = Fx1x0;
hence ||. G/.y1 - G/.y0 .|| < r by H5,LMX00;
end;
end;
hence G is_continuous_on E by P2,NFCONT_1:19;
end;
assume Q2: g `| E is_continuous_on E;
for x0 be Point of [:X,Y:],r be Real st x0 in Z & 0<r ex s be Real
st 0<s & for x1 be Point of [:X,Y:] st x1 in Z & ||. x1- x0 .|| < s
holds ||. F/.x1 - F/.x0 .|| < r
proof
let x0 be Point of [:X,Y:],
r be Real;
assume H1: x0 in Z & 0<r;
set y0 = J.x0;
I.y0 = x0 by A2,FUNCT_1:34;
then y0 in E by FUNCT_2:38,H1;
then consider s be Real such that
F10: 0 < s &
for y1 be Point of product <*X,Y*>
st y1 in E & ||. y1- y0 .|| < s
holds ||. G/.y1 - G/.y0 .|| < r by H1,Q2,NFCONT_1:19;
take s;
thus 0 < s by F10;
let x1 be Point of [:X,Y:];
assume H3: x1 in Z & ||. x1- x0 .|| < s;
set y1 = J.x1;
I.y1 = x1 by A2,FUNCT_1:34; then
G9: y1 in E by FUNCT_2:38,H3;
||. y1- y0 .|| = ||. x1-x0 .|| by X2;
then
H5: ||. G/.y1 - G/.y0 .|| < r by F10,G9,H3;
H7: F/.x1 = F.x1 by H3,P1,PARTFUN1:def 6
.= (G/.y1)*J by AS1,H3,IJ1,P1,LM166;
H8: F/.x0 = F.x0 by H1,P1,PARTFUN1:def 6
.= (G/.y0)*J by AS1,H1,IJ1,P1,LM166;
reconsider Gy1y0 = G/.y1 - G/.y0 as Lipschitzian LinearOperator
of product <*X,Y*>,W by LOPBAN_1:def 9;
reconsider Fx1x0 = F/.x1 - F/.x0 as Lipschitzian LinearOperator
of [:X,Y:],W by LOPBAN_1:def 9;
now
let t be VECTOR of [:X,Y:];
U2: ((G/.y1 - G/.y0)*J).t = (G/.y1 - G/.y0).(J.t) by A2,FUNCT_1:13
.= (G/.y1).(J.t) - (G/.y0).(J.t) by LOPBAN_1:40;
U3: (F/.x1).t = (G/.y1).(J.t) by A2,H7,FUNCT_1:13;
(F/.x0).t = (G/.y0).(J.t) by A2,H8,FUNCT_1:13;
hence (Gy1y0*J).t = Fx1x0.t by U2,U3,LOPBAN_1:40;
end;
then Gy1y0*J = Fx1x0;
hence ||. F/.x1 - F/.x0 .|| < r by H5,LMX00;
end;
hence f`|Z is_continuous_on Z by P1,NFCONT_1:19;
end;
theorem
for X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f be PartFunc of [:X,Y:], W
st Z is open holds
( 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 )
iff
f is_differentiable_on Z & f`|Z is_continuous_on Z
proof
let X, Y, W be RealNormSpace,
Z be Subset of [:X,Y:],
f be PartFunc of [:X,Y:], W;
assume AS: Z is open;
set I = (IsoCPNrSP(X,Y)");
set J = IsoCPNrSP(X,Y);
set g = f*I;
set E = I"Z;
X1: I = (IsoCPNrSP(X,Y)") & I is one-to-one onto &
( for x be Point of X, y be Point of Y holds I.<*x,y*> =[x,y] ) &
0. [:X,Y:] = I.(0.product <*X,Y*>) & I is isometric by defISOA1,defISOA2;
I"Z = J.:Z by FUNCT_1:84;
then OP1: E is open by AS,LM025;
D1: dom <*X,Y*> = Seg len <*X,Y*> by FINSEQ_1:def 3
.= Seg 2 by FINSEQ_1:44;
then
D2:1 in dom <*X,Y*>;
then In(1,dom<*X,Y*>)=1 by SUBSET_1:def 8;
then
BX1: <*X,Y*> .In(1,dom<*X,Y*>) = X;
D3: 2 in dom <*X,Y*> by D1;
then In(2,dom<*X,Y*>)=2 by SUBSET_1:def 8;
then
BX2: <*X,Y*> .In(2,dom<*X,Y*>) = Y;
JE1: J"E = J".: (I"Z) by FUNCT_1:85
.= Z by X1,FUNCT_1:77;
hereby
assume P1: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;
P2: g is_partial_differentiable_on E,1 by P1,LM300;
P3: g is_partial_differentiable_on E,2 by P1,LM300;
P4: f `partial`1|Z =g`partial|(E,1)*J by LM400,P1;
P5: f `partial`2|Z =g`partial|(E,2)*J by LM401,P1;
for i be set st i in dom <*X,Y*> holds
g is_partial_differentiable_on E,i & g`partial|(E,i) is_continuous_on E
proof
let i be set;
assume CX: i in dom <*X,Y*>;
then
C1: i = 1 or i = 2 by D1,TARSKI:def 2,FINSEQ_1:2;
thus g is_partial_differentiable_on E,i
by CX,D1,P2,P3,TARSKI:def 2,FINSEQ_1:2;
thus g`partial|(E,i) is_continuous_on E
by BX1,BX2,C1,P1,P4,P5,JE1,LM045;
end;
then
GF1: g is_differentiable_on E & g`|E is_continuous_on E
by NDIFF_5:57,OP1;
hence f is_differentiable_on Z by LM155;
hence f`|Z is_continuous_on Z by GF1,LMX1;
end;
assume X0: f is_differentiable_on Z & f`|Z is_continuous_on Z;
then
X1: g is_differentiable_on E by LM155;
X3: g`|E is_continuous_on E by X0,LMX1;
P2: g is_partial_differentiable_on E,1 by D2,OP1,X1,X3,NDIFF_5:57;
hence f is_partial_differentiable_on`1 Z by LM300;
P3: g is_partial_differentiable_on E,2 by D3,OP1,X1,X3,NDIFF_5:57;
hence f is_partial_differentiable_on`2 Z by LM300;
P6: g`partial|(E,1) is_continuous_on E by D2,OP1,X1,X3,NDIFF_5:57;
P7: g`partial|(E,2) is_continuous_on E by D3,OP1,X1,X3,NDIFF_5:57;
f `partial`1|Z =g`partial|(E,1)*J by P2,LM300,LM400;
hence f `partial`1|Z is_continuous_on Z by BX1,P6,LM045,JE1;
f `partial`2|Z = g`partial|(E,2)*J by P3,LM300,LM401;
hence f `partial`2|Z is_continuous_on Z by BX2,P7,LM045,JE1;
end;