let G be RealNormSpace-Sequence; for F being RealNormSpace
for f being PartFunc of (product G),F
for X being Subset of (product G) 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 ) )
let F be RealNormSpace; for f being PartFunc of (product G),F
for X being Subset of (product G) 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 ) )
let f be PartFunc of (product G),F; for X being Subset of (product G) 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 ) )
let X be Subset of (product G); ( X is open implies ( ( 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 ) ) )
assume A1:
X is open
; ( ( 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 ) )
set m = len G;
A2:
dom G = Seg (len G)
by FINSEQ_1:def 3;
hereby ( f is_differentiable_on X & f `| X is_continuous_on X implies 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 ) )
assume A3:
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 )
;
( f is_differentiable_on X & f `| X is_continuous_on X )A4:
now for i being Element of NAT st 1 <= i & i <= len G holds
( X c= dom (f `partial| (X,i)) & ( for y0 being Point of (product G)
for r being Real st y0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (product G) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) ) ) )let i be
Element of
NAT ;
( 1 <= i & i <= len G implies ( X c= dom (f `partial| (X,i)) & ( for y0 being Point of (product G)
for r being Real st y0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (product G) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) ) ) ) )assume
( 1
<= i &
i <= len G )
;
( X c= dom (f `partial| (X,i)) & ( for y0 being Point of (product G)
for r being Real st y0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (product G) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) ) ) )then
i in Seg (len G)
;
then
f `partial| (
X,
i)
is_continuous_on X
by A3, A2;
hence
(
X c= dom (f `partial| (X,i)) & ( for
y0 being
Point of
(product G) for
r being
Real st
y0 in X &
0 < r holds
ex
s being
Real st
(
0 < s & ( for
y1 being
Point of
(product G) st
y1 in X &
||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) ) ) )
by NFCONT_1:19;
verum end; A5:
1
<= len G
by NAT_1:14;
then
len G in dom G
by A2;
then A6:
f is_partial_differentiable_on X,
len G
by A3;
for
x being
Point of
(product G) st
x in X holds
f is_differentiable_in x
by A1, A3, Th56;
hence A7:
f is_differentiable_on X
by A1, A6, NDIFF_1:31;
f `| X is_continuous_on Xthen A8:
dom (f `| X) = X
by NDIFF_1:def 9;
for
y0 being
Point of
(product G) for
r being
Real st
y0 in X &
0 < r holds
ex
s being
Real st
(
0 < s & ( for
y1 being
Point of
(product G) st
y1 in X &
||.(y1 - y0).|| < s holds
||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r ) )
proof
let y0 be
Point of
(product G);
for r being Real st y0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (product G) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r ) )let r be
Real;
( y0 in X & 0 < r implies ex s being Real st
( 0 < s & ( for y1 being Point of (product G) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r ) ) )
assume A9:
(
y0 in X &
0 < r )
;
ex s being Real st
( 0 < s & ( for y1 being Point of (product G) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r ) )
defpred S1[
Nat,
Real]
means for
i being
Element of
NAT st
i = $1 holds
(
0 < $2 & ( for
y1 being
Point of
(product G) st
y1 in X &
||.(y1 - y0).|| < $2 holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r / (2 * (len G)) ) );
consider S being
FinSequence of
REAL such that A12:
(
dom S = Seg (len G) & ( for
i being
Nat st
i in Seg (len G) holds
S1[
i,
S . i] ) )
from FINSEQ_1:sch 5(A10);
take s =
min S;
( 0 < s & ( for y1 being Point of (product G) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r ) )
A13:
len S = len G
by A12, FINSEQ_1:def 3;
then
min_p S in dom S
by RFINSEQ2:def 2;
hence
s > 0
by A12;
for y1 being Point of (product G) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r
let y1 be
Point of
(product G);
( y1 in X & ||.(y1 - y0).|| < s implies ||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r )
assume A14:
(
y1 in X &
||.(y1 - y0).|| < s )
;
||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r
reconsider DD =
(diff (f,y1)) - (diff (f,y0)) as
Lipschitzian LinearOperator of
(product G),
F by LOPBAN_1:def 9;
A15:
upper_bound (PreNorms DD) = ||.((diff (f,y1)) - (diff (f,y0))).||
by LOPBAN_1:30;
now for mt being Real st mt in PreNorms DD holds
mt <= r / 2let mt be
Real;
( mt in PreNorms DD implies mt <= r / 2 )assume
mt in PreNorms DD
;
mt <= r / 2then consider t being
VECTOR of
(product G) such that A16:
(
mt = ||.(DD . t).|| &
||.t.|| <= 1 )
;
consider w0 being
FinSequence of
F such that A17:
(
dom w0 = dom G & ( for
i being
set st
i in dom G holds
w0 . i = (partdiff (f,y0,i)) . ((proj (In (i,(dom G)))) . t) ) &
(diff (f,y0)) . t = Sum w0 )
by A1, A3, Th56, A9;
reconsider Sw0 =
Sum w0 as
Point of
F ;
consider w1 being
FinSequence of
F such that A18:
(
dom w1 = dom G & ( for
i being
set st
i in dom G holds
w1 . i = (partdiff (f,y1,i)) . ((proj (In (i,(dom G)))) . t) ) &
(diff (f,y1)) . t = Sum w1 )
by A1, A3, Th56, A14;
reconsider Sw1 =
Sum w1 as
Point of
F ;
deffunc H1(
set )
-> Element of the
carrier of
F =
(w1 /. $1) - (w0 /. $1);
consider w2 being
FinSequence of
F such that A19:
(
len w2 = len G & ( for
i being
Nat st
i in dom w2 holds
w2 . i = H1(
i) ) )
from FINSEQ_2:sch 1();
A20:
(
len w1 = len G &
len w0 = len G )
by A2, A17, A18, FINSEQ_1:def 3;
then
Sum w2 = (Sum w1) - (Sum w0)
by A19, A20, RLVECT_2:5;
then A21:
mt = ||.(Sum w2).||
by A16, A18, A17, LOPBAN_1:40;
deffunc H2(
Nat)
-> Element of
REAL =
In (
||.(w2 /. $1).||,
REAL);
consider ys being
FinSequence of
REAL such that A22:
(
len ys = len G & ( for
j being
Nat st
j in dom ys holds
ys . j = H2(
j) ) )
from FINSEQ_2:sch 1();
then A24:
||.(Sum w2).|| <= Sum ys
by A19, A22, Th7;
reconsider rm =
r / (2 * (len G)) as
Element of
REAL by XREAL_0:def 1;
deffunc H3(
Nat)
-> Element of
REAL =
rm;
consider rs being
FinSequence of
REAL such that A25:
(
len rs = len G & ( for
j being
Nat st
j in dom rs holds
rs . j = H3(
j) ) )
from FINSEQ_2:sch 1();
A26:
dom rs = Seg (len G)
by A25, FINSEQ_1:def 3;
then A28:
rng rs c= {rm}
;
then
{rm} c= rng rs
;
then
rs = (len G) |-> (r / (2 * (len G)))
by A26, A28, XBOOLE_0:def 10, FUNCOP_1:9;
then Sum rs =
(len G) * (r / (2 * (len G)))
by RVSUM_1:80
.=
(len G) * ((r / 2) / (len G))
by XCMPLX_1:78
;
then A31:
Sum rs = r / 2
by XCMPLX_1:87;
now for i being Element of NAT st i in dom ys holds
ys . i <= rs . ilet i be
Element of
NAT ;
( i in dom ys implies ys . i <= rs . i )assume
i in dom ys
;
ys . i <= rs . ithen A32:
i in Seg (len G)
by A22, FINSEQ_1:def 3;
then A33:
(
i in dom w2 &
i in dom w1 &
i in dom w0 )
by A17, A18, A19, FINSEQ_1:def 3;
then A34:
(
ys . i = ||.(w2 /. i).|| &
w2 /. i = w2 . i )
by A23, PARTFUN1:def 6;
A35:
i in dom rs
by A25, A32, FINSEQ_1:def 3;
reconsider p1 =
partdiff (
f,
y1,
i),
p0 =
partdiff (
f,
y0,
i) as
Lipschitzian LinearOperator of
(G . (In (i,(dom G)))),
F by LOPBAN_1:def 9;
reconsider P1 =
p1 . ((proj (In (i,(dom G)))) . t) as
VECTOR of
F ;
reconsider P0 =
p0 . ((proj (In (i,(dom G)))) . t) as
VECTOR of
F ;
(
w0 /. i = w0 . i &
w1 /. i = w1 . i )
by A33, PARTFUN1:def 6;
then
(
w0 /. i = P0 &
w1 /. i = P1 )
by A2, A17, A18, A32;
then A36:
w2 . i = P1 - P0
by A33, A19;
( 1
<= i &
i <= len S )
by A13, A32, FINSEQ_1:1;
then A37:
(
s <= S . i &
f is_partial_differentiable_on X,
i )
by A2, A32, A3, RFINSEQ2:2;
then
||.(y1 - y0).|| < S . i
by A14, XXREAL_0:2;
then
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r / (2 * (len G))
by A12, A32, A14;
then
||.((partdiff (f,y1,i)) - ((f `partial| (X,i)) /. y0)).|| < r / (2 * (len G))
by Def9, A14, A37;
then A38:
||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| < r / (2 * (len G))
by Def9, A9, A37;
reconsider PP =
(partdiff (f,y1,i)) - (partdiff (f,y0,i)) as
Lipschitzian LinearOperator of
(G . (In (i,(dom G)))),
F by LOPBAN_1:def 9;
A39:
upper_bound (PreNorms PP) = ||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).||
by LOPBAN_1:30;
reconsider pt =
(proj (In (i,(dom G)))) . t as
VECTOR of
(G . (In (i,(dom G)))) ;
A40:
PP . pt = P1 - P0
by LOPBAN_1:40;
||.pt.|| <= ||.t.||
by Th31;
then
||.pt.|| <= 1
by A16, XXREAL_0:2;
then
(
||.(PP . pt).|| in PreNorms PP & not
PreNorms PP is
empty &
PreNorms PP is
bounded_above )
by LOPBAN_1:27;
then
||.(PP . pt).|| <= upper_bound (PreNorms PP)
by SEQ_4:def 1;
then
||.(P1 - P0).|| <= r / (2 * (len G))
by A40, A38, A39, XXREAL_0:2;
hence
ys . i <= rs . i
by A34, A25, A35, A36;
verum end; then
Sum ys <= r / 2
by A31, A25, A22, INTEGRA5:3;
hence
mt <= r / 2
by A21, A24, XXREAL_0:2;
verum end;
then
(
||.((diff (f,y1)) - (diff (f,y0))).|| <= r / 2 &
r / 2
< r )
by A15, A9, SEQ_4:45, XREAL_1:216;
then
||.((diff (f,y1)) - (diff (f,y0))).|| < r
by XXREAL_0:2;
then
||.((diff (f,y1)) - ((f `| X) /. y0)).|| < r
by A7, A9, NDIFF_1:def 9;
hence
||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r
by A7, A14, NDIFF_1:def 9;
verum
end; hence
f `| X is_continuous_on X
by A8, NFCONT_1:19;
verum
end;
assume A41:
( f is_differentiable_on X & f `| X is_continuous_on 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 )
then A42:
( X c= dom f & ( for x being Point of (product G) st x in X holds
f is_differentiable_in x ) )
by A1, NDIFF_1:31;
thus
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 )
verumproof
let i be
set ;
( i in dom G implies ( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) )
assume
i in dom G
;
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )
then reconsider i0 =
i as
Element of
NAT ;
now for x being Point of (product G) st x 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);
( x in X implies ( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj ((In (i,(dom G))),(0. (product G)))) ) )assume
x in X
;
( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj ((In (i,(dom G))),(0. (product G)))) )then
f is_differentiable_in x
by A41, A1, NDIFF_1:31;
hence
(
f is_partial_differentiable_in x,
i &
partdiff (
f,
x,
i)
= (diff (f,x)) * (reproj ((In (i,(dom G))),(0. (product G)))) )
by Th41;
verum end;
then
for
x being
Point of
(product G) st
x in X holds
f is_partial_differentiable_in x,
i
;
hence A44:
f is_partial_differentiable_on X,
i
by A1, Th32, A42;
f `partial| (X,i) is_continuous_on X
then A45:
dom (f `partial| (X,i)) = X
by Def9;
for
y0 being
Point of
(product G) for
r being
Real st
y0 in X &
0 < r holds
ex
s being
Real st
(
0 < s & ( for
y1 being
Point of
(product G) st
y1 in X &
||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) )
proof
let y0 be
Point of
(product G);
for r being Real st y0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (product G) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) )let r be
Real;
( y0 in X & 0 < r implies ex s being Real st
( 0 < s & ( for y1 being Point of (product G) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) ) )
assume A46:
(
y0 in X &
0 < r )
;
ex s being Real st
( 0 < s & ( for y1 being Point of (product G) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) )
then consider s being
Real such that A47:
(
0 < s & ( for
y1 being
Point of
(product G) st
y1 in X &
||.(y1 - y0).|| < s holds
||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r ) )
by A41, NFCONT_1:19;
take
s
;
( 0 < s & ( for y1 being Point of (product G) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) )
thus
0 < s
by A47;
for y1 being Point of (product G) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r
let y1 be
Point of
(product G);
( y1 in X & ||.(y1 - y0).|| < s implies ||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r )
assume A48:
(
y1 in X &
||.(y1 - y0).|| < s )
;
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r
then
||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r
by A47;
then
||.((diff (f,y1)) - ((f `| X) /. y0)).|| < r
by A48, A41, NDIFF_1:def 9;
then A49:
||.((diff (f,y1)) - (diff (f,y0))).|| < r
by A46, A41, NDIFF_1:def 9;
(
f is_differentiable_in y1 &
f is_differentiable_in y0 )
by A41, A1, A48, A46, NDIFF_1:31;
then A50:
(
partdiff (
f,
y1,
i)
= (diff (f,y1)) * (reproj ((In (i,(dom G))),(0. (product G)))) &
partdiff (
f,
y0,
i)
= (diff (f,y0)) * (reproj ((In (i,(dom G))),(0. (product G)))) )
by Th41;
reconsider PP =
(partdiff (f,y1,i)) - (partdiff (f,y0,i)) as
Lipschitzian LinearOperator of
(G . (In (i,(dom G)))),
F by LOPBAN_1:def 9;
reconsider DD =
(diff (f,y1)) - (diff (f,y0)) as
Lipschitzian LinearOperator of
(product G),
F by LOPBAN_1:def 9;
A51:
(
upper_bound (PreNorms PP) = ||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| &
upper_bound (PreNorms DD) = ||.((diff (f,y1)) - (diff (f,y0))).|| )
by LOPBAN_1:30;
A52:
(
PreNorms PP is
bounded_above &
PreNorms DD is
bounded_above )
by LOPBAN_1:28;
now for a being object st a in PreNorms PP holds
a in PreNorms DDlet a be
object ;
( a in PreNorms PP implies a in PreNorms DD )assume
a in PreNorms PP
;
a in PreNorms DDthen consider t being
VECTOR of
(G . (In (i,(dom G)))) such that A53:
(
a = ||.(PP . t).|| &
||.t.|| <= 1 )
;
A54:
dom (reproj ((In (i,(dom G))),(0. (product G)))) = the
carrier of
(G . (In (i,(dom G))))
by FUNCT_2:def 1;
reconsider tm =
(reproj ((In (i,(dom G))),(0. (product G)))) . t as
Point of
(product G) ;
A55:
||.tm.|| <= 1
by A53, Th21;
(
(partdiff (f,y1,i)) . t = (diff (f,y1)) . tm &
(partdiff (f,y0,i)) . t = (diff (f,y0)) . tm )
by A54, A50, FUNCT_1:13;
then
||.(PP . t).|| = ||.(((diff (f,y1)) . tm) - ((diff (f,y0)) . tm)).||
by LOPBAN_1:40;
then
||.(PP . t).|| = ||.(DD . tm).||
by LOPBAN_1:40;
hence
a in PreNorms DD
by A53, A55;
verum end;
then
PreNorms PP c= PreNorms DD
;
then
||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| <= ||.((diff (f,y1)) - (diff (f,y0))).||
by A52, A51, SEQ_4:48;
then
||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| < r
by A49, XXREAL_0:2;
then
||.((partdiff (f,y1,i)) - ((f `partial| (X,i)) /. y0)).|| < r
by Def9, A46, A44;
hence
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r
by Def9, A48, A44;
verum
end;
hence
f `partial| (
X,
i)
is_continuous_on X
by A45, NFCONT_1:19;
verum
end;