:: Differentiable Functions on Normed Linear Spaces
:: by Yasunari Shidama
::
:: Received June 2, 2011
:: Copyright (c) 2011-2021 Association of Mizar Users

theorem Th1: :: NDIFF_5:1
for S being RealNormSpace
for R being Function of REAL,S holds
( R is RestFunc-like iff for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
() * ||.(R /. z).|| < r ) ) )
proof end;

theorem Th2: :: NDIFF_5:2
for S being RealNormSpace
for R being RestFunc of S st R /. 0 = 0. S holds
for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st |.h.| < d holds
||.(R /. h).|| <= e * |.h.| ) )
proof end;

theorem Th3: :: NDIFF_5:3
for S, T being RealNormSpace
for R being RestFunc of S
for L being Lipschitzian LinearOperator of S,T holds L * R is RestFunc of T
proof end;

theorem Th4: :: NDIFF_5:4
for S, T being RealNormSpace
for R1 being RestFunc of S st R1 /. 0 = 0. S holds
for R2 being RestFunc of S,T st R2 /. (0. S) = 0. T holds
for L being LinearFunc of S holds R2 * (L + R1) is RestFunc of T
proof end;

theorem Th5: :: NDIFF_5:5
for S, T being RealNormSpace
for R1 being RestFunc of S st R1 /. 0 = 0. S holds
for R2 being RestFunc of S,T st R2 /. (0. S) = 0. T holds
for L1 being LinearFunc of S
for L2 being Lipschitzian LinearOperator of S,T holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of T
proof end;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

theorem Th6: :: NDIFF_5:6
for S, T being RealNormSpace
for x0 being Real
for g being PartFunc of REAL, the carrier of S st g is_differentiable_in x0 holds
for f being PartFunc of the carrier of S, the carrier of T st f is_differentiable_in g /. x0 holds
( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) )
proof end;

theorem Th7: :: NDIFF_5:7
for S being RealNormSpace
for xseq being FinSequence of S
for yseq being FinSequence of REAL st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = ||.(xseq /. i).|| ) holds
||.(Sum xseq).|| <= Sum yseq
proof end;

theorem Th8: :: NDIFF_5:8
for S being RealNormSpace
for x being Point of S
for N1, N2 being Neighbourhood of x holds N1 /\ N2 is Neighbourhood of x
proof end;

theorem Th9: :: NDIFF_5:9
for X being non-empty FinSequence
for x being set st x in product X holds
x is FinSequence
proof end;

registration
let G be RealNormSpace-Sequence;
coherence
proof end;
end;

Lm1: now :: thesis: for G being RealLinearSpace-Sequence holds dom (carr G) = dom G
let G be RealLinearSpace-Sequence; :: thesis: dom (carr G) = dom G
len (carr G) = len G by PRVECT_1:def 11;
hence dom (carr G) = Seg (len G) by FINSEQ_1:def 3
.= dom G by FINSEQ_1:def 3 ;
:: thesis: verum
end;

definition
let G be RealLinearSpace-Sequence;
let z be Element of product (carr G);
let j be Element of dom G;
:: original: .
redefine func z . j -> Element of (G . j);
correctness
coherence
z . j is Element of (G . j)
;
proof end;
end;

theorem Th10: :: NDIFF_5:10
for G being RealNormSpace-Sequence holds the carrier of () = product (carr G)
proof end;

theorem Th11: :: NDIFF_5:11
for G being RealNormSpace-Sequence
for i being Element of dom G
for r being set
for x being Function st r in the carrier of (G . i) & x in product (carr G) holds
x +* (i,r) in the carrier of ()
proof end;

definition
let G be RealNormSpace-Sequence;
attr G is non-trivial means :Def1: :: NDIFF_5:def 1
for j being Element of dom G holds not G . j is trivial ;
end;

:: deftheorem Def1 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 );

registration
correctness
existence
ex b1 being RealNormSpace-Sequence st b1 is non-trivial
;
proof end;
end;

registration
let G be non-trivial RealNormSpace-Sequence;
let i be Element of dom G;
cluster G . i -> non trivial for RealNormSpace;
correctness
coherence
for b1 being RealNormSpace st b1 = G . i holds
not b1 is trivial
;
by Def1;
end;

registration
let G be non-trivial RealNormSpace-Sequence;
cluster product G -> non trivial ;
correctness
coherence
not product G is trivial
;
proof end;
end;

theorem Th12: :: NDIFF_5:12
for G being RealNormSpace-Sequence
for p, q being Point of ()
for r0, p0, q0 being Element of product (carr G) st p = p0 & q = q0 holds
( p + q = r0 iff for i being Element of dom G holds r0 . i = (p0 . i) + (q0 . i) )
proof end;

theorem Th13: :: NDIFF_5:13
for G being RealNormSpace-Sequence
for p being Point of ()
for r being Real
for r0, p0 being Element of product (carr G) st p = p0 holds
( r * p = r0 iff for i being Element of dom G holds r0 . i = r * (p0 . i) )
proof end;

theorem Th14: :: NDIFF_5:14
for G being RealNormSpace-Sequence
for p0 being Element of product (carr G) holds
( 0. () = p0 iff for i being Element of dom G holds p0 . i = 0. (G . i) )
proof end;

theorem Th15: :: NDIFF_5:15
for G being RealNormSpace-Sequence
for p, q being Point of ()
for r0, p0, q0 being Element of product (carr G) st p = p0 & q = q0 holds
( p - q = r0 iff for i being Element of dom G holds r0 . i = (p0 . i) - (q0 . i) )
proof end;

Lm2: now :: thesis: for S being RealLinearSpace
for p, q being Point of S
for z1 being Real holds p + (z1 * (q - p)) = ((1 - z1) * p) + (z1 * q)
let S be RealLinearSpace; :: thesis: for p, q being Point of S
for z1 being Real holds p + (z1 * (q - p)) = ((1 - z1) * p) + (z1 * q)

let p, q be Point of S; :: thesis: for z1 being Real holds p + (z1 * (q - p)) = ((1 - z1) * p) + (z1 * q)
let z1 be Real; :: thesis: p + (z1 * (q - p)) = ((1 - z1) * p) + (z1 * q)
thus p + (z1 * (q - p)) = p + ((z1 * q) + (z1 * (- p))) by RLVECT_1:def 5
.= p + ((z1 * q) + (- (z1 * p))) by RLVECT_1:25
.= (p + (- (z1 * p))) + (z1 * q) by RLVECT_1:def 3
.= ((1 * p) - (z1 * p)) + (z1 * q) by RLVECT_1:def 8
.= ((1 - z1) * p) + (z1 * q) by RLVECT_1:35 ; :: thesis: verum
end;

notation
let S be RealLinearSpace;
let p, q be Point of S;
synonym [.p,q.] for LSeg (p,q);
end;

definition
let S be RealLinearSpace;
let p, q be Point of S;
func ].p,q.[ -> Subset of S equals :: NDIFF_5:def 2
[.p,q.] \ {p,q};
correctness
coherence
[.p,q.] \ {p,q} is Subset of S
;
;
end;

:: deftheorem defines ]. NDIFF_5:def 2 :
for S being RealLinearSpace
for p, q being Point of S holds ].p,q.[ = [.p,q.] \ {p,q};

theorem LMOPN: :: NDIFF_5:16
for S being RealLinearSpace
for p, q being Point of S st p <> q holds
].p,q.[ = { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) }
proof end;

Lm3: for x being Real st ( for e being Real st 0 < e holds
x <= e ) holds
x <= 0

proof end;

theorem Th17: :: NDIFF_5:17
for T being RealNormSpace
for R being PartFunc of REAL,T st R is total holds
( R is RestFunc-like iff for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
||.(R /. z).|| / |.z.| < r ) ) )
proof end;

theorem Th18: :: NDIFF_5:18
for R being Function of REAL,REAL holds
( R is RestFunc-like iff for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
|.(R . z).| / |.z.| < r ) ) )
proof end;

reconsider jj = 1 as Real ;

Lm4: for T being 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 st x in ].0,1.[ holds
||.(diff (f,x)).|| <= diff (g,x) ) holds
||.((f /. 1) - (f /. 0)).|| <= (g /. 1) - (g /. 0)

proof end;

theorem Th19: :: NDIFF_5:19
for S, T being RealNormSpace
for f being PartFunc of S,T
for p, q being Point of S
for M being Real st [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds
f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds
f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds
||.(diff (f,x)).|| <= M ) holds
||.((f /. q) - (f /. p)).|| <= M * ||.(q - p).||
proof end;

theorem Th20: :: NDIFF_5:20
for S, T being RealNormSpace
for f being PartFunc of S,T
for p, q being Point of S
for M being Real
for L being Point of st [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds
f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds
f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds
||.((diff (f,x)) - L).|| <= M ) holds
||.(((f /. q) - (f /. p)) - (L . (q - p))).|| <= M * ||.(q - p).||
proof end;

definition
let G be RealNormSpace-Sequence;
let i be Element of dom G;
func proj i -> Function of (),(G . i) means :Def3: :: NDIFF_5:def 3
for x being Element of product (carr G) holds it . x = x . i;
existence
ex b1 being Function of (),(G . i) st
for x being Element of product (carr G) holds b1 . x = x . i
proof end;
uniqueness
for b1, b2 being Function of (),(G . i) st ( for x being Element of product (carr G) holds b1 . x = x . i ) & ( for x being Element of product (carr G) holds b2 . x = x . i ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines proj NDIFF_5:def 3 :
for G being RealNormSpace-Sequence
for i being Element of dom G
for b3 being Function of (),(G . i) holds
( b3 = proj i iff for x being Element of product (carr G) holds b3 . x = x . i );

definition
let G be RealNormSpace-Sequence;
let i be Element of dom G;
let x be Element of ();
func reproj (i,x) -> Function of (G . i),() means :Def4: :: NDIFF_5:def 4
for r being Element of (G . i) holds it . r = x +* (i,r);
existence
ex b1 being Function of (G . i),() st
for r being Element of (G . i) holds b1 . r = x +* (i,r)
proof end;
uniqueness
for b1, b2 being Function of (G . i),() st ( for r being Element of (G . i) holds b1 . r = x +* (i,r) ) & ( for r being Element of (G . i) holds b2 . r = x +* (i,r) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines reproj NDIFF_5:def 4 :
for G being RealNormSpace-Sequence
for i being Element of dom G
for x being Element of ()
for b4 being Function of (G . i),() holds
( b4 = reproj (i,x) iff for r being Element of (G . i) holds b4 . r = x +* (i,r) );

definition
let G be RealNormSpace-Sequence;
let F be RealNormSpace;
let i be set ;
let f be PartFunc of (),F;
let x be Element of ();
pred f is_partial_differentiable_in x,i means :: NDIFF_5:def 6
f * (reproj ((In (i,(dom G))),x)) is_differentiable_in (proj (In (i,(dom G)))) . x;
end;

:: deftheorem NDIFF_5:def 5 :
canceled;

:: deftheorem defines is_partial_differentiable_in NDIFF_5:def 6 :
for G being RealNormSpace-Sequence
for F being RealNormSpace
for i being set
for f being PartFunc of (),F
for x being Element of () holds
( f is_partial_differentiable_in x,i iff f * (reproj ((In (i,(dom G))),x)) is_differentiable_in (proj (In (i,(dom G)))) . x );

definition
let G be RealNormSpace-Sequence;
let F be RealNormSpace;
let i be set ;
let f be PartFunc of (),F;
let x be Point of ();
func partdiff (f,x,i) -> Point of (R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),F)) equals :: NDIFF_5:def 7
diff ((f * (reproj ((In (i,(dom G))),x))),((proj (In (i,(dom G)))) . x));
coherence
diff ((f * (reproj ((In (i,(dom G))),x))),((proj (In (i,(dom G)))) . x)) is Point of (R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),F))
;
end;

:: deftheorem defines partdiff NDIFF_5:def 7 :
for G being RealNormSpace-Sequence
for F being RealNormSpace
for i being set
for f being PartFunc of (),F
for x being Point of () holds partdiff (f,x,i) = diff ((f * (reproj ((In (i,(dom G))),x))),((proj (In (i,(dom G)))) . x));

definition
let G be RealNormSpace-Sequence;
let F be RealNormSpace;
let i be set ;
let f be PartFunc of (),F;
let X be set ;
pred f is_partial_differentiable_on X,i means :: NDIFF_5:def 8
( X c= dom f & ( for x being Point of () st x in X holds
f | X is_partial_differentiable_in x,i ) );
end;

:: deftheorem defines is_partial_differentiable_on NDIFF_5:def 8 :
for G being RealNormSpace-Sequence
for F being RealNormSpace
for i being set
for f being PartFunc of (),F
for X being set holds
( f is_partial_differentiable_on X,i iff ( X c= dom f & ( for x being Point of () st x in X holds
f | X is_partial_differentiable_in x,i ) ) );

theorem Th21: :: NDIFF_5:21
for G being RealNormSpace-Sequence
for i being Element of dom G
for xi being Element of (G . i) holds ||.((reproj (i,(0. ()))) . xi).|| = ||.xi.||
proof end;

theorem Th22: :: NDIFF_5:22
for G being RealNormSpace-Sequence
for i being Element of dom G
for x being Point of ()
for r being Point of (G . i) holds
( ((reproj (i,x)) . r) - x = (reproj (i,(0. ()))) . (r - ((proj i) . x)) & x - ((reproj (i,x)) . r) = (reproj (i,(0. ()))) . (((proj i) . x) - r) )
proof end;

theorem Th23: :: NDIFF_5:23
for G being RealNormSpace-Sequence
for i being Element of dom G
for x being Point of ()
for Z being Subset of () st Z is open & x in Z holds
ex N being Neighbourhood of (proj i) . x st
for z being Point of (G . i) st z in N holds
(reproj (i,x)) . z in Z
proof end;

theorem Th24: :: NDIFF_5:24
for G being RealNormSpace-Sequence
for T being RealNormSpace
for i being set
for f being PartFunc of (),T
for Z being Subset of () st Z is open holds
( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Point of () st x in Z holds
f is_partial_differentiable_in x,i ) ) )
proof end;

theorem :: NDIFF_5:25
for G being RealNormSpace-Sequence
for F being RealNormSpace
for f being PartFunc of (),F
for X, i being set st i in dom G & f is_partial_differentiable_on X,i holds
X is Subset of () by XBOOLE_1:1;

definition
let G be RealNormSpace-Sequence;
let S be RealNormSpace;
let i be set ;
let f be PartFunc of (),S;
let X be set ;
assume A2: f is_partial_differentiable_on X,i ;
func f partial| (X,i) -> PartFunc of (),(R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),S)) means :Def9: :: NDIFF_5:def 9
( dom it = X & ( for x being Point of () st x in X holds
it /. x = partdiff (f,x,i) ) );
existence
ex b1 being PartFunc of (),(R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),S)) st
( dom b1 = X & ( for x being Point of () st x in X holds
b1 /. x = partdiff (f,x,i) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of (),(R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),S)) st dom b1 = X & ( for x being Point of () st x in X holds
b1 /. x = partdiff (f,x,i) ) & dom b2 = X & ( for x being Point of () st x in X holds
b2 /. x = partdiff (f,x,i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines partial| NDIFF_5:def 9 :
for G being RealNormSpace-Sequence
for S being RealNormSpace
for i being set
for f being PartFunc of (),S
for X being set st f is_partial_differentiable_on X,i holds
for b6 being PartFunc of (),(R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),S)) holds
( b6 = f partial| (X,i) iff ( dom b6 = X & ( for x being Point of () st x in X holds
b6 /. x = partdiff (f,x,i) ) ) );

theorem Th26: :: NDIFF_5:26
for G being RealNormSpace-Sequence
for F being RealNormSpace
for f1, f2 being PartFunc of (),F
for x being Point of ()
for i being set st i in dom G holds
( (f1 + f2) * (reproj ((In (i,(dom G))),x)) = (f1 * (reproj ((In (i,(dom G))),x))) + (f2 * (reproj ((In (i,(dom G))),x))) & (f1 - f2) * (reproj ((In (i,(dom G))),x)) = (f1 * (reproj ((In (i,(dom G))),x))) - (f2 * (reproj ((In (i,(dom G))),x))) )
proof end;

theorem Th27: :: NDIFF_5:27
for r being Real
for G being RealNormSpace-Sequence
for F being RealNormSpace
for f being PartFunc of (),F
for x being Point of ()
for i being set st i in dom G holds
r (#) (f * (reproj ((In (i,(dom G))),x))) = (r (#) f) * (reproj ((In (i,(dom G))),x))
proof end;

theorem :: NDIFF_5:28
for G being RealNormSpace-Sequence
for F being RealNormSpace
for f1, f2 being PartFunc of (),F
for x being Point of ()
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)) )
proof end;

theorem :: NDIFF_5:29
for G being RealNormSpace-Sequence
for F being RealNormSpace
for f1, f2 being PartFunc of (),F
for x being Point of ()
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)) )
proof end;

theorem :: NDIFF_5:30
for r being Real
for G being RealNormSpace-Sequence
for F being RealNormSpace
for f being PartFunc of (),F
for x being Point of ()
for i being set st i in dom G & f is_partial_differentiable_in x,i holds
( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) )
proof end;

theorem Th31: :: NDIFF_5:31
for G being RealNormSpace-Sequence
for i being Element of dom G
for x being Point of () holds ||.((proj i) . x).|| <=
proof end;

registration
let G be RealNormSpace-Sequence;
cluster -> len G -element for Element of the carrier of ();
coherence
for b1 being Point of () holds b1 is len G -element
proof end;
end;

theorem Th32: :: NDIFF_5:32
for G being RealNormSpace-Sequence
for T being RealNormSpace
for i being set
for Z being Subset of ()
for f being PartFunc of (),T st Z is open holds
( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Point of () st x in Z holds
f is_partial_differentiable_in x,i ) ) )
proof end;

theorem Th33: :: NDIFF_5:33
for G being RealNormSpace-Sequence
for i, j being Element of dom G
for x being Point of (G . i)
for z being Element of product (carr G) st z = (reproj (i,(0. ()))) . x holds
( ( i = j implies z . j = x ) & ( i <> j implies z . j = 0. (G . j) ) )
proof end;

theorem Th34: :: NDIFF_5:34
for G being RealNormSpace-Sequence
for i being Element of dom G
for x, y being Point of (G . i) holds (reproj (i,(0. ()))) . (x + y) = ((reproj (i,(0. ()))) . x) + ((reproj (i,(0. ()))) . y)
proof end;

theorem Th35: :: NDIFF_5:35
for G being RealNormSpace-Sequence
for i being Element of dom G
for x, y being Point of () holds (proj i) . (x + y) = ((proj i) . x) + ((proj i) . y)
proof end;

theorem :: NDIFF_5:36
for G being RealNormSpace-Sequence
for i being Element of dom G
for x, y being Point of (G . i) holds (reproj (i,(0. ()))) . (x - y) = ((reproj (i,(0. ()))) . x) - ((reproj (i,(0. ()))) . y)
proof end;

theorem Th37: :: NDIFF_5:37
for G being RealNormSpace-Sequence
for i being Element of dom G
for x, y being Point of () holds (proj i) . (x - y) = ((proj i) . x) - ((proj i) . y)
proof end;

theorem Th38: :: NDIFF_5:38
for G being RealNormSpace-Sequence
for i being Element of dom G
for x being Point of (G . i) st x <> 0. (G . i) holds
(reproj (i,(0. ()))) . x <> 0. ()
proof end;

theorem Th39: :: NDIFF_5:39
for G being RealNormSpace-Sequence
for i being Element of dom G
for x being Point of (G . i)
for a being Real holds (reproj (i,(0. ()))) . (a * x) = a * ((reproj (i,(0. ()))) . x)
proof end;

theorem Th40: :: NDIFF_5:40
for G being RealNormSpace-Sequence
for i being Element of dom G
for x being Point of ()
for a being Real holds (proj i) . (a * x) = a * ((proj i) . x)
proof end;

theorem Th41: :: NDIFF_5:41
for G being RealNormSpace-Sequence
for S being RealNormSpace
for f being PartFunc of (),S
for x being Point of ()
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. ()))) )
proof end;

Lm5: for G being RealNormSpace-Sequence
for S being RealNormSpace
for f being PartFunc of (),S
for x being Point of () ex L being Lipschitzian LinearOperator of (),S st
for h being Element of () 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 (In (i,(dom G)))) . h) ) & L . h = Sum w )

proof end;

theorem Th42: :: NDIFF_5:42
for S being RealNormSpace
for h, g being FinSequence of S st len h = (len g) + 1 & ( for i being Nat st i in dom g holds
g /. i = (h /. i) - (h /. (i + 1)) ) holds
(h /. 1) - (h /. (len h)) = Sum g
proof end;

theorem :: NDIFF_5:43
for G being RealNormSpace-Sequence
for x, y being Element of product (carr G)
for Z being set holds x +* (y | Z) is Element of product (carr G) by CARD_3:79;

theorem Th44: :: NDIFF_5:44
for G being RealNormSpace-Sequence
for x, y being Point of ()
for Z, x0 being Element of product (carr G)
for X being set st Z = 0. () & x0 = x & y = Z +* (x0 | X) holds
<=
proof end;

theorem Th45: :: NDIFF_5:45
for G being RealNormSpace-Sequence
for S being RealNormSpace
for f being PartFunc of (),S
for x, y being Point of () ex h being FinSequence of () ex g being FinSequence of S ex Z, y0 being Element of product (carr G) st
( y0 = y & Z = 0. () & len h = (len G) + 1 & len g = len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) & ( for i being Nat st i in dom g holds
g /. i = (f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1)))) ) & ( for i being Nat
for hi being Point of () st i in dom h & h /. i = hi holds
||.hi.|| <= ) & (f /. (x + y)) - (f /. x) = Sum g )
proof end;

theorem Th46: :: NDIFF_5:46
for G being RealNormSpace-Sequence
for i being Element of dom G
for x, y being Point of ()
for xi being Point of (G . i) st y = (reproj (i,x)) . xi holds
(proj i) . y = xi
proof end;

theorem Th47: :: NDIFF_5:47
for G being RealNormSpace-Sequence
for i being Element of dom G
for y being Point of ()
for q being Point of (G . i) st q = (proj i) . y holds
y = (reproj (i,y)) . q
proof end;

theorem Th48: :: NDIFF_5:48
for G being RealNormSpace-Sequence
for i being Element of dom G
for x, y being Point of ()
for xi being Point of (G . i) st y = (reproj (i,x)) . xi holds
reproj (i,x) = reproj (i,y)
proof end;

theorem Th49: :: NDIFF_5:49
for G being RealNormSpace-Sequence
for i, j being Element of dom G
for x, y being Point of ()
for xi being Point of (G . i) st y = (reproj (i,x)) . xi & i <> j holds
(proj j) . x = (proj j) . y
proof end;

theorem :: NDIFF_5:50
for G being RealNormSpace-Sequence
for F being RealNormSpace
for i being Element of dom G
for x being Point of ()
for xi being Point of (G . i)
for f being PartFunc of (),F
for g being PartFunc of (G . i),F st (proj i) . x = xi & g = f * (reproj (i,x)) holds
diff (g,xi) = partdiff (f,x,i)
proof end;

theorem Th51: :: NDIFF_5:51
for G being RealNormSpace-Sequence
for F being RealNormSpace
for f being PartFunc of (),F
for x being Point of ()
for i being set
for M being Real
for L being Point of (R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),F))
for p, q being Point of (G . (In (i,(dom G)))) st i in dom G & ( for h being Point of (G . (In (i,(dom G)))) st h in ].p,q.[ holds
||.((partdiff (f,((reproj ((In (i,(dom G))),x)) . h),i)) - L).|| <= M ) & ( for h being Point of (G . (In (i,(dom G)))) st h in [.p,q.] holds
(reproj ((In (i,(dom G))),x)) . h in dom f ) & ( for h being Point of (G . (In (i,(dom G)))) st h in [.p,q.] holds
f is_partial_differentiable_in (reproj ((In (i,(dom G))),x)) . h,i ) holds
||.(((f /. ((reproj ((In (i,(dom G))),x)) . q)) - (f /. ((reproj ((In (i,(dom G))),x)) . p))) - (L . (q - p))).|| <= M * ||.(q - p).||
proof end;

theorem Th52: :: NDIFF_5:52
for G being RealNormSpace-Sequence
for x, y, z, w being Point of ()
for i being Element of dom G
for d being Real
for p, q, r being Point of (G . i) st ||.(y - x).|| < d & ||.(z - x).|| < d & p = (proj i) . y & z = (reproj (i,y)) . q & r in [.p,q.] & w = (reproj (i,y)) . r holds
||.(w - x).|| < d
proof end;

theorem Th53: :: NDIFF_5:53
for G being RealNormSpace-Sequence
for S being RealNormSpace
for f being PartFunc of (),S
for X being Subset of ()
for x, y, z being Point of ()
for i being set
for p, q being Point of (G . (In (i,(dom G))))
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 () st x in X holds
f is_partial_differentiable_in x,i ) & ( for z being Point of () st ||.(z - x).|| < d holds
z in X ) & ( for z being Point of () st ||.(z - x).|| < d holds
||.((partdiff (f,z,i)) - (partdiff (f,x,i))).|| <= r ) & z = (reproj ((In (i,(dom G))),y)) . p & q = (proj (In (i,(dom G)))) . y holds
||.(((f /. z) - (f /. y)) - ((partdiff (f,x,i)) . (p - q))).|| <= ||.(p - q).|| * r
proof end;

theorem Th54: :: NDIFF_5:54
for G being RealNormSpace-Sequence
for h being FinSequence of ()
for y, x being Point of ()
for y0, Z being Element of product (carr G)
for j being Element of NAT st y = y0 & Z = 0. () & len h = (len G) + 1 & 1 <= j & j <= len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) holds
x + (h /. j) = (reproj ((In ((((len G) + 1) -' j),(dom G))),(x + (h /. (j + 1))))) . ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y))
proof end;

theorem Th55: :: NDIFF_5:55
for G being RealNormSpace-Sequence
for h being FinSequence of ()
for y, x being Point of ()
for y0, Z being Element of product (carr G)
for j being Element of NAT st y = y0 & Z = 0. () & len h = (len G) + 1 & 1 <= j & j <= len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) holds
((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y)) - ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + (h /. (j + 1)))) = (proj (In ((((len G) + 1) -' j),(dom G)))) . y
proof end;

theorem Th56: :: NDIFF_5:56
for G being RealNormSpace-Sequence
for S being RealNormSpace
for f being PartFunc of (),S
for X being Subset of ()
for x being Point of () st X is open & x in X & ( for i being set st i in dom G holds
( f is_partial_differentiable_on X,i & f partial| (X,i) is_continuous_on X ) ) holds
( f is_differentiable_in x & ( for h being Point of () ex w being FinSequence of S st
( dom w = dom G & ( for i being set st i in dom G holds
w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . h) ) & (diff (f,x)) . h = Sum w ) ) )
proof end;

theorem :: NDIFF_5:57
for G being RealNormSpace-Sequence
for F being RealNormSpace
for f being PartFunc of (),F
for X being Subset of () st X is open holds
( ( for i being set st i in dom G holds
( f is_partial_differentiable_on X,i & f partial| (X,i) is_continuous_on X ) ) iff ( f is_differentiable_on X & f | X is_continuous_on X ) )
proof end;