environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, CARD_3, FUNCT_1, RELAT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, PARTFUN1, BORSUK_1, REAL_NS1, PRE_TOPC, AFINSQ_1, XBOOLE_0, FDIFF_1, STRUCT_0, RLVECT_1, NORMSP_1, COMPLEX1, ARYTM_3, REAL_1, ARYTM_1, SQUARE_1, RVSUM_1, LOPBAN_1, XXREAL_0, CARD_1, SUPINF_2, SEQ_1, VALUED_1, SEQ_2, ORDINAL2, VALUED_0, TARSKI, NAT_1, RCOMP_1, XXREAL_1, PDIFF_1, FCONT_1, FUNCT_7, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, XCMPLX_0, FUNCT_2, FUNCT_7, PRE_TOPC, XREAL_0, COMPLEX1, ORDINAL1, NUMBERS, REAL_1, RLVECT_1, VALUED_0, VALUED_1, SEQ_1, SEQ_2, RVSUM_1, FINSEQ_1, FINSEQ_2, FINSEQ_7, SQUARE_1, RCOMP_1, VFUNCT_1, NORMSP_0, NORMSP_1, EUCLID, LOPBAN_1, NFCONT_1, FDIFF_1, NDIFF_1, REAL_NS1, XXREAL_0, STRUCT_0;
definitions TARSKI;
theorems TARSKI, ABSVALUE, XBOOLE_0, XBOOLE_1, XREAL_0, RCOMP_1, RLVECT_1, SEQ_4, COMPLEX1, SEQ_1, SEQ_2, FINSEQ_1, FINSEQ_2, FINSEQ_7, RVSUM_1, RELAT_1, FUNCT_1, VFUNCT_1, FUNCT_2, NORMSP_1, LOPBAN_1, PARTFUN1, PARTFUN2, NFCONT_1, FDIFF_1, NDIFF_1, FRECHET, REAL_NS1, VALUED_1, VECTSP_1, NORMSP_0, CARD_1, ORDINAL1;
schemes SEQ_1, FUNCT_2, CLASSES1;
registrations RELSET_1, STRUCT_0, ORDINAL1, XREAL_0, MEMBERED, LOPBAN_1, FDIFF_1, NDIFF_1, FUNCT_1, FUNCT_2, NAT_1, REAL_NS1, NUMBERS, XBOOLE_0, VALUED_0, VALUED_1, EUCLID, SQUARE_1, FINSEQ_1, RVSUM_1, NORMSP_1, NORMSP_0, CARD_1;
constructors HIDDEN, REAL_1, SQUARE_1, RSSPACE3, SEQ_2, FINSEQ_7, VFUNCT_1, COMPLEX1, NFCONT_1, RCOMP_1, FDIFF_1, NDIFF_1, REAL_NS1, EXTREAL1, RVSUM_1, RELSET_1, BINOP_2, COMSEQ_2, XREAL_0, FUNCT_7, NUMBERS, GR_CY_1, MONOID_0, VALUED_2;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities LOPBAN_1, EUCLID;
expansions TARSKI;
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 Real holds
( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) )
Lm2:
for i, n being Nat st i in Seg n holds
proj (i,n) is onto
definition
let m,
n be non
zero Nat;
let f be
PartFunc of
(REAL m),
(REAL n);
let x be
Element of
REAL m;
assume A1:
f is_differentiable_in x
;
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;
reconsider I = (proj (1,1)) " as Function of REAL,(REAL 1) by Th2;
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
definition
let m,
n be non
zero Nat;
let i be
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
;
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 defines
partdiff PDIFF_1:def 16 :
for m, n being non zero Nat
for i, j being 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 defines
partdiff PDIFF_1:def 18 :
for m, n being non zero Nat
for i, j being 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
for
m,
n being non
zero Nat for
i,
j being
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))*>
definition
let m,
n be non
zero Nat;
let i be
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
;
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;
theorem Th28:
for
m,
n being non
zero Nat for
i being
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
for
n being non
zero Nat for
i being
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:
for
m,
n being non
zero Nat for
i being
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
for
n being non
zero Nat for
i being
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)) )