:: 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-2012 Association of Mizar Users


begin

theorem Th1: :: PDIFF_6:1
for m, n being Element of NAT
for f being set holds
( f is PartFunc of (REAL m),(REAL n) iff f is PartFunc of (REAL-NS m),(REAL-NS n) )
proofend;

theorem Th2: :: PDIFF_6:2
for n, m being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Element of REAL m
for y being Point of (REAL-NS m) st f = g & x = y holds
( f is_differentiable_in x iff g is_differentiable_in y )
proofend;

theorem Th3: :: PDIFF_6:3
for n, m being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Element of REAL m
for y being Point of (REAL-NS m) st f = g & x = y & f is_differentiable_in x holds
diff (f,x) = diff (g,y)
proofend;

theorem Th4: :: PDIFF_6:4
for m, n being Element of NAT
for f1, f2 being PartFunc of (REAL m),(REAL n)
for g1, g2 being PartFunc of (REAL-NS m),(REAL-NS n) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2
proofend;

theorem Th5: :: PDIFF_6:5
for m, n being Element of NAT
for f1, f2 being PartFunc of (REAL m),(REAL n)
for g1, g2 being PartFunc of (REAL-NS m),(REAL-NS n) st f1 = g1 & f2 = g2 holds
f1 - f2 = g1 - g2
proofend;

theorem Th6: :: PDIFF_6:6
for m, n being Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for a being Real st f = g holds
a (#) f = a (#) g
proofend;

theorem Th7: :: PDIFF_6:7
for m, n being Element of NAT
for f1, f2 being Function of (REAL m),(REAL n)
for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2
proofend;

theorem Th8: :: PDIFF_6:8
for m, n being Element of NAT
for f1, f2 being Function of (REAL m),(REAL n)
for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) st f1 = g1 & f2 = g2 holds
f1 - f2 = g1 - g2
proofend;

theorem Th9: :: PDIFF_6:9
for m, n being Element of NAT
for f being Function of (REAL m),(REAL n)
for g being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for r being Real st f = g holds
r (#) f = r * g
proofend;

theorem Th10: :: PDIFF_6:10
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x being 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)))
proofend;

definition
let n, m be Nat;
let IT be Function of (REAL m),(REAL n);
attrIT is additive  means :Def1: :: PDIFF_6:def 1
 for x, y being Element of REAL m holds IT . (x + y) = (IT . x) + (IT . y);
attrIT is homogeneous  means :Def2: :: PDIFF_6:def 2
 for x being Element of REAL m
for r being Real holds IT . (r * x) = r * (IT . x);
end;

:: deftheorem Def1 defines additive PDIFF_6:def_1_:_
 for n, m being Nat
for IT being Function of (REAL m),(REAL n) holds
( IT is additive iff for x, y being Element of REAL m holds IT . (x + y) = (IT . x) + (IT . y) );

:: deftheorem Def2 defines homogeneous PDIFF_6:def_2_:_
 for n, m being Nat
for IT being Function of (REAL m),(REAL n) holds
( IT is homogeneous iff for x being Element of REAL m
for r being Real holds IT . (r * x) = r * (IT . x) );

theorem Th11: :: PDIFF_6:11
for m, n being Element of NAT
for IT being Function of (REAL m),(REAL n) st IT is additive holds
IT . (0* m) = 0* n
proofend;

theorem Th12: :: PDIFF_6:12
for m, n being Element of NAT
for f being Function of (REAL m),(REAL n)
for g being Function of (REAL-NS m),(REAL-NS n) st f = g holds
( f is additive iff g is additive )
proofend;

theorem Th13: :: PDIFF_6:13
for m, n being Element of NAT
for f being Function of (REAL m),(REAL n)
for g being Function of (REAL-NS m),(REAL-NS n) st f = g holds
( f is homogeneous iff g is homogeneous )
proofend;

registration
let n, m be Nat;
cluster(REAL m) --> (0* n) ->  additive homogeneous for Function of (REAL m),(REAL n);
coherence
 for b1 being Function of (REAL m),(REAL n) st b1 = (REAL m) --> (0* n) holds
( b1 is additive & b1 is homogeneous )
proofend;
end;

registration
let n, m be Nat;
cluster non empty Relation-like REAL m -defined REAL n -valued Function-like total V30( REAL m, REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued additive homogeneous for Element of K6(K7((REAL m),(REAL n)));
existence
 ex b1 being Function of (REAL m),(REAL n) st
( b1 is additive & b1 is homogeneous )
proofend;
end;

definition
let m, n be Nat;
mode LinearOperator of m,n is additive homogeneous Function of (REAL m),(REAL n);
end;

theorem Th14: :: PDIFF_6:14
for m, n being Element of NAT
for f being set holds
( f is LinearOperator of m,n iff f is LinearOperator of (REAL-NS m),(REAL-NS n) )
proofend;

definition
let m, n be Nat;
let IT be Function of (REAL m),(REAL n);
let x be Element of REAL m;
:: original:.
redefine funcIT . x ->  Element of REAL n;
coherence
 IT . x is Element of REAL n
proofend;
end;

definition
let m, n be Nat;
let IT be Function of (REAL m),(REAL n);
attrIT is Lipschitzian  means :Def3: :: PDIFF_6:def 3
 ex K being Real st
( 0 <= K &amp; ( for x being Element of REAL m holds |.(IT . x).| <= K * |.x.| ) );
end;

:: deftheorem Def3 defines Lipschitzian PDIFF_6:def_3_:_
 for m, n being Nat
for IT being Function of (REAL m),(REAL n) holds
( IT is Lipschitzian iff ex K being Real st
( 0 <= K &amp; ( for x being Element of REAL m holds |.(IT . x).| <= K * |.x.| ) ) );

theorem Th15: :: PDIFF_6:15
for m being Element of NAT
for xseq, yseq being FinSequence of REAL m st len xseq = (len yseq) + 1 &amp; xseq | (len yseq) = yseq holds
ex v being Element of REAL m st
( v = xseq . (len xseq) &amp; Sum xseq = (Sum yseq) + v )
proofend;

theorem Th16: :: PDIFF_6:16
for m, n being Element of NAT
for f being LinearOperator of m,n
for xseq being FinSequence of REAL m
for yseq being FinSequence of REAL n st len xseq = len yseq &amp; ( for i being Element of NAT st i in dom xseq holds
yseq . i = f . (xseq . i) ) holds
Sum yseq = f . (Sum xseq)
proofend;

theorem Th17: :: PDIFF_6:17
for m being Element of NAT
for xseq being FinSequence of REAL m
for yseq being FinSequence of REAL st len xseq = len yseq &amp; ( for i being Element of NAT st i in dom xseq holds
ex v being Element of REAL m st
( v = xseq . i &amp; yseq . i = |.v.| ) ) holds
|.(Sum xseq).| <= Sum yseq
proofend;

registration
let m, n be Nat;
cluster Function-like V30( REAL m, REAL n) additive homogeneous  ->  Lipschitzian for Element of K6(K7((REAL m),(REAL n)));
coherence
 for b1 being LinearOperator of m,n holds b1 is Lipschitzian
proofend;
end;

registration
let m, n be Element of NAT ;
cluster Function-like V30( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) additive homogeneous  ->  Lipschitzian for Element of K6(K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n)));
coherence
 for b1 being LinearOperator of (REAL-NS m),(REAL-NS n) holds b1 is Lipschitzian
proofend;
end;

theorem Th18: :: PDIFF_6:18
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_differentiable_in x holds
diff (f,x) is LinearOperator of (REAL-NS m),(REAL-NS n)
proofend;

theorem :: PDIFF_6:19
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_differentiable_in x holds
diff (f,x) is LinearOperator of m,n
proofend;

theorem :: PDIFF_6:20
for n, m being non empty Element of NAT
for g1, g2 being PartFunc of (REAL m),(REAL n)
for y0 being Element of REAL m st g1 is_differentiable_in y0 &amp; g2 is_differentiable_in y0 holds
( g1 + g2 is_differentiable_in y0 &amp; diff ((g1 + g2),y0) = (diff (g1,y0)) + (diff (g2,y0)) )
proofend;

theorem :: PDIFF_6:21
for n, m being non empty Element of NAT
for g1, g2 being PartFunc of (REAL m),(REAL n)
for y0 being Element of REAL m st g1 is_differentiable_in y0 &amp; g2 is_differentiable_in y0 holds
( g1 - g2 is_differentiable_in y0 &amp; diff ((g1 - g2),y0) = (diff (g1,y0)) - (diff (g2,y0)) )
proofend;

theorem :: PDIFF_6:22
for n, m being non empty Element of NAT
for g being PartFunc of (REAL m),(REAL n)
for y0 being Element of REAL m
for r being Real st g is_differentiable_in y0 holds
( r (#) g is_differentiable_in y0 &amp; diff ((r (#) g),y0) = r (#) (diff (g,y0)) )
proofend;

theorem Th23: :: PDIFF_6:23
for m being Element of NAT
for x0 being Element of REAL m
for y0 being Point of (REAL-NS m)
for r being 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  }
proofend;

theorem Th24: :: PDIFF_6:24
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x0 being Element of REAL m
for L, R being Function of (REAL m),(REAL n) st L is LinearOperator of m,n &amp; ex r0 being Real st
( 0 < r0 &amp;  {  y where y is Element of REAL m : |.(y - x0).| < r0  }  c= dom f &amp; ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 &amp; ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m &amp; |.z.| < d &amp; w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) &amp; ( for x being 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 &amp; diff (f,x0) = L )
proofend;

theorem :: PDIFF_6:25
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for x0 being Element of REAL m holds
( f is_differentiable_in x0 iff ex r0 being Real st
( 0 < r0 &amp;  {  y where y is Element of REAL m : |.(y - x0).| < r0  }  c= dom f &amp; ex L, R being Function of (REAL m),(REAL n) st
( L is LinearOperator of m,n &amp; ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 &amp; ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m &amp; |.z.| < d &amp; w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) &amp; ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )
proofend;

begin

::Differentiation of Functions from Normed Linear Spaces $ {\cal R}^m$ to
:: Normed Linear Spaces $ {\cal R}^n$
theorem Th26: :: PDIFF_6:26
for n, i being Element of NAT
for y1, y2 being Point of (REAL-NS n) holds (Proj (i,n)) . (y1 + y2) = ((Proj (i,n)) . y1) + ((Proj (i,n)) . y2)
proofend;

theorem Th27: :: PDIFF_6:27
for n, i being Element of NAT
for y1 being Point of (REAL-NS n)
for r being Real holds (Proj (i,n)) . (r * y1) = r * ((Proj (i,n)) . y1)
proofend;

theorem Th28: :: PDIFF_6:28
for m, n being non empty Element of NAT
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x0 being Point of (REAL-NS m)
for i being Element of NAT st 1 <= i &amp; i <= n &amp; g is_differentiable_in x0 holds
( (Proj (i,n)) * g is_differentiable_in x0 &amp; (Proj (i,n)) * (diff (g,x0)) = diff (((Proj (i,n)) * g),x0) )
proofend;

theorem :: PDIFF_6:29
for m, n being non empty Element of NAT
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x0 being Point of (REAL-NS m) holds
( g is_differentiable_in x0 iff for i being Element of NAT st 1 <= i &amp; i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 )
proofend;

definition
let X be set ;
let n, m be non empty Element of NAT ;
let f be PartFunc of (REAL m),(REAL n);
predf is_differentiable_on X means :Def4: :: PDIFF_6:def 4
( X c= dom f &amp; ( for x being Element of REAL m st x in X holds
f | X is_differentiable_in x ) );
end;

:: deftheorem Def4 defines is_differentiable_on PDIFF_6:def_4_:_
 for X being set
for n, m being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n) holds
( f is_differentiable_on X iff ( X c= dom f &amp; ( for x being Element of REAL m st x in X holds
f | X is_differentiable_in x ) ) );

theorem Th30: :: PDIFF_6:30
for X being set
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n) st f = g holds
( f is_differentiable_on X iff g is_differentiable_on X )
proofend;

theorem :: PDIFF_6:31
for X being set
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n) st f is_differentiable_on X holds
X is Subset of (REAL m)
proofend;

theorem :: PDIFF_6:32
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for Z being Subset of (REAL m) st ex Z0 being Subset of (REAL-NS m) st
( Z = Z0 &amp; Z0 is open ) holds
( f is_differentiable_on Z iff ( Z c= dom f &amp; ( for x being Element of REAL m st x in Z holds
f is_differentiable_in x ) ) )
proofend;

theorem :: PDIFF_6:33
for m, n being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for Z being Subset of (REAL m) st f is_differentiable_on Z holds
ex Z0 being Subset of (REAL-NS m) st
( Z = Z0 &amp; Z0 is open )
proofend;