begin
theorem NDIFF126:
theorem NDIFF27:
theorem NDIFF29:
theorem NDIFF211:
theorem NDIFF212:
theorem NDIFF213:
theorem PDIFF617:
theorem Lm1:
theorem LMPROD1:
theorem LM001:
theorem LM003:
:: deftheorem defTRV defines non-trivial NDIFF_5:def 1 :
for G being RealNormSpace-Sequence holds
( G is non-trivial iff for j being Element of dom G holds not G . j is trivial );
theorem ADD1:
theorem MLT1:
theorem ZR1:
theorem SUB1:
begin
:: deftheorem defines ]. NDIFF_5:def 2 :
for S being RealLinearSpace
for p, q being Point of S holds ].p,q.[ = { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) } ;
theorem LMDefCLS1:
LMFDAF10A:
for x being Real st ( for e being Real st 0 < e holds
x <= e ) holds
x <= 0
theorem NDIFF126A:
theorem NDIFF126B:
LMFDAF10:
for T being non trivial RealNormSpace
for f being PartFunc of REAL,T
for g being PartFunc of REAL,REAL st dom f = [.0,1.] & dom g = [.0,1.] & f | [.0,1.] is continuous & g | [.0,1.] is continuous & f is_differentiable_on ].0,1.[ & g is_differentiable_on ].0,1.[ & ( for x being real number st x in ].0,1.[ holds
||.(diff (f,x)).|| <= diff (g,x) ) holds
||.((f /. 1) - (f /. 0)).|| <= (g /. 1) - (g /. 0)
theorem FDAF10:
theorem FDAF20:
begin
:: deftheorem Def1 defines proj NDIFF_5:def 3 :
for G being RealNormSpace-Sequence
for i being Element of dom G
for b3 being Function of (product G),(G . i) holds
( b3 = proj i iff for x being Element of product (carr G) holds b3 . x = x . i );
:: deftheorem Def5 defines reproj NDIFF_5:def 4 :
for G being RealNormSpace-Sequence
for i being Element of dom G
for x being Element of (product G)
for b4 being Function of (G . i),(product G) holds
( b4 = reproj (i,x) iff for r being Element of (G . i) holds b4 . r = x +* (i,r) );
:: deftheorem Defmode defines modetrans NDIFF_5:def 5 :
for G being non-trivial RealNormSpace-Sequence
for j being set st j in dom G holds
modetrans (G,j) = j;
:: deftheorem Def9 defines is_partial_differentiable_in NDIFF_5:def 6 :
for G being non-trivial RealNormSpace-Sequence
for F being non trivial RealNormSpace
for i being set
for f being PartFunc of (product G),F
for x being Element of (product G) holds
( f is_partial_differentiable_in x,i iff f * (reproj ((modetrans (G,i)),x)) is_differentiable_in (proj (modetrans (G,i))) . x );
definition
let G be
non-trivial RealNormSpace-Sequence;
let F be non
trivial RealNormSpace;
let i be
set ;
let f be
PartFunc of
(product G),
F;
let x be
Point of
(product G);
func partdiff (
f,
x,
i)
-> Point of
(R_NormSpace_of_BoundedLinearOperators ((G . (modetrans (G,i))),F)) equals
diff (
(f * (reproj ((modetrans (G,i)),x))),
((proj (modetrans (G,i))) . x));
coherence
diff ((f * (reproj ((modetrans (G,i)),x))),((proj (modetrans (G,i))) . x)) is Point of (R_NormSpace_of_BoundedLinearOperators ((G . (modetrans (G,i))),F))
;
end;
:: deftheorem defines partdiff NDIFF_5:def 7 :
for G being non-trivial RealNormSpace-Sequence
for F being non trivial RealNormSpace
for i being set
for f being PartFunc of (product G),F
for x being Point of (product G) holds partdiff (f,x,i) = diff ((f * (reproj ((modetrans (G,i)),x))),((proj (modetrans (G,i))) . x));
begin
:: deftheorem Def19 defines is_partial_differentiable_on NDIFF_5:def 8 :
for G being non-trivial RealNormSpace-Sequence
for F being non trivial RealNormSpace
for i being set
for f being PartFunc of (product G),F
for X being set holds
( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Point of (product G) st x in X holds
f | X is_partial_differentiable_in x,i ) ) );
theorem XTh5:
theorem XTh6:
theorem XLm5:
theorem XTh34:
theorem Th25:
definition
let G be
non-trivial RealNormSpace-Sequence;
let S be non
trivial RealNormSpace;
let i be
set ;
assume AS:
i in dom G
;
let f be
PartFunc of
(product G),
S;
let X be
set ;
assume A1:
f is_partial_differentiable_on X,
i
;
func f `partial| (
X,
i)
-> PartFunc of
(product G),
(R_NormSpace_of_BoundedLinearOperators ((G . (modetrans (G,i))),S)) means :
Def19f:
(
dom it = X & ( for
x being
Point of
(product G) st
x in X holds
it /. x = partdiff (
f,
x,
i) ) );
existence
ex b1 being PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((G . (modetrans (G,i))),S)) st
( dom b1 = X & ( for x being Point of (product G) st x in X holds
b1 /. x = partdiff (f,x,i) ) )
uniqueness
for b1, b2 being PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((G . (modetrans (G,i))),S)) st dom b1 = X & ( for x being Point of (product G) st x in X holds
b1 /. x = partdiff (f,x,i) ) & dom b2 = X & ( for x being Point of (product G) st x in X holds
b2 /. x = partdiff (f,x,i) ) holds
b1 = b2
end;
:: deftheorem Def19f defines `partial| NDIFF_5:def 9 :
for G being non-trivial RealNormSpace-Sequence
for S being non trivial RealNormSpace
for i being set st i in dom G holds
for f being PartFunc of (product G),S
for X being set st f is_partial_differentiable_on X,i holds
for b6 being PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((G . (modetrans (G,i))),S)) holds
( b6 = f `partial| (X,i) iff ( dom b6 = X & ( for x being Point of (product G) st x in X holds
b6 /. x = partdiff (f,x,i) ) ) );
theorem Th26:
for
G being
non-trivial RealNormSpace-Sequence for
F being non
trivial RealNormSpace for
f1,
f2 being
PartFunc of
(product G),
F for
x being
Point of
(product G) for
i being
set st
i in dom G holds
(
(f1 + f2) * (reproj ((modetrans (G,i)),x)) = (f1 * (reproj ((modetrans (G,i)),x))) + (f2 * (reproj ((modetrans (G,i)),x))) &
(f1 - f2) * (reproj ((modetrans (G,i)),x)) = (f1 * (reproj ((modetrans (G,i)),x))) - (f2 * (reproj ((modetrans (G,i)),x))) )
theorem Th27:
theorem
for
G being
non-trivial RealNormSpace-Sequence for
F being non
trivial RealNormSpace for
f1,
f2 being
PartFunc of
(product G),
F for
x being
Point of
(product G) for
i being
set st
i in dom G &
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
G being
non-trivial RealNormSpace-Sequence for
F being non
trivial RealNormSpace for
f1,
f2 being
PartFunc of
(product G),
F for
x being
Point of
(product G) for
i being
set st
i in dom G &
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
begin
theorem XTh50:
theorem XTh8:
theorem XLm7:
theorem XTh9:
theorem YTh9:
theorem
theorem YTh9M:
theorem XTh11:
theorem XTh16:
theorem YTh16:
theorem Th21X:
Lm8:
for G being non-trivial RealNormSpace-Sequence
for S being non trivial RealNormSpace
for f being PartFunc of (product G),S
for x being Point of (product G) ex L being bounded LinearOperator of (product G),S st
for h being Element of (product G) ex w being FinSequence of S st
( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . h) ) & L . h = Sum w )
theorem Th26:
theorem
theorem LMPRT3:
theorem Th28:
theorem XTh39:
theorem XTh39A:
theorem XTh40:
theorem XTh40a:
theorem
theorem XTh42:
for
G being
non-trivial RealNormSpace-Sequence for
F being non
trivial RealNormSpace for
f being
PartFunc of
(product G),
F for
x being
Point of
(product G) for
i being
set for
M being
Real for
L being
Point of
(R_NormSpace_of_BoundedLinearOperators ((G . (modetrans (G,i))),F)) for
p,
q being
Point of
(G . (modetrans (G,i))) st
i in dom G & ( for
h being
Point of
(G . (modetrans (G,i))) st
h in ].p,q.[ holds
||.((partdiff (f,((reproj ((modetrans (G,i)),x)) . h),i)) - L).|| <= M ) & ( for
h being
Point of
(G . (modetrans (G,i))) st
h in [.p,q.] holds
(reproj ((modetrans (G,i)),x)) . h in dom f ) & ( for
h being
Point of
(G . (modetrans (G,i))) st
h in [.p,q.] holds
f is_partial_differentiable_in (reproj ((modetrans (G,i)),x)) . h,
i ) holds
||.(((f /. ((reproj ((modetrans (G,i)),x)) . q)) - (f /. ((reproj ((modetrans (G,i)),x)) . p))) - (L . (q - p))).|| <= M * ||.(q - p).||
theorem XTh44:
theorem XTh45:
for
G being
non-trivial RealNormSpace-Sequence for
S being non
trivial RealNormSpace for
f being
PartFunc of
(product G),
S for
X being
Subset of
(product G) for
x,
y,
z being
Point of
(product G) for
i being
set for
p,
q being
Point of
(G . (modetrans (G,i))) for
d,
r being
Real st
i in dom G &
X is
open &
x in X &
||.(y - x).|| < d &
||.(z - x).|| < d &
X c= dom f & ( for
x being
Point of
(product G) st
x in X holds
f is_partial_differentiable_in x,
i ) & ( for
z being
Point of
(product G) st
||.(z - x).|| < d holds
z in X ) & ( for
z being
Point of
(product G) st
||.(z - x).|| < d holds
||.((partdiff (f,z,i)) - (partdiff (f,x,i))).|| <= r ) &
z = (reproj ((modetrans (G,i)),y)) . p &
q = (proj (modetrans (G,i))) . y holds
||.(((f /. z) - (f /. y)) - ((partdiff (f,x,i)) . (p - q))).|| <= ||.(p - q).|| * r
theorem Th46:
theorem Th46X:
theorem Th48X:
theorem