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

theorem Th1: :: PDIFF_6:1

for n, m being 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) )

proof end;

theorem Th2: :: PDIFF_6:2

for n, m being non zero 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 )

proof end;

theorem Th3: :: PDIFF_6:3

for n, m being non zero 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)

proof end;

theorem Th4: :: PDIFF_6:4

for n, m being 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

proof end;

theorem Th5: :: PDIFF_6:5

for n, m being 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

proof end;

theorem Th6: :: PDIFF_6:6

for n, m being 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

proof end;

theorem Th7: :: PDIFF_6:7

for n, m being 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

proof end;

theorem Th8: :: PDIFF_6:8

for n, m being 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

proof end;

theorem Th9: :: PDIFF_6:9

for n, m being 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

proof end;

theorem Th10: :: PDIFF_6:10

for m, n being non zero 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)))

proof end;

definition

let n, m be Nat;
let IT be Function of (REAL m),(REAL n);

attr IT is additive means :Def1: :: PDIFF_6:def 1
for x, y being Element of REAL m holds IT . (x + y) = (IT . x) + (IT . y);

attr IT 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 n, m being Nat
for IT being Function of (REAL m),(REAL n) st IT is additive holds
IT . (0* m) = 0* n

proof end;

theorem Th12: :: PDIFF_6:12

for n, m being 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 )

proof end;

theorem Th13: :: PDIFF_6:13

for n, m being 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 )

proof end;

registration

let n, m be Nat;

cluster (REAL m) --> (0* n) -> additive homogeneous for Function of (REAL m),(REAL n);

coherence
for b₁ being Function of (REAL m),(REAL n) st b₁ = (REAL m) --> (0* n) holds
( b₁ is additive & b₁ is homogeneous )

proof end;

end;

registration

let n, m be Nat;

cluster Relation-like REAL m -defined REAL n -valued non empty Function-like total V30( REAL m, REAL n) Function-yielding complex-functions-valued ext-real-functions-valued real-functions-valued additive homogeneous for Element of K16(K17((REAL m),(REAL n)));

existence
ex b₁ being Function of (REAL m),(REAL n) st
( b₁ is additive & b₁ is homogeneous )

proof 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: :: PDIFF_6:14

for n, m being Nat
for f being set holds
( f is LinearOperator of m,n iff f is LinearOperator of (REAL-NS m),(REAL-NS n) )

proof end;

definition

let m, n be Nat;
let IT be Function of (REAL m),(REAL n);

attr IT is Lipschitzian means :Def3: :: PDIFF_6:def 3
ex K being Real st
( 0 <= K & ( 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 & ( for x being Element of REAL m holds |.(IT . x).| <= K * |.x.| ) ) );

theorem Th15: :: PDIFF_6:15

for m being Nat
for xseq, yseq being FinSequence of REAL m st len xseq = (len yseq) + 1 & xseq | (len yseq) = yseq holds
ex v being Element of REAL m st
( v = xseq . (len xseq) & Sum xseq = (Sum yseq) + v )

proof end;

theorem Th16: :: PDIFF_6:16

for n, m being 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 & ( for i being Nat st i in dom xseq holds
yseq . i = f . (xseq . i) ) holds
Sum yseq = f . (Sum xseq)

proof end;

theorem Th17: :: PDIFF_6:17

for m being Nat
for xseq being FinSequence of REAL m
for yseq being FinSequence of REAL st len xseq = len yseq & ( for i being Nat st i in dom xseq holds
ex v being Element of REAL m st
( v = xseq . i & yseq . i = |.v.| ) ) holds
|.(Sum xseq).| <= Sum yseq

proof end;

registration

let m, n be Nat;

cluster Function-like V30( REAL m, REAL n) additive homogeneous -> Lipschitzian for Element of K16(K17((REAL m),(REAL n)));

coherence
for b₁ being LinearOperator of m,n holds b₁ is Lipschitzian

proof end;

end;

registration

let m, n be Nat;

cluster Function-like V30( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) additive homogeneous -> Lipschitzian for Element of K16(K17( the carrier of (REAL-NS m), the carrier of (REAL-NS n)));

coherence
for b₁ being LinearOperator of (REAL-NS m),(REAL-NS n) holds b₁ is Lipschitzian

proof end;

end;

theorem Th18: :: PDIFF_6:18

for m, n being non zero 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)

proof end;

theorem :: PDIFF_6:19

for m, n being non zero 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

proof end;

theorem :: PDIFF_6:20

for n, m being non zero Nat
for g1, g2 being PartFunc of (REAL m),(REAL n)
for y0 being 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 end;

theorem :: PDIFF_6:21

for n, m being non zero Nat
for g1, g2 being PartFunc of (REAL m),(REAL n)
for y0 being 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 end;

theorem :: PDIFF_6:22

for n, m being non zero 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 & diff ((r (#) g),y0) = r (#) (diff (g,y0)) )

proof end;

theorem Th23: :: PDIFF_6:23

for m being 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 }

proof end;

theorem Th24: :: PDIFF_6:24

for m, n being non zero 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 & ex r0 being Real st
( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( 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 & diff (f,x0) = L )

proof end;

theorem :: PDIFF_6:25

for m, n being non zero 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 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ex L, R being Function of (REAL m),(REAL n) st
( L is LinearOperator of m,n & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )

proof end;

::Differentiation of Functions from Normed Linear Spaces $ {\cal R}^m$ to
:: Normed Linear Spaces $ {\cal R}^n$

theorem Th26: :: PDIFF_6:26

for i, n being Nat
for y1, y2 being Point of (REAL-NS n) holds (Proj (i,n)) . (y1 + y2) = ((Proj (i,n)) . y1) + ((Proj (i,n)) . y2)

proof end;

theorem Th27: :: PDIFF_6:27

for i, n being Nat
for y1 being Point of (REAL-NS n)
for r being Real holds (Proj (i,n)) . (r * y1) = r * ((Proj (i,n)) . y1)

proof end;

theorem Th28: :: PDIFF_6:28

for m, n being non zero Nat
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x0 being Point of (REAL-NS m)
for i being 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 end;

theorem :: PDIFF_6:29

for m, n being non zero 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 Nat st 1 <= i & i <= n holds
(Proj (i,n)) * g is_differentiable_in x0 )

proof 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 :: PDIFF_6:def 4
( X c= dom f & ( for x being Element of REAL m st x in X holds
f | X is_differentiable_in x ) );

end;

:: deftheorem defines is_differentiable_on PDIFF_6:def 4 :
for X being set
for n, m being non zero Nat
for f being PartFunc of (REAL m),(REAL n) holds
( f is_differentiable_on X iff ( X c= dom f & ( 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 zero 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 )

proof end;

theorem :: PDIFF_6:31

for X being set
for m, n being non zero Nat
for f being PartFunc of (REAL m),(REAL n) st f is_differentiable_on X holds
X is Subset of (REAL m) by XBOOLE_1:1;

theorem :: PDIFF_6:32

for m, n being non zero 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 & Z0 is open ) holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_differentiable_in x ) ) )

proof end;

theorem :: PDIFF_6:33

for m, n being non zero 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 & Z0 is open )

proof end;