let G be RealNormSpace-Sequence; for S being RealNormSpace
for f being PartFunc of (product G),S
for x being Point of (product G)
for i being set st f is_differentiable_in x holds
( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj ((In (i,(dom G))),(0. (product G)))) )
let S be RealNormSpace; for f being PartFunc of (product G),S
for x being Point of (product G)
for i being set st f is_differentiable_in x holds
( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj ((In (i,(dom G))),(0. (product G)))) )
let f be PartFunc of (product G),S; for x being Point of (product G)
for i being set st f is_differentiable_in x holds
( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj ((In (i,(dom G))),(0. (product G)))) )
let x be Point of (product G); for i being set st f is_differentiable_in x holds
( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj ((In (i,(dom G))),(0. (product G)))) )
let i0 be set ; ( f is_differentiable_in x implies ( f is_partial_differentiable_in x,i0 & partdiff (f,x,i0) = (diff (f,x)) * (reproj ((In (i0,(dom G))),(0. (product G)))) ) )
assume A1:
f is_differentiable_in x
; ( f is_partial_differentiable_in x,i0 & partdiff (f,x,i0) = (diff (f,x)) * (reproj ((In (i0,(dom G))),(0. (product G)))) )
set i = In (i0,(dom G));
consider N being Neighbourhood of x such that
A2:
( N c= dom f & ex R being RestFunc of (product G),S st
for y being Point of (product G) st y in N holds
(f /. y) - (f /. x) = ((diff (f,x)) . (y - x)) + (R /. (y - x)) )
by A1, NDIFF_1:def 7;
consider R being RestFunc of (product G),S such that
A3:
for y being Point of (product G) st y in N holds
(f /. y) - (f /. x) = ((diff (f,x)) . (y - x)) + (R /. (y - x))
by A2;
consider r0 being Real such that
A4:
( 0 < r0 & { z where z is Point of (product G) : ||.(z - x).|| < r0 } c= N )
by NFCONT_1:def 1;
set u = f * (reproj ((In (i0,(dom G))),x));
reconsider x0 = (proj (In (i0,(dom G)))) . x as Point of (G . (In (i0,(dom G)))) ;
set Z = 0. (product G);
set Nx0 = { z where z is Point of (G . (In (i0,(dom G)))) : ||.(z - x0).|| < r0 } ;
then
{ z where z is Point of (G . (In (i0,(dom G)))) : ||.(z - x0).|| < r0 } is Subset of (G . (In (i0,(dom G))))
by TARSKI:def 3;
then reconsider Nx0 = { z where z is Point of (G . (In (i0,(dom G)))) : ||.(z - x0).|| < r0 } as Neighbourhood of x0 by A4, NFCONT_1:def 1;
A5:
for xi being Element of (G . (In (i0,(dom G)))) st xi in Nx0 holds
(reproj ((In (i0,(dom G))),x)) . xi in N
proof
let xi be
Element of
(G . (In (i0,(dom G))));
( xi in Nx0 implies (reproj ((In (i0,(dom G))),x)) . xi in N )
assume
xi in Nx0
;
(reproj ((In (i0,(dom G))),x)) . xi in N
then A6:
ex
z being
Point of
(G . (In (i0,(dom G)))) st
(
xi = z &
||.(z - x0).|| < r0 )
;
((reproj ((In (i0,(dom G))),x)) . xi) - x = (reproj ((In (i0,(dom G))),(0. (product G)))) . (xi - x0)
by Th22;
then
||.(((reproj ((In (i0,(dom G))),x)) . xi) - x).|| < r0
by Th21, A6;
then
(reproj ((In (i0,(dom G))),x)) . xi in { z where z is Point of (product G) : ||.(z - x).|| < r0 }
;
hence
(reproj ((In (i0,(dom G))),x)) . xi in N
by A4;
verum
end;
A7:
R is total
by NDIFF_1:def 5;
then A8:
dom R = the carrier of (product G)
by PARTFUN1:def 2;
reconsider R1 = R * (reproj ((In (i0,(dom G))),(0. (product G)))) as PartFunc of (G . (In (i0,(dom G)))),S ;
A9:
dom (reproj ((In (i0,(dom G))),(0. (product G)))) = the carrier of (G . (In (i0,(dom G))))
by FUNCT_2:def 1;
A10:
dom R1 = the carrier of (G . (In (i0,(dom G))))
by A7, PARTFUN1:def 2;
for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of (G . (In (i0,(dom G)))) st z <> 0. (G . (In (i0,(dom G)))) & ||.z.|| < d holds
(||.z.|| ") * ||.(R1 /. z).|| < r ) )
proof
let r be
Real;
( r > 0 implies ex d being Real st
( d > 0 & ( for z being Point of (G . (In (i0,(dom G)))) st z <> 0. (G . (In (i0,(dom G)))) & ||.z.|| < d holds
(||.z.|| ") * ||.(R1 /. z).|| < r ) ) )
assume
r > 0
;
ex d being Real st
( d > 0 & ( for z being Point of (G . (In (i0,(dom G)))) st z <> 0. (G . (In (i0,(dom G)))) & ||.z.|| < d holds
(||.z.|| ") * ||.(R1 /. z).|| < r ) )
then consider d being
Real such that A11:
(
d > 0 & ( for
z being
Point of
(product G) st
z <> 0. (product G) &
||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) )
by A7, NDIFF_1:23;
take
d
;
( d > 0 & ( for z being Point of (G . (In (i0,(dom G)))) st z <> 0. (G . (In (i0,(dom G)))) & ||.z.|| < d holds
(||.z.|| ") * ||.(R1 /. z).|| < r ) )
now for z being Point of (G . (In (i0,(dom G)))) st z <> 0. (G . (In (i0,(dom G)))) & ||.z.|| < d holds
(||.z.|| ") * ||.(R1 /. z).|| < rlet z be
Point of
(G . (In (i0,(dom G))));
( z <> 0. (G . (In (i0,(dom G)))) & ||.z.|| < d implies (||.z.|| ") * ||.(R1 /. z).|| < r )assume A12:
(
z <> 0. (G . (In (i0,(dom G)))) &
||.z.|| < d )
;
(||.z.|| ") * ||.(R1 /. z).|| < rA13:
||.((reproj ((In (i0,(dom G))),(0. (product G)))) . z).|| = ||.z.||
by Th21;
R /. ((reproj ((In (i0,(dom G))),(0. (product G)))) . z) = R . ((reproj ((In (i0,(dom G))),(0. (product G)))) . z)
by A8, PARTFUN1:def 6;
then
R /. ((reproj ((In (i0,(dom G))),(0. (product G)))) . z) = R1 . z
by A9, FUNCT_1:13;
then
R /. ((reproj ((In (i0,(dom G))),(0. (product G)))) . z) = R1 /. z
by A10, PARTFUN1:def 6;
hence
(||.z.|| ") * ||.(R1 /. z).|| < r
by A11, A13, A12, Th38;
verum end;
hence
(
d > 0 & ( for
z being
Point of
(G . (In (i0,(dom G)))) st
z <> 0. (G . (In (i0,(dom G)))) &
||.z.|| < d holds
(||.z.|| ") * ||.(R1 /. z).|| < r ) )
by A11;
verum
end;
then reconsider R1 = R1 as RestFunc of (G . (In (i0,(dom G)))),S by A7, NDIFF_1:23;
reconsider dfx = diff (f,x) as Lipschitzian LinearOperator of (product G),S by LOPBAN_1:def 9;
reconsider LD1 = dfx * (reproj ((In (i0,(dom G))),(0. (product G)))) as Function of (G . (In (i0,(dom G)))),S ;
A14:
now for x, y being Element of (G . (In (i0,(dom G)))) holds LD1 . (x + y) = (LD1 . x) + (LD1 . y)let x,
y be
Element of
(G . (In (i0,(dom G))));
LD1 . (x + y) = (LD1 . x) + (LD1 . y)
LD1 . (x + y) = dfx . ((reproj ((In (i0,(dom G))),(0. (product G)))) . (x + y))
by FUNCT_2:15;
then
LD1 . (x + y) = dfx . (((reproj ((In (i0,(dom G))),(0. (product G)))) . x) + ((reproj ((In (i0,(dom G))),(0. (product G)))) . y))
by Th34;
then
LD1 . (x + y) = (dfx . ((reproj ((In (i0,(dom G))),(0. (product G)))) . x)) + (dfx . ((reproj ((In (i0,(dom G))),(0. (product G)))) . y))
by VECTSP_1:def 20;
then
LD1 . (x + y) = (LD1 . x) + (dfx . ((reproj ((In (i0,(dom G))),(0. (product G)))) . y))
by FUNCT_2:15;
hence
LD1 . (x + y) = (LD1 . x) + (LD1 . y)
by FUNCT_2:15;
verum end;
then reconsider LD1 = LD1 as LinearOperator of (G . (In (i0,(dom G)))),S by A14, LOPBAN_1:def 5, VECTSP_1:def 20;
consider K0 being Real such that
A15:
( 0 <= K0 & ( for x being VECTOR of (product G) holds ||.(dfx . x).|| <= K0 * ||.x.|| ) )
by LOPBAN_1:def 8;
then
LD1 is Lipschitzian
by A15;
then reconsider LD1 = LD1 as Point of (R_NormSpace_of_BoundedLinearOperators ((G . (In (i0,(dom G)))),S)) by LOPBAN_1:def 9;
then A16:
(reproj ((In (i0,(dom G))),x)) .: Nx0 c= dom f
;
dom (reproj ((In (i0,(dom G))),x)) = the carrier of (G . (In (i0,(dom G))))
by FUNCT_2:def 1;
then A17:
Nx0 c= dom (f * (reproj ((In (i0,(dom G))),x)))
by A16, FUNCT_3:3;
A18:
for y being Point of (G . (In (i0,(dom G)))) st y in Nx0 holds
((f * (reproj ((In (i0,(dom G))),x))) /. y) - ((f * (reproj ((In (i0,(dom G))),x))) /. x0) = (LD1 . (y - x0)) + (R1 /. (y - x0))
proof
let y be
Point of
(G . (In (i0,(dom G))));
( y in Nx0 implies ((f * (reproj ((In (i0,(dom G))),x))) /. y) - ((f * (reproj ((In (i0,(dom G))),x))) /. x0) = (LD1 . (y - x0)) + (R1 /. (y - x0)) )
assume A19:
y in Nx0
;
((f * (reproj ((In (i0,(dom G))),x))) /. y) - ((f * (reproj ((In (i0,(dom G))),x))) /. x0) = (LD1 . (y - x0)) + (R1 /. (y - x0))
then A20:
(reproj ((In (i0,(dom G))),x)) . y in N
by A5;
A21:
(reproj ((In (i0,(dom G))),x)) . x0 = x +* (
(In (i0,(dom G))),
x0)
by Def4;
A22:
the
carrier of
(product G) = product (carr G)
by Th10;
x . (In (i0,(dom G))) = x0
by Def3, A22;
then A23:
x = x +* (
(In (i0,(dom G))),
x0)
by FUNCT_7:35;
A24:
(reproj ((In (i0,(dom G))),x)) . x0 in N
by A5, NFCONT_1:4;
(f * (reproj ((In (i0,(dom G))),x))) /. y = (f * (reproj ((In (i0,(dom G))),x))) . y
by A19, A17, PARTFUN1:def 6;
then
(f * (reproj ((In (i0,(dom G))),x))) /. y = f . ((reproj ((In (i0,(dom G))),x)) . y)
by FUNCT_2:15;
then A25:
(f * (reproj ((In (i0,(dom G))),x))) /. y = f /. ((reproj ((In (i0,(dom G))),x)) . y)
by A20, A2, PARTFUN1:def 6;
R /. ((reproj ((In (i0,(dom G))),(0. (product G)))) . (y - x0)) = R . ((reproj ((In (i0,(dom G))),(0. (product G)))) . (y - x0))
by A8, PARTFUN1:def 6;
then
R /. ((reproj ((In (i0,(dom G))),(0. (product G)))) . (y - x0)) = R1 . (y - x0)
by A9, FUNCT_1:13;
then A26:
R /. ((reproj ((In (i0,(dom G))),(0. (product G)))) . (y - x0)) = R1 /. (y - x0)
by A10, PARTFUN1:def 6;
x0 in Nx0
by NFCONT_1:4;
then
(f * (reproj ((In (i0,(dom G))),x))) /. x0 = (f * (reproj ((In (i0,(dom G))),x))) . x0
by A17, PARTFUN1:def 6;
then
(f * (reproj ((In (i0,(dom G))),x))) /. x0 = f . ((reproj ((In (i0,(dom G))),x)) . x0)
by FUNCT_2:15;
then
((f * (reproj ((In (i0,(dom G))),x))) /. y) - ((f * (reproj ((In (i0,(dom G))),x))) /. x0) = (f /. ((reproj ((In (i0,(dom G))),x)) . y)) - (f /. x)
by A25, A23, A24, A2, A21, PARTFUN1:def 6;
then
((f * (reproj ((In (i0,(dom G))),x))) /. y) - ((f * (reproj ((In (i0,(dom G))),x))) /. x0) = ((diff (f,x)) . (((reproj ((In (i0,(dom G))),x)) . y) - x)) + (R /. (((reproj ((In (i0,(dom G))),x)) . y) - x))
by A3, A19, A5;
then
((f * (reproj ((In (i0,(dom G))),x))) /. y) - ((f * (reproj ((In (i0,(dom G))),x))) /. x0) = (dfx . ((reproj ((In (i0,(dom G))),(0. (product G)))) . (y - x0))) + (R /. (((reproj ((In (i0,(dom G))),x)) . y) - x))
by Th22;
then
((f * (reproj ((In (i0,(dom G))),x))) /. y) - ((f * (reproj ((In (i0,(dom G))),x))) /. x0) = (dfx . ((reproj ((In (i0,(dom G))),(0. (product G)))) . (y - x0))) + (R /. ((reproj ((In (i0,(dom G))),(0. (product G)))) . (y - x0)))
by Th22;
hence
((f * (reproj ((In (i0,(dom G))),x))) /. y) - ((f * (reproj ((In (i0,(dom G))),x))) /. x0) = (LD1 . (y - x0)) + (R1 /. (y - x0))
by A26, FUNCT_2:15;
verum
end;
hence
f is_partial_differentiable_in x,i0
by A17, NDIFF_1:def 6; partdiff (f,x,i0) = (diff (f,x)) * (reproj ((In (i0,(dom G))),(0. (product G))))
f * (reproj ((In (i0,(dom G))),x)) is_differentiable_in x0
by A17, A18, NDIFF_1:def 6;
hence
partdiff (f,x,i0) = (diff (f,x)) * (reproj ((In (i0,(dom G))),(0. (product G))))
by A17, A18, NDIFF_1:def 7; verum