:: Differentiation of Vector-Valued Functions on $n$-Dimensional Real Normed
:: Linear Spaces
:: by Takao Inou\'e , Noboru Endou and Yasunari Shidama
::
:: Received February 23, 2010
:: Copyright (c) 2010-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 PRE_TOPC, RLVECT_1, FUNCT_1, ARYTM_3, ARYTM_1, FINSEQ_1,
VALUED_1, MSSUBFAM, FINSEQ_2, CARD_3, RVSUM_1, RELAT_1, COMPLEX1,
SQUARE_1, RCOMP_1, PARTFUN1, NORMSP_1, XBOOLE_0, LOPBAN_1, FDIFF_1,
REAL_NS1, BORSUK_1, EUCLID, NUMBERS, FUNCOP_1, STRUCT_0, UNIALG_1,
EUCLID_7, MATRIXR2, RFINSEQ2, REAL_1, SUBSET_1, CARD_1, TARSKI, XXREAL_0,
NAT_1, ORDINAL4, SUPINF_2, VALUED_2, FCONT_1, XCMPLX_0;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
COMPLEX1, XREAL_0, REAL_1, NAT_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, FUNCOP_1, STRUCT_0, RLVECT_1, FINSEQ_1, FINSEQ_2, SQUARE_1,
VALUED_1, VALUED_2, RVSUM_1, VECTSP_1, PRE_TOPC, VFUNCT_1, NORMSP_0,
EUCLID, LOPBAN_1, NFCONT_1, NDIFF_1, REAL_NS1, PDIFF_1, INTEGR15,
EUCLID_7, RFINSEQ2;
constructors REAL_1, SQUARE_1, RSSPACE3, FINSEQOP, VFUNCT_1, COMPLEX1,
NFCONT_1, NDIFF_1, PDIFF_1, BINOP_2, MONOID_0, INTEGR15, RELSET_1,
EUCLID_7, RFINSEQ2, JORDAN2B, VALUED_2, XREAL_0;
registrations RELSET_1, STRUCT_0, XREAL_0, LOPBAN_1, FUNCT_2, NAT_1, REAL_NS1,
NUMBERS, XBOOLE_0, XXREAL_0, VALUED_0, EUCLID, CARD_1, VALUED_2,
SQUARE_1, FINSEQ_1, RVSUM_1, ORDINAL1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions LOPBAN_1;
equalities LOPBAN_1, RVSUM_1, EUCLID, VALUED_1, FINSEQ_1, XCMPLX_0, RFINSEQ2,
SQUARE_1;
expansions LOPBAN_1;
theorems TARSKI, ABSVALUE, XBOOLE_0, XBOOLE_1, EUCLID, XREAL_1, XCMPLX_0,
RLVECT_1, COMPLEX1, FINSEQ_1, FINSEQ_2, ORDINAL1, NAT_1, XXREAL_0,
RVSUM_1, RELAT_1, FUNCT_1, VFUNCT_1, FUNCT_2, SQUARE_1, INTEGR15,
FUNCOP_1, EUCLID_7, FINSEQ_4, FINSEQ_5, NORMSP_1, LOPBAN_1, PARTFUN1,
PARTFUN2, NFCONT_1, NDIFF_1, REAL_NS1, VALUED_1, PDIFF_1, RFINSEQ2,
RLVECT_4, JORDAN2C, VECTSP_1, NORMSP_0, VALUED_2, XREAL_0;
schemes FUNCT_2, NAT_1, FINSEQ_1, RECDEF_1;
begin
:: The Basic Properties for Differentiation of
:: Functions from $ {\cal R}^m$ to $ {\cal R}^n$
reserve i,n,m for Nat;
theorem Th1:
for f be set holds
f is PartFunc of REAL m,REAL n iff f is PartFunc of REAL-NS m,REAL-NS n
proof
let f be set;
the carrier of REAL-NS m = REAL m &
the carrier of REAL-NS n = REAL n by REAL_NS1:def 4;
hence thesis;
end;
theorem Th2:
for n,m be non zero Nat, f be PartFunc of REAL m,REAL n,
g be PartFunc of REAL-NS m,REAL-NS n,
x be Element of REAL m, y be Point of REAL-NS m st
f=g & x=y holds f is_differentiable_in x iff g is_differentiable_in y
proof
let n,m be non zero Nat,
f be PartFunc of REAL m,REAL n,
g be PartFunc of REAL-NS m,REAL-NS n,
x be Element of REAL m, y be Point of REAL-NS m;
assume A1: f=g & x=y;
hereby assume f is_differentiable_in x; then
ex g be PartFunc of REAL-NS m,REAL-NS n, y be Point of REAL-NS m st
f=g & x=y & g is_differentiable_in y by PDIFF_1:def 7;
hence g is_differentiable_in y by A1;
end;
assume g is_differentiable_in y;
hence f is_differentiable_in x by A1,PDIFF_1:def 7;
end;
theorem Th3:
for n,m be non zero Nat, f be PartFunc of REAL m,REAL n,
g be PartFunc of REAL-NS m,REAL-NS n,
x be Element of REAL m, y be Point of REAL-NS m st
f=g & x=y & f is_differentiable_in x holds diff(f,x) = diff(g,y)
proof
let n,m be non zero Nat,
f be PartFunc of REAL m,REAL n,
g be PartFunc of REAL-NS m,REAL-NS n,
x be Element of REAL m, y be Point of REAL-NS m;
assume A1: f=g & x=y & f is_differentiable_in x; then
ex g be PartFunc of REAL-NS m,REAL-NS n, y be Point of REAL-NS m st
f=g & x=y & diff(f,x) = diff(g,y) by PDIFF_1:def 8;
hence thesis by A1;
end;
theorem Th4:
for f1,f2 be PartFunc of REAL m,REAL n,
g1,g2 be PartFunc of REAL-NS m,REAL-NS n st
f1 = g1 & f2 = g2 holds f1 + f2 = g1 + g2
proof
let f1,f2 be PartFunc of REAL m,REAL n,
g1,g2 be PartFunc of REAL-NS m,REAL-NS n;
assume
A1: f1 = g1 & f2 = g2;
the carrier of REAL-NS m = REAL m &
the carrier of REAL-NS n = REAL n by REAL_NS1:def 4; then
reconsider g12 = g1 + g2 as PartFunc of REAL m,REAL n;
A2: dom f1 /\ dom f2 = dom g12 by A1,VFUNCT_1:def 1;
A3: f1<++>f2 = f1+f2 by INTEGR15:def 9;
for c be object st c in dom g12 holds (g1+g2).c = f1.c + f2.c
proof
let c be object;
assume
A4: c in dom g12;
then
A5: c in dom (g1+g2);
c in dom f1 & c in dom f2 by A2,A4,XBOOLE_0:def 4;
then
A6: f1/.c = f1.c & f2/.c = f2.c by PARTFUN1:def 6;
A7:f1/.c = g1/.c & f2/.c = g2/.c by A1,REAL_NS1:def 4;
g12.c = (g1 + g2)/.c by A4,PARTFUN1:def 6
.= g1/.c + g2/.c by A5,VFUNCT_1:def 1;
hence thesis by A6,A7,REAL_NS1:2;
end;
hence thesis by A2,A3,VALUED_2:def 45;
end;
theorem Th5:
for f1,f2 be PartFunc of REAL m,REAL n,
g1,g2 be PartFunc of REAL-NS m,REAL-NS n st
f1 = g1 & f2 = g2 holds f1 - f2 = g1 - g2
proof
let f1,f2 be PartFunc of REAL m,REAL n,
g1,g2 be PartFunc of REAL-NS m,REAL-NS n;
assume
A1: f1 = g1 & f2 = g2;
the carrier of REAL-NS m = REAL m &
the carrier of REAL-NS n = REAL n by REAL_NS1:def 4; then
reconsider g12 = g1 - g2 as PartFunc of REAL m,REAL n;
A2: dom f1 /\ dom f2 = dom g12 by A1,VFUNCT_1:def 2;
A3: f1<-->f2 = f1-f2 by INTEGR15:def 10;
for c be object st c in dom g12 holds (g1-g2).c = f1.c - f2.c
proof
let c be object;
assume
A4: c in dom g12;
then
A5: c in dom (g1-g2);
c in dom f1 & c in dom f2 by A2,A4,XBOOLE_0:def 4;
then
A6: f1/.c = f1.c & f2/.c = f2.c by PARTFUN1:def 6;
A7:f1/.c = g1/.c & f2/.c = g2/.c by A1,REAL_NS1:def 4;
g12.c = (g1 - g2)/.c by A4,PARTFUN1:def 6
.= g1/.c - g2/.c by A5,VFUNCT_1:def 2;
hence thesis by A6,A7,REAL_NS1:5;
end;
hence thesis by A2,A3,VALUED_2:def 46;
end;
theorem Th6:
for f be PartFunc of REAL m,REAL n,
g be PartFunc of REAL-NS m,REAL-NS n, a be Real st
f = g holds a(#)f = a(#)g
proof
let f be PartFunc of REAL m,REAL n,
g be PartFunc of REAL-NS m,REAL-NS n,
a be Real;
assume A1: f = g;
the carrier of REAL-NS m = REAL m
& the carrier of REAL-NS n = REAL n by REAL_NS1:def 4; then
reconsider aG = a(#)g as PartFunc of REAL m,REAL n;
A2:dom f = dom aG by A1,VFUNCT_1:def 4;
A3: a(#)f = f[#]a by INTEGR15:def 11;
for c be object st c in dom aG holds aG .c = a (#) (f.c)
proof
let c be object;
assume
A4: c in dom aG; then
A5:c in dom(a(#)g);
A6:f/.c = g/.c by A1,REAL_NS1:def 4;
A7: f/.c = f.c by A2,A4,PARTFUN1:def 6;
aG.c = (a(#)g)/.c by A4,PARTFUN1:def 6
.= a*(g/.c) by A5,VFUNCT_1:def 4;
hence aG.c = a(#)(f.c) by A6,A7,REAL_NS1:3;
end;
hence thesis by A2,A3,VALUED_2:def 39;
end;
theorem Th7:
for f1,f2 be Function of REAL m,REAL n, g1,g2 be Point of
R_NormSpace_of_BoundedLinearOperators(REAL-NS m,REAL-NS n) st
f1 = g1 & f2 = g2 holds f1 + f2 = g1 + g2
proof
let f1,f2 be Function of REAL m,REAL n,
g1,g2 be Point of
R_NormSpace_of_BoundedLinearOperators(REAL-NS m,REAL-NS n);
assume A1: f1 = g1 & f2 = g2;
A2:the carrier of REAL-NS m = REAL m
& the carrier of REAL-NS n = REAL n by REAL_NS1:def 4; then
reconsider g12 = g1 + g2 as Function of REAL m, REAL n by LOPBAN_1:def 9;
g1 is LinearOperator of REAL-NS m,REAL-NS n &
g2 is LinearOperator of REAL-NS m,REAL-NS n by LOPBAN_1:def 9; then
dom g1 = REAL m & dom g2 = REAL m by A2,FUNCT_2:def 1; then
A3:dom f1 /\ dom f2 = dom g12 by A1,FUNCT_2:def 1;
A4: f1<++>f2 = f1+f2 by INTEGR15:def 9;
for c be object st c in dom g12 holds g12.c = f1.c + f2.c
proof
let c be object;
assume
A5: c in dom g12;
then reconsider x = c as VECTOR of REAL-NS m by REAL_NS1:def 4;
reconsider c1 = c as Element of REAL m by A5;
g12.x = g1.x + g2.x by LOPBAN_1:35;
hence g12.c = f1/.c1 + f2/.c1 by A1,REAL_NS1:2
.= f1.c + f2.c;
end;
hence thesis by A3,A4,VALUED_2:def 45;
end;
theorem Th8:
for f1,f2 be Function of REAL m,REAL n, g1,g2 be Point of
R_NormSpace_of_BoundedLinearOperators(REAL-NS m,REAL-NS n) st
f1 = g1 & f2 = g2 holds f1 - f2 = g1 - g2
proof
let f1,f2 be Function of REAL m,REAL n,
g1,g2 be Point of
R_NormSpace_of_BoundedLinearOperators(REAL-NS m,REAL-NS n);
assume A1: f1 = g1 & f2 = g2;
A2:the carrier of REAL-NS m=REAL m
& the carrier of REAL-NS n= REAL n by REAL_NS1:def 4; then
reconsider g12 = g1 - g2 as Function of REAL m,REAL n by LOPBAN_1:def 9;
g1 is LinearOperator of REAL-NS m,REAL-NS n &
g2 is LinearOperator of REAL-NS m,REAL-NS n by LOPBAN_1:def 9; then
dom g1 = REAL m & dom g2 = REAL m by A2,FUNCT_2:def 1; then
A3:dom f1 /\ dom f2 = dom g12 by A1,FUNCT_2:def 1;
A4: f1<-->f2 = f1-f2 by INTEGR15:def 10;
for c be object st c in dom g12 holds g12.c = f1.c - f2.c
proof
let c be object;
assume
A5: c in dom g12;
then reconsider x = c as VECTOR of REAL-NS m by REAL_NS1:def 4;
reconsider c1 = c as Element of REAL m by A5;
g12.x = g1.x - g2.x by LOPBAN_1:40;
hence g12.c = f1/.c1 - f2/.c1 by A1,REAL_NS1:5
.= f1.c - f2.c;
end;
hence thesis by A3,A4,VALUED_2:def 46;
end;
theorem Th9:
for f be Function of REAL m,REAL n,
g be Point of R_NormSpace_of_BoundedLinearOperators(REAL-NS m,REAL-NS n),
r be Real st
f = g holds r(#)f = r*g
proof
let f be Function of REAL m,REAL n,
g be Point of
R_NormSpace_of_BoundedLinearOperators(REAL-NS m,REAL-NS n),
r be Real;
assume A1: f = g;
the carrier of REAL-NS m = REAL m
& the carrier of REAL-NS n = REAL n by REAL_NS1:def 4; then
reconsider rG = r*g as Function of REAL m,REAL n by LOPBAN_1:def 9;
dom f = REAL m by FUNCT_2:def 1; then
A2:dom f = dom rG by FUNCT_2:def 1;
A3: r(#)f = f[#]r by INTEGR15:def 11;
for c be object st c in dom rG holds rG.c = r(#)f.c
proof
let c be object;
assume
A4: c in dom rG;
then reconsider x = c as VECTOR of REAL-NS m by REAL_NS1:def 4;
reconsider c1 = c as Element of REAL m by A4;
rG.x = r* g.x by LOPBAN_1:36;
hence rG.c = r*f/.c1 by A1,REAL_NS1:3
.= r(#)f.c;
end;
hence thesis by A2,A3,VALUED_2:def 39;
end;
theorem Th10:
for m,n be non zero Nat
for f be PartFunc of REAL m,REAL n, x be Element of REAL m st
f is_differentiable_in x holds
diff(f,x) is
Point of R_NormSpace_of_BoundedLinearOperators(REAL-NS m,REAL-NS n)
proof
let m,n be non zero Nat;
let f be PartFunc of REAL m,REAL n,
x be Element of REAL m;
assume f is_differentiable_in x; then
ex g be PartFunc of REAL-NS m,REAL-NS n, y be Point of REAL-NS m st
f=g & x=y & diff(f,x) = diff(g,y) by PDIFF_1:def 8;
hence thesis;
end;
definition
let n,m be Nat;
let IT be Function of REAL m,REAL n;
attr IT is additive means :Def1:
for x,y being Element of REAL m holds IT.(x+y) = IT.x+IT.y;
attr IT is homogeneous means :Def2:
for x being Element of REAL m, r being Real holds IT.(r*x) = r*IT.x;
end;
theorem Th11:
for IT be Function of REAL m,REAL n st IT is additive holds IT.(0*m) = 0*n
proof
let IT be Function of REAL m,REAL n;
assume A1: IT is additive;
IT.(0*m) = IT.(0*m + 0*m) by RVSUM_1:16; then
IT.(0*m) = IT.(0*m) + IT.(0*m) by A1; then
0*n = IT.(0*m) + IT.(0*m) -(IT.(0*m)) by RVSUM_1:37;
hence 0*n = IT.(0*m) by RVSUM_1:42;
end;
theorem Th12:
for f be Function of REAL m,REAL n, g be Function of REAL-NS m,REAL-NS n st
f=g holds f is additive iff g is additive
proof
let f be Function of REAL m,REAL n,
g be Function of REAL-NS m,REAL-NS n;
assume A1: f=g;
hereby assume A2:f is additive;
now let x,y be Point of REAL-NS m;
reconsider x1=x,y1=y as Element of REAL m by REAL_NS1:def 4;
g.(x+y) = f.(x1+y1) by A1,REAL_NS1:2
.= f.x1+ f.y1 by A2;
hence g.(x+y) = g.x+ g.y by A1,REAL_NS1:2;
end;
hence g is additive by VECTSP_1:def 20;
end;
assume A3:g is additive;
now let x,y be Element of REAL m;
reconsider x1=x, y1=y as Point of REAL-NS m by REAL_NS1:def 4;
f.(x+y) = g.(x1+y1) by A1,REAL_NS1:2
.= g.x1+ g.y1 by A3,VECTSP_1:def 20;
hence f.(x+y) = f.x+ f.y by A1,REAL_NS1:2;
end;
hence f is additive;
end;
theorem Th13:
for f be Function of REAL m,REAL n, g be Function of REAL-NS m,REAL-NS n st
f=g holds f is homogeneous iff g is homogeneous
proof
let f be Function of REAL m,REAL n,
g be Function of REAL-NS m,REAL-NS n;
assume A1: f=g;
hereby assume A2:f is homogeneous;
now let x be Point of REAL-NS m ,r be Real;
reconsider x1=x as Element of REAL m by REAL_NS1:def 4;
g.(r*x) = f.(r*x1) by A1,REAL_NS1:3
.= r*(f.x1) by A2;
hence g.(r*x) = r*(g.x) by A1,REAL_NS1:3;
end;
hence g is homogeneous;
end;
assume A3:g is homogeneous;
now let x being Element of REAL m, r be Real;
reconsider x1=x as Point of REAL-NS m by REAL_NS1:def 4;
f.(r*x) = g.(r*x1) by A1,REAL_NS1:3
.= r*(g.x1) by A3;
hence f.(r*x) = r*(f.x) by A1,REAL_NS1:3;
end;
hence f is homogeneous;
end;
registration
let n,m be Nat;
cluster (REAL m) --> 0*n -> additive homogeneous for
Function of REAL m,REAL n;
coherence
proof
let f be Function of REAL m,REAL n such that
A1: f = (REAL m) --> 0*n;
reconsider n1=n as Nat;
hereby let x,y be Element of REAL m;
A2: 0.(REAL-NS n1) = 0*n by REAL_NS1:def 4;
f.(x+y) = 0*n by A1,FUNCOP_1:7
.= 0.(REAL-NS n1) by REAL_NS1:def 4
.= 0.(REAL-NS n1)+0.(REAL-NS n1) by RLVECT_1:4
.= 0*n+0*n by A2,REAL_NS1:2
.= f.x+0*n by A1,FUNCOP_1:7;
hence f.(x+y) = f.x+f.y by A1,FUNCOP_1:7;
end;
hereby let x be Element of REAL m, r be Real;
A3: 0.(REAL-NS n1) = 0*n by REAL_NS1:def 4;
f.(r*x) = 0*n by A1,FUNCOP_1:7
.= 0.(REAL-NS n1) by REAL_NS1:def 4
.=r*(0.(REAL-NS n1)) by RLVECT_1:10
.=r*(0*n) by A3,REAL_NS1:3;
hence f.(r*x) = r*f.x by A1,FUNCOP_1:7;
end;
end;
end;
registration
let n,m be Nat;
cluster additive homogeneous for Function of REAL m,REAL n;
existence
proof
take (REAL m) --> 0*n;
thus thesis;
end;
end;
definition let m,n be Nat;
mode LinearOperator of m,n
is additive homogeneous Function of REAL m,REAL n;
end;
theorem Th14:
for f be set holds f is LinearOperator of m,n
iff f is LinearOperator of REAL-NS m,REAL-NS n
proof
let f be set;
REAL m = the carrier of REAL-NS m
& REAL n = the carrier of REAL-NS n by REAL_NS1:def 4;
hence f is additive homogeneous Function of REAL m,REAL n
iff f is additive homogeneous Function of REAL-NS m,REAL-NS n
by Th12,Th13;
end;
definition let m,n be Nat, IT be Function of REAL m,REAL n;
attr IT is Lipschitzian means :Def3:
ex K being Real st 0 <= K &
for x being Element of REAL m holds |. IT.x .| <= K * |. x .|;
end;
theorem Th15:
for xseq,yseq be FinSequence of REAL m st
len xseq = len yseq + 1 & xseq| (len yseq) = yseq holds
ex v be Element of REAL m st v=xseq.(len xseq) & Sum xseq = Sum yseq + v
proof
let xseq,yseq be FinSequence of REAL m;
assume A1: len xseq = len yseq + 1 & xseq| (len yseq) = yseq;
A2:len xseq= len (accum xseq) & xseq.1=(accum xseq).1 &
(for k being Nat st 1<=k & k<len xseq holds
(accum xseq).(k+1)=(accum xseq)/.k+xseq/.(k+1)) by EUCLID_7:def 10;
A3:Sum xseq=(accum xseq).(len xseq) by A1,EUCLID_7:def 11;
set g = accum xseq;
set i= len yseq;
per cases;
suppose A4: i= 0; then
reconsider v = xseq.(len xseq) as Element of REAL m
by A1,A3,EUCLID_7:def 10;
take v;
Sum yseq = 0*m by A4,EUCLID_7:def 11;
hence v = xseq.(len xseq) & Sum xseq = Sum yseq + v
by A1,A2,A3,A4,RVSUM_1:16;
end;
suppose A5: i <> 0;
A6: len yseq=len (accum yseq) & yseq.1=(accum yseq).1
& (for k being Nat st 1<=k & k<len yseq holds
(accum yseq).(k+1)=(accum yseq)/.k + yseq/.(k+1)) by EUCLID_7:def 10;
A7: Sum yseq = (accum yseq).i by A5,EUCLID_7:def 11;
set g0 = accum yseq;
A8: i <= len g by A1,A2,NAT_1:11; then
A9: len(g|i) = i by FINSEQ_1:59;
A10: for k be Nat st 1 <= k & k <= len(g|i) holds (g|i).k = g0.k
proof
defpred PP[Nat] means
1 <= $1 & $1 <= len(g|i) implies (g|i).$1 = g0.$1;
A11: PP[0];
A12: now let k be Nat;
assume A13: PP[k];
now assume A14: 1 <= k+1 & k+1 <= len(g|i); then
A15: k+1 <= len yseq by A8,FINSEQ_1:59; then
k+1 in Seg i by A14; then
A16: (g|i).(k+1) = g.(k+1) & xseq.(k+1) = (xseq|Seg i).(k+1) by FUNCT_1:49;
A17: k < len yseq by A15,NAT_1:13;
now assume A18: k<>0; then
A19: 1 <= k by NAT_1:14; then
A20: k in Seg i by A17;
len yseq <= len xseq by A1,NAT_1:12; then
A21: k < len xseq by A17,XXREAL_0:2; then
g/.k = g.k by A2,A19,FINSEQ_4:15; then
g/.k = (g|i).k by A20,FUNCT_1:49; then
A22: g/.k = g0/.k by A6,A17,A19,A13,A14,FINSEQ_4:15,NAT_1:13;
k+1 <= len xseq by A15,A1,NAT_1:12; then
xseq/.(k+1) = xseq.(k+1) by A14,FINSEQ_4:15; then
xseq/.(k+1) = yseq/.(k+1) by A1,A14,A9,A16,FINSEQ_4:15; then
(g/.k)+(xseq/.(k+1)) = g0.(k+1) by A6,A17,A18,A22,NAT_1:14;
hence (g|i).(k+1) = g0.(k+1) by A2,A16,A18,A21,NAT_1:14;
end;
hence (g|i).(k+1) = g0.(k+1) by A1,A6,A16,EUCLID_7:def 10;
end;
hence PP[k+1];
end;
thus for k be Nat holds PP[k] from NAT_1:sch 2(A11,A12);
end;
1 <= i by A5,NAT_1:14; then
i in Seg i; then
A23:i in dom(g|i) by A9,FINSEQ_1:def 3; then
i in dom g by RELAT_1:57; then
g.i = g/.i by PARTFUN1:def 6; then
(g|i).i = g/.i by A23,FUNCT_1:47; then
A24:g0.i = g/.i by A6,A9,A10,FINSEQ_1:14;
dom xseq = Seg (i+1) by A1,FINSEQ_1:def 3; then
xseq.(len xseq) in rng xseq by A1,FINSEQ_1:4,FUNCT_1:3; then
reconsider v=xseq.(len xseq) as Element of REAL m;
take v;
thus v=xseq.(len xseq);
A25:i < len xseq by A1,NAT_1:13;
1<=i+1 by NAT_1:11; then
g/.i + xseq/.(i+1) = Sum yseq + v by A7,A24,A1,FINSEQ_4:15;
hence Sum xseq = Sum yseq + v by A1,A25,A2,A3,A5,NAT_1:14;
end;
end;
theorem Th16:
for f be LinearOperator of m,n, xseq be FinSequence of REAL m,
yseq be FinSequence of REAL n st
len xseq = len yseq &
( for i be Nat st i in dom xseq holds yseq.i=f.(xseq.i) )
holds Sum yseq=f.(Sum xseq)
proof
let f be LinearOperator of m,n;
defpred P[Nat] means
for xseq be FinSequence of REAL m, yseq be FinSequence of REAL n st
$1= len xseq & len xseq = len yseq &
for i be Nat st i in dom xseq holds yseq.i=f.(xseq.i)
holds Sum yseq = f.(Sum xseq);
A1:P[0]
proof
let xseq be FinSequence of REAL m, yseq be FinSequence of REAL n;
assume 0 = len xseq & len xseq = len yseq &
for i be Nat st i in dom xseq holds yseq.i=f.(xseq.i); then
Sum xseq = 0*m & Sum yseq = 0*n by EUCLID_7:def 11;
hence thesis by Th11;
end;
A2:now let i be Nat;
assume A3: P[i];
now let xseq be FinSequence of REAL m, yseq be FinSequence of REAL n;
assume A4: i+1=len xseq & len xseq = len yseq &
for k be Nat st k in dom xseq holds yseq.k=f.(xseq.k);
set xseq0=xseq|i, yseq0=yseq|i;
A5: i=len xseq0 by A4,FINSEQ_1:59,NAT_1:11; then
A6: len xseq0 = len yseq0 by A4,FINSEQ_1:59,NAT_1:11;
for k be Nat st k in dom xseq0 holds yseq0.k=f.(xseq0.k)
proof
let k be Nat;
assume A7: k in dom xseq0; then
A8: k in Seg i by RELAT_1:57;
k in dom xseq by A7,RELAT_1:57; then
A9: yseq.k=f.(xseq.k) by A4;
xseq.k = xseq0.k by A8,FUNCT_1:49;
hence yseq0.k = f.(xseq0.k) by A8,A9,FUNCT_1:49;
end; then
A10:Sum yseq0 = f.(Sum xseq0) by A5,A6,A3;
consider v be Element of REAL m such that
A11: v=xseq.(len xseq) & Sum xseq = Sum xseq0 + v by A4,A5,Th15;
consider w be Element of REAL n such that
A12:w=yseq.(len yseq) & Sum yseq = Sum yseq0 + w by A4,A5,A6,Th15;
dom xseq = Seg (i+1) by A4,FINSEQ_1:def 3; then
w =f.v by A4,A12,A11,FINSEQ_1:4;
hence Sum yseq =f.(Sum xseq) by A10,A11,A12,Def1;
end;
hence P[i+1];
end;
A13:for k be Nat holds P[k] from NAT_1:sch 2(A1,A2);
let xseq be FinSequence of REAL m, yseq be FinSequence of REAL n;
assume len xseq = len yseq &
for i be Nat st i in dom xseq holds yseq.i=f.(xseq.i);
hence Sum yseq = f.(Sum xseq) by A13;
end;
theorem Th17:
for xseq be FinSequence of REAL m, yseq be FinSequence of REAL st
len xseq = len yseq &
( for i be Nat st i in dom xseq holds
ex v be Element of REAL m st v = xseq.i & yseq.i = |.v .| )
holds |.Sum xseq.| <= Sum yseq
proof
defpred P[Nat] means
for xseq be FinSequence of REAL m, yseq be FinSequence of REAL st
$1=len xseq & len xseq = len yseq &
( for i be Nat st i in dom xseq holds
ex v be Element of REAL m st v=xseq.i & yseq.i=|.v .| )
holds |.Sum xseq.| <= Sum yseq;
A1:P[0]
proof
let xseq be FinSequence of REAL m, yseq be FinSequence of REAL;
assume 0=len xseq & len xseq = len yseq &
( for i be Nat st i in dom xseq holds
ex v be Element of REAL m st v = xseq.i & yseq.i = |.v .| ); then
Sum xseq = 0*m & <*> REAL = yseq by EUCLID_7:def 11;
hence thesis by EUCLID:7,RVSUM_1:72;
end;
A2:now let i be Nat;
assume A3: P[i];
now let xseq be FinSequence of REAL m, yseq be FinSequence of REAL;
set xseq0=xseq|i, yseq0=yseq|i;
assume
A4: i+1=len xseq & len xseq = len yseq &
( for i be Nat st i in dom xseq holds
ex v be Element of REAL m st v=xseq.i & yseq.i=|.v .|);
A5: for k be Nat st k in dom xseq0 holds
ex v be Element of REAL m st v=xseq0.k & yseq0.k=|.v .|
proof
let k be Nat;
assume k in dom xseq0; then
A6: k in Seg i & k in dom xseq by RELAT_1:57; then
consider v be Element of REAL m such that
A7: v=xseq.k & yseq.k=|.v .| by A4;
take v;
thus thesis by A6,A7,FUNCT_1:49;
end;
dom xseq = Seg(i+1) by A4,FINSEQ_1:def 3; then
consider w be Element of REAL m such that
A8: w=xseq.(i+1) & yseq.(i+1)=|.w .| by A4,FINSEQ_1:4;
A9: 1 <= i + 1 & i + 1 <= len yseq by A4,NAT_1:11;
yseq = (yseq|i)^<*yseq/.(i+1) *> by A4,FINSEQ_5:21; then
yseq = yseq0 ^<*(yseq.(i+1))*> by A9,FINSEQ_4:15; then
A10: Sum yseq = Sum yseq0 + yseq.(i+1) by RVSUM_1:74;
A11: i=len xseq0 by A4,FINSEQ_1:59,NAT_1:11; then
A12: ex v be Element of REAL m st v=xseq.(len xseq)
& Sum xseq = Sum xseq0 + v by A4,Th15;
A13: |. Sum xseq0 + w.|<= |.Sum xseq0 .| + |. w .| by EUCLID:12;
len xseq0 = len yseq0 by A4,A11,FINSEQ_1:59,NAT_1:11; then
|. Sum xseq0 .| <= Sum yseq0 by A3,A5,A11; then
|. Sum xseq0 .| + |. w .| <= Sum yseq0 + yseq.(i+1) by A8,XREAL_1:6;
hence |. Sum xseq .| <= Sum yseq by A4,A8,A10,A12,A13,XXREAL_0:2;
end;
hence P[i+1];
end;
for i be Nat holds P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
registration
let m,n be Nat;
cluster -> Lipschitzian for LinearOperator of m,n;
coherence
proof
let f be LinearOperator of m,n;
A1: m in NAT & n in NAT by ORDINAL1:def 12;
defpred KSX[Nat,object] means $2 = |. f.(Base_FinSeq(m,$1)) .|;
A2:for k0 be Nat st k0 in Seg m holds ex v be Element of REAL st KSX[k0,v]
proof let k0 be Nat;
assume k0 in Seg m;
consider v be Real such that
A3: KSX[k0,v];
reconsider v as Element of REAL by XREAL_0:def 1;
KSX[k0,v] by A3;
hence thesis;
end;
consider KS be FinSequence of REAL such that
A4: dom KS = Seg m &
for i be Nat st i in Seg m holds KSX[i,KS.i] from FINSEQ_1:sch 5(A2);
set K = Sum KS + 1;
now let j be Nat;
assume j in dom KS; then
KS.j = |. f.(Base_FinSeq(m,j)) .| by A4;
hence 0 <= KS.j;
end; then
A5:0 <= Sum KS by RVSUM_1:84;
reconsider m0=m as Nat;
now let x be Element of REAL m;
A6: len (ProjFinSeq x) = m by EUCLID_7:def 12;
defpred PFX[set,set] means $2=f.((ProjFinSeq x).$1);
A7: now let k be Nat;
assume k in Seg m; then
k in dom (ProjFinSeq x) by A6,FINSEQ_1:def 3; then
reconsider v= (ProjFinSeq x).k as Element of REAL m by PARTFUN1:4;
f.v is Element of REAL n;
hence ex x being Element of REAL n st PFX[k,x];
end;
consider fx be FinSequence of REAL n such that
A8: dom fx = Seg m &
for i be Nat st i in Seg m holds PFX[i,fx.i] from FINSEQ_1:sch 5(A7);
A9: x= Sum (ProjFinSeq x) & len fx = m by A1,A8,EUCLID_7:31,FINSEQ_1:def 3;
now let i be Nat;
assume i in dom (ProjFinSeq x); then
i in Seg m by A6,FINSEQ_1:def 3;
hence fx.i = f.((ProjFinSeq x).i) by A8;
end; then
A10: Sum fx = f.x by A6,A9,Th16;
reconsider x0 = x as Element of REAL m;
A11: for i being Nat st 1<=i & i<=m holds ex v be Element of REAL n st
v=fx.i & |. v .| <= |.x .| * |. f.(Base_FinSeq(m,i)) .|
proof
let i being Nat;
assume A12: 1<=i & i<=m; then
A13: (ProjFinSeq x).i = |( x,Base_FinSeq(m,i) )|*Base_FinSeq(m,i)
by EUCLID_7:def 12;
A14: i in Seg m by A12; then
reconsider v=fx.i as Element of REAL n by A8,PARTFUN1:4;
take v;
v = f.((ProjFinSeq x).i) by A8,A14; then
v = |(x,Base_FinSeq(m,i))| * f.(Base_FinSeq(m,i)) by A13,Def2; then
v = x0.i * f.(Base_FinSeq(m,i)) by A12,EUCLID_7:30; then
|. v .| = |. x0.i .|*|. f.(Base_FinSeq(m,i)) .| by EUCLID:11;
hence thesis by A14,REAL_NS1:8,XREAL_1:64;
end;
defpred ZFX[set,set] means
ex v be Element of REAL n st v=fx.$1 & $2=|.v .|;
A15:now let k be Nat;
assume k in Seg m; then
reconsider v= fx.k as Element of REAL n by A8,PARTFUN1:4;
|.v .| in REAL by XREAL_0:def 1;
hence ex x being Element of REAL st ZFX[k,x];
end;
consider zfx be FinSequence of REAL such that
A16: dom zfx = Seg m &
for i be Nat st i in Seg m holds ZFX[i,zfx.i] from FINSEQ_1:sch 5(A15);
A17:len zfx = m by A1,A16,FINSEQ_1:def 3; then
A18:len fx = len zfx by A8,FINSEQ_1:def 3;
for i be Nat st i in dom fx holds
ex v be Element of REAL n st v=fx.i & zfx.i=|.v .| by A8,A16; then
A19: |. f.x .| <= Sum zfx by A10,A18,Th17;
A20:now let j be Nat;
assume A21: j in Seg m; then
A22: ex v be Element of REAL n st v=fx.j & zfx.j=|.v .| by A16;
1<=j & j<=m by A21,FINSEQ_1:1; then
ex v be Element of REAL n st
v = fx.j & |. v .| <= |.x .| * |. f.(Base_FinSeq(m,j)) .| by A11; then
zfx.j <= |.x .| * KS.j by A4,A21,A22;
hence zfx.j <= (|.x .| * KS).j by VALUED_1:6;
end;
A23:zfx is Element of m-tuples_on REAL by A17,FINSEQ_2:92;
len KS = m by A1,A4,FINSEQ_1:def 3; then
reconsider KS0=KS as Element of REAL m0 by FINSEQ_2:92;
(|.x .| * KS0) is Element of m0-tuples_on REAL; then
Sum zfx <= Sum(|.x .| * KS) by A20,A23,RVSUM_1:82; then
Sum zfx <= |.x .| * Sum KS by RVSUM_1:87; then
A24: |. f.x .| <= |.x .| * Sum KS by A19,XXREAL_0:2;
0 + Sum KS <= 1+ Sum KS by XREAL_1:6; then
|.x .| * Sum KS <= |.x .| * (1+ Sum KS) by XREAL_1:64;
hence |.f.x .| <= K * |.x .| by A24,XXREAL_0:2;
end;
hence thesis by A5;
end;
end;
registration
let m,n;
cluster -> Lipschitzian for LinearOperator of REAL-NS m,REAL-NS n;
coherence
proof
let f be LinearOperator of REAL-NS m,REAL-NS n;
reconsider g=f as LinearOperator of m,n by Th14;
consider K being Real such that
A1: 0 <= K & for x being Element of REAL m holds |. g.x .| <= K * |. x .|
by Def3;
take K;
thus 0 <= K by A1;
let x being Point of REAL-NS m;
reconsider x1=x as Element of REAL m by REAL_NS1:def 4;
reconsider y= g.x1 as Element of REAL n;
||. f.x .|| = |.y.| by REAL_NS1:1; then
||. f.x .|| <= K * |.x1.| by A1;
hence ||. f.x .|| <= K * ||. x .|| by REAL_NS1:1;
end;
end;
theorem Th18:
for m,n be non zero Nat,
f be PartFunc of REAL m,REAL n, x be Element of REAL m st
f is_differentiable_in x holds
diff(f,x) is LinearOperator of REAL-NS m,REAL-NS n
proof
let m,n be non zero Nat;
let f be PartFunc of REAL m,REAL n,
x be Element of REAL m;
assume f is_differentiable_in x; then
diff(f,x) is Point of R_NormSpace_of_BoundedLinearOperators
(REAL-NS m,REAL-NS n) by Th10;
hence thesis by LOPBAN_1:def 9;
end;
theorem
for m,n be non zero Nat,
f be PartFunc of REAL m,REAL n, x be Element of REAL m st
f is_differentiable_in x holds
diff(f,x) is LinearOperator of m, n
proof
let m,n be non zero Nat;
let f be PartFunc of REAL m,REAL n, x be Element of REAL m;
assume f is_differentiable_in x; then
diff(f,x) is LinearOperator of REAL-NS m,REAL-NS n by Th18;
hence thesis by Th14;
end;
theorem
for n,m be non zero Nat, g1,g2 be PartFunc of REAL m,REAL n,
y0 be Element of REAL m st
g1 is_differentiable_in y0 & g2 is_differentiable_in y0 holds
g1+g2 is_differentiable_in y0 &
diff(g1+g2,y0) = diff(g1,y0) + diff(g2,y0)
proof
let n,m be non zero Nat,
g1,g2 be PartFunc of REAL m,REAL n,
y0 be Element of REAL m;
assume A1: g1 is_differentiable_in y0 & g2 is_differentiable_in y0;
reconsider f1=g1 as PartFunc of REAL-NS m,REAL-NS n by Th1;
reconsider f2=g2 as PartFunc of REAL-NS m,REAL-NS n by Th1;
reconsider x0=y0 as Point of REAL-NS m by REAL_NS1:def 4;
f1 is_differentiable_in x0 & f2 is_differentiable_in x0 by A1,Th2; then
A2:f1+f2 is_differentiable_in x0 & diff(f1+f2,x0)=diff(f1,x0)+diff(f2,x0)
by NDIFF_1:35;
f1+f2 = g1+g2 by Th4;
hence g1+g2 is_differentiable_in y0 by A2,Th2; then
A3:diff(g1+g2,y0) = diff(f1+f2,x0) by Th4,Th3;
diff(f1,x0) = diff(g1,y0) & diff(f2,x0) = diff(g2,y0) by Th3,A1;
hence diff(g1+g2,y0) = diff(g1,y0)+diff(g2,y0) by A2,A3,Th7;
end;
theorem
for n,m be non zero Nat, g1,g2 be PartFunc of REAL m,REAL n,
y0 be Element of REAL m st
g1 is_differentiable_in y0 & g2 is_differentiable_in y0 holds
g1-g2 is_differentiable_in y0 &
diff(g1-g2,y0) = diff(g1,y0) - diff(g2,y0)
proof
let n,m be non zero Nat,
g1,g2 be PartFunc of REAL m,REAL n,
y0 be Element of REAL m;
assume A1: g1 is_differentiable_in y0 & g2 is_differentiable_in y0;
reconsider f1=g1 as PartFunc of REAL-NS m,REAL-NS n by Th1;
reconsider f2=g2 as PartFunc of REAL-NS m,REAL-NS n by Th1;
reconsider x0=y0 as Point of REAL-NS m by REAL_NS1:def 4;
f1 is_differentiable_in x0 & f2 is_differentiable_in x0 by A1,Th2; then
A2:f1-f2 is_differentiable_in x0 & diff(f1-f2,x0)=diff(f1,x0)-diff(f2,x0)
by NDIFF_1:36;
f1-f2 = g1-g2 by Th5;
hence g1-g2 is_differentiable_in y0 by A2,Th2; then
A3:diff(g1-g2,y0) = diff(f1-f2,x0) by Th3,Th5;
diff(f1,x0) = diff(g1,y0) & diff(f2,x0) = diff(g2,y0) by Th3,A1;
hence diff(g1-g2,y0) = diff(g1,y0)-diff(g2,y0) by A2,A3,Th8;
end;
theorem
for n,m be non zero Nat, g be PartFunc of REAL m,REAL n,
y0 be Element of REAL m, r be Real st
g is_differentiable_in y0 holds
r(#)g is_differentiable_in y0 & diff((r(#)g),y0) = r(#)diff(g,y0)
proof
let n,m be non zero Nat,
g be PartFunc of REAL m,REAL n,
y0 be Element of REAL m, r be Real;
assume A1: g is_differentiable_in y0;
reconsider f=g as PartFunc of REAL-NS m,REAL-NS n by Th1;
reconsider x0=y0 as Point of REAL-NS m by REAL_NS1:def 4;
f is_differentiable_in x0 by A1,Th2; then
A2:r(#)f is_differentiable_in x0 & diff(r(#)f,x0)=r*diff(f,x0) by NDIFF_1:37;
r(#)f = r(#)g by Th6;
hence r(#)g is_differentiable_in y0 by A2,Th2; then
diff(r(#)g,y0) = diff(r(#)f,x0) by Th3,Th6;
hence diff(r(#)g,y0) = r(#)diff(g,y0) by A2,Th9,Th3,A1;
end;
theorem Th23:
for x0 be Element of REAL m, y0 be Point of REAL-NS m,
r be Real st x0=y0 holds
{y where y is Element of REAL m: |.y-x0.| < r}
= {z where z is Point of REAL-NS m: ||.z-y0.|| < r}
proof
let x0 be Element of REAL m, y0 be Point of REAL-NS m, r be Real;
assume A1: x0=y0;
now let w be object;
assume w in {y where y is Element of REAL m: |.y-x0.| < r}; then
consider y be Element of REAL m such that
A2: y=w & |.y-x0.| < r;
reconsider z=y as Point of REAL-NS m by REAL_NS1:def 4;
||.z-y0.|| < r by A1,A2,REAL_NS1:1,5;
hence w in {z1 where z1 is Point of REAL-NS m: ||.z1-y0.|| < r} by A2;
end; then
A3: {y where y is Element of REAL m: |.y-x0.| < r}
c= {z where z is Point of REAL-NS m: ||.z-y0.|| < r} by TARSKI:def 3;
now let w be object;
assume w in {z where z is Point of REAL-NS m: ||.z-y0.|| < r}; then
consider y be Point of REAL-NS m such that
A4: y=w & ||.y-y0.|| < r;
reconsider z=y as Element of REAL m by REAL_NS1:def 4;
|.z-x0.| < r by A1,A4,REAL_NS1:1,5;
hence w in {z1 where z1 is Element of REAL m: |.z1-x0.| < r} by A4;
end; then
{z where z is Point of REAL-NS m: ||.z-y0.|| < r}
c= {y where y is Element of REAL m: |.y-x0.| < r} by TARSKI:def 3;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem Th24:
for m,n be non zero Nat,
f be PartFunc of REAL m,REAL n, x0 be Element of REAL m,
L,R be Function of REAL m,REAL n st
L is LinearOperator of m,n &
ex r0 be Real st
0 < r0 & {y where y is Element of REAL m: |.y-x0.| < r0} c= dom f &
(for r be Real st r > 0
ex d be Real st d > 0 &
(for z be Element of REAL m,w be Element of REAL n st
z <> 0*m & |.z.| < d & w = R.z holds (|.z.|"* |. w .|) < r) ) &
for x be Element of REAL m st|.x-x0.| < r0 holds
f/.x - f/.x0 = L.(x-x0) + R.(x-x0)
holds
f is_differentiable_in x0 & diff(f,x0) = L
proof
let m,n be non zero Nat;
let f be PartFunc of REAL m,REAL n,
x0 be Element of REAL m,
L,R be Function of REAL m,REAL n;
reconsider g=f as PartFunc of REAL-NS m,REAL-NS n by Th1;
reconsider y0=x0 as Point of REAL-NS m by REAL_NS1:def 4;
assume A1: L is LinearOperator of m,n;
given r0 be Real such that
A2:0 < r0 & {y where y is Element of REAL m: |.y-x0.| < r0} c= dom f &
(for r be Real st r > 0
ex d be Real st d > 0 &
(for z be Element of REAL m,w be Element of REAL n st
z <> 0*m & |.z.| < d & w=R.z holds (|.z.|"* |. w .|) < r)) &
for x be Element of REAL m st |.x-x0.| < r0 holds
f/.x - f/.x0 = L.(x-x0) + R.(x-x0);
L is LinearOperator of REAL-NS m,REAL-NS n by A1,Th14; then
reconsider GL=L as Point of R_NormSpace_of_BoundedLinearOperators
(REAL-NS m,REAL-NS n) by LOPBAN_1:def 9;
REAL m = the carrier of REAL-NS m &
REAL n = the carrier of REAL-NS n by REAL_NS1:def 4; then
reconsider GR=R as Function of REAL-NS m,REAL-NS n;
the carrier of REAL-NS m = REAL m by REAL_NS1:def 4; then
A3: dom R = the carrier of REAL-NS m by FUNCT_2:def 1;
now let r be Real;
assume r > 0; then
consider d be Real such that
A4: d > 0 & (for z be Element of REAL m,w be Element of REAL n st
z <> 0*m & |.z.| < d & w=R.z holds (|.z.|"* |. w .|) < r) by A2;
take d;
thus d > 0 by A4;
thus for z be Point of REAL-NS m st
z <> 0.(REAL-NS m) & ||.z.|| < d holds (||.z.||"* ||. GR/.z .||) < r
proof
let z be Point of REAL-NS m;
assume A5: z <> 0.(REAL-NS m) & ||.z.|| < d;
reconsider s=z as Element of REAL m by REAL_NS1:def 4;
reconsider w = R.s as Element of REAL n;
A6: s <> 0*m by A5,REAL_NS1:def 4;
|. s .| < d by A5,REAL_NS1:1; then
(|. s .|"* |. w .|) < r by A4,A6; then
(||.z.||"* |. w .|) < r by REAL_NS1:1;
hence (||.z.||"* ||. GR/.z .||) < r by REAL_NS1:1;
end;
end; then
reconsider GR as RestFunc of REAL-NS m,REAL-NS n by NDIFF_1:23;
set N = {y where y is Point of REAL-NS m : ||.y-y0.|| < r0};
reconsider N as Neighbourhood of y0 by A2,NFCONT_1:3;
A7: N c= dom g by A2,Th23;
A8:for y be Point of REAL-NS m st y in N holds
g/.y - g/.y0 = GL.(y-y0) + GR/.(y-y0)
proof
let y be Point of REAL-NS m;
assume A9: y in N;
reconsider x=y as Element of REAL m by REAL_NS1:def 4;
x in {s where s is Element of REAL m: |.s-x0.| < r0} by A9,Th23; then
ex s be Element of REAL m st s=x & |.s-x0.| < r0; then
A10: f/.x - f/.x0 = L.(x-x0) + R.(x-x0) by A2;
A11:y0 in N by NFCONT_1:4; then
f/.x = f.x & f/.x0 = f.x0 by A9,A7,PARTFUN1:def 6; then
A12:f/.x = g/.y & f/.x0 = g/.y0 by A9,A11,A7,PARTFUN1:def 6;
x-x0 = y-y0 by REAL_NS1:5; then
L.(x-x0) = GL.(y-y0) & R.(x-x0) = GR/.(y-y0) by A3,PARTFUN1:def 6; then
L.(x-x0) + R.(x-x0)= GL.(y-y0) + GR/.(y-y0) by REAL_NS1:2;
hence g/.y -g/.y0 = GL.(y-y0) + GR/.(y-y0) by A10,A12,REAL_NS1:5;
end; then
A13:g is_differentiable_in y0 by A7,NDIFF_1:def 6;
hence
A14: f is_differentiable_in x0 by Th2;
diff(g,y0)= GL by A13,A8,A7,NDIFF_1:def 7;
hence thesis by Th3,A14;
end;
theorem
for m,n be non zero Nat,
f be PartFunc of REAL m,REAL n, x0 be Element of REAL m holds
f is_differentiable_in x0
iff
ex r0 be Real st 0 < r0 &
{y where y is Element of REAL m: |.y-x0.| < r0} c= dom f &
ex L,R be Function of REAL m,REAL n st
L is LinearOperator of m,n &
(for r be Real st r > 0
ex d be Real st d > 0 &
(for z be Element of REAL m,w be Element of REAL n st
z <> 0*m & |.z.| < d & w=R.z holds (|.z.|"* |. w .|) < r)) &
for x be Element of REAL m st |.x-x0.| < r0 holds
f/.x - f/.x0 = L.(x-x0) + R.(x-x0)
proof
let m,n be non zero Nat;
let f be PartFunc of REAL m,REAL n,
x0 be Element of REAL m;
reconsider g=f as PartFunc of REAL-NS m,REAL-NS n by Th1;
reconsider y0=x0 as Point of REAL-NS m by REAL_NS1:def 4;
hereby assume f is_differentiable_in x0; then
g is_differentiable_in y0 by Th2; then
consider N being Neighbourhood of y0 such that
A1: N c= dom g & ex GL be Point of R_NormSpace_of_BoundedLinearOperators
(REAL-NS m,REAL-NS n), GR be RestFunc of REAL-NS m,REAL-NS n st
for y be Point of REAL-NS m st y in N holds
g/.y - g/.y0 = GL.(y-y0) + GR/.(y-y0) by NDIFF_1:def 6;
consider GL be Point of R_NormSpace_of_BoundedLinearOperators
(REAL-NS m,REAL-NS n), GR be RestFunc of REAL-NS m,REAL-NS n such that
A2: for y be Point of REAL-NS m st y in N holds
g/.y - g/.y0 = GL.(y-y0) + GR/.(y-y0) by A1;
consider r0 be Real such that
A3: 0<r0 & {y where y is Point of REAL-NS m : ||.y-y0 .|| < r0 } c= N
by NFCONT_1:def 1;
take r0;
thus 0 <r0 by A3;
{y where y is Point of REAL-NS m : ||.y-y0 .|| < r0 } c= dom g
by A3,A1,XBOOLE_1:1;
hence {y where y is Element of REAL m: |.y-x0.| < r0} c= dom f by Th23;
A4: GR is total by NDIFF_1:def 5; then
A5: dom GR = the carrier of REAL-NS m by PARTFUN1:def 2;
A6: the carrier of REAL-NS m = REAL m &
the carrier of REAL-NS n = REAL n by REAL_NS1:def 4; then
reconsider L=GL as Function of REAL m,REAL n by LOPBAN_1:def 9;
reconsider R=GR as Function of REAL m,REAL n by A6,A4;
take L,R;
GL is LinearOperator of REAL-NS m,REAL-NS n by LOPBAN_1:def 9;
hence L is LinearOperator of m,n by Th14;
thus for r be Real st r > 0 ex d be Real st d > 0 &
(for z be Element of REAL m,w be Element of REAL n st
z <> 0*m & |.z.| < d & w=R.z holds (|.z.|"* |. w .|) < r )
proof
let r be Real;
assume r > 0; then
consider d be Real such that
A7: d > 0 &
(for z be Point of REAL-NS m st z <> 0.(REAL-NS m) & ||.z.|| < d holds
(||.z.||"* ||. GR/.z .||) < r) by A4,NDIFF_1:23;
take d;
thus d> 0 by A7;
let z be Element of REAL m, w be Element of REAL n;
assume A8:z <> 0*m & |.z.| < d & w=R.z;
reconsider s = z as Element of REAL-NS m by REAL_NS1:def 4;
A9: s <> 0.(REAL-NS m) by A8,REAL_NS1:def 4;
||. s .|| < d by A8,REAL_NS1:1; then
(||.s.||"* ||. GR/.s .||) < r by A7,A9; then
(|.z.|"* ||. GR/.s .||) < r by REAL_NS1:1;
hence (|.z.|"* |. w .|) < r by A5,A8,PARTFUN1:def 6,REAL_NS1:1;
end;
thus for x be Element of REAL m st |.x-x0.| < r0 holds
f/.x - f/.x0 = L.(x-x0) + R.(x-x0)
proof
let x be Element of REAL m;
assume |.x-x0.| < r0; then
x in {s where s is Element of REAL m: |.s-x0.| < r0}; then
A10: x in {y where y is Point of REAL-NS m : ||.y-y0 .|| < r0} by Th23;
reconsider y=x as Point of REAL-NS m by REAL_NS1:def 4;
A11: g/.y - g/.y0 = GL.(y-y0) + GR/.(y-y0) by A3,A10,A2;
A12: y in N & y0 in N by A3,A10,NFCONT_1:4; then
f/.x = f.x & f/.x0 = f.x0 by A1,PARTFUN1:def 6; then
A13:f/.x = g/.y & f/.x0 = g/.y0 by A12,A1,PARTFUN1:def 6;
x-x0 = y-y0 by REAL_NS1:5; then
L.(x-x0) =GL.(y-y0) & R.(x-x0) = GR/.(y-y0) by A5,PARTFUN1:def 6; then
L.(x-x0) + R.(x-x0)= GL.(y-y0) + GR/.(y-y0) by REAL_NS1:2;
hence f/.x - f/.x0 = L.(x-x0) + R.(x-x0) by A11,A13,REAL_NS1:5;
end;
end;
assume ex r0 be Real st 0 < r0 &
{y where y is Element of REAL m: |.y-x0.| < r0} c= dom f &
ex L,R be Function of REAL m,REAL n st
L is LinearOperator of m,n &
(for r be Real st r > 0
ex d be Real st d > 0 &
(for z be Element of REAL m, w be Element of REAL n st
z <> 0*m & |.z.| < d & w = R.z
holds (|.z.|"* |. w .|) < r)
) &
for x be Element of REAL m st |.x-x0.| < r0 holds
f/.x - f/.x0 = L.(x-x0) + R.(x-x0);
hence f is_differentiable_in x0 by Th24;
end;
begin
::Differentiation of Functions from Normed Linear Spaces $ {\cal R}^m$ to
:: Normed Linear Spaces $ {\cal R}^n$
theorem Th26:
for y1,y2 be Point of REAL-NS n holds
Proj(i,n).(y1 + y2) = Proj(i,n).y1 + Proj(i,n).y2
proof
let y1,y2 be Point of REAL-NS n;
reconsider yy1 = y1, yy2 = y2 as Element of REAL n by REAL_NS1:def 4;
reconsider ry1 = yy1.i as Element of REAL by XREAL_0:def 1;
reconsider ry2 = yy2.i as Element of REAL by XREAL_0:def 1;
Proj(i,n).y1 = <* proj(i,n).y1 *> & Proj(i,n).y2 = <* proj(i,n).y2 *>
by PDIFF_1:def 4; then
A1:Proj(i,n).y1 = <* ry1 *> & Proj(i,n).y2 = <* ry2 *> by PDIFF_1:def 1;
A2:<* ry1 *> is Element of REAL 1 &
<* ry2 *> is Element of REAL 1 by FINSEQ_2:98;
Proj(i,n).(y1 + y2) = <* proj(i,n).(y1 + y2) *> by PDIFF_1:def 4
.= <* proj(i,n).(yy1 + yy2) *> by REAL_NS1:2
.= <* (yy1 + yy2).i *> by PDIFF_1:def 1
.= <* (yy1.i + yy2.i) *> by RVSUM_1:11
.= <* ry1 *> + <* ry2 *> by RVSUM_1:13;
hence thesis by A1,A2,REAL_NS1:2;
end;
theorem Th27:
for y1 be Point of REAL-NS n, r being Real holds
Proj(i,n).(r*y1) = r*(Proj(i,n).y1)
proof
let y1 be Point of REAL-NS n, r being Real;
reconsider yy1 = y1 as Element of REAL n by REAL_NS1:def 4;
reconsider y1i = yy1.i as Element of REAL by XREAL_0:def 1;
Proj(i,n).y1 = <* proj(i,n).y1 *> by PDIFF_1:def 4; then
A1:Proj(i,n).y1 = <* y1i *> by PDIFF_1:def 1;
A2:<* y1i *> is Element of REAL 1 by FINSEQ_2:98;
Proj(i,n).(r*y1) = <* proj(i,n).(r*y1) *> by PDIFF_1:def 4
.= <* proj(i,n).(r*yy1) *> by REAL_NS1:3
.= <* (r*yy1).i *> by PDIFF_1:def 1
.= <* r*(yy1.i) *> by RVSUM_1:44
.= r*<* y1i *> by RVSUM_1:47;
hence thesis by A1,A2,REAL_NS1:3;
end;
theorem Th28:
for m,n be non zero Nat,
g be PartFunc of REAL-NS m,REAL-NS n, x0 be Point of REAL-NS m,
i be Nat st
1 <= i & i <= n & g is_differentiable_in x0 holds
(Proj(i,n)*g) is_differentiable_in x0 &
Proj(i,n)*(diff(g,x0)) = diff((Proj(i,n)*g),x0)
proof
let m,n be non zero Nat;
let g be PartFunc of REAL-NS m,REAL-NS n,
x0 be Point of REAL-NS m, i be Nat;
assume A1: 1 <= i & i <= n & g is_differentiable_in x0; then
consider N being Neighbourhood of x0 such that
A2:N c= dom g & ex GR be RestFunc of REAL-NS m,REAL-NS n st
for x be Point of REAL-NS m st x in N holds
g/.x - g/.x0 = (diff(g,x0)).(x-x0) + GR/.(x-x0) by NDIFF_1:def 7;
consider GR be RestFunc of REAL-NS m,REAL-NS n such that
A3:for x be Point of REAL-NS m st x in N holds
g/.x - g/.x0 = (diff(g,x0)).(x-x0) + GR/.(x-x0) by A2;
set RLB0 = R_NormSpace_of_BoundedLinearOperators(REAL-NS m,REAL-NS 1);
reconsider DFG = diff(g,x0) as LinearOperator of REAL-NS m,REAL-NS n
by LOPBAN_1:def 9;
reconsider PG = Proj(i,n) as Function of
the carrier of REAL-NS n,the carrier of REAL-NS 1;
PG*DFG is Function of
the carrier of REAL-NS m,the carrier of REAL-NS 1; then
reconsider L = Proj(i,n)*(diff(g,x0)) as Function of REAL-NS m,REAL-NS 1;
A4:
for x,y being VECTOR of REAL-NS m holds L.(x + y) = (L.x) + (L.y)
proof
let x,y being VECTOR of REAL-NS m;
A5: dom L = the carrier of REAL-NS m by FUNCT_2:def 1;
A6: DFG.(x + y) = DFG.x + DFG.y by VECTSP_1:def 20;
L.(x+y) = Proj(i,n).(DFG.(x + y)) by A5,FUNCT_1:12
.= Proj(i,n).(DFG.x) + Proj(i,n).(DFG.y) by A6,Th26
.= Proj(i,n).(DFG.x) + L.y by A5,FUNCT_1:12;
hence L.(x+y) = L.x + L.y by A5,FUNCT_1:12;
end;
for x being VECTOR of REAL-NS m, r being Real holds L.(r*x) = r*(L.x)
proof
let x being VECTOR of REAL-NS m, r being Real;
A7: dom L = the carrier of REAL-NS m by FUNCT_2:def 1;
DFG.(r*x) = r*(DFG.x) by LOPBAN_1:def 5; then
Proj(i,n).(DFG.(r*x)) = r*(Proj(i,n).(DFG.x)) by Th27; then
L.(r*x) = r*(Proj(i,n).(DFG.x)) by A7,FUNCT_1:12;
hence L.(r*x) = r*(L.x) by A7,FUNCT_1:12;
end; then
reconsider L as LinearOperator of REAL-NS m,REAL-NS 1
by A4,LOPBAN_1:def 5,VECTSP_1:def 20;
reconsider L as Point of RLB0 by LOPBAN_1:def 9;
A8:
GR is total by NDIFF_1:def 5; then
reconsider FGR = GR as Function of the carrier of REAL-NS m,
the carrier of REAL-NS n;
A9:Proj(i,n)*FGR is Function of the carrier of REAL-NS m,
the carrier of REAL-NS 1;
Proj(i,n)*GR is RestFunc of REAL-NS m,REAL-NS 1
proof
A10:dom GR = the carrier of (REAL-NS m) by A8,PARTFUN1:def 2;
reconsider R = Proj(i,n)*GR as PartFunc of REAL-NS m,REAL-NS 1;
for r be Real st r > 0 ex d be Real st d > 0 &
(for z be Point of REAL-NS m st z <> 0.(REAL-NS m) & ||.z.|| < d
holds (||.z.||"* ||. R/.z .||) < r)
proof
let r be Real;
assume r > 0; then
consider d be Real such that
A11: d > 0 &
(for z be Point of (REAL-NS m) st z <> 0.(REAL-NS m) & ||.z.|| < d holds
(||.z.||"* ||. GR/.z .||) < r) by A8,NDIFF_1:23;
take d;
thus d> 0 by A11;
let z be Point of (REAL-NS m);
assume A12: z <> 0.(REAL-NS m) & ||.z.|| < d;
A13: GR/.z = GR.z by A10,PARTFUN1:def 6;
A14:i in Seg n by A1;
reconsider GRz = GR/.z as Point of REAL-NS n;
reconsider GRz1 = GRz as Element of REAL n by REAL_NS1:def 4;
reconsider GRzi = GRz1.i as Element of REAL by XREAL_0:def 1;
dom Proj(i,n) = the carrier of REAL-NS n by PARTFUN1:def 2; then
A15:z in dom (Proj(i,n)*GR) by A10,A13,FUNCT_1:11; then
(Proj(i,n)*GR).z = Proj(i,n).(GR.z) by FUNCT_1:12
.= <* proj(i,n).(GRz1) *> by A13,PDIFF_1:def 4; then
A16: (Proj(i,n)*GR).z = <* GRzi *> by PDIFF_1:def 1;
A17: |.GRzi.| <= ||. GR/.z .|| by A14,REAL_NS1:9;
A18:0 <= ||.z.|| by NORMSP_1:4;
0 <= |.GRzi.| by COMPLEX1:46; then
A19: ||.z.||"* |.GRzi.| <= ||.z.||"* ||. GR/.z .|| by A17,A18,XREAL_1:66;
||.z.||"* ||. GR/.z .|| < r by A11,A12; then
A20: ||.z.||"* |.GRzi.| < r by A19,XXREAL_0:2;
(Proj(i,n)*GR).z in rng(Proj(i,n)*GR) by A15,FUNCT_1:3; then
reconsider Rz = (Proj(i,n)*GR).z as VECTOR of REAL-NS 1;
set VGRzi = <* GRzi *>;
VGRzi is Element of REAL 1 by FINSEQ_2:98; then
||. Rz .|| = |. VGRzi .| by A16,REAL_NS1:1; then
||.z.||"* ||. Rz .|| < r by A20,JORDAN2C:10;
hence thesis by A15,PARTFUN1:def 6;
end;
hence thesis by A9,NDIFF_1:23;
end; then
reconsider R = Proj(i,n)*GR as RestFunc of REAL-NS m,REAL-NS 1;
set pg = Proj(i,n)*g;
A21:dom Proj(i,n) = the carrier of REAL-NS n by FUNCT_2:def 1; then
rng g c= dom Proj(i,n); then
A22:dom g = dom (Proj(i,n)*g) by RELAT_1:27;
A23:dom Proj(i,n) = REAL n by A21,REAL_NS1:def 4;
A24:for x be Point of REAL-NS m st x in N holds
pg/.x - pg/.x0 = L.(x-x0) + R/.(x-x0)
proof
let x be Point of REAL-NS m;
now assume A25: x in N; then
A26: g/.x - g/.x0 = (diff(g,x0)).(x-x0) + GR/.(x-x0) by A3;
A27: x0 in N by NFCONT_1:4; then
A28: pg/.x = pg.x & pg/.x0 = pg.x0 by A2,A22,A25,PARTFUN1:def 6;
A29: g/.x = g.x & g/.x0 = g.x0 by A2,A25,A27,PARTFUN1:def 6;
reconsider PGSx = pg/.x - pg/.x0 as Element of REAL 1 by REAL_NS1:def 4;
pg.x in rng pg by A2,A22,A25,FUNCT_1:3; then
reconsider PGdx = pg.x as Element of REAL 1 by REAL_NS1:def 4;
pg.x0 in rng pg by A2,A22,A27,FUNCT_1:3; then
reconsider PGdx0 = pg.x0 as Element of REAL 1 by REAL_NS1:def 4;
g.x in rng g by A2,A25,FUNCT_1:3; then
reconsider Gx = g.x as Element of REAL n by REAL_NS1:def 4;
g.x0 in rng g by A2,A27,FUNCT_1:3; then
reconsider Gx0 = g.x0 as Element of REAL n by REAL_NS1:def 4;
set ProjGx = Proj(i,n).(g.x);
Gx in dom Proj(i,n) by A23; then
ProjGx in rng Proj(i,n) by FUNCT_1:3; then
reconsider ProjGx as Element of REAL 1 by REAL_NS1:def 4;
set ProjGx0 = Proj(i,n).(g.x0);
Gx0 in dom Proj(i,n) by A23; then
ProjGx0 in rng Proj(i,n) by FUNCT_1:3; then
reconsider ProjGx0 as Element of REAL 1 by REAL_NS1:def 4;
reconsider Gx1 = Gx as Element of REAL-NS n by REAL_NS1:def 4;
reconsider Gx01 = Gx0 as Element of REAL-NS n by REAL_NS1:def 4;
reconsider Gsx = g/.x as Element of REAL n by REAL_NS1:def 4;
reconsider Gsx0 = g/.x0 as Element of REAL n by REAL_NS1:def 4;
set dxx0 = x-x0;
reconsider Ldxx0 = L.(x-x0) as Element of REAL-NS 1;
A30: dom R = the carrier of (REAL-NS m) by A9,PARTFUN1:def 2; then
A31: R/.(x-x0) = R.dxx0 by PARTFUN1:def 6; then
reconsider Rdxx0 = R.(x-x0) as Element of REAL-NS 1;
reconsider Ldiff = diff(g,x0).(x-x0) as Element of REAL n
by REAL_NS1:def 4;
set ProjLdiff = Proj(i,n).Ldiff;
ProjLdiff in rng Proj(i,n) by A21,FUNCT_1:3; then
reconsider ProjLdiff as Element of REAL 1 by REAL_NS1:def 4;
A32: dom GR = the carrier of REAL-NS m by A8,PARTFUN1:def 2; then
GR.dxx0 in rng GR by FUNCT_1:3; then
reconsider Rdiff = GR.dxx0 as Element of REAL n by REAL_NS1:def 4;
A33: Rdiff = GR/.dxx0 by A32,PARTFUN1:def 6;
set ProjRdiff = Proj(i,n).Rdiff;
ProjRdiff in rng Proj(i,n) by A23,FUNCT_1:3; then
reconsider ProjRdiff as Element of REAL 1 by REAL_NS1:def 4;
dom L = the carrier of REAL-NS m by FUNCT_2:def 1; then
L.(x-x0) = Proj(i,n).Ldiff & R.(x-x0) = Proj(i,n).Rdiff
by A30,FUNCT_1:12; then
A34: Ldxx0 + Rdxx0 = ProjLdiff + ProjRdiff by REAL_NS1:2;
Proj(i,n).Ldiff = <* proj(i,n).Ldiff *> by PDIFF_1:def 4; then
A35: Proj(i,n).Ldiff = <* Ldiff.i *> by PDIFF_1:def 1;
Rdiff in dom Proj(i,n) by A23; then
Proj(i,n).Rdiff = <* proj(i,n).Rdiff *> by PDIFF_1:def 4; then
A36: Proj(i,n).Rdiff = <* Rdiff.i *> by PDIFF_1:def 1;
reconsider diffGR = (diff(g,x0)).(x-x0) + GR/.(x-x0)
as Element of REAL n by REAL_NS1:def 4;
reconsider Rsdiff = GR/.(x-x0) as Element of REAL n by REAL_NS1:def 4;
PGSx = PGdx - PGdx0 by A28,REAL_NS1:5
.= ProjGx - PGdx0 by A2,A22,A25,FUNCT_1:12
.= ProjGx - ProjGx0 by A2,A22,A27,FUNCT_1:12
.= <* proj(i,n).Gx1 *> - ProjGx0 by PDIFF_1:def 4
.= <* proj(i,n).Gx1 *> - <* proj(i,n).Gx01 *> by PDIFF_1:def 4
.= <* Gx.i *> - <* proj(i,n).Gx01 *> by PDIFF_1:def 1
.= <* Gx.i *> - <* Gx0.i *> by PDIFF_1:def 1
.= <* Gx.i - Gx0.i *> by RVSUM_1:29
.= <* (Gsx - Gsx0).i *> by A29,RVSUM_1:27
.= <* diffGR.i *> by A26,REAL_NS1:5
.= <* (Ldiff + Rsdiff).i *> by REAL_NS1:2
.= <* Ldiff.i + Rsdiff.i *> by RVSUM_1:11;
hence thesis by A31,A34,A35,A36,A33,RVSUM_1:13;
end;
hence thesis;
end;
hence Proj(i,n)*g is_differentiable_in x0 by A2,A22,NDIFF_1:def 6;
hence Proj(i,n)*(diff(g,x0)) = diff((Proj(i,n)*g),x0)
by A2,A22,A24,NDIFF_1:def 7;
end;
theorem
for m,n be non zero Nat, g be PartFunc of REAL-NS m,REAL-NS n,
x0 be Point of REAL-NS m holds
g is_differentiable_in x0 iff
(for i be Nat st 1<=i & i <=n holds
Proj(i,n)*g is_differentiable_in x0)
proof
let m,n be non zero Nat;
let g be PartFunc of REAL-NS m,REAL-NS n;
let x0 be Point of REAL-NS m;
set RB= R_NormSpace_of_BoundedLinearOperators(REAL-NS m,REAL-NS n);
(for i be Nat st 1<=i & i<=n holds
Proj(i,n)*g is_differentiable_in x0) implies
g is_differentiable_in x0
proof
assume A1: for i be Nat st 1 <= i & i <= n holds
Proj(i,n)*g is_differentiable_in x0;
defpred Pd[Nat,Element of REAL] means
$2 > 0 &
{y where y is Point of REAL-NS m : ||. y - x0 .|| < $2}
c= dom (Proj($1,n)*g) &
ex Ri be RestFunc of REAL-NS m,REAL-NS 1 st
for x be Point of REAL-NS m st
x in {y where y is Point of REAL-NS m : ||. y - x0 .|| < $2} holds
(Proj($1,n)*g)/.x - (Proj($1,n)*g)/.x0
= (diff((Proj($1,n)*g),x0)).(x-x0) + Ri/.(x-x0);
A2: for k be Nat st k in Seg n ex dk be Element of REAL st Pd[k,dk]
proof
let k be Nat;
assume k in Seg n; then
1 <= k & k <= n by FINSEQ_1:1; then
Proj(k,n)*g is_differentiable_in x0 by A1; then
consider Nk be Neighbourhood of x0 such that
A3: Nk c= dom (Proj(k,n)*g) & ex Rk be RestFunc of REAL-NS m,REAL-NS 1 st
for x be Point of REAL-NS m st
x in Nk holds (Proj(k,n)*g)/.x - (Proj(k,n)*g)/.x0
= (diff((Proj(k,n)*g),x0)).(x-x0) + Rk/.(x-x0) by NDIFF_1:def 7;
consider dk be Real such that
A4: 0 < dk & {y where y is Point of REAL-NS m: ||. y-x0 .|| < dk} c= Nk
by NFCONT_1:def 1;
reconsider dk as Element of REAL by XREAL_0:def 1;
take dk;
thus 0 < dk by A4;
thus {y where y is Point of REAL-NS m: ||. y-x0 .|| < dk}
c= dom(Proj(k,n)*g) by A4,A3,XBOOLE_1:1;
thus ex Rk be RestFunc of REAL-NS m,REAL-NS 1 st
for x be Point of REAL-NS m st
x in {y where y is Point of REAL-NS m: ||. y-x0 .|| < dk} holds
(Proj(k,n)*g)/.x - (Proj(k,n)*g)/.x0
= (diff((Proj(k,n)*g),x0)).(x-x0)+Rk/.(x-x0)
proof
consider Rk be RestFunc of REAL-NS m,REAL-NS 1 such that
A5: for x be Point of REAL-NS m st
x in Nk holds (Proj(k,n)*g)/.x - (Proj(k,n)*g)/.x0
= (diff((Proj(k,n)*g),x0)).(x-x0) + Rk/.(x-x0) by A3;
take Rk;
thus for x be Point of REAL-NS m st
x in {y where y is Point of REAL-NS m: ||. y-x0 .|| < dk} holds
(Proj(k,n)*g)/.x - (Proj(k,n)*g)/.x0
= (diff((Proj(k,n)*g),x0)).(x-x0)+Rk/.(x-x0) by A4,A5;
end;
end;
consider d be FinSequence of REAL such that
A6: dom d = Seg n & for k be Nat st k in Seg n holds
Pd[k,d/.k] from RECDEF_1:sch 17(A2);
set d0 = min d;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
len d = nn by A6,FINSEQ_1:def 3; then
A7:min_p d in dom d by RFINSEQ2:def 2; then
d/.(min_p d) > 0 by A6; then
A8:d0 > 0 by A7,PARTFUN1:def 6;
defpred LX[set,set] means
ex y be Element of REAL n st $2 = y &
for i be Nat st i in Seg n holds
y.i = proj(1,1).((diff((Proj(i,n)*g),x0)).$1);
A9: for x be Point of REAL-NS m holds ex y be Point of REAL-NS n st LX[x,y]
proof
let x being Point of REAL-NS m;
defpred YX[Nat,set] means
$2 = proj(1,1).((diff((Proj($1,n)*g),x0)).x);
A10: for i be Nat st i in Seg n
ex r being Element of REAL st YX[i,r]
proof let i be Nat;
assume i in Seg n;
proj(1,1).((diff((Proj(i,n)*g),x0)).x) in REAL by XREAL_0:def 1;
hence thesis;
end;
consider y be FinSequence of REAL such that
A11: dom y = Seg n & for i be Nat st i in Seg n holds YX[i,y/.i]
from RECDEF_1:sch 17(A10);
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
len y = nn by A11,FINSEQ_1:def 3; then
reconsider y as Element of REAL n by FINSEQ_2:92;
A12: now let i be Nat;
assume i in Seg n; then
YX[i,y/.i] & y/.i = y.i by A11,PARTFUN1:def 6;
hence y.i =proj(1,1).((diff((Proj(i,n)*g),x0)).x);
end;
reconsider y0=y as Point of REAL-NS n by REAL_NS1:def 4;
ex y be Element of REAL n st y0=y &
for i be Nat st i in Seg n holds
y.i = proj(1,1).((diff((Proj(i,n)*g),x0)).x) by A12;
hence ex y0 be Point of REAL-NS n st LX[x,y0];
end;
consider L be Function of REAL-NS m,REAL-NS n such that
A13: for x be Point of REAL-NS m holds LX[x,L.x] from FUNCT_2:sch 3(A9);
A14:for x,y be VECTOR of REAL-NS m holds L.(x+y) = L.x + L.y
proof
let x,y be VECTOR of REAL-NS m;
consider Lx be Element of REAL n such that
A15: L.x = Lx & for i be Nat st i in Seg n holds
Lx.i = proj(1,1).((diff((Proj(i,n)*g),x0)).x) by A13;
consider Ly be Element of REAL n such that
A16: L.y = Ly & for i be Nat st i in Seg n holds
Ly.i = proj(1,1).((diff((Proj(i,n)*g),x0)).y) by A13;
consider Lxy be Element of REAL n such that
A17: L.(x+y) = Lxy & for i be Nat st i in Seg n holds
Lxy.i = proj(1,1).((diff((Proj(i,n)*g),x0)).(x+y)) by A13;
dom Lxy = Seg n by FINSEQ_1:89; then
A18: dom Lxy = dom (Lx + Ly) by FINSEQ_1:89;
for i0 be Nat st i0 in dom Lxy holds Lxy.i0 = (Lx + Ly).i0
proof
let i0 be Nat;
reconsider i = i0 as Nat;
assume i0 in dom Lxy; then
i in Seg n by FINSEQ_1:89; then
A19: Lxy.i = proj(1,1).((diff((Proj(i,n)*g),x0)).(x+y)) &
Lx.i = proj(1,1).((diff((Proj(i,n)*g),x0)).x) &
Ly.i = proj(1,1).((diff((Proj(i,n)*g),x0)).y) by A15,A16,A17;
diff((Proj(i,n)*g),x0) is LinearOperator of REAL-NS m,REAL-NS 1
by LOPBAN_1:def 9; then
A20: diff((Proj(i,n)*g),x0).(x+y)
= diff((Proj(i,n)*g),x0).x + diff((Proj(i,n)*g),x0).y
by VECTSP_1:def 20;
reconsider Diffxy = diff((Proj(i,n)*g),x0).(x+y)
as Element of REAL 1 by REAL_NS1:def 4;
reconsider Diffx = diff((Proj(i,n)*g),x0).x
as Element of REAL 1 by REAL_NS1:def 4;
reconsider Diffy = diff((Proj(i,n)*g),x0).y
as Element of REAL 1 by REAL_NS1:def 4;
Diffxy = Diffx + Diffy by A20,REAL_NS1:2; then
Lxy.i0 = (Diffx + Diffy).1 by A19,PDIFF_1:def 1; then
Lxy.i0 = Diffx.1 + Diffy.1 by RVSUM_1:11; then
Lxy.i0 = Lx.i0 + Diffy.1 by A19,PDIFF_1:def 1; then
Lxy.i0 = Lx.i0 + Ly.i0 by A19,PDIFF_1:def 1;
hence thesis by RVSUM_1:11;
end; then
Lxy = Lx + Ly by A18,FINSEQ_1:13;
hence thesis by A15,A16,A17,REAL_NS1:2;
end;
for x be VECTOR of REAL-NS m, r be Real holds L.(r*x) = r*(L.x)
proof
let x be VECTOR of REAL-NS m, r be Real;
consider Lx be Element of REAL n such that
A21: L.x = Lx & for i be Nat st i in Seg n holds
Lx.i = proj(1,1).((diff((Proj(i,n)*g),x0)).x) by A13;
consider Lrx be Element of REAL n such that
A22: L.(r*x) = Lrx & for i be Nat st i in Seg n holds
Lrx.i = proj(1,1).((diff((Proj(i,n)*g),x0)).(r*x)) by A13;
dom (r*Lx) = Seg n by FINSEQ_1:89; then
A23: dom (r*Lx) = dom Lrx by FINSEQ_1:89;
for i0 be Nat st i0 in dom (r*Lx) holds (r*Lx).i0 = Lrx.i0
proof
let i0 be Nat;
reconsider i = i0 as Nat;
assume i0 in dom(r*Lx); then
i0 in Seg n by FINSEQ_1:89; then
A24: Lx.i = proj(1,1).((diff((Proj(i,n)*g),x0)).x) &
Lrx.i = proj(1,1).((diff((Proj(i,n)*g),x0)).(r*x)) by A21,A22;
diff((Proj(i,n)*g),x0) is LinearOperator of REAL-NS m,REAL-NS 1
by LOPBAN_1:def 9; then
A25: diff((Proj(i,n)*g),x0).(r*x)
= r * diff((Proj(i,n)*g),x0).x by LOPBAN_1:def 5;
reconsider Diffrx = diff((Proj(i,n)*g),x0).(r*x)
as Element of REAL 1 by REAL_NS1:def 4;
reconsider Diffx = diff((Proj(i,n)*g),x0).x
as Element of REAL 1 by REAL_NS1:def 4;
Diffrx = r*Diffx by A25,REAL_NS1:3; then
Lrx.i0 = (r*Diffx).1 by A24,PDIFF_1:def 1; then
Lrx.i0 = r*(Diffx.1) by RVSUM_1:45; then
Lrx.i0 = r*(Lx.i0) by A24,PDIFF_1:def 1;
hence thesis by RVSUM_1:45;
end; then
r*Lx = Lrx by A23,FINSEQ_1:13;
hence thesis by A21,A22,REAL_NS1:3;
end; then
reconsider L as LinearOperator of REAL-NS m,REAL-NS n
by A14,LOPBAN_1:def 5,VECTSP_1:def 20;
reconsider L0 = L as Point of RB by LOPBAN_1:def 9;
deffunc RD(Element of REAL-NS m) = g/.($1+x0) - g/.x0 - L.$1;
consider R be Function of REAL-NS m,REAL-NS n such that
A26: for x be Element of REAL-NS m holds R.x = RD(x) from FUNCT_2:sch 4;
A27:for x be Element of REAL-NS m, i be Nat st
i in Seg n & x+x0 in dom g holds
(Proj(i,n)*R).x
= (Proj(i,n)*g)/.(x+x0) - (Proj(i,n)*g)/.x0 - (Proj(i,n)*L).x
proof
let x be Element of REAL-NS m, i be Nat;
assume that
A28: i in Seg n and
A29: x+x0 in dom g;
x0 - x0 = 0.(REAL-NS m) by RLVECT_1:15; then
x0 - x0 = 0*m by REAL_NS1:def 4; then
||. x0 - x0 .|| = |. 0*m .| by REAL_NS1:1; then
A30: ||. x0 - x0 .|| = 0 by EUCLID:7;
A31: 0 < d/.i & {y where y is Point of REAL-NS m : ||. y - x0 .|| < d/.i}
c= dom (Proj(i,n)*g) by A28,A6; then
x0 in {y where y is Point of REAL-NS m : ||. y - x0 .|| < d/.i}
by A30; then
A32: x0 in dom (Proj(i,n)*g) by A31;
A33: dom (Proj(i,n)*g) c= dom g by RELAT_1:25;
reconsider gxx0 = g/.(x+x0), gx0 = g/.x0, Lx = L.x as Element of REAL n
by REAL_NS1:def 4;
reconsider Lx1 = L.x as Point of REAL-NS n;
A34: -gx0 = (-1)*(g/.x0) & -Lx = (-1)*(L.x) by REAL_NS1:3; then
gxx0 + -gx0 = g/.(x+x0) + (-1)*(g/.x0) by REAL_NS1:2; then
A35: gxx0 + -gx0 + -Lx = g/.(x+x0) + (-1)*(g/.x0) + (-1)*(L.x)
by A34,REAL_NS1:2;
gxx0-gx0 = g/.(x+x0)-g/.x0 by REAL_NS1:5; then
A36: g/.(x+x0) - g/.x0 - L.x = gxx0 - gx0 - Lx by REAL_NS1:5;
(Proj(i,n)*R).x = Proj(i,n).(R.x) by FUNCT_2:15; then
(Proj(i,n)*R).x = Proj(i,n).(g/.(x+x0) - g/.x0 - L.x) by A26; then
(Proj(i,n)*R).x = Proj(i,n).(g/.(x+x0) + (-1)*(g/.x0))
+ Proj(i,n).((-1)*(L.x)) by A36,A35,Th26; then
A37: (Proj(i,n)*R).x = Proj(i,n).(g/.(x+x0)) + Proj(i,n).((-1)*(g/.x0))
+ Proj(i,n).((-1)*(L.x)) by Th26;
Proj(i,n).((-1)*(g/.x0)) = (-1)*(Proj(i,n).(g/.x0)) &
Proj(i,n).((-1)*(Lx1)) = (-1)*(Proj(i,n).(Lx1)) by Th27; then
(Proj(i,n)*R).x = Proj(i,n).(g/.(x+x0)) + -Proj(i,n).(g/.x0)
+ (-1)*Proj(i,n).(L.x) by A37,RLVECT_1:16; then
(Proj(i,n)*R).x = Proj(i,n).(g/.(x+x0)) + -Proj(i,n).(g/.x0)
+ -Proj(i,n).(L.x) by RLVECT_1:16; then
(Proj(i,n)*R).x = Proj(i,n).(g/.(x+x0)) - Proj(i,n).(g/.x0)
+ -Proj(i,n).(L.x) by RLVECT_1:def 11; then
A38: (Proj(i,n)*R).x = Proj(i,n).(g/.(x+x0)) - Proj(i,n).(g/.x0)
- Proj(i,n).(L.x) by RLVECT_1:def 11;
g/.(x+x0) in the carrier of REAL-NS n &
g/.x0 in the carrier of REAL-NS n; then
A39: g/.(x+x0) in dom (Proj(i,n)) & g/.x0 in dom (Proj(i,n)) by FUNCT_2:def 1;
A40: Proj(i,n).(g/.(x+x0)) = Proj(i,n)/.(g/.(x+x0))
.= (Proj(i,n)*g)/.(x+x0) by A29,A39,PARTFUN2:4;
Proj(i,n).(g/.x0) = Proj(i,n)/.(g/.x0)
.= (Proj(i,n)*g)/.x0 by A32,A33,A39,PARTFUN2:4;
hence thesis by A38,A40,FUNCT_2:15;
end;
for r be Real st r > 0 ex d be Real st d > 0 &
for z be Point of REAL-NS m st
z <> 0.(REAL-NS m) & ||. z .|| < d holds (||.z.||"* ||. R/.z .||) < r
proof
let r be Real;
assume A41: r > 0;
set r0 = (sqrt n)"*r;
A42: sqrt n > 0 by SQUARE_1:25; then
A43: r0 > 0 by A41,XREAL_1:129;
defpred DD[Nat,Element of REAL] means
$2 > 0 &
for z be Point of REAL-NS m st
z <> 0.(REAL-NS m) & ||. z .|| < $2 holds
(||. z .||"* ||. (Proj($1,n)*R)/.z .||) < r0;
A44: for k be Nat st k in Seg n ex dd be Element of REAL st DD[k,dd]
proof
let k be Nat;
assume A45: k in Seg n; then
1 <= k & k <= n by FINSEQ_1:1; then
Proj(k,n)*g is_differentiable_in x0 by A1; then
consider Nk be Neighbourhood of x0 such that
A46: Nk c= dom (Proj(k,n)*g) & ex PR be RestFunc of REAL-NS m,REAL-NS 1 st
for x be Point of REAL-NS m st x in Nk holds
(Proj(k,n)*g)/.x - (Proj(k,n)*g)/.x0
= diff(Proj(k,n)*g,x0).(x-x0) + PR/.(x-x0) by NDIFF_1:def 7;
consider d0 be Real such that
A47: 0 < d0 & {y where y is Point of REAL-NS m: ||. y-x0 .|| < d0} c= Nk
by NFCONT_1:def 1;
consider PR be RestFunc of REAL-NS m,REAL-NS 1 such that
A48: for x be Point of REAL-NS m st x in Nk holds
(Proj(k,n)*g)/.x - (Proj(k,n)*g)/.x0
= diff(Proj(k,n)*g,x0).(x-x0) + PR/.(x-x0) by A46;
PR is total by NDIFF_1:def 5; then
consider d1 be Real such that
A49: d1 > 0 & for z be Point of REAL-NS m st
z <> 0.(REAL-NS m) & ||. z .|| < d1 holds
( ||. z .||"* ||. PR/.z .||) < r0 by A43,NDIFF_1:23;
reconsider d0,d1 as Real;
reconsider dd = min(d0,d1) as Element of REAL by XREAL_0:def 1;
take dd;
for z be Point of REAL-NS m st z <> 0.(REAL-NS m) & ||. z .|| < dd holds
(||. z .||"* ||. (Proj(k,n)*R)/.z .||) < r0
proof
let z be Point of REAL-NS m;
assume A50: z <> 0.(REAL-NS m) & ||. z .|| < dd;
dd <= d1 by XXREAL_0:17; then
||. z .|| < d1 by A50,XXREAL_0:2; then
A51: ( ||. z .||"* ||. PR/.z .||) < r0 by A50,A49;
dd <= d0 by XXREAL_0:17; then
A52: ||. z .|| < d0 by A50,XXREAL_0:2;
A53: z+x0 - x0 = z by RLVECT_4:1; then
A54: z+x0 in {y where y is Point of REAL-NS m: ||. y-x0 .|| < d0} by A52;
then
z+x0 in Nk by A47; then
A55: z+x0 in dom (Proj(k,n)*g) by A46;
(Proj(k,n)*g)/.(z+x0) - (Proj(k,n)*g)/.x0
= diff(Proj(k,n)*g,x0).(z+x0-x0) + PR/.(z+x0-x0) by A54,A47,A48; then
A56: PR/.z = (Proj(k,n)*g)/.(z+x0) - (Proj(k,n)*g)/.x0
- diff(Proj(k,n)*g,x0).z by A53,RLVECT_4:1;
dom(Proj(k,n)*g) c= dom g by RELAT_1:25; then
A57: (Proj(k,n)*R).z
= (Proj(k,n)*g)/.(z+x0) - (Proj(k,n)*g)/.x0 - (Proj(k,n)*L).z
by A55,A45,A27;
consider y be Element of REAL n such that
A58: L.z = y & for i be Nat st i in Seg n holds
y.i = proj(1,1).((diff((Proj(i,n)*g),x0)).z) by A13;
A59: y.k = proj(1,1).((diff((Proj(k,n)*g),x0)).z) by A58,A45;
(diff((Proj(k,n)*g),x0)).z is Element of REAL 1 by REAL_NS1:def 4; then
consider Dk be Element of REAL such that
A60: (diff((Proj(k,n)*g),x0)).z = <* Dk *> by FINSEQ_2:97;
reconsider y1 = y as Point of REAL-NS n by REAL_NS1:def 4;
dom L = the carrier of REAL-NS m by FUNCT_2:def 1; then
(Proj(k,n)*L).z = (Proj(k,n)).(L.z) by FUNCT_1:13; then
(Proj(k,n)*L).z = <* proj(k,n).y1 *> by A58,PDIFF_1:def 4; then
(Proj(k,n)*L).z = <* proj(1,1).((diff((Proj(k,n)*g),x0)).z) *>
by A59,PDIFF_1:def 1;
hence thesis by A51,A56,A57,A60,PDIFF_1:1;
end;
hence thesis by A47,A49,XXREAL_0:21;
end;
consider dd be FinSequence of REAL such that
A61: dom dd = Seg n & for i be Nat st i in Seg n holds DD[i,dd/.i]
from RECDEF_1:sch 17(A44);
set d = min dd;
take d;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
len dd = nn by A61,FINSEQ_1:def 3; then
A62: min_p dd in dom dd by RFINSEQ2:def 2; then
A63: dd/.(min_p dd) > 0 by A61;
for z be Point of REAL-NS m st
z <> 0.(REAL-NS m) & ||. z .|| < d holds (||.z.||"* ||. R/.z .||) < r
proof
let z be Point of REAL-NS m;
assume A64: z <> 0.(REAL-NS m) & ||. z .|| < d;
reconsider Rz = R/.z as Element of REAL n by REAL_NS1:def 4;
reconsider zr = (||. z .|| * r0)^2 as Element of REAL by XREAL_0:def 1;
reconsider R0 = n |-> zr as Element of n-tuples_on REAL;
reconsider SRz = sqr Rz as Element of n-tuples_on REAL;
||. z .|| <> 0 by A64,NORMSP_0:def 5; then
A65: ||. z .|| > 0 by NORMSP_1:4;
A66: for i0 be Nat st i0 in Seg n holds SRz.i0 < R0.i0
proof
let i0 be Nat;
reconsider i = i0 as Nat;
assume A67: i0 in Seg n; then
i in dom Rz by FINSEQ_2:124; then
(sqr Rz).i = sqrreal.(Rz.i) by FUNCT_1:13; then
A68: (sqr Rz).i = (Rz.i)^2 by RVSUM_1:def 2;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
1 <= i & i <= nn by A67,FINSEQ_1:1; then
1 <= i & i <= len dd by A61,FINSEQ_1:def 3; then
d <= dd.i by RFINSEQ2:2; then
d <= dd/.i by A67,A61,PARTFUN1:def 6; then
||. z .|| < dd/.i by A64,XXREAL_0:2; then
(||. z .||" * ||. (Proj(i,n)*R)/.z .||) < r0 by A64,A67,A61; then
A69: ||. (Proj(i,n)*R)/.z .|| < r0 / (||. z .||") by A65,XREAL_1:81;
Rz.i in REAL by XREAL_0:def 1;
then reconsider Rzi = <* Rz.i *> as Element of REAL 1 by FINSEQ_2:98;
(Proj(i,n)*R).z = Proj(i,n).(R.z) by FUNCT_2:15; then
(Proj(i,n)*R).z = <* proj(i,n).Rz *> by PDIFF_1:def 4; then
(Proj(i,n)*R).z = <* Rz.i *> by PDIFF_1:def 1; then
||. (Proj(i,n)*R).z .|| = |. Rzi .| by REAL_NS1:1; then
|. Rz.i .| < ||. z .|| * r0 by A69,JORDAN2C:10; then
|. Rz.i .| ^2 < (||. z .|| * r0)^2 by COMPLEX1:46,SQUARE_1:16; then
(Rz.i0)^2 < (||. z .|| * r0)^2 by COMPLEX1:75;
hence thesis by A67,A68,FINSEQ_2:57;
end;
A70: for i be Nat st i in dom (sqr Rz) holds 0 <= (sqr Rz).i
proof
let i be Nat;
assume i in dom(sqr Rz); then
i in dom (sqrreal*Rz) & dom(sqrreal*Rz) c= dom Rz by RELAT_1:25; then
(sqr Rz).i = sqrreal.(Rz.i) by FUNCT_1:13; then
(sqr Rz).i = (Rz.i)^2 by RVSUM_1:def 2;
hence thesis by XREAL_1:63;
end;
A71: (||. z .|| * r0)^2 >= 0 by XREAL_1:63;
A72: ex i be Nat st i in Seg n & SRz.i < R0.i
proof
take 1;
1 <= n by NAT_1:14;
hence 1 in Seg n;
hence SRz.1 < R0.1 by A66;
end;
A73: sqrt n > 0 by SQUARE_1:25;
for i0 be Nat st i0 in Seg n holds SRz.i0 <= R0.i0 by A66; then
Sum SRz < Sum R0 by A72,RVSUM_1:83; then
Sum (sqr Rz) < n * (||. z .|| * r0)^2 by RVSUM_1:80; then
|. Rz .| < sqrt (n * (||. z .|| * r0)^2)
by A70,RVSUM_1:84,SQUARE_1:27; then
|. Rz .| < sqrt n * sqrt (||. z .|| * r0)^2 by A71,SQUARE_1:29; then
|. Rz .| < sqrt n * |. ||. z .|| * r0 .| by COMPLEX1:72; then
|. Rz .| < sqrt n * (||. z .|| * r0) by A42,A41,A65,ABSVALUE:def 1; then
|. Rz .| < sqrt n * r0 * ||. z .||; then
|. Rz .| / ||. z .|| < sqrt n * r0 by A65,XREAL_1:83; then
||. z .||" * ||. R/.z .|| < sqrt n * (sqrt n)"*r by REAL_NS1:1; then
||. z .||" * ||. R/.z .|| < 1*r by A73,XCMPLX_0:def 7;
hence ||. z .||" * ||. R/.z .|| < r;
end;
hence thesis by A63,A62,PARTFUN1:def 6;
end; then
reconsider R as RestFunc of REAL-NS m,REAL-NS n by NDIFF_1:23;
set N = {y where y is Point of REAL-NS m : ||. y - x0 .|| < d0};
reconsider N as Neighbourhood of x0 by A8,NFCONT_1:3;
now let x be object;
assume x in N; then
consider y be Point of REAL-NS m such that
A74: x = y & ||. y - x0 .|| < d0;
1 <= n by NAT_1:14; then
A75: 1 in Seg n & 1 in dom d by A6; then
A76: {z where z is Point of REAL-NS m : ||. z - x0 .|| < d/.1}
c= dom(Proj(1,n)*g) by A6;
dom(Proj(1,n)*g) c= dom g by RELAT_1:25; then
A77: {z where z is Point of REAL-NS m : ||. z - x0 .|| < d/.1} c= dom g
by A76,XBOOLE_1:1;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
len d = nn by A6,FINSEQ_1:def 3; then
1 <= len d by NAT_1:14; then
d0 <= d.1 by RFINSEQ2:2; then
d0 <= d/.1 by A75,PARTFUN1:def 6; then
||. y - x0 .|| < d/.1 by A74,XXREAL_0:2; then
y in {z where z is Point of REAL-NS m : ||. z - x0 .|| < d/.1};
hence x in dom g by A74,A77;
end; then
A78: N c= dom g by TARSKI:def 3;
ex L be Point of RB, R be RestFunc of REAL-NS m,REAL-NS n st
for x be Point of REAL-NS m st x in N holds
g/.x - g/.x0 = L.(x-x0) + R/.(x-x0)
proof
take L0;
take R;
hereby let x be Point of REAL-NS m;
assume x in N;
A79: dom R = the carrier of REAL-NS m by PARTFUN1:def 2;
R.(x-x0) = g/.(x-x0+x0) - g/.x0 - L.(x-x0) by A26; then
R.(x-x0) = g/.(x-(x0-x0)) - g/.x0 - L0.(x-x0) by RLVECT_1:29; then
R.(x-x0) = g/.(x-(x0 + -x0)) - g/.x0 - L0.(x-x0) by RLVECT_1:def 11; then
R.(x-x0) = g/.(x-0.(REAL-NS m)) - g/.x0 - L0.(x-x0) by RLVECT_1:5; then
R.(x-x0) = g/.x - g/.x0 - L0.(x-x0) by RLVECT_1:13; then
R.(x-x0) = g/.x - g/.x0 + -(L0.(x-x0)) by RLVECT_1:def 11; then
R/.(x-x0) = g/.x - g/.x0 + -(L0.(x-x0)) by A79,PARTFUN1:def 6; then
L0.(x-x0) + R/.(x-x0)
= g/.x - g/.x0 + (-(L0.(x-x0)) + L0.(x-x0)) by RLVECT_1:def 3; then
L0.(x-x0) + R/.(x-x0) = g/.x - g/.x0 + (0.(REAL-NS n)) by RLVECT_1:5;
hence g/.x - g/.x0 = L0.(x-x0) + R/.(x-x0) by RLVECT_1:4;
end;
end;
hence thesis by A78,NDIFF_1:def 6;
end;
hence thesis by Th28;
end;
definition
let X be set;
let n,m be non zero Nat;
let f be PartFunc of REAL m,REAL n;
pred f is_differentiable_on X means
X c= dom f &
for x be Element of REAL m st x in X holds f|X is_differentiable_in x;
end;
theorem Th30:
for X be set, m,n be non zero Nat, f be PartFunc of REAL m,REAL n,
g be PartFunc of REAL-NS m,REAL-NS n st f=g holds
f is_differentiable_on X iff g is_differentiable_on X
proof
let X be set,
m,n be non zero Nat,
f be PartFunc of REAL m,REAL n,
g be PartFunc of REAL-NS m,REAL-NS n;
assume A1: f=g;
A2: now assume A3: f is_differentiable_on X; then
A4: X c=dom f &
for x be Element of REAL m st x in X holds f|X is_differentiable_in x;
now let y be Point of REAL-NS m;
reconsider x=y as Element of REAL m by REAL_NS1:def 4;
assume y in X; then
f|X is_differentiable_in x by A3; then
ex g be PartFunc of REAL-NS m,REAL-NS n, y be Point of REAL-NS m st
(f|X)=g & x=y & g is_differentiable_in y by PDIFF_1:def 7;
hence g|X is_differentiable_in y by A1;
end;
hence g is_differentiable_on X by A1,A4,NDIFF_1:def 8;
end;
now assume A5: g is_differentiable_on X;
hence X c= dom f by A1,NDIFF_1:def 8;
A6: X c=dom g
& for x be Point of REAL-NS m st x in X holds g|X is_differentiable_in x
by A5,NDIFF_1:def 8;
now let y be Element of REAL m;
reconsider x=y as Point of REAL-NS m by REAL_NS1:def 4;
assume y in X; then
g|X is_differentiable_in x by A5,NDIFF_1:def 8;
hence f|X is_differentiable_in y by A1,PDIFF_1:def 7;
end;
hence f is_differentiable_on X by A1,A6;
end;
hence thesis by A2;
end;
theorem
for X be set, m,n be non zero Nat,
f be PartFunc of REAL m,REAL n holds
f is_differentiable_on X implies X is Subset of REAL m
by XBOOLE_1:1;
theorem
for m,n be non zero Nat, f be PartFunc of REAL m,REAL n,
Z be Subset of REAL m st
ex Z0 be Subset of REAL-NS m st Z=Z0 & Z0 is open
holds
( f is_differentiable_on Z
iff
Z c=dom f &
for x be Element of REAL m st x in Z holds f is_differentiable_in x )
proof
let m,n be non zero Nat;
let f be PartFunc of REAL m,REAL n;
let Z be Subset of REAL m;
assume ex Z0 be Subset of REAL-NS m st Z=Z0 & Z0 is open; then
consider Z0 be Subset of REAL-NS m such that
A1:Z=Z0 & Z0 is open;
the carrier of REAL-NS m = REAL m &
the carrier of REAL-NS n = REAL n by REAL_NS1:def 4; then
reconsider g=f as PartFunc of REAL-NS m,REAL-NS n;
A2:
g is_differentiable_on Z0 iff Z0 c=dom g &
for x be Point of REAL-NS m st x in Z0 holds g is_differentiable_in x
by A1,NDIFF_1:31;
thus f is_differentiable_on Z implies Z c=dom f & for x be Element of REAL m
st x in Z holds f is_differentiable_in x
by A1,A2,Th30,PDIFF_1:def 7;
assume
A3: Z c=dom f &
for x be Element of REAL m st x in Z holds f is_differentiable_in x;
now let y be Point of REAL-NS m;
reconsider x=y as Element of REAL m by REAL_NS1:def 4;
assume y in Z0; then
f is_differentiable_in x by A1,A3; then
ex g be PartFunc of REAL-NS m,REAL-NS n, y be Point of REAL-NS m st
f=g & x=y & g is_differentiable_in y by PDIFF_1:def 7;
hence g is_differentiable_in y;
end;
hence f is_differentiable_on Z by A1,A2,A3,Th30;
end;
theorem
for m,n be non zero Nat, f be PartFunc of REAL m,REAL n,
Z be Subset of REAL m st
f is_differentiable_on Z
ex Z0 be Subset of REAL-NS m st Z=Z0 & Z0 is open
proof
let m,n be non zero Nat;
let f be PartFunc of REAL m,REAL n,
Z be Subset of REAL m;
assume A1: f is_differentiable_on Z;
the carrier of REAL-NS m = REAL m &
the carrier of REAL-NS n = REAL n by REAL_NS1:def 4; then
reconsider g=f as PartFunc of REAL-NS m,REAL-NS n;
reconsider Z0=Z as Subset of REAL-NS m by REAL_NS1:def 4;
take Z0;
g is_differentiable_on Z0 by A1,Th30;
hence thesis by NDIFF_1:32;
end;