:: Partial Differentiation on Normed Linear Spaces $ {\cal R}^n$
:: by Noboru Endou , Yasunari Shidama and Keiichi Miyajima
::
:: Received June 6, 2007
:: Copyright (c) 2007 Association of Mizar Users
:: deftheorem Def1 defines proj PDIFF_1:def 1 :
set W = (proj 1,1) " ;
Lm1:
( proj 1,1 is bijective & dom (proj 1,1) = REAL 1 & rng (proj 1,1) = REAL & ( for x being Element of REAL holds
( (proj 1,1) . <*x*> = x & ((proj 1,1) " ) . x = <*x*> ) ) )
theorem :: PDIFF_1:1
theorem Th2: :: PDIFF_1:2
:: deftheorem defines <>* PDIFF_1:def 2 :
:: deftheorem defines <>* PDIFF_1:def 3 :
definition
let i,
n be
Element of
NAT ;
func Proj i,
n -> Function of
(REAL-NS n),
(REAL-NS 1) means :
Def4:
:: PDIFF_1:def 4
for
x being
Point of
(REAL-NS n) holds
it . x = <*((proj i,n) . x)*>;
existence
ex b1 being Function of (REAL-NS n),(REAL-NS 1) st
for x being Point of (REAL-NS n) holds b1 . x = <*((proj i,n) . x)*>
uniqueness
for b1, b2 being Function of (REAL-NS n),(REAL-NS 1) st ( for x being Point of (REAL-NS n) holds b1 . x = <*((proj i,n) . x)*> ) & ( for x being Point of (REAL-NS n) holds b2 . x = <*((proj i,n) . x)*> ) holds
b1 = b2
end;
:: deftheorem Def4 defines Proj PDIFF_1:def 4 :
definition
let i be
Element of
NAT ;
let x be
FinSequence of
REAL ;
func reproj i,
x -> Function means :
Def5:
:: PDIFF_1:def 5
(
dom it = REAL & ( for
r being
Element of
REAL holds
it . r = Replace x,
i,
r ) );
existence
ex b1 being Function st
( dom b1 = REAL & ( for r being Element of REAL holds b1 . r = Replace x,i,r ) )
uniqueness
for b1, b2 being Function st dom b1 = REAL & ( for r being Element of REAL holds b1 . r = Replace x,i,r ) & dom b2 = REAL & ( for r being Element of REAL holds b2 . r = Replace x,i,r ) holds
b1 = b2
end;
:: deftheorem Def5 defines reproj PDIFF_1:def 5 :
definition
let n,
i be
Element of
NAT ;
let x be
Point of
(REAL-NS n);
func reproj i,
x -> Function of
(REAL-NS 1),
(REAL-NS n) means :
Def6:
:: PDIFF_1:def 6
for
r being
Element of
(REAL-NS 1) ex
q being
Element of
REAL ex
y being
Element of
REAL n st
(
r = <*q*> &
y = x &
it . r = (reproj i,y) . q );
existence
ex b1 being Function of (REAL-NS 1),(REAL-NS n) st
for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st
( r = <*q*> & y = x & b1 . r = (reproj i,y) . q )
uniqueness
for b1, b2 being Function of (REAL-NS 1),(REAL-NS n) st ( for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st
( r = <*q*> & y = x & b1 . r = (reproj i,y) . q ) ) & ( for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st
( r = <*q*> & y = x & b2 . r = (reproj i,y) . q ) ) holds
b1 = b2
end;
:: deftheorem Def6 defines reproj PDIFF_1:def 6 :
:: deftheorem Def7 defines is_differentiable_in PDIFF_1:def 7 :
definition
let m,
n be non
empty Element of
NAT ;
let f be
PartFunc of
REAL m,
REAL n;
let x be
Element of
REAL m;
assume A1:
f is_differentiable_in x
;
func diff f,
x -> Function of
REAL m,
REAL n means :
Def8:
:: PDIFF_1:def 8
ex
g being
PartFunc of
(REAL-NS m),
(REAL-NS n) ex
y being
Point of
(REAL-NS m) st
(
f = g &
x = y &
it = diff g,
y );
correctness
existence
ex b1 being Function of REAL m, REAL n ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b1 = diff g,y );
uniqueness
for b1, b2 being Function of REAL m, REAL n st ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b1 = diff g,y ) & ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b2 = diff g,y ) holds
b1 = b2;
end;
:: deftheorem Def8 defines diff PDIFF_1:def 8 :
theorem Th3: :: PDIFF_1:3
reconsider I = (proj 1,1) " as Function of REAL , REAL 1 by Th2;
theorem Th4: :: PDIFF_1:4
theorem Th5: :: PDIFF_1:5
theorem Th6: :: PDIFF_1:6
theorem Th7: :: PDIFF_1:7
theorem Th8: :: PDIFF_1:8
theorem :: PDIFF_1:9
theorem Th10: :: PDIFF_1:10
:: deftheorem Def9 defines is_partial_differentiable_in PDIFF_1:def 9 :
definition
let m,
n be non
empty Element of
NAT ;
let i be
Element of
NAT ;
let f be
PartFunc of
(REAL-NS m),
(REAL-NS n);
let x be
Point of
(REAL-NS m);
func partdiff f,
x,
i -> Point of
(R_NormSpace_of_BoundedLinearOperators (REAL-NS 1),(REAL-NS n)) equals :: PDIFF_1:def 10
diff (f * (reproj i,x)),
((Proj i,m) . x);
coherence
diff (f * (reproj i,x)),((Proj i,m) . x) is Point of (R_NormSpace_of_BoundedLinearOperators (REAL-NS 1),(REAL-NS n))
;
end;
:: deftheorem defines partdiff PDIFF_1:def 10 :
:: deftheorem Def11 defines is_partial_differentiable_in PDIFF_1:def 11 :
:: deftheorem defines partdiff PDIFF_1:def 12 :
theorem Th11: :: PDIFF_1:11
theorem Th12: :: PDIFF_1:12
theorem Th13: :: PDIFF_1:13
theorem Th14: :: PDIFF_1:14
theorem Th15: :: PDIFF_1:15
:: deftheorem Def13 defines is_partial_differentiable_in PDIFF_1:def 13 :
definition
let m,
n be non
empty Element of
NAT ;
let i be
Element of
NAT ;
let f be
PartFunc of
REAL m,
REAL n;
let x be
Element of
REAL m;
assume A1:
f is_partial_differentiable_in x,
i
;
func partdiff f,
x,
i -> Element of
REAL n means :
Def14:
:: PDIFF_1:def 14
ex
g being
PartFunc of
(REAL-NS m),
(REAL-NS n) ex
y being
Point of
(REAL-NS m) st
(
f = g &
x = y &
it = (partdiff g,y,i) . <*1*> );
correctness
existence
ex b1 being Element of REAL n ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b1 = (partdiff g,y,i) . <*1*> );
uniqueness
for b1, b2 being Element of REAL n st ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b1 = (partdiff g,y,i) . <*1*> ) & ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & b2 = (partdiff g,y,i) . <*1*> ) holds
b1 = b2;
end;
:: deftheorem Def14 defines partdiff PDIFF_1:def 14 :
theorem Th16: :: PDIFF_1:16
theorem Th17: :: PDIFF_1:17
theorem :: PDIFF_1:18
theorem :: PDIFF_1:19
:: deftheorem Def15 defines is_partial_differentiable_in PDIFF_1:def 15 :
definition
let m,
n be non
empty Element of
NAT ;
let i,
j be
Element of
NAT ;
let f be
PartFunc of
(REAL-NS m),
(REAL-NS n);
let x be
Point of
(REAL-NS m);
func partdiff f,
x,
i,
j -> Point of
(R_NormSpace_of_BoundedLinearOperators (REAL-NS 1),(REAL-NS 1)) equals :: PDIFF_1:def 16
diff (((Proj j,n) * f) * (reproj i,x)),
((Proj i,m) . x);
correctness
coherence
diff (((Proj j,n) * f) * (reproj i,x)),((Proj i,m) . x) is Point of (R_NormSpace_of_BoundedLinearOperators (REAL-NS 1),(REAL-NS 1));
;
end;
:: deftheorem defines partdiff PDIFF_1:def 16 :
for
m,
n being non
empty Element of
NAT for
i,
j being
Element of
NAT for
f being
PartFunc of
(REAL-NS m),
(REAL-NS n) for
x being
Point of
(REAL-NS m) holds
partdiff f,
x,
i,
j = diff (((Proj j,n) * f) * (reproj i,x)),
((Proj i,m) . x);
:: deftheorem Def17 defines is_partial_differentiable_in PDIFF_1:def 17 :
definition
let m,
n be non
empty Element of
NAT ;
let i,
j be
Element of
NAT ;
let h be
PartFunc of
REAL m,
REAL n;
let z be
Element of
REAL m;
func partdiff h,
z,
i,
j -> real number equals :: PDIFF_1:def 18
diff (((proj j,n) * h) * (reproj i,z)),
((proj i,m) . z);
correctness
coherence
diff (((proj j,n) * h) * (reproj i,z)),((proj i,m) . z) is real number ;
;
end;
:: deftheorem defines partdiff PDIFF_1:def 18 :
for
m,
n being non
empty Element of
NAT for
i,
j being
Element of
NAT for
h being
PartFunc of
REAL m,
REAL n for
z being
Element of
REAL m holds
partdiff h,
z,
i,
j = diff (((proj j,n) * h) * (reproj i,z)),
((proj i,m) . z);
theorem Th20: :: PDIFF_1:20
theorem :: PDIFF_1:21
theorem Th22: :: PDIFF_1:22
theorem :: PDIFF_1:23
theorem :: PDIFF_1:24
for
n,
m being non
empty Element of
NAT for
i,
j being
Element of
NAT for
f being
PartFunc of
(REAL-NS m),
(REAL-NS n) for
h being
PartFunc of
REAL m,
REAL n for
x being
Point of
(REAL-NS m) for
z being
Element of
REAL m st
f = h &
x = z &
f is_partial_differentiable_in x,
i,
j holds
(partdiff f,x,i,j) . <*1*> = <*(partdiff h,z,i,j)*>
:: deftheorem Def19 defines is_partial_differentiable_on PDIFF_1:def 19 :
theorem Th25: :: PDIFF_1:25
definition
let m,
n be non
empty Element of
NAT ;
let i be
Element of
NAT ;
let f be
PartFunc of
(REAL-NS m),
(REAL-NS n);
let X be
set ;
assume A1:
f is_partial_differentiable_on X,
i
;
func f `partial| X,
i -> PartFunc of
(REAL-NS m),
(R_NormSpace_of_BoundedLinearOperators (REAL-NS 1),(REAL-NS n)) means :: PDIFF_1:def 20
(
dom it = X & ( for
x being
Point of
(REAL-NS m) st
x in X holds
it /. x = partdiff f,
x,
i ) );
existence
ex b1 being PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators (REAL-NS 1),(REAL-NS n)) st
( dom b1 = X & ( for x being Point of (REAL-NS m) st x in X holds
b1 /. x = partdiff f,x,i ) )
uniqueness
for b1, b2 being PartFunc of (REAL-NS m),(R_NormSpace_of_BoundedLinearOperators (REAL-NS 1),(REAL-NS n)) st dom b1 = X & ( for x being Point of (REAL-NS m) st x in X holds
b1 /. x = partdiff f,x,i ) & dom b2 = X & ( for x being Point of (REAL-NS m) st x in X holds
b2 /. x = partdiff f,x,i ) holds
b1 = b2
end;
:: deftheorem defines `partial| PDIFF_1:def 20 :
theorem Th26: :: PDIFF_1:26
theorem Th27: :: PDIFF_1:27
theorem Th28: :: PDIFF_1:28
for
n,
m being non
empty Element of
NAT for
i being
Element of
NAT for
f1,
f2 being
PartFunc of
(REAL-NS m),
(REAL-NS n) for
x being
Point of
(REAL-NS m) st
f1 is_partial_differentiable_in x,
i &
f2 is_partial_differentiable_in x,
i holds
(
f1 + f2 is_partial_differentiable_in x,
i &
partdiff (f1 + f2),
x,
i = (partdiff f1,x,i) + (partdiff f2,x,i) )
theorem :: PDIFF_1:29
for
n being non
empty Element of
NAT for
i being
Element of
NAT for
g1,
g2 being
PartFunc of
REAL n,
REAL for
y being
Element of
REAL n st
g1 is_partial_differentiable_in y,
i &
g2 is_partial_differentiable_in y,
i holds
(
g1 + g2 is_partial_differentiable_in y,
i &
partdiff (g1 + g2),
y,
i = (partdiff g1,y,i) + (partdiff g2,y,i) )
theorem Th30: :: PDIFF_1:30
for
n,
m being non
empty Element of
NAT for
i being
Element of
NAT for
f1,
f2 being
PartFunc of
(REAL-NS m),
(REAL-NS n) for
x being
Point of
(REAL-NS m) st
f1 is_partial_differentiable_in x,
i &
f2 is_partial_differentiable_in x,
i holds
(
f1 - f2 is_partial_differentiable_in x,
i &
partdiff (f1 - f2),
x,
i = (partdiff f1,x,i) - (partdiff f2,x,i) )
theorem :: PDIFF_1:31
for
n being non
empty Element of
NAT for
i being
Element of
NAT for
g1,
g2 being
PartFunc of
REAL n,
REAL for
y being
Element of
REAL n st
g1 is_partial_differentiable_in y,
i &
g2 is_partial_differentiable_in y,
i holds
(
g1 - g2 is_partial_differentiable_in y,
i &
partdiff (g1 - g2),
y,
i = (partdiff g1,y,i) - (partdiff g2,y,i) )
theorem Th32: :: PDIFF_1:32
theorem :: PDIFF_1:33