:: by Takao Inou\'e , Noboru Endou and Yasunari Shidama

::

:: Received February 23, 2010

:: Copyright (c) 2010-2016 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) )

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 )

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)

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

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

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

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

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

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

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)))

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);

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

:: 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) );

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) );

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

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 )

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 )

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;

coherence

for b_{1} being Function of (REAL m),(REAL n) st b_{1} = (REAL m) --> (0* n) holds

( b_{1} is additive & b_{1} is homogeneous )

end;
coherence

for b

( b

proof end;

registration

let n, m be Nat;

ex b_{1} being Function of (REAL m),(REAL n) st

( b_{1} is additive & b_{1} is homogeneous )

end;
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

( b

proof end;

definition
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) )

for f being set holds

( f is LinearOperator of m,n iff f is LinearOperator of (REAL-NS m),(REAL-NS n) )

proof 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.| ) ) );

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 )

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)

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

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;

for b_{1} being LinearOperator of m,n holds b_{1} is Lipschitzian

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

coherence for b

proof end;

registration

let m, n be Nat;

for b_{1} being LinearOperator of (REAL-NS m),(REAL-NS n) holds b_{1} is Lipschitzian

end;
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

proof 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)

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

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)) )

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)) )

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)) )

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 }

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 )

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)) ) ) ) )

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;

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)

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)

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) )

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 )

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);

end;
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 ) );

( X c= dom f & ( for x being Element of REAL m st x in X holds

f | X is_differentiable_in x ) );

:: 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 ) ) );

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 )

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;

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 ) ) )

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 )

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;

:: Normed Linear Spaces $ {\cal R}^n$