environ
vocabularies HIDDEN, PRE_TOPC, RLVECT_1, FUNCT_1, ARYTM_3, ARYTM_1, FINSEQ_1, FINSEQ_2, FCONT_1, XXREAL_2, RVSUM_1, RELAT_1, COMPLEX1, SQUARE_1, ORDINAL2, RCOMP_1, XBOOLE_0, PARTFUN1, NORMSP_1, XXREAL_1, ORDINAL4, LOPBAN_1, FDIFF_1, PDIFF_1, REAL_NS1, FUNCT_2, EUCLID, AFINSQ_1, NUMBERS, STRUCT_0, CFCONT_1, RFINSEQ, REAL_1, SUBSET_1, CARD_1, TARSKI, XXREAL_0, CARD_3, NAT_1, VALUED_1, SEQ_4, SEQ_2, SEQFUNC, PDIFF_9, FUNCT_7, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, SQUARE_1, NAT_1, COMPLEX1, NAT_D, XXREAL_2, FINSEQ_1, VALUED_1, FINSEQ_2, SEQ_2, RVSUM_1, VALUED_2, RFINSEQ, SEQ_4, RCOMP_1, FDIFF_1, SEQFUNC, FINSEQ_7, STRUCT_0, PRE_TOPC, RLVECT_1, NORMSP_0, NORMSP_1, VFUNCT_1, EUCLID, LOPBAN_1, NFCONT_1, NDIFF_1, REAL_NS1, PDIFF_1, INTEGR15, PDIFF_6, PDIFF_7, NFCONT_4;
definitions TARSKI;
theorems TARSKI, ABSVALUE, XBOOLE_0, XBOOLE_1, EUCLID, XREAL_1, COMPLEX1, FINSEQ_1, FINSEQ_2, FINSEQ_3, RFINSEQ, NAT_1, XXREAL_0, FINSEQ_7, RVSUM_1, RELAT_1, FUNCT_1, FUNCT_2, SQUARE_1, FINSEQ_5, NORMSP_1, LOPBAN_1, PARTFUN1, PARTFUN2, NFCONT_1, FDIFF_1, NDIFF_1, REAL_NS1, VALUED_1, PDIFF_1, TOPREAL7, XXREAL_2, PDIFF_6, SEQ_4, PDIFF_7, PDIFF_8, NFCONT_4, SEQ_2, VALUED_2, RFUNCT_2, RCOMP_1, INT_1, XREAL_0, INTEGR15, ORDINAL1, RFUNCT_1;
schemes SEQ_1, NAT_1, RECDEF_1;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, MEMBERED, VALUED_0, FINSEQ_1, STRUCT_0, EUCLID, LOPBAN_1, REAL_NS1, NORMSP_1, SEQ_2, VALUED_2, VALUED_1, PARTFUN1, SQUARE_1, CARD_1;
constructors HIDDEN, REAL_1, SQUARE_1, RSSPACE3, NORMSP_2, FINSEQ_7, NFCONT_1, FDIFF_1, NDIFF_1, PDIFF_1, BINOP_2, MONOID_0, INTEGR15, RELSET_1, RFINSEQ, NAT_D, PDIFF_6, SEQ_4, MEASURE6, VFUNCT_1, PDIFF_7, VALUED_2, NFCONT_4, SEQFUNC, COMSEQ_2, NUMBERS;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities FINSEQ_1, NORMSP_0, EUCLID, LOPBAN_1, PDIFF_1, FINSEQ_2, PDIFF_7, INTEGR15;
expansions TARSKI, PDIFF_1, PDIFF_7, FUNCT_2;
Lm1:
for x being Real
for y being Element of REAL 1 st <*x*> = y holds
|.x.| = |.y.|
Lm2:
for m being non zero Element of NAT
for x being Element of REAL m
for Z being Subset of (REAL m)
for i being Nat st Z is open & x in Z & 1 <= i & i <= m holds
ex N being Neighbourhood of (proj (i,m)) . x st
for z being Element of REAL st z in N holds
(reproj (i,x)) . z in Z
definition
let m,
n be non
zero Element of
NAT ;
let Z be
set ;
let f be
PartFunc of
(REAL m),
(REAL n);
assume A1:
Z c= dom f
;
existence
ex b1 being PartFunc of (REAL m),(Funcs ((REAL m),(REAL n))) st
( dom b1 = Z & ( for x being Element of REAL m st x in Z holds
b1 /. x = diff (f,x) ) )
uniqueness
for b1, b2 being PartFunc of (REAL m),(Funcs ((REAL m),(REAL n))) st dom b1 = Z & ( for x being Element of REAL m st x in Z holds
b1 /. x = diff (f,x) ) & dom b2 = Z & ( for x being Element of REAL m st x in Z holds
b2 /. x = diff (f,x) ) holds
b1 = b2
end;
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
theorem Th22:
for
m,
n being non
zero 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
Subset of
(REAL m) for
Y being
Subset of
(REAL-NS m) for
i being
Nat st 1
<= i &
i <= m &
X is
open &
g = f &
X = Y &
f is_partial_differentiable_on X,
i holds
for
x0,
x1 being
Element of
REAL m for
y0,
y1 being
Point of
(REAL-NS m) st
x0 = y0 &
x1 = y1 &
x0 in X &
x1 in X holds
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| = ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).||
Lm3:
for i being Element of NAT
for f being PartFunc of (REAL i),REAL
for g being PartFunc of (REAL-NS i),REAL
for x being Element of REAL i
for y being Point of (REAL-NS i) st f = g & x = y holds
( f is_continuous_in x iff ( y in dom g & ( for s being sequence of (REAL-NS i) st rng s c= dom g & s is convergent & lim s = y holds
( g /* s is convergent & g /. y = lim (g /* s) ) ) ) )
definition
let m be non
zero Element of
NAT ;
let Z be
set ;
let i be
Nat;
let f be
PartFunc of
(REAL m),
REAL;
assume A1:
f is_partial_differentiable_on Z,
i
;
existence
ex b1 being PartFunc of (REAL m),REAL st
( dom b1 = Z & ( for x being Element of REAL m st x in Z holds
b1 /. x = partdiff (f,x,i) ) )
uniqueness
for b1, b2 being PartFunc of (REAL m),REAL st dom b1 = Z & ( for x being Element of REAL m st x in Z holds
b1 /. x = partdiff (f,x,i) ) & dom b2 = Z & ( for x being Element of REAL m st x in Z holds
b2 /. x = partdiff (f,x,i) ) holds
b1 = b2
end;
Lm4:
for m being non zero Element of NAT
for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL m),(REAL 1)
for x1, x0, v being Element of REAL m st <>* f = g holds
|.(((diff (f,x1)) . v) - ((diff (f,x0)) . v)).| = |.(((diff (g,x1)) . v) - ((diff (g,x0)) . v)).|
Lm5:
for i, k being Element of NAT
for f, g being PartFunc of (REAL i),REAL
for x being Element of REAL i holds (f * (reproj (k,x))) (#) (g * (reproj (k,x))) = (f (#) g) * (reproj (k,x))
theorem Th64:
for
m being non
zero Element of
NAT for
i being
Element of
NAT for
f,
g being
PartFunc of
(REAL m),
REAL for
x being
Element of
REAL m st
f is_partial_differentiable_in x,
i &
g is_partial_differentiable_in x,
i holds
(
f (#) g is_partial_differentiable_in x,
i &
partdiff (
(f (#) g),
x,
i)
= ((partdiff (f,x,i)) * (g . x)) + ((f . x) * (partdiff (g,x,i))) )
theorem Th65:
for
m being non
zero Element of
NAT for
i being
Element of
NAT for
X being
Subset of
(REAL m) for
f,
g being
PartFunc of
(REAL m),
REAL st
X is
open & 1
<= i &
i <= m &
f is_partial_differentiable_on X,
i &
g is_partial_differentiable_on X,
i holds
(
f + g is_partial_differentiable_on X,
i &
(f + g) `partial| (
X,
i)
= (f `partial| (X,i)) + (g `partial| (X,i)) & ( for
x being
Element of
REAL m st
x in X holds
((f + g) `partial| (X,i)) /. x = (partdiff (f,x,i)) + (partdiff (g,x,i)) ) )
theorem Th66:
for
m being non
zero Element of
NAT for
i being
Element of
NAT for
X being
Subset of
(REAL m) for
f,
g being
PartFunc of
(REAL m),
REAL st
X is
open & 1
<= i &
i <= m &
f is_partial_differentiable_on X,
i &
g is_partial_differentiable_on X,
i holds
(
f - g is_partial_differentiable_on X,
i &
(f - g) `partial| (
X,
i)
= (f `partial| (X,i)) - (g `partial| (X,i)) & ( for
x being
Element of
REAL m st
x in X holds
((f - g) `partial| (X,i)) /. x = (partdiff (f,x,i)) - (partdiff (g,x,i)) ) )
theorem Th68:
for
m being non
zero Element of
NAT for
i being
Element of
NAT for
X being
Subset of
(REAL m) for
f,
g being
PartFunc of
(REAL m),
REAL st
X is
open & 1
<= i &
i <= m &
f is_partial_differentiable_on X,
i &
g is_partial_differentiable_on X,
i holds
(
f (#) g is_partial_differentiable_on X,
i &
(f (#) g) `partial| (
X,
i)
= ((f `partial| (X,i)) (#) g) + (f (#) (g `partial| (X,i))) & ( for
x being
Element of
REAL m st
x in X holds
((f (#) g) `partial| (X,i)) /. x = ((partdiff (f,x,i)) * (g . x)) + ((f . x) * (partdiff (g,x,i))) ) )
Lm6:
for i being Element of NAT
for I being non empty FinSequence of NAT
for X being set st 1 <= i & i <= len I & rng I c= X holds
I /. i in X
theorem Th74:
for
m being non
zero Element of
NAT for
X being
Subset of
(REAL m) for
I being non
empty FinSequence of
NAT for
f,
g being
PartFunc of
(REAL m),
REAL st
X is
open &
rng I c= Seg m &
f is_partial_differentiable_on X,
I &
g is_partial_differentiable_on X,
I holds
for
i being
Element of
NAT st
i <= (len I) - 1 holds
(
(PartDiffSeq ((f + g),X,I)) . i is_partial_differentiable_on X,
I /. (i + 1) &
(PartDiffSeq ((f + g),X,I)) . i = ((PartDiffSeq (f,X,I)) . i) + ((PartDiffSeq (g,X,I)) . i) )
theorem Th76:
for
m being non
zero Element of
NAT for
X being
Subset of
(REAL m) for
I being non
empty FinSequence of
NAT for
f,
g being
PartFunc of
(REAL m),
REAL st
X is
open &
rng I c= Seg m &
f is_partial_differentiable_on X,
I &
g is_partial_differentiable_on X,
I holds
for
i being
Element of
NAT st
i <= (len I) - 1 holds
(
(PartDiffSeq ((f - g),X,I)) . i is_partial_differentiable_on X,
I /. (i + 1) &
(PartDiffSeq ((f - g),X,I)) . i = ((PartDiffSeq (f,X,I)) . i) - ((PartDiffSeq (g,X,I)) . i) )
set Z0 = 0 ;