:: Differentiable Functions on Normed Linear Spaces
:: by Yasunari Shidama
::
:: Received June 2, 2011
:: Copyright (c) 2011-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, ZFMISC_1, NORMSP_1, PRE_TOPC, PARTFUN1, FUNCT_1,
FUNCT_4, NAT_1, FDIFF_1, SUBSET_1, SEQ_4, RELAT_1, GLIB_000, LOPBAN_1,
ORDINAL4, RFINSEQ, RCOMP_1, TARSKI, SEQ_1, ARYTM_3, VALUED_1, FUNCT_2,
ARYTM_1, SEQ_2, ORDINAL2, SUPINF_2, FCONT_1, COMPLEX1, STRUCT_0, CARD_1,
VALUED_0, XXREAL_0, GROUP_2, FUNCOP_1, MEMBERED, FINSEQ_5, XXREAL_2,
XBOOLE_0, CARD_3, FINSEQ_1, FINSEQ_2, AFINSQ_1, RLVECT_1, SQUARE_1,
RVSUM_1, XXREAL_1, PDIFF_1, PRVECT_1, PRVECT_2, ALGSTR_0, EUCLID,
CFCONT_1, RFINSEQ2, NORMSP_0, MONOID_0, RLTOPSP1, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, FUNCOP_1, FUNCT_4, CARD_1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, REAL_1, SQUARE_1, NAT_1, MEMBERED, VALUED_0, COMPLEX1,
NAT_D, XXREAL_2, CARD_3, FINSEQ_1, VALUED_1, FINSEQ_2, SEQ_1, SEQ_2,
RVSUM_1, RFINSEQ, SEQ_4, RCOMP_1, FCONT_1, FDIFF_1, FINSEQ_5, FINSEQ_7,
RFINSEQ2, STRUCT_0, MONOID_0, ALGSTR_0, PRE_TOPC, RLVECT_1, NORMSP_0,
NORMSP_1, VFUNCT_1, EUCLID, LOPBAN_1, PRVECT_1, NFCONT_1, NDIFF_1,
PRVECT_2, NFCONT_3, NDIFF_3, RLTOPSP1, FUNCT_7;
constructors REAL_1, SQUARE_1, SEQ_2, FDIFF_1, NFCONT_1, RSSPACE, VFUNCT_1,
NDIFF_1, RELSET_1, FINSEQ_7, FINSEQ_5, RVSUM_1, BINOP_2, PRVECT_2,
RLVECT_2, NAT_D, FINSEQOP, RFINSEQ, RFINSEQ2, SEQ_4, FCONT_1, NFCONT_3,
NDIFF_3, MONOID_0, RLTOPSP1, FUNCT_7, COMSEQ_2, FUNCT_4, NUMBERS,
RCOMP_1;
registrations RELSET_1, STRUCT_0, ORDINAL1, XREAL_0, MEMBERED, FUNCT_1,
NDIFF_1, FUNCT_2, NUMBERS, XBOOLE_0, VALUED_0, PRVECT_2, FINSEQ_2,
FINSEQ_1, CARD_3, NORMSP_0, NORMSP_1, RELAT_1, XXREAL_0, LOPBAN_1,
LOPBAN_2, PRVECT_3, FUNCOP_1, NAT_1, FINSEQ_5, XXREAL_2, RCOMP_1,
VALUED_1, FDIFF_1, NFCONT_3, FINSET_1, XCMPLX_0, CARD_1, MONOID_0,
FUNCT_4, SQUARE_1, PRVECT_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, FUNCT_2, MONOID_0;
equalities RLVECT_1, LOPBAN_1, EUCLID, RFINSEQ2, FINSEQ_1, FINSEQ_2, STRUCT_0,
ALGSTR_0, NORMSP_0, RCOMP_1, XCMPLX_0;
expansions TARSKI, FUNCT_2, LOPBAN_1, FINSEQ_1, STRUCT_0;
theorems TARSKI, ABSVALUE, XBOOLE_0, XBOOLE_1, RLVECT_1, XCMPLX_0, XCMPLX_1,
ZFMISC_1, SEQ_1, SEQ_2, NAT_1, RELAT_1, FUNCT_1, VFUNCT_1, FUNCT_2,
FUNCT_3, FINSEQ_4, RLVECT_2, FINSEQ_3, ORDINAL1, FINSEQ_1, CARD_3,
FUNCT_4, SEQ_4, NORMSP_1, LOPBAN_1, PARTFUN1, PARTFUN2, NFCONT_1,
FDIFF_1, NDIFF_1, FUNCOP_1, XREAL_1, COMPLEX1, XXREAL_0, VALUED_1,
VALUED_0, VECTSP_1, NORMSP_0, XREAL_0, RCOMP_1, FINSEQ_2, FINSEQ_7,
RVSUM_1, SQUARE_1, PRVECT_1, PRVECT_2, PDIFF_7, EUCLID, XXREAL_2,
FINSEQ_5, NAT_D, RFINSEQ2, INTEGRA5, FCONT_1, NAT_2, NFCONT_3, NDIFF_2,
NDIFF_3, CARD_1, ROLLE, XXREAL_1, RLTOPSP1, FUNCT_7, SUBSET_1;
schemes FUNCT_2, SEQ_1, FINSEQ_1, NAT_1, FINSEQ_2;
begin :: Preliminaries
reserve j for set;
reserve p,r for Real;
reserve S,T,F for RealNormSpace;
reserve x0 for Point of S;
reserve g for PartFunc of S,T;
reserve c for constant sequence of S;
reserve R for RestFunc of S,T;
reserve G for RealNormSpace-Sequence;
reserve i for Element of dom G;
reserve f for PartFunc of product G,F;
reserve x for Element of product G;
theorem Th1:
for R be Function of REAL,S
holds R is RestFunc-like
iff for r be Real st r > 0
ex d be Real st d > 0 &
for z be Real
st z <> 0 & |. z .| < d holds |.z.|"* ||. R/.z .|| < r
proof
let R be Function of REAL,S;
A1:dom R = REAL by PARTFUN1:def 2;
A2:now assume
A3: R is RestFunc-like;
assume not
(for r be Real st r > 0
ex d be Real st d > 0 & for z be Real
st z <> 0 & |. z .| < d holds |. z .|"* ||. R/.z .|| < r); then
consider r be Real such that
A4: r > 0 and
A5: for d be Real st d > 0 holds
ex z be Real st z <> 0 & |. z .| < d
& not |. z .|"* ||. R/.z .|| < r;
defpred P[Nat,Real] means
$2 <> 0 & |. $2 .| < (1/($1+1)) & not |. $2 .|"* ||. R/.$2 .|| < r;
A6: for n be Element of NAT ex z be Element of REAL st P[n,z]
proof
let n be Element of NAT;
set d = 1/(n + 1);
consider z be Real such that
A7: z <> 0 & |. z .| < d
& not |. z .|"* ||. R/.z .|| < r by A5;
reconsider z as Element of REAL by XREAL_0:def 1;
take z;
thus thesis by A7;
end;
consider s be Real_Sequence such that
A8: for n being Element of NAT holds P[n,s.n] from FUNCT_2:sch 3(A6);
A9: for n being Nat holds P[n,s.n]
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A8;
end;
A10: now let p be Real;
assume A11: 0<p;
consider n be Nat such that
A12: p"<n by SEQ_4:3;
reconsider q0=0, q1=1 as Real;
p" + q0 < n + q1 by A12,XREAL_1:8; then
A13: 1/(n+1) < 1/p" by A11,XREAL_1:76;
take n;
let m be Nat;
assume n<=m; then
n + 1 <= m + 1 by XREAL_1:6; then
1/(m+1) <= 1/(n+1) by XREAL_1:118; then
|. s.m - 0 .| < 1/(n+1) by A9,XXREAL_0:2;
hence |. s.m - 0 .| <p by A13,XXREAL_0:2;
end; then
s is convergent by SEQ_2:def 6; then
lim s = 0 by A10,SEQ_2:def 7; then
reconsider s as 0-convergent non-zero Real_Sequence
by A10,A9,SEQ_1:5,SEQ_2:def 6,FDIFF_1:def 1;
(s")(#)(R/*s) is convergent & lim( (s")(#)(R/*s) ) = 0.S
by A3,NDIFF_3:def 1; then
consider n0 be Nat such that
A16: for m be Nat st n0 <=m
holds ||. ((s")(#)(R/*s)).m - 0.S .|| < r by A4,NORMSP_1:def 7;
A17: n0 in NAT by ORDINAL1:def 12;
A19: ||.(s.n0)"*(R/.(s.n0)).||
= |.(s.n0)".| * ||. R/.(s.n0) .|| by NORMSP_1:def 1
.=|. s.n0 .|" * ||. R/.(s.n0) .|| by COMPLEX1:66;
A20:rng s c= dom R by A1;
||. ((s")(#)(R/*s)).n0 - 0.S .||
= ||. ((s")(#)(R/*s)).n0 .|| by RLVECT_1:13
.= ||. (s".n0)*((R/*s).n0) .|| by NDIFF_1:def 2
.= ||. (s.n0)"*((R/*s).n0) .|| by VALUED_1:10
.= ||. (s.n0)"*(R/.(s.n0)) .|| by A20,FUNCT_2:109,A17;
hence
for r be Real st r > 0
ex d be Real st d > 0 & for z be Real st
z <> 0 & |. z .| < d holds |. z .|"* ||. R/.z .|| < r by A9,A16,A19;
end;
now assume
A21:for r be Real st r > 0
ex d be Real st d > 0 &
for z be Real
st z <> 0 & |. z .| < d holds |. z .|"* ||. R/.z .|| < r;
now let s be 0-convergent non-zero Real_Sequence;
A22: s is convergent & lim s = 0;
A23: now let r be Real;
assume r > 0; then
consider d be Real such that
A24: d > 0 and
A25: for z be Real st z <> 0 & |.z.| < d
holds |.z.|"* ||. R/.z .|| < r by A21;
consider n0 be Nat such that
A26: for m be Nat st n0 <=m
holds |. s.m-0 .| < d by A22,A24,SEQ_2:def 7;
take n0;
thus for m be Nat st n0 <=m
holds ||. ((s")(#)(R/*s)).m- 0.S .|| < r
proof
A27: rng s c= dom R by A1;
let m be Nat;
assume n0 <=m; then
A28: |. s.m-0 .| < d by A26;
A30: m in NAT by ORDINAL1:def 12;
|. s.m .|" * ||. R/.(s.m) .||
= |.(s.m)".| * ||. R/.(s.m) .|| by COMPLEX1:66
.= ||. (s.m)"*(R/.(s.m)) .|| by NORMSP_1:def 1
.= ||. (s.m)"*((R/*s).m) .|| by A27,FUNCT_2:109,A30
.= ||. (s".m)*((R/*s).m) .|| by VALUED_1:10
.= ||. ((s")(#)(R/*s)).m .|| by NDIFF_1:def 2
.= ||. ((s")(#)(R/*s)).m- 0.S .|| by RLVECT_1:13;
hence thesis by A25,A28,SEQ_1:5;
end;
end;
hence (s")(#)(R/*s) is convergent by NORMSP_1:def 6;
hence lim ((s")(#)(R/*s)) = 0.S by A23,NORMSP_1:def 7;
end;
hence R is RestFunc-like by NDIFF_3:def 1;
end;
hence thesis by A2;
end;
theorem Th2:
for R be RestFunc of S st R/.0=0.S
for e be Real st e > 0 ex d be Real st
d > 0 & for h be Real st |.h.| < d holds ||.R/.h.|| <= e*|.h.|
proof
let R be RestFunc of S such that
A1: R/.0=0.S;
let e be Real such that
A2: e > 0;
R is total by NDIFF_3:def 1; then
consider d be Real such that
A3: d > 0 and
A4: for z be Real st z <> 0 & |.z.| < d
holds |.z.|"* ||. R/.z .|| < e by A2,Th1;
take d;
now let h be Real such that
A5: |.h.| < d;
A6: 0 <= |.h.| by COMPLEX1:46;
per cases;
suppose A7: h <> 0; then
|.h.|"*||. R/.h .|| <= e by A4,A5; then
|.h.|*(|.h.|"*||. R/.h .||) <= |.h.|*e by A6,XREAL_1:64; then
A8: |.h.|*|.h.|"*||. R/.h .|| <= e * |.h.|;
|.h.| <> 0 by A7,COMPLEX1:45; then
1*||. R/.h .|| <= e * |.h.| by A8,XCMPLX_0:def 7;
hence ||. R/.h .|| <= e* |.h.|;
end;
suppose A9: h = 0;
reconsider p0=0 as Real;
p0* |.h.| <= e* |.h.| by A2,A6;
hence ||. R/.h .|| <= e* |.h.| by A1,A9;
end;
end;
hence thesis by A3;
end;
theorem Th3:
for R be RestFunc of S
for L be Lipschitzian LinearOperator of S,T holds
L*R is RestFunc of T
proof
let R be RestFunc of S;
let L be Lipschitzian LinearOperator of S,T;
consider K be Real such that
A1: 0 <= K and
A2: for z be Point of S holds ||. L.z .|| <= K * ||.z.|| by LOPBAN_1:def 8;
dom L = the carrier of S by FUNCT_2:def 1; then
A3:rng R c= dom L;
A4:R is total by NDIFF_3:def 1; then
A5:dom R = REAL by PARTFUN1:def 2;
now let e be Real such that
A6: e > 0;
set e1 = e/2/(1 + K);
consider d be Real such that
A7: 0 < d and
A8: for h be Real st h <> 0 & |.h.| < d
holds |.h.|"* ||. R/.h .|| < e1
by A1,A4,A6,Th1;
A9: e/2 < e by A6,XREAL_1:216;
now let h be Real;
reconsider hh=h as Element of REAL by XREAL_0:def 1;
assume A10: h <> 0 & |.h.| < d; then
|.h.|"* ||.(R/.h).|| < e1 by A8; then
(K +1)*(|.h.|"* ||.R/.h.||) <= (K +1)*e1 by A1,XREAL_1:64; then
A11: (K +1)*(|.h.|"* ||.R/.h.||) <= e/2 by A1,XCMPLX_1:87;
|.h.| <> 0 by A10,COMPLEX1:45; then
A12: |.h.| > 0 by COMPLEX1:46;
reconsider p0=0, p1=1 as Element of REAL by XREAL_0:def 1;
p0 + K < p1 + K by XREAL_1:8; then
A13: K * ||.R/.h.|| <= (K +1) * ||.R/.h.|| by XREAL_1:64;
||.L.(R/.h).|| <= K * ||.R/.h.|| by A2; then
||.L.(R/.h).|| <= (K +1) * ||.R/.h.|| by A13,XXREAL_0:2; then
|.h.|"* ||.L.(R/.h).|| <= |.h.|"*((K +1)*||. R/.h .||) by A12,XREAL_1:64
; then
A14: |.h.|"* ||.L.(R/.h).|| <= e/2 by A11,XXREAL_0:2;
L.(R/.h) = L/.(R/.h); then
L.(R/.hh) =(L*R)/.hh by A5,A3,PARTFUN2:5;
hence |.h.|"* ||.(L*R)/.h.|| < e by A9,A14,XXREAL_0:2;
end;
hence ex d be Real st d > 0 &
for h be Real st h <> 0 & |.h.| < d
holds |.h.|"* ||.(L*R)/.h.|| < e by A7;
end;
hence thesis by A4,Th1;
end;
theorem Th4:
for R1 be RestFunc of S st R1/.0 = 0.S
for R2 be RestFunc of S,T st R2/.(0.S) = 0.T
for L be LinearFunc of S holds
R2*(L+R1) is RestFunc of T
proof
let R1 be RestFunc of S;
assume R1/.0 = 0.S; then
consider d0 be Real such that
A1: 0 < d0 and
A2: for h be Real
st |.h.| < d0 holds ||.R1/.h.|| <= 1* |.h.| by Th2;
let R2 be RestFunc of S,T such that
A3:R2/.(0.S) = 0.T;
let L be LinearFunc of S;
consider r be Point of S such that
A4: for h be Real holds L/.h = h*r by NDIFF_3:def 2;
reconsider K = ||.r.|| as Real;
R2 is total by NDIFF_1:def 5; then
dom R2 = the carrier of S by PARTFUN1:def 2; then
A5:rng(L+R1) c= dom R2;
R1 is total by NDIFF_3:def 1; then
L+R1 is total by VFUNCT_1:32; then
A6:dom(L+R1) = REAL by PARTFUN1:def 2; then
dom(R2*(L+R1)) = REAL by A5,RELAT_1:27; then
A7:R2*(L+R1) is total by PARTFUN1:def 2;
now let e be Real such that
A8: e > 0;
A9: e/2 < e by A8,XREAL_1:216;
set e1 = e/2/(1 + K);
consider d be Real such that
A10: 0 < d and
A11: for z be Point of S st ||.z.|| < d
holds ||.R2/.z.|| <= e1*||.z.|| by A3,A8,NDIFF_2:7;
set d1 = d/(1 + K);
set dd1 = min(d0,d1);
A12: dd1 <= d1 & dd1 <= d0 by XXREAL_0:17;
A13: now let hh be Real such that
A14: hh <> 0 and
A15: |.hh.| < dd1;
reconsider h=hh as Element of REAL by XREAL_0:def 1;
|.h.| < d0 by A12,A15,XXREAL_0:2; then
A16: ||.R1/.h.|| <=1* |.h.| by A2;
reconsider p0=0 as Element of REAL by XREAL_0:def 1;
L.h = L/.h .= h*r by A4; then
||. L.h .|| - K * |.h.| + K * |.h.| <= p0 + K * |.h.|
by NORMSP_1:def 1; then
||.L.h+R1/.h.|| <= ||.L.h.|| + ||.R1/.h.||
& ||.L.h.|| + ||. R1/.h .|| <= K * |.h.| + 1 * |.h.|
by A16,NORMSP_1:def 1,XREAL_1:7; then
A17: ||.L.h+R1/.h.|| <= ( K +1) * |.h.| by XXREAL_0:2; then
A18: e1 * ||. L.h+R1/.h .|| <= e1*((K +1)*|.h.|) by A8,XREAL_1:64;
|.h.| < d1 by A12,A15,XXREAL_0:2; then
(K +1) * |.h.| < (K +1) * d1 by XREAL_1:68; then
||. L.h+R1/.h .|| < (K +1) * d1 by A17,XXREAL_0:2; then
||. L.h+R1/.h.|| < d by XCMPLX_1:87; then
||. R2/.(L.h+R1/.h) .|| <= e1 * ||. L.h+R1/.h .|| by A11; then
A19: ||. R2/.(L.h+R1/.h) .|| <= e1*((K +1)*|.h.|) by A18,XXREAL_0:2;
A20: R2/.(L.h+R1/.h) = R2/.(L/.h+R1/.h)
.=R2/.((L+R1)/.h) by A6,VFUNCT_1:def 1
.=(R2*(L+R1))/.h by A6,A5,PARTFUN2:5;
A21: |.h.| <> 0 by A14,COMPLEX1:45; then
|.h.| > 0 by COMPLEX1:46; then
|.h.|"* ||.(R2*(L+R1))/.h.|| <= |.h.|"* (e1* (K +1) * |.h.|)
by A20,A19,XREAL_1:64; then
|.h.|"* ||. (R2*(L+R1))/.h .|| <= |.h.|*|.h.|"*e1*(K +1); then
|.h.|"* ||. (R2*(L+R1))/.h .|| <= 1 * e1 * (K +1)
by A21,XCMPLX_0:def 7; then
|.h.|"* ||. (R2*(L+R1))/.h .|| <= e/2 by XCMPLX_1:87;
hence |.hh.|"* ||.(R2*(L+R1))/.hh.|| < e by A9,XXREAL_0:2;
end;
0 < dd1 by A1,A10,XXREAL_0:15;
hence
ex dd1 be Real st dd1 > 0 &
for h be Real st h <> 0 & |.h.| < dd1
holds |.h.|"* ||. (R2*(L+R1))/.h .|| < e by A13;
end;
hence thesis by A7,Th1;
end;
theorem Th5:
for R1 be RestFunc of S st R1/.0=0.S
for R2 be RestFunc of S,T st R2/.(0.S)=0.T
for L1 be LinearFunc of S
for L2 be Lipschitzian LinearOperator of S,T holds
L2*R1 + R2*(L1+R1) is RestFunc of T
proof
let R1 be RestFunc of S such that
A1: R1/.0=0.S;
let R2 be RestFunc of S,T such that
A2: R2/.(0.S)=0.T;
let L1 be LinearFunc of S;
let L2 be Lipschitzian LinearOperator of S,T;
L2*R1 is RestFunc of T & R2*(L1+R1) is RestFunc of T
by A1,A2,Th4,Th3;
hence thesis by NDIFF_3:7;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
theorem Th6:
for x0 be Real
for g be PartFunc of REAL,the carrier of S st
g is_differentiable_in x0
for f be 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
let x0 be Real;
let g be PartFunc of REAL,the carrier of S such that
A1: g is_differentiable_in x0;
consider N1 being Neighbourhood of x0 such that
A2: N1 c= dom g and
A3: ex L1 be LinearFunc of S,R1 be RestFunc of S st
diff(g,x0) = L1/.1
& for x be Real
st x in N1 holds g/.x-g/.x0 = L1/.(x-x0) + R1/.(x-x0)
by A1,NDIFF_3:def 4;
let f be PartFunc of the carrier of S,the carrier of T;
assume f is_differentiable_in g/.x0; then
consider N2 being Neighbourhood of g/.x0 such that
A4: N2 c= dom f and
A5: ex R2 be RestFunc of S,T
st R2/.(0.S) = 0.T
& R2 is_continuous_in 0.S
& for y be Point of S st y in N2
holds f/.y-f/.(g/.x0) = diff(f,g/.x0).(y-g/.x0) + R2/.(y-g/.x0)
by NDIFF_1:47;
consider R2 be RestFunc of S,T such that
A6: R2/.0.S=0.T and
A7: for y be Point of S st y in N2
holds f/.y-f/.(g/.x0) = diff(f,g/.x0).(y-g/.x0) + R2/.(y-g/.x0) by A5;
reconsider L2 = diff(f,g/.x0) as Lipschitzian LinearOperator of S,T
by LOPBAN_1:def 9;
consider L1 be LinearFunc of S,R1 be RestFunc of S such that
A8: diff(g,x0) = L1/.1
& for x be Real st x in N1
holds g/.x-g/.x0 = L1/.(x-x0) + R1/.(x-x0) by A3;
consider r be Point of S such that
A9: for p be Real holds L1/.p = p*r by NDIFF_3:def 2;
reconsider p0=0 as Element of REAL by XREAL_0:def 1;
g/.x0-g/.x0 = L1/.(x0-x0) + R1/.(x0-x0) by A8,RCOMP_1:16; then
0.S = L1/.0 + R1/.0 by RLVECT_1:15; then
0.S = p0*r + R1/.0 by A9; then
0.S = 0.S + R1/.0 by RLVECT_1:10; then
R1/.0 = 0.S by RLVECT_1:4; then
reconsider R0=L2*R1+R2*(L1+R1) as RestFunc of T by A6,Th5;
A10: dom(L2*L1) = REAL by FUNCT_2:def 1;
reconsider q = L2.r as Point of T;
now let pp be Real;
reconsider p=pp as Element of REAL by XREAL_0:def 1;
L2.(L1/.p) = L2.(p*r) by A9; then
L2.(L1/.p) = p*q by LOPBAN_1:def 5;
then (L2*L1).p = p*q by A10,FUNCT_1:12;
hence (L2*L1)/.pp = pp*q by A10,PARTFUN1:def 6;
end; then
reconsider L0=L2*L1 as LinearFunc of T by NDIFF_3:def 2;
g is_continuous_in x0 by A1,NDIFF_3:22; then
consider N3 be Neighbourhood of x0 such that
A11: g.:N3 c= N2 by NFCONT_3:10;
consider N be Neighbourhood of x0 such that
A12: N c= N1 and
A13: N c= N3 by RCOMP_1:17;
A14: dom L2 = the carrier of S by FUNCT_2:def 1; then
A15: rng R1 c= dom L2;
A16: rng L1 c= dom L2 by A14;
now let x be object;
assume
A17: x in N; then
reconsider x9 = x as Real;
A18: x in N1 by A12,A17; then
g.x9 in g.:N3 by A2,A13,A17,FUNCT_1:def 6; then
g.x9 in N2 by A11;
hence x in dom(f*g) by A2,A4,A18,FUNCT_1:11;
end; then
A19: N c= dom(f*g);
A20: now let x be Real such that
A21: x in N;
A22: g/.x-g/.x0 = L1/.(x-x0) + R1/.(x-x0) by A8,A12,A21;
x in N1 by A12,A21; then
g.x in g.:N3 by A2,A13,A21,FUNCT_1:def 6; then
g.x in N2 by A11; then
A24: g/.x in N2 by A2,A12,A21,PARTFUN1:def 6;
A25: x0 in N by RCOMP_1:16;
A26: R1 is total by NDIFF_3:def 1; then
A27: dom R1 = REAL by PARTFUN1:def 2;
A28: dom(L2*R1) = REAL by A26,PARTFUN1:def 2;
L1+R1 is total by A26,VFUNCT_1:32; then
A29: dom(L1+R1)=REAL by PARTFUN1:def 2;
R2 is total by NDIFF_1:def 5; then
dom R2 = the carrier of S by PARTFUN1:def 2; then
A30: rng (L1+R1) c= dom R2; then
dom (R2*(L1+R1)) = dom(L1+R1) by RELAT_1:27; then
A31: dom (L2*R1+R2*(L1+R1)) = REAL /\ REAL by A28,A29,VFUNCT_1:def 1;
reconsider dxx0 = x - x0 as Element of REAL by XREAL_0:def 1;
L2.(R1/.(x-x0)) = L2/.(R1/.(x-x0)); then
A32: L2.(R1/.(x-x0)) =(L2*R1)/.(dxx0) by A27,A15,PARTFUN2:5;
A33: R2/.(L1/.(x-x0)+R1/.(x-x0))
=R2/.((L1+R1)/.(dxx0)) by A29,VFUNCT_1:def 1
.=(R2*(L1+R1))/.(dxx0) by A29,A30,PARTFUN2:5;
A34: dom L1 = REAL by FUNCT_2:def 1;
A35: (L2*L1)/.(x-x0) = L2/.(L1/.(dxx0)) by PARTFUN2:5,A34,A16;
thus (f*g)/.x-(f*g)/.x0 =f/.(g/.x) -(f*g)/.x0 by A19,A21,PARTFUN2:3
.=f/.(g/.x) -f/.(g/.x0) by A19,A25,PARTFUN2:3
.=diff(f,g/.x0).(g/.x-g/.x0) + R2/.(g/.x-g/.x0) by A7,A24
.=L2.(L1/.(x-x0)) + L2.(R1/.(x-x0)) + (R2*(L1+R1))/.(x-x0) by A22,A33,
VECTSP_1:def 20
.=L2.(L1/.(x-x0)) + ((L2*R1)/.(x-x0) + (R2*(L1+R1))/.(x-x0)) by A32,
RLVECT_1:def 3
.=L0/.(x-x0) + R0/.(x-x0) by A35,A31,VFUNCT_1:def 1;
end;
hence A36: f*g is_differentiable_in x0 by A19,NDIFF_3:def 3;
dom L1 = REAL by FUNCT_2:def 1;
then (L2*L1)/.1 = L2/.(L1/.jj) by PARTFUN2:5,A16
.= diff(f,g/.x0).diff(g,x0) by A8;
hence thesis by A36,A19,A20,NDIFF_3:def 4;
end;
theorem Th7:
for S be RealNormSpace,
xseq be FinSequence of S,
yseq be FinSequence of REAL st
len xseq = len yseq &
( for i be Element of NAT st i in dom xseq holds
yseq.i = ||. xseq/.i .|| )
holds ||.Sum xseq.|| <= Sum yseq
proof
let S be RealNormSpace,
xseq be FinSequence of S,
yseq be FinSequence of REAL;
assume that
A1: len xseq = len yseq and
A2: for i be Element of NAT st
i in dom xseq holds yseq.i = ||. xseq/.i .||;
defpred P[Nat] means
for xseq be FinSequence of S, yseq be FinSequence of REAL st
$1=len xseq & len xseq = len yseq &
( for i be Element of NAT st i in dom xseq holds
yseq.i = ||. xseq/.i .|| )
holds ||.Sum xseq.|| <= Sum yseq;
A3:P[0]
proof
let xseq be FinSequence of S, yseq be FinSequence of REAL;
assume
A4: 0 = len xseq & len xseq = len yseq
& ( for i be Element of NAT st i in dom xseq holds
yseq.i = ||. xseq/.i .|| );
consider Sx be sequence of the carrier of S such that
A5: Sum xseq = Sx.(len xseq)
& Sx.0 = 0.S
& for j be Nat, v be Element of S st
j < len xseq & v = xseq.(j+1) holds Sx.(j+1) = Sx.j + v
by RLVECT_1:def 12;
yseq = {} by A4;
hence thesis by A4,A5,RVSUM_1:72;
end;
A6:now let i be Nat;
assume A7: P[i];
now let xseq be FinSequence of S, yseq be FinSequence of REAL;
set xseq0=xseq|i, yseq0=yseq|i;
assume
A8: i+1=len xseq & len xseq = len yseq &
( for i be Element of NAT st i in dom xseq holds
yseq.i = ||. xseq/.i .|| );
A9: for k be Element of NAT st k in dom xseq0 holds yseq0.k = ||. xseq0/.k .||
proof
let k be Element of NAT;
assume
A10: k in dom xseq0; then
A11: k in Seg i & k in dom xseq by RELAT_1:57; then
A12: yseq.k = ||. xseq/.k .|| by A8;
xseq/.k = xseq.k by A11,PARTFUN1:def 6; then
xseq/.k = xseq0.k by A11,FUNCT_1:49; then
xseq/.k = xseq0/.k by A10,PARTFUN1:def 6;
hence thesis by A11,A12,FUNCT_1:49;
end;
A13: dom xseq = Seg(i+1) by A8,FINSEQ_1:def 3; then
A14: yseq.(i+1) = ||. xseq/.(i+1) .|| by A8,FINSEQ_1:4;
A15: 1 <= i + 1 by NAT_1:11;
yseq = (yseq|i)^<*yseq/.(i+1) *> by A8,FINSEQ_5:21; then
yseq = yseq0 ^<*(yseq.(i+1))*> by A8,A15,FINSEQ_4:15; then
A16: Sum yseq = Sum yseq0 + yseq.(i+1) by RVSUM_1:74;
reconsider v = xseq.(len xseq) as Element of S
by A13,A8,FINSEQ_1:4,PARTFUN1:4;
A18: v = xseq/.(i+1) by A8,A13,FINSEQ_1:4,PARTFUN1:def 6;
A19: i=len xseq0 by A8,FINSEQ_1:59,NAT_1:11; then
xseq0 = xseq| (dom xseq0) by FINSEQ_1:def 3; then
A20: Sum xseq = Sum xseq0 + v by A8,A19,RLVECT_1:38;
A21: ||. Sum xseq0 + v.|| <= ||.Sum xseq0 .|| + ||. v .|| by NORMSP_1:def 1;
len xseq0 = len yseq0 by A8,A19,FINSEQ_1:59,NAT_1:11; then
||. Sum xseq0 .|| + ||.v.|| <= Sum yseq0 + yseq.(i+1)
by A7,A9,A19,A14,A18,XREAL_1:6;
hence ||. Sum xseq .|| <= Sum yseq by A16,A20,A21,XXREAL_0:2;
end;
hence P[i+1];
end;
for i be Nat holds P[i] from NAT_1:sch 2(A3,A6);
hence thesis by A1,A2;
end;
theorem Th8:
for S be RealNormSpace, x be Point of S, N1,N2 be Neighbourhood of x holds
N1/\ N2 is Neighbourhood of x
proof
let S be RealNormSpace, x be Point of S,
N1,N2 be Neighbourhood of x;
consider N be Neighbourhood of x such that
A1: N c= N1 & N c= N2 by NDIFF_1:1;
A2:N c= N1/\ N2 by A1,XBOOLE_1:19;
consider g be Real such that
A3: 0 < g and
A4: {y where y is Point of S: ||.y-x .|| < g} c= N by NFCONT_1:def 1;
{y where y is Point of S: ||.y-x .|| < g} c= N1 /\ N2 by A2,A4;
hence thesis by A3,NFCONT_1:def 1;
end;
theorem Th9:
for X be non-empty FinSequence,
x be set st x in product X holds x is FinSequence
proof
let X be non-empty FinSequence, x be set;
assume x in product X; then
consider g be Function such that
A1: x = g & dom g = dom X
& for i be object st i in dom X holds g.i in X.i by CARD_3:def 5;
dom g = Seg len X by A1,FINSEQ_1:def 3;
hence x is FinSequence by A1,FINSEQ_1:def 2;
end;
registration
let G be RealNormSpace-Sequence;
cluster product G -> constituted-FinSeqs;
coherence
proof
let a be Element of product G;
product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop G:],
productnorm G #) by PRVECT_2:6;
hence thesis by Th9;
end;
end;
Lm1: now let G be RealLinearSpace-Sequence;
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;
end;
definition
let G be RealLinearSpace-Sequence;
let z be Element of product carr G;
let j be Element of dom G;
redefine func z.j -> Element of G.j; :: redefines . (FUNCT_1, definition)
correctness
proof
reconsider zz=z as FinSequence by Th9;
dom carr G = dom G by Lm1; then
zz.j in carr G.j by CARD_3:9;
hence thesis by PRVECT_1:def 11;
end;
end;
theorem Th10:
the carrier of product G = product carr G
proof
product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop G:],
productnorm G #) by PRVECT_2:6;
hence thesis;
end;
theorem Th11:
for i be Element of dom G, r be set, x be Function
st r in the carrier of (G.i) & x in product carr G
holds x +* (i,r) in the carrier of product G
proof
let i be Element of dom G, r be set, x be Function;
assume A1: r in the carrier of (G.i) & x in product carr G; then
consider g be Function such that
A2: x = g & dom g = dom carr G
& for i be object st i in dom carr G holds g.i in (carr G).i
by CARD_3:def 5;
set h = x +* (i,r);
set s = i .--> r;
s = {i} --> r by FUNCOP_1:def 9; then
A3:dom s = {i};
A4:dom h = dom carr G by A2,FUNCT_7:30;
for j be object st j in dom carr G holds h.j in (carr G).j
proof
let j be object;
assume A5: j in dom carr G;
per cases;
suppose not j in dom s; then
j <> i by A3,TARSKI:def 1; then
h.j = x.j by FUNCT_7:32;
hence h.j in (carr G).j by A2,A5;
end;
suppose j in dom s; then
A6: j = i by TARSKI:def 1; then
h.j = r by A5,A2,FUNCT_7:31;
hence h.j in (carr G).j by A1,A6,PRVECT_1:def 11;
end;
end; then
x +* (i,r) in product carr G by A4,CARD_3:def 5;
hence thesis by Th10;
end;
definition
let G be RealNormSpace-Sequence;
attr G is non-trivial means :Def1:
for j be Element of dom G holds G.j is non trivial;
end;
registration
cluster non-trivial for RealNormSpace-Sequence;
correctness
proof
take G = <* the non trivial RealNormSpace *>;
let j be Element of dom G;
dom G = Seg 1 by FINSEQ_1:38; then
j = 1 by FINSEQ_1:2,TARSKI:def 1;
hence thesis;
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 by Def1;
end;
registration
let G be non-trivial RealNormSpace-Sequence;
cluster product G -> non trivial;
correctness
proof
A1:the carrier of product G = product carr G by Th10;
not
for x,y be set st x in product carr G & y in product carr G holds x = y
proof
assume
A2: for x,y be set st x in product carr G & y in product carr G holds x = y;
consider z be object such that
A3: z in product carr G by XBOOLE_0:def 1;
consider g be Function such that
A4: z = g & dom g = dom carr G
& for i be object st i in dom carr G holds g.i in (carr G).i
by A3,CARD_3:def 5;
set i = the Element of dom G;
now let r,s be object;
assume A5: r in the carrier of (G.i) & s in the carrier of (G.i);
g +* (i,r) in the carrier of product G &
g +* (i,s) in the carrier of product G by Th11,A3,A4,A5; then
g +* (i,r) in product carr G &
g +* (i,s) in product carr G by Th10; then
A6: g +* (i,r) = g +* (i,s) by A2;
i in dom G; then
A7: i in dom g by A4,Lm1; then
(g +* (i,r)).i = r by FUNCT_7:31;
hence r=s by A6,A7,FUNCT_7:31;
end;
hence contradiction by ZFMISC_1:def 10;
end;
hence thesis by A1;
end;
end;
theorem Th12:
for G be RealNormSpace-Sequence, p,q be Point of product G,
r0,p0,q0 be Element of product carr G st p=p0 & q=q0
holds p+q = r0
iff for i be Element of dom G holds r0.i = p0.i + q0.i
proof
let G be RealNormSpace-Sequence, p,q be Point of product G,
r0,p0,q0 be Element of product carr G;
assume A1: p=p0 & q=q0;
len carr G = len G by PRVECT_1:def 11; then
A2:dom carr G = Seg len G by FINSEQ_1:def 3
.= dom G by FINSEQ_1:def 3;
A3: product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop G:],
productnorm G #) by PRVECT_2:6;
hereby assume A4: p+q = r0;
hereby let i be Element of dom G;
reconsider i0=i as Element of dom carr G by A2;
(addop G).i0 = the addF of (G.i0) by PRVECT_1:def 12;
hence r0.i = p0.i + q0.i by A1,A4,A3,PRVECT_1:def 8;
end;
end;
assume A5: for i be Element of dom G holds r0.i = p0.i + q0.i;
reconsider pq=p+q as Element of product carr G by Th10;
A6:ex g be Function st
pq = g & dom g = dom carr G
& for i be object st i in dom carr G holds g.i in (carr G).i
by CARD_3:def 5;
A7:ex g be Function st
r0 = g & dom g = dom carr G
& for i be object st i in dom carr G holds g.i in (carr G).i
by CARD_3:def 5;
now let i0 be object;
assume A8: i0 in dom pq; then
reconsider i1=i0 as Element of dom G by A2,A6;
reconsider i =i0 as Element of dom carr G by A8,A6;
(addop G).i = the addF of (G.i) by PRVECT_1:def 12; then
pq.i0 = p0.i1 + q0.i1 by A1,A3,PRVECT_1:def 8;
hence pq.i0 = r0.i0 by A5;
end;
hence p+q = r0 by A6,A7,FUNCT_1:2;
end;
theorem Th13:
for G be RealNormSpace-Sequence, p be Point of product G,
r be Real, r0,p0 be Element of product carr G
st p=p0
holds r*p = r0
iff for i be Element of dom G holds r0.i = r*(p0.i)
proof
let G be RealNormSpace-Sequence, p be Point of product G,
r be Real, r0,p0 be Element of product carr G;
assume A1: p=p0;
hereby assume A2: r*p = r0;
hereby let i be Element of dom G;
reconsider i0=i as Element of dom carr G by Lm1;
A3: (multop G).i0 = the Mult of (G.i0) by PRVECT_2:def 8;
reconsider rr=r as Element of REAL by XREAL_0:def 1;
product G = NORMSTR(# product carr G,zeros G,[:addop G:],
[:multop G:], productnorm G #) by PRVECT_2:6;
hence r0.i = rr*(p0.i) by A1,A2,A3,PRVECT_2:def 2
.= r*(p0.i);
end;
end;
assume A4: for i be Element of dom G holds r0.i = r* (p0.i);
reconsider rp = r*p as Element of product carr G by Th10;
A5:ex g be Function st
rp = g & dom g = dom carr G
& for i be object st i in dom carr G holds g.i in (carr G).i
by CARD_3:def 5;
A6:ex g be Function st
r0 = g & dom g = dom carr G
& for i be object st i in dom carr G holds g.i in (carr G).i
by CARD_3:def 5;
now let i0 be object;
assume A7: i0 in dom rp; then
reconsider i1=i0 as Element of dom G by Lm1,A5;
reconsider i=i0 as Element of dom carr G by A7,A5;
A8: product G = NORMSTR(# product carr G,zeros G,[:addop G:],
[:multop G:], productnorm G #) by PRVECT_2:6;
reconsider r as Element of REAL by XREAL_0:def 1;
(multop G).i = the Mult of (G.i) by PRVECT_2:def 8; then
rp.i0 = r*(p0.i1) by A1,A8,PRVECT_2:def 2;
hence rp.i0 = r0.i0 by A4;
end;
hence r*p = r0 by A5,A6,FUNCT_1:2;
end;
theorem Th14:
for G be RealNormSpace-Sequence, p0 be Element of product carr G
holds 0.(product G)=p0
iff for i be Element of dom G holds p0.i = 0.(G.i)
proof
let G be RealNormSpace-Sequence,
p0 be Element of product carr G;
A1:dom carr G = dom G by Lm1;
A2:product G = NORMSTR(# product carr G,zeros G,[:addop G:]
,[:multop G:], productnorm G #) by PRVECT_2:6;
hence 0.(product G) = p0 implies
for i be Element of dom G holds p0.i = 0.(G.i) by A1,PRVECT_1:def 14;
assume A3:for i be Element of dom G holds p0.i = 0.(G.i);
now let i0 be Element of dom carr G;
reconsider i=i0 as Element of dom G by Lm1;
p0.i = 0.(G.i) by A3;
hence p0.i0 = 0.(G.i0);
end;
hence 0.(product G)=p0 by A2,PRVECT_1:def 14;
end;
theorem Th15:
for G be RealNormSpace-Sequence, p,q be Point of product G,
r0,p0,q0 be Element of product carr G
st p=p0 & q=q0
holds p-q = r0
iff for i be Element of dom G holds r0.i = p0.i - q0.i
proof
let G be RealNormSpace-Sequence, p,q be Point of product G,
r0,p0,q0 be Element of product carr G;
assume A1: p=p0 & q=q0;
reconsider qq0=(-1)*q as Element of product carr G by Th10;
A2:p-q = p+(-1)*q by RLVECT_1:16;
hereby assume A3: p-q = r0;
thus for i be Element of dom G holds r0.i = p0.i - q0.i
proof
let i be Element of dom G;
A4: r0.i = p0.i + qq0.i by Th12,A3,A1,A2;
qq0.i = (-1)*(q0.i) by A1,Th13;
hence thesis by A4,RLVECT_1:16;
end;
end;
assume A5: for i be Element of dom G holds r0.i = p0.i - q0.i;
now let i be Element of dom G;
A6: qq0.i = (-1)*(q0.i) by A1,Th13;
r0.i = p0.i - q0.i by A5;
hence r0.i = p0.i + qq0.i by A6,RLVECT_1:16;
end;
hence p-q = r0 by A2,Th12,A1;
end;
begin :: Mean value theorem for vector-valued functions
Lm2: now let S be RealLinearSpace; let p,q be Point of S;
let z1 be Real;
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;
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
[.p,q.] \ {p,q};
correctness;
end;
theorem LMOPN:
for S be RealLinearSpace, p,q be Point of S st p <> q
holds ].p,q.[ = { p+t*(q-p) where t is Real : 0 < t & t < 1}
proof
let S be RealLinearSpace, p,q be Point of S;
assume AS1: p <> q;
set A = { p+t*(q-p) where t is Real : 0 < t & t < 1};
for x be object holds (x in ].p,q.[ iff x in A)
proof
let x be object;
hereby assume x in ].p,q.[; then
P1: x in [.p,q.] & not x in {p,q} by XBOOLE_0:def 5; then
x in {(1-r)*p + r*q where r is Real : 0 <= r & r <= 1}
by RLTOPSP1:def 2; then
consider t be Real such that
P2: x= (1-t)*p+t*q & 0 <= t & t <= 1;
P3: x= p+t*(q-p) by P2,Lm2;
P4: 0 <> t
proof
assume t = 0; then
x = p + 0.S by P3,RLVECT_1:10
.= p by RLVECT_1:4;
hence contradiction by P1,TARSKI:def 2;
end;
1 <> t
proof
assume t = 1; then
x = p + (q-p) by P3,RLVECT_1:def 8
.= q- (p - p) by RLVECT_1:29
.= q - 0.S by RLVECT_1:15
.= q by RLVECT_1:13;
hence contradiction by P1,TARSKI:def 2;
end; then
0 < t & t < 1 by P2,P4,XXREAL_0:1;
hence x in A by P3;
end;
assume x in A; then
consider t be Real such that
P4: x= p+t*(q-p) & 0 < t & t < 1;
x= (1-t)*p+t*q by Lm2,P4; then
x in {(1-r)*p + r*q where r is Real : 0 <= r & r <= 1} by P4; then
P5: x in [.p,q.] by RLTOPSP1:def 2;
P6: x <> p
proof
assume x = p; then
P7: 0.S = t*(q-p) + p - p by P4,RLVECT_1:15
.= t*(q-p) + (p-p) by RLVECT_1:28
.= t*(q-p) + 0.S by RLVECT_1:15
.= t*(q-p) by RLVECT_1:4;
q-p <> 0.S by AS1,RLVECT_1:21;
hence contradiction by P4,P7,RLVECT_1:11;
end;
x <> q
proof
assume x = q; then
q-p = t*(q-p) + (p-p) by P4,RLVECT_1:28
.=t*(q-p) + 0.S by RLVECT_1:15
.=t*(q-p) by RLVECT_1:4; then
1*(q-p) = t*(q-p) by RLVECT_1:def 8; then
1*(q-p) - t*(q-p) =0.S by RLVECT_1:15; then
P7: (1-t)* (q-p) = 0.S by RLVECT_1:35;
q-p <> 0.S by AS1,RLVECT_1:21; then
1-t = 0 by RLVECT_1:11,P7;
hence contradiction by P4;
end; then
not x in {p,q} by P6,TARSKI:def 2;
hence x in ]. p,q .[ by P5,XBOOLE_0:def 5;
end;
hence thesis by TARSKI:2;
end;
Lm3:
for x be Real st
for e be Real st 0 < e holds x <= e holds x <= 0
proof
let x be Real;
assume A1: for e be Real st 0 < e holds x <= e;
assume A2: not x <= 0; then
x <= x/2 by A1; then
x - (x/2) <= (x/2) - (x/2) by XREAL_1:9;
hence contradiction by A2;
end;
theorem Th17:
for T be RealNormSpace, R be PartFunc of REAL,T
st R is total holds
R is RestFunc-like
iff for r be Real st r > 0
ex d be Real st d > 0 & for z be Real
st z <> 0 & |.z.| < d holds ( ||. R/.z .||/ |.z.| ) < r
proof
let T be RealNormSpace, R be PartFunc of REAL,T;
assume A1: R is total;
A2:now assume A3: R is RestFunc-like;
assume not
(for r be Real st r > 0
ex d be Real st d > 0 & for z be Real
st z <> 0 & |.z.| < d holds ( ||. R/.z .||/ |.z.|) < r ); then
consider r be Real such that
A4: r > 0 and
A5: for d be Real st d > 0 holds
ex z be Real st z <> 0 & |.z.| < d
& not ( ||. R/.z .||/ |.z.| ) < r;
defpred P[Nat,Element of REAL]
means $2 <> 0 & |.$2.| < (1/($1+1))
& not ( (||. R/.$2 .||/|.$2.| ) < r );
A6: now let n be Element of NAT;
consider z be Real such that
A7: z <> 0 & |.z.| < 1/(n + 1)
& not ( ||. R/.z .||/ |.z.| ) < r by A5;
reconsider z as Element of REAL by XREAL_0:def 1;
take z;
thus P[n,z] by A7;
end;
consider s be Real_Sequence such that
A8: for n being Element of NAT holds P[n,s.n] from FUNCT_2:sch 3(A6);
A9: for n being Nat holds P[n,s.n]
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A8;
end;
A10: now let p be Real;
assume A11: 0<p;
consider n be Nat such that
A12: p"<n by SEQ_4:3;
p" + (0 qua Real) < n + 1 by A12,XREAL_1:8; then
A13: 1/(n+1) < 1/p" by A11,XREAL_1:76;
take n;
let m be Nat;
assume n<=m; then
n + 1 <= m + 1 by XREAL_1:6; then
1/(m+1) <= 1/(n+1) by XREAL_1:118; then
|.s.m-0 .| < 1/(n+1) by A9,XXREAL_0:2;
hence |.s.m-0 .| <p by A13,XXREAL_0:2;
end; then
s is convergent by SEQ_2:def 6; then
lim s = 0 by A10,SEQ_2:def 7; then
reconsider s as 0-convergent non-zero Real_Sequence
by A9,A10,SEQ_1:5,SEQ_2:def 6,FDIFF_1:def 1;
(s")(#)(R/*s) is convergent & lim ((s")(#)(R/*s)) = 0.T
by A3,NDIFF_3:def 1; then
consider n be Nat such that
A16: for m be Nat st n <=m
holds ||. ((s")(#)(R/*s)).m - 0.T .|| < r by A4,NORMSP_1:def 7;
A17: n in NAT by ORDINAL1:def 12;
A19: ||.(s.n)"*(R/.(s.n)).||
= |.(s.n)".| * ||. R/.(s.n) .|| by NORMSP_1:def 1
.= ||. R/.(s.n) .||/|.s.n.| by COMPLEX1:66;
dom R = REAL by A1,PARTFUN1:def 2; then
A20:rng s c= dom R;
||. ((s")(#)(R/*s)).n- 0.T.||
= ||. ((s")(#)(R/*s)).n .|| by RLVECT_1:13
.= ||. (s".n)*((R/*s).n) .|| by NDIFF_1:def 2
.= ||. (s.n)"*((R/*s).n) .|| by VALUED_1:10
.= ||. (s.n)"*(R/.(s.n)) .|| by A20,FUNCT_2:109,A17;
hence
for r be Real st r > 0
ex d be Real st d > 0 & for z be Real st
z <> 0 & |.z.| < d holds ( ||. R/.z .||/|.z.| ) < r by A9,A16,A19;
end;
now assume
A21: for r be Real st r > 0
ex d be Real st d > 0 & for z be Real
st z <> 0 & |.z.| < d holds ( ||. R/.z .||/|.z.|) < r;
now let s be 0-convergent non-zero Real_Sequence;
A22: s is convergent & lim s = 0;
A23: now let r be Real;
assume r > 0; then
consider d be Real such that
A24: d > 0 and
A25: for z be Real st z <> 0 & |.z.| < d holds
( ||. R/.z .||/|.z.|) < r by A21;
consider n be Nat such that
A26: for m be Nat st n <=m holds |.s.m-0 .| < d
by A22,A24,SEQ_2:def 7;
take n;
thus for m be Nat st n <=m
holds ||. ((s")(#)(R/*s)).m- 0.T.|| < r
proof
dom R = REAL by A1,PARTFUN1:def 2; then
A27: rng s c= dom R;
let m be Nat;
A28: m in NAT by ORDINAL1:def 12;
assume n <=m; then
A29: |.s.m-0 .| < d by A26;
||.(R/.(s.m)).|| / |.s.m.|
= |.(s.m)".| * ||.(R/.(s.m)).|| by COMPLEX1:66
.= ||.(s.m)"*(R/.(s.m)).|| by NORMSP_1:def 1
.= ||.(s.m)"*((R/*s).m).|| by A27,FUNCT_2:109,A28
.= ||.(s".m)*((R/*s).m).|| by VALUED_1:10
.= ||. ((s")(#)(R/*s)).m .|| by NDIFF_1:def 2
.= ||. ((s")(#)(R/*s)).m- 0.T.|| by RLVECT_1:13;
hence thesis by A25,A29,SEQ_1:5;
end;
end;
hence (s")(#)(R/*s) is convergent by NORMSP_1:def 6;
hence lim ((s")(#)(R/*s)) = 0.T by A23,NORMSP_1:def 7;
end;
hence R is RestFunc-like by A1,NDIFF_3:def 1;
end;
hence thesis by A2;
end;
theorem Th18:
for R be Function of REAL,REAL holds R is RestFunc-like iff
for r be Real st r > 0
ex d be Real st d > 0 & for z be Real
st z <> 0 & |.z.| < d holds (|.R.z.|/ |.z.|) < r
proof
let R be Function of REAL,REAL;
A1:now assume
A2: R is RestFunc-like;
assume not
(for r be Real st r > 0
ex d be Real st d > 0 & for z be Real
st z <> 0 & |.z.| < d holds ( |.R.z.|/ |.z.| ) < r); then
consider r be Real such that
A3: r > 0 and
A4: for d be Real st d > 0 holds
ex z be Real st z <> 0 & |.z.| < d
& not ( |.R.z.|/|.z.|) < r;
defpred P[Nat,Element of REAL]
means $2 <> 0 & |.$2.| < 1/($1+1) & not |.R.$2.|/|.$2.| < r;
A5: now let n be Element of NAT;
consider z be Real such that
A6: z <> 0 & |.z.| < 1/(n + 1)
& not ( |.R.z.|/|.z.|) < r by A4;
reconsider z as Element of REAL by XREAL_0:def 1;
take z;
thus P[n,z] by A6;
end;
consider s be Real_Sequence such that
A7: for n being Element of NAT holds P[n,s.n] from FUNCT_2:sch 3(A5);
A8: for n being Nat holds P[n,s.n]
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A7;
end;
A9: now let p be Real;
assume
A10: 0<p;
consider n be Nat such that
A11: p"<n by SEQ_4:3;
p" + (0 qua Real) < n + 1 by A11,XREAL_1:8; then
A12: 1/(n+1) < 1/p" by A10,XREAL_1:76;
take n;
let m be Nat;
assume n<=m; then
n + 1 <= m + 1 by XREAL_1:6; then
1/(m+1) <= 1/(n+1) by XREAL_1:118; then
|.s.m-0 .| < 1/(n+1) by A8,XXREAL_0:2;
hence |.s.m-0 .| < p by A12,XXREAL_0:2;
end; then
s is convergent by SEQ_2:def 6; then
lim s = 0 by A9,SEQ_2:def 7; then
reconsider s as 0-convergent non-zero Real_Sequence
by A9,A8,SEQ_1:5,SEQ_2:def 6,FDIFF_1:def 1;
(s")(#)(R/*s) is convergent & lim ((s")(#)(R/*s)) = 0
by A2,FDIFF_1:def 2; then
consider n be Nat such that
A15: for m be Nat st n <=m holds |.((s")(#)(R/*s)).m- 0 .| < r
by A3,SEQ_2:def 7;
A16: n in NAT by ORDINAL1:def 12;
A18: |.(s.n)"*(R.(s.n)).| = |.(s.n)".| * |.R.(s.n).| by COMPLEX1:65
.= |.R.(s.n).|/|.s.n.| by COMPLEX1:66;
|. ((s")(#)(R/*s)).n- 0 .|
= |. (s".n)*((R/*s).n) .| by SEQ_1:8
.= |. (s.n)"*((R/*s).n) .| by VALUED_1:10
.= |. (s.n)"*(R.(s.n)) .| by FUNCT_2:115,A16;
hence
for r be Real st r > 0
ex d be Real st d > 0 & for z be Real st
z <> 0 & |.z.| < d holds ( |.R.z.|/|.z.| ) < r by A8,A15,A18;
end;
now assume
A19: for r be Real st r > 0
ex d be Real st d > 0 & for z be Real
st z <> 0 & |.z.| < d holds ( |.R.z.|/|.z.| ) < r;
now let s be 0-convergent non-zero Real_Sequence;
A20: s is convergent & lim s = 0;
A21: now let r be Real;
assume A22: r > 0;
consider d be Real such that
A23: d > 0 and
A24: for z be Real st z <> 0 & |.z.| < d
holds |.R.z.|/|.z.| < r by A22,A19;
consider n be Nat such that
A25: for m be Nat st n <= m holds |.s.m-0 .| < d
by A20,A23,SEQ_2:def 7;
take n;
hereby let m be Nat;
A26: m in NAT by ORDINAL1:def 12;
assume n <=m; then
A27: |.s.m-0 .| < d by A25;
|.R.(s.m).| / |.s.m.|
= |.(s.m)".| * |.R.(s.m).| by COMPLEX1:66
.= |.(s.m)" * R.(s.m).| by COMPLEX1:65
.= |.(s.m)" * (R/*s).m.| by FUNCT_2:115,A26
.= |.s".m * (R/*s).m .| by VALUED_1:10
.= |.(s"(#)(R/*s)).m - 0 .| by SEQ_1:8;
hence |. ((s")(#)(R/*s)).m- 0 .| < r by A24,A27,SEQ_1:5;
end;
end;
hence (s")(#)(R/*s) is convergent by SEQ_2:def 6;
hence lim((s")(#)(R/*s)) = 0 by A21,SEQ_2:def 7;
end;
hence R is RestFunc-like by FDIFF_1:def 2;
end;
hence thesis by A1;
end;
reconsider jj=1 as Real;
Lm4:
for T be RealNormSpace,
f be PartFunc of REAL,T,
g be 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 be Real st x in ].0,1.[ holds
||. diff(f,x) .|| <= diff(g,x))
holds
||. f/.1 -f/.0 .|| <= g/.1 - g/.0
proof
let T be RealNormSpace,
f be PartFunc of REAL,T,
g be PartFunc of REAL,REAL;
assume A1: 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 be Real st x in ].0,1.[ holds
||. diff(f,x) .|| <= diff(g,x));
now let e be Real;
assume A2: 0 < e;
set e1=e/2;
set B = {x where x is Real : x in [.0,1.]
& ||. f/.x -f/.0 .|| - (g.x - g.0) - e1*x - e1 <= 0};
now let z be object;
assume z in B; then
ex x be Real st z=x & x in [.0,1.]
& ||. f/.x -f/.0 .|| - (g.x - g.0) - e1*x - e1 <= 0;
hence z in REAL;
end; then
reconsider B as Subset of REAL by TARSKI:def 3;
now let r be Real;
assume r in B; then
ex x be Real st r = x & x in [.0,1.]
& ||. f/.x -f/.0 .|| - (g.x - g.0) - e1*x - e1 <= 0; then
A3: ex t be Real st r = t & 0<=t & t<=1; then
|.r.| = r by ABSVALUE:def 1;
hence |.r.| < 2 by A3,XXREAL_0:2;
end; then
A4: B is real-bounded by SEQ_4:4;
set s = upper_bound B;
A5: ex d be Real st 0 < d & d in B
proof
0 in [.0,1.]; then
consider d1 be Real such that
A6: 0 < d1 & for x1 be Real st x1 in [.0,1.] & |.x1-0 .| < d1
holds ||. f/.x1 - f/.0 .|| < e1 by A2,A1,NFCONT_3:17;
set d2=d1/2;
A7: d2 < d1 by A6,XREAL_1:216;
take d = min(d2,1);
thus A8: 0 < d by A6,XXREAL_0:21;
A9: d <= 1 by XXREAL_0:17; then
A10: d in [.0,1.] by A8;
A11: d <= d2 by XXREAL_0:17;
|.d-0 .| = d by A8,ABSVALUE:def 1; then
|.d-0 .| < d1 by A11,A7,XXREAL_0:2; then
A12: ||. f/.d - f/.0 .|| < e1 by A6,A10;
A13: [.0,d.] c= dom g by A1,A9,XXREAL_1:34;
A14: g| [.0,d.] is continuous by A1,A9,FCONT_1:16,XXREAL_1:34;
A15: ].0,d.[ c=].0,1.[ by A9,XXREAL_1:46; then
consider x0 be Real such that
A16: x0 in ].0,d.[
& diff(g,x0) =(g.d-g.0)/(d-0) by A1,A8,A13,A14,FDIFF_1:26,ROLLE:3;
||. diff(f,x0) .|| <= diff(g,x0) by A1,A16,A15; then
0 <= g.d-g.0 by A8,A16; then
(0 qua Real) + ||. f/.d - f/.0 .|| <= (g.d - g.0) + e1
by A12,XREAL_1:7; then
(0 qua Real) + ||. f/.d - f/.0 .|| <= (g.d - g.0) + e1+ e1*d
by A8,A2,XREAL_1:7; then
||. f/.d - f/.0 .|| -( (g.d - g.0) + e1+ e1*d ) <= 0 by XREAL_1:47; then
||. f/.d -f/.0 .|| - (g.d - g.0) - e1*d - e1 <= 0;
hence d in B by A10;
end; then
A17: 0 < s by A4,SEQ_4:def 1;
now let r be Real;
assume r in B; then
ex x be Real st r = x & x in [.0,1.]
& ||. f/.x -f/.0 .|| - (g.x - g.0 ) - e1*x - e1 <= 0; then
ex t be Real st r=t & 0<=t & t<=1;
hence r<=1;
end; then
A18: s <= 1 by A5,SEQ_4:45;
defpred P[Nat,Element of REAL]
means $2 in B & |.s-$2.| <= 1/($1+1);
A19:now let x be Element of NAT;
reconsider t = 1/(1+x) as Real;
consider r be Real such that
A20: r in B & s-t < r by A4,A5,SEQ_4:def 1;
reconsider r as Element of REAL by XREAL_0:def 1;
take r;
s-t + t < r + t by A20,XREAL_1:8; then
A21: s -r < t+r -r by XREAL_1:14;
r <= s by A4,A20,SEQ_4:def 1; then
0 <= s - r by XREAL_1:48;
hence P[x,r] by A20,A21,SEQ_2:1;
end;
consider sq be sequence of REAL such that
A22: for x being Element of NAT holds P[x, sq.x] from FUNCT_2:sch 3(A19);
A23: for x being Nat holds P[x, sq.x]
proof let x be Nat;
x in NAT by ORDINAL1:def 12;
hence thesis by A22;
end;
reconsider sq as Real_Sequence;
A24: now let p1 be Real;
assume A25: 0 < p1;
set p = p1/2;
consider n be Nat such that
A26: 1/p < n by SEQ_4:3;
1/p + (0 qua Real) < n+1 by A26,XREAL_1:8; then
A27: 1/(n+1) <= 1/(1/p) by A25,XREAL_1:118;
take n;
thus for m be Nat st n<=m holds |.sq.m-s.| < p1
proof
let m be Nat;
assume n<=m; then
0 < n+1 & n+1 <= m+1 by XREAL_1:6; then
1/(m+1) <= 1/(n+1) by XREAL_1:118; then
A28: 1/(m+1) <= p by A27,XXREAL_0:2;
sq.m in B & |.s-sq.m.| <= 1/(m+1) by A23; then
|.sq.m-s.| <= 1/(1+m) by COMPLEX1:60; then
A29: |.sq.m-s.| <= p by A28,XXREAL_0:2;
p < p1 by A25,XREAL_1:216;
hence thesis by A29,XXREAL_0:2;
end;
end; then
A30:sq is convergent by SEQ_2:def 6; then
A31:lim sq = s by A24,SEQ_2:def 7;
deffunc F(Real) = ||. f/.$1 -f/.0 .|| - (g.$1 - g.0) - e1*$1 - e1;
A32:for x being Element of REAL holds F(x) in REAL by XREAL_0:def 1;
consider Lg0 be Function of REAL,REAL such that
A33: for x being Element of REAL holds Lg0.x = F(x) from FUNCT_2:sch 8(A32);
A34: for x being Real holds Lg0.x = F(x)
proof let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
Lg0.x = F(x) by A33;
hence thesis;
end;
set Lg = Lg0| [.0,1.];
A35: dom Lg0 = REAL by FUNCT_2:def 1; then
A36:
dom Lg = [.0,1.] by RELAT_1:62;
now let y be object;
assume y in rng sq; then
ex x be object st x in NAT & sq.x = y by FUNCT_2:11; then
y in B by A23; then
ex x be Real st y=x & x in [.0,1.]
& ||. f/.x -f/.0 .|| - (g.x - g.0) - e1*x - e1 <= 0;
hence y in [.0,1.];
end; then
A37:
rng sq c= dom Lg by A36;
A38:s in [.0,1.] by A18,A17;
now let r be Real;
set r3=r/3;
assume A39: 0<r; then
consider t1 be Real such that
A40: 0 < t1 & for x1 be Real st x1 in [.0,1.] & |.x1-s.| < t1
holds ||. f/.x1 - f/.s .|| < r3 by A1,A38,NFCONT_3:17;
consider t2 be Real such that
A41: 0 < t2 & for x1 be Real st x1 in [.0,1.] & |.x1-s.| < t2
holds |.g.x1 - g.s.| < r3
by A39,A38,A1,FCONT_1:14;
set t30 = r3/e1;
set t3 = t30/2;
0 < t3 & t3 < t30 by A2,A39,XREAL_1:216; then
e1*t3 < (r3/e1)*e1 by A2,XREAL_1:97; then
A42: e1*t3 < r3 by A2,XCMPLX_1:87;
take t = min(min(t1,t2),t3);
A43: min(t1,t2) <= t1 & min(t1,t2) <= t2 & 0 < min(t1,t2)
by A40,A41,XXREAL_0:17,21;
hence 0 < t by A2,A39,XXREAL_0:21;
A44: t <= t3 by XXREAL_0:17;
A45: t <= min(t1,t2) by XXREAL_0:17; then
A46: t <= t1 by A43,XXREAL_0:2;
A47: t <= t2 by A43,A45,XXREAL_0:2;
thus for x1 be Real st x1 in dom Lg & |.x1-s.| < t
holds |.Lg.x1 - Lg.s.| < r
proof
let x1 be Real;
assume that
A48: x1 in dom Lg and
A49: |.x1-s.| < t;
x1 in [.0,1.] by A35,A48,RELAT_1:62; then
A50: Lg.x1 = Lg0.x1 by FUNCT_1:49
.= ||. f/.x1 -f/.0 .|| - (g.x1 - g.0) - e1*x1 - e1 by A34;
Lg.s = Lg0.s by A38,FUNCT_1:49; then
Lg.s = ||. f/.s -f/.0 .|| - (g.s - g.0) - e1*s - e1 by A34; then
(Lg.x1 - Lg.s)
= ||. f/.x1 -f/.0 .|| -||. f/.s -f/.0 .|| - (g.x1 - g.s) -e1*(x1-s)
by A50; then
A51: |.Lg.x1 - Lg.s.|
<= |.||. f/.x1 -f/.0 .|| - ||. f/.s -f/.0 .|| - (g.x1 - g.s).|
+|.e1*(x1-s).| by COMPLEX1:57;
|.||. f/.x1 -f/.0 .|| -||. f/.s -f/.0 .|| - (g.x1 - g.s).|
+ |.e1*(x1-s).|
<= |.||. f/.x1 -f/.0 .|| -||. f/.s -f/.0 .||.| +|.g.x1 - g.s.|
+ |.e1*(x1-s).| by COMPLEX1:57,XREAL_1:6; then
A52: |.Lg.x1 - Lg.s.|
<= |.||. f/.x1 -f/.0 .|| -||. f/.s -f/.0 .||.| +|.g.x1 - g.s.|
+ |.e1*(x1-s).| by A51,XXREAL_0:2;
(f/.x1 -f/.0)- (f/.s -f/.0)
= f/.x1 -(f/.0 -(-(f/.s -f/.0))) by RLVECT_1:29
.= f/.x1 -(f/.0 + (f/.s -f/.0)) by RLVECT_1:17
.= f/.x1 -(f/.s- (f/.0 -f/.0)) by RLVECT_1:29
.= f/.x1 -(f/.s- 0.T) by RLVECT_1:5
.= f/.x1 -f/.s by RLVECT_1:13; then
|.||. f/.x1 -f/.0 .|| -||. f/.s -f/.0 .||.| +|.g.x1 - g.s.|
<= ||. f/.x1 -f/.s .|| + |.g.x1 - g.s.| by NORMSP_1:9,XREAL_1:6; then
|.||. f/.x1 -f/.0 .|| -||. f/.s -f/.0 .||.| +|.g.x1 - g.s.|
+ |.e1*(x1-s).|
<= ||. f/.x1 -f/.s .|| + |.g.x1 - g.s.| + |.e1*(x1-s).|
by XREAL_1:6; then
A54: |.Lg.x1 - Lg.s.|
<= ||. f/.x1 -f/.s .|| + |.g.x1 - g.s.| + |.e1*(x1-s).|
by A52,XXREAL_0:2;
|.x1-s.| < t2 by A49,A47,XXREAL_0:2; then
|.g.x1 -g.s.| < r3 by A48,A36,A41; then
A55: ||. f/.x1 -f/.s .|| + |.g.x1 - g.s.|
< ||. f/.x1 -f/.s .|| + r3 by XREAL_1:8;
|.x1-s.| < t3 by A49,A44,XXREAL_0:2; then
|.x1-s.|*e1 <= t3*e1 by A2,XREAL_1:64; then
|.x1-s.|*|.e1.| <= t3*e1 by A2,ABSVALUE:def 1; then
|.e1*(x1-s).| <= t3*e1 by COMPLEX1:65; then
A56: |.e1*(x1-s).| < r3 by A42,XXREAL_0:2;
|.x1-s.| < t1 by A49,A46,XXREAL_0:2; then
||. f/.x1 -f/.s .|| < r3 by A48,A36,A40; then
||. f/.x1 -f/.s .|| + r3 < r3 + r3 by XREAL_1:8; then
||. f/.x1 -f/.s .|| + |.g.x1 - g.s.| < r3 + r3 by A55,XXREAL_0:2; then
||. f/.x1 -f/.s .|| + |.g.x1 - g.s.|+ |.e1*(x1-s).|
< r3 + r3 + r3 by A56,XREAL_1:8;
hence |.Lg.x1 - Lg.s.| < r by A54,XXREAL_0:2;
end;
end; then
A57:Lg is_continuous_in s by FCONT_1:3; then
A57a:Lg/*sq is convergent & Lg.s = lim (Lg/*sq) by A30,A31,A37,FCONT_1:def 1;
A58:for n be Nat holds 0 <= (-(Lg/*sq)).n
proof
let n be Nat;
A59: n in NAT by ORDINAL1:def 12;
(-(Lg/*sq)).n = - (Lg/*sq).n by SEQ_1:10; then
A60: (-(Lg/*sq)).n = - Lg.(sq.n) by A37,FUNCT_2:108,A59;
P[n, sq.n] by A23; then
A61: ex x be Real st sq.n=x & x in [.0,1.]
& ||. f/.x -f/.0 .|| - (g.x - g.0) - e1*x - e1 <= 0; then
Lg0.(sq.n) <=0 by A34; then
Lg.(sq.n) <=0 by A61,FUNCT_1:49;
hence 0 <= (-(Lg/*sq)).n by A60;
end;
-(Lg/*sq) is convergent by A57,A30,A31,A37,FCONT_1:def 1,SEQ_2:9; then
0 <= lim -(Lg/*sq) by A58,SEQ_2:17; then
0 <= - lim (Lg/*sq) by A57a,SEQ_2:10; then
Lg.s <= 0 by A57a; then
Lg0.s <= 0 by A38,FUNCT_1:49; then
A62: ||. f/.s -f/.0 .|| - (g.s - g.0) - e1*s - e1 <= 0 by A34;
A63: s = 1
proof
assume s <> 1; then
s < 1 by A18,XXREAL_0:1; then
A64: s in ].0,1.[ by A17; then
f is_differentiable_in s by A1,NDIFF_3:10; then
consider N1 being Neighbourhood of s such that
A65: N1 c= dom f & ex L1 be LinearFunc of T,R1 be RestFunc of T
st diff(f,s)=L1/.1
& for x be Real
st x in N1 holds f/.x-f/.s = L1/.(x-s) + R1/.(x-s)
by NDIFF_3:def 4;
consider L1 be LinearFunc of T,R1 be RestFunc of T such that
A66: diff(f,s)=L1/.1
& for x be Real st x in N1 holds
f/.x-f/.s = L1/.(x-s) + R1/.(x-s) by A65;
g is_differentiable_in s by A1,A64,FDIFF_1:9; then
consider N2 being Neighbourhood of s such that
A67: N2 c= dom g & ex L2 be LinearFunc,R2 be RestFunc
st diff(g,s)=L2.1
& for x be Real st x in N2 holds
g.x-g.s = L2.(x-s) + R2.(x-s) by FDIFF_1:def 5;
consider L2 be LinearFunc,R2 be RestFunc such that
A68: diff(g,s)=L2.1
& for x be Real st x in N2 holds
g.x-g.s = L2.(x-s) + R2.(x-s) by A67;
consider NN3 being Neighbourhood of s such that
A69: NN3 c= N1 & NN3 c= N2 by RCOMP_1:17;
consider g0 be Real such that
A70: 0 < g0 & ].s-g0,s+g0.[ c= ].0,1.[ by A64,RCOMP_1:19;
reconsider NN4 = ].s-g0,s+g0.[ as Neighbourhood of s
by A70,RCOMP_1:def 6;
consider N3 being Neighbourhood of s such that
A71: N3 c= NN3 & N3 c= NN4 by RCOMP_1:17;
consider d1 be Real such that
A73: 0<d1 & N3 = ]. s-d1,s+d1.[ by RCOMP_1:def 6;
set e2=e1/2;
R1 is total & R1 is RestFunc-like by NDIFF_3:def 1; then
consider d2 be Real such that
A74: 0<d2 & for t be Real st t <> 0 & |.t.| < d2
holds ||. (R1/.t) .|| / |.t.| < e2 by A2,Th17;
R2 is total & R2 is RestFunc-like by FDIFF_1:def 2; then
consider d3 be Real such that
A75: 0<d3 & for t be Real st t <> 0 & |.t.| < d3
holds |.R2.t.|/|.t.| < e2 by A2,Th18;
A76: min(d1,d2) <= d1 & min(d1,d2) <= d2 & 0 < min(d1,d2)
by A73,A74,XXREAL_0:17,21;
set d40= min(min(d1,d2),d3);
A77: d40 <= min(d1,d2) & d40 <= d3 & 0 < d40 by A75,A76,XXREAL_0:17,21;
set d4=d40/2;
A78: d40 <= d1 & d40 <= d2 by A76,A77,XXREAL_0:2;
d4 < d40 by A77,XREAL_1:216; then
A79a: 0 < d4 & d4 < d1 & d4 < d2 & d4 < d3 by A77,A78,XXREAL_0:2; then
s-d1< s+d4 & s+d4< s+d1 by XREAL_1:8; then
A80: s+d4 in N3 by A73; then
A81: f/.(s+d4)-f/.s = L1/.((s+d4)-s) + R1/.((s+d4)-s) by A66,A71,A69;
A82: g.(s+d4)-g.s = L2.((s+d4)-s) + R2.((s+d4)-s) by A71,A69,A80,A68;
consider df1 be Point of T such that
A83: for p be Real holds L1/.p = p*df1 by NDIFF_3:def 2;
L1/.1 = 1*df1 by A83; then
L1/.1 = df1 by RLVECT_1:def 8; then
A84: L1/.d4 = d4*diff(f,s) by A66,A83;
consider df2 be Real such that
A85: for p be Real holds L2.p = df2*p by FDIFF_1:def 3;
L2.1 = df2*1 by A85; then
A86: L2.d4 = d4*diff(g,s) by A68,A85;
A87: ||. f/.(s+d4)-f/.s .|| <= ||. L1/.d4 .|| + ||. R1/. d4 .||
by A81,NORMSP_1:def 1;
A88: ||. L1/.d4 .|| = |.d4.|*||. diff(f,s) .|| by A84,NORMSP_1:def 1
.= ||. diff(f,s) .||*d4 by A77,ABSVALUE:def 1;
A89: 0 < |.d4.| by A77,ABSVALUE:def 1;
|.d4.| < d2 by A79a,ABSVALUE:def 1; then
||. R1/.d4 .|| / |.d4.| < e2 by A74,A77; then
||. R1/.d4 .|| <= e2 * |.d4.| by A89,XREAL_1:81; then
||. R1/.d4 .|| <= e2 * d4 by A77,ABSVALUE:def 1; then
||. L1/.d4 .|| + ||. R1/.d4 .||
<= ||. diff(f,s) .|| * d4 + e2 * d4 by A88,XREAL_1:6; then
A90: ||. f/.(s+d4)-f/.s .||
<= ||. diff(f,s) .|| * d4 + e2 * d4 by A87,XXREAL_0:2;
||. diff(f,s) .||*d4 <=diff(g,s)*d4
by A64,A1,A77,XREAL_1:64; then
||. diff(f,s) .||*d4 + e2*d4 <= diff(g,s)*d4 + e2*d4 by XREAL_1:6; then
A91: ||. f/.(s+d4)-f/.s .|| <= diff(g,s)*d4 + e2*d4 by A90,XXREAL_0:2;
|.d4.| < d3 by A79a,ABSVALUE:def 1; then
|.R2.d4.|/ |.d4.| < e2 by A75,A77; then
|.R2.d4.| <= e2* |.d4.| by A89,XREAL_1:81; then
|.R2.d4.| <= e2* d4 by A77,ABSVALUE:def 1; then
-(e2*d4) <= R2.d4 by ABSVALUE:5; then
d4*diff(g,s) -(e2*d4) <= g.(s+d4)-g.s by A82,A86,XREAL_1:6; then
d4*diff(g,s) <= g.(s+d4)-g.s + e2*d4 by XREAL_1:20; then
diff(g,s)*d4 + e2*d4
<= (g.(s+d4)-g.s + e2*d4) + e2*d4 by XREAL_1:6; then
||. f/.(s+d4)-f/.s .|| <= g.(s+d4)-g.s + e1*d4 by A91,XXREAL_0:2; then
||. f/.(s+d4)-f/.s .|| - (g.(s+d4)-g.s + e1*d4) <= 0 by XREAL_1:47; then
A92: ||. f/.(s+d4)-f/.s .|| - g.(s+d4)+g.s - e1*d4
+ (||. f/.s -f/.0 .|| - (g.s - g.0 ) - e1*s - e1)
<= (0 qua Real)+ (0 qua Real) by A62;
||. f/.(s+d4)-f/.0 .|| - (g.(s+d4) -g.0 + e1*(d4+s) + e1)
<= ||. f/.(s+d4)-f/.s .|| + ||. f/.s -f/.0 .||
- (g.(s+d4) -g.0 + e1*(d4+s) + e1) by NORMSP_1:10,XREAL_1:9; then
A93: ||. f/.(s+d4)-f/.0 .|| - (g.(s+d4) -g.0) - e1*(s+d4) -e1 <= 0 by A92;
|.(0 qua Real)+1-2*(s+d4).|< 1 -(0 qua Real)
by A80,A71,A70,RCOMP_1:3; then
s + d4 in [.0,1.] by RCOMP_1:2; then
A94: s+d4 in B by A93;
s +(0 qua Real) < s + d4 by A77,XREAL_1:8;
hence contradiction by A94,A4,SEQ_4:def 1;
end;
0 in dom g & 1 in dom g by A1; then
g/.1 = g.1 & g/.0 = g.0 by PARTFUN1:def 6; then
||. f/.1 -f/.0 .|| - (g/.1 - g/.0 ) - e + e <= (0 qua Real) + e
by A63,A62,XREAL_1:6;
hence ||. f/.1 -f/.0 .|| - (g/.1 - g/.0) <= e;
end; then
||. f/.1 -f/.0 .|| - (g/.1 - g/.0) + (g/.1 - g/.0)
<= (0 qua Real) + (g/.1 - g/.0) by Lm3,XREAL_1:6;
hence thesis;
end;
theorem Th19:
for S,T be RealNormSpace,
f be PartFunc of S,T, p,q be Point of S, M be Real
st [.p,q.] c= dom f
& (for x be Point of S st x in [.p,q.] holds f is_continuous_in x)
& (for x be Point of S st x in ].p,q.[ holds f is_differentiable_in x)
& (for x be Point of S st x in ].p,q.[ holds ||. diff(f,x) .|| <= M)
holds ||. f/.q - f/.p .|| <= M*||. q-p .||
proof
let S,T be RealNormSpace,
f be PartFunc of S,T, p,q be Point of S, M be Real;
assume A1: [.p,q.] c= dom f
& (for x be Point of S st x in [.p,q.] holds f is_continuous_in x)
& (for x be Point of S st x in ].p,q.[ holds f is_differentiable_in x)
& (for x be Point of S st x in ].p,q.[ holds ||. diff(f,x) .|| <= M);
per cases ;
suppose B2: p=q ;
B3: ||. f/.q - f/.p .||
= ||. 0.T .|| by B2,RLVECT_1:15
.= 0;
M*||. q-p .|| = M * ||. 0.S .|| by B2,RLVECT_1:15
.= 0 ;
hence thesis by B3;
end;
suppose p<>q ;
then
X1: ]. p,q .[
= { p+t*(q-p) where t is Real : 0 < t & t < 1}
by LMOPN;
deffunc PP(Real) = $1*(q-p)+p;
consider pt0 be Function of REAL,the carrier of S such that
A2: for t being Element of REAL holds pt0.t = PP(t) from FUNCT_2:sch 4;
A3: for t being Real holds pt0.t = PP(t)
proof let t be Real;
reconsider t as Element of REAL by XREAL_0:def 1;
pt0.t = PP(t) by A2;
hence thesis;
end;
set pt=pt0 | ([.0,1.]);
A4:dom pt0 = REAL by FUNCT_2:def 1; then
A5:dom pt = [.0,1.] by RELAT_1:62;
A6:now let t be Real;
assume t in [.0,1.];
pt0/.t = pt0.t by A4,PARTFUN1:def 6,XREAL_0:def 1;
hence pt0/.t = t*(q-p)+p by A3;
end;
A7: ].0,1.[ c= [.0,1.] by XXREAL_1:25;
A8:now let t be Real;
assume t in ].0,1.[;
hence pt/.t = pt0/.t by A5,A7,PARTFUN2:15
.= pt0.t by A4,PARTFUN1:def 6,XREAL_0:def 1
.= t*(q-p)+p by A3;
end; then
A10:pt is_differentiable_on ].0,1.[
& for t be Real
st t in ].0,1.[ holds (pt`|].0,1.[ ).t = (q-p)
by A5,A7,NDIFF_3:21;
reconsider phi = f*pt as PartFunc of REAL,T;
A11:rng pt c= [.p,q.]
proof
let y be object;
assume y in rng pt; then
consider x be object such that
A12: x in dom pt & y = pt.x by FUNCT_1:def 3;
A13: y = pt0.x by A12,FUNCT_1:47;
reconsider x as Element of REAL by A12;
consider r be Real such that
A14: x=r & 0<=r & r<=1 by A12,A5;
y = p+ x*(q-p) by A3,A13 .= (1-x)*p + x*q by Lm2; then
y in {(1-r1)*p + r1*q where r1 is Real :
0 <= r1 & r1 <= 1 } by A14;
hence y in [. p,q .] by RLTOPSP1:def 2;
end; then
rng pt c= dom f by A1; then
A15:
dom phi = [.0,1.] by A5,RELAT_1:27;
A16:
for t be Real st t in [.0,1.] holds phi/.t = f/.(p+t*(q-p))
proof
let t be Real;
assume A17: t in [.0,1.]; then
A18: phi/.t =phi.t by A15,PARTFUN1:def 6
.= f.(pt.t) by A17,A15,FUNCT_1:12;
A19: pt.t in rng pt by A17,A5,FUNCT_1:def 3;
pt.t = pt0.t by A17,A5,FUNCT_1:47
.= p+t*(q-p) by A3;
hence thesis by A18,A11,A19,A1,PARTFUN1:def 6;
end;
now let x0 be Real;
assume A20: x0 in dom phi; then
A21: pt is_continuous_in x0 by A5,A6,A15,NFCONT_3:33,def 2;
pt.x0 in rng pt by A5,A20,A15,FUNCT_1:def 3; then
pt.x0 in [.p,q.] by A11; then
pt/.x0 in [.p,q.] by A20,A15,A5,PARTFUN1:def 6;
hence phi is_continuous_in x0 by A1,A20,A21,NFCONT_3:15;
end; then
phi is continuous by NFCONT_3:def 2; then
A22:phi| [.0,1.] is continuous;
A23:
now let x be Real;
assume A24: x in ].0,1.[; then
A25: pt is_differentiable_in x by A10,NDIFF_3:10;
(pt`|].0,1.[ ).x = (q-p) by A24,A8,A5,A7,NDIFF_3:21; then
A26: diff(pt,x) = (q-p) by A10,A24,NDIFF_3:def 6;
A27: pt.x = pt/.x by A24,A7,A5,PARTFUN1:def 6;
A28: ex r be Real st x=r & 0<r & r<1 by A24;
A29: pt.x= pt0.x by A24,A7,A5,FUNCT_1:47;
A30: pt0.x = p+ x*(q-p) by A3;
pt.x in ].p,q.[ by X1,A28,A29,A30; then
A31: f is_differentiable_in pt/.x by A27,A1;
hence phi is_differentiable_in x by A25,Th6;
thus diff(phi,x) = diff(f,p+ x*(q-p)).(q-p)
by A26,A27,A29,A30,A31,A25,Th6;
end; then
].0,1.[ c= dom phi & for x be Real st x in ].0,1.[ holds
phi is_differentiable_in x by A15,XXREAL_1:25; then
A32:phi is_differentiable_on ].0,1.[ by NDIFF_3:10;
deffunc GG(Real) = In(M*||. q-p .||*$1,REAL);
consider g0 be Function of REAL,REAL such that
A33: for t being Element of REAL holds g0.t = GG(t) from FUNCT_2:sch 4;
A34: for t being Real holds g0.t = GG(t)
proof let t be Real;
reconsider t as Element of REAL by XREAL_0:def 1;
g0.t = GG(t) by A33;
hence thesis;
end;
set g=g0 | ([.0,1.]);
A35: for t be Real st t in [.0,1.] holds
g0.t = (M*||. q-p .||)*t + (0 qua Real)
proof let t be Real;
assume t in [.0,1.];
thus g0.t = GG(t) by A34
.=(M*||. q-p .||)*t + (0 qua Real);
end;
dom g0 = REAL by FUNCT_2:def 1; then
A36:dom g = [.0,1.] by RELAT_1:62;
A37:g| [.0,1.] is continuous by A35,FCONT_1:41;
A38:now let t be Real;
assume t in ].0,1.[;
hence g.t =g0.t by A36,A7,FUNCT_1:47
.= GG(t) by A34
.= M*||. q-p .||*t + (0 qua Real);
end; then
A39:g is_differentiable_on ].0,1.[
& for t be Real
st t in ].0,1.[ holds (g`|].0,1.[ ).t = M*||. q-p .||
by A36,A7,FDIFF_1:23;
for t be Real st t in ].0,1.[ holds ||. diff(phi,t) .|| <= diff(g,t)
proof
let t be Real;
assume
A40: t in ].0,1.[; then
A41: ||.diff(phi,t).|| = ||. diff(f,p+ t*(q-p)).(q-p) .|| by A23;
reconsider L= diff(f,p+ t*(q-p)) as Lipschitzian LinearOperator of S,T
by LOPBAN_1:def 9;
A42: ||.L.(q-p).|| <= ||.diff(f,p+ t*(q-p)).|| * ||.(q-p).|| by LOPBAN_1:32;
A43: ex r be Real st t=r & 0<r & r<1 by A40;
p+ t*(q-p) in ].p,q.[ by A43,X1;
then
A44: ||. diff(f,p+ t*(q-p)).|| * ||.q-p.|| <= M * ||.q-p.||
by A1,XREAL_1:64;
diff(g,t) = (g`|].0,1.[ ).t by A40,A39,FDIFF_1:def 7; then
diff(g,t) = M*||. q-p .|| by A40,A38,A36,A7,FDIFF_1:23;
hence thesis by A44,A42,A41,XXREAL_0:2;
end; then
A45:
||. phi/.1 -phi/.0 .|| <= g/.1 - g/.0
by Lm4,A15,A22,A32,A36,A37,A38,A7,FDIFF_1:23;
A46:
1 in [.0,1.] & 0 in [.0,1.]; then
A47:g/.1 =g.1 by A36,PARTFUN1:def 6
.=g0.1 by A36,A46,FUNCT_1:47
.= GG(1) by A34
.= M*||. q-p .||*1;
A48:g/.0 = g.0 by A36,A46,PARTFUN1:def 6
.=g0.0 by A36,A46,FUNCT_1:47
.= GG(0) by A34
.= M*||. q-p .|| * ( 0 qua Real);
A49:phi/.1 = f/.(p+1*(q-p)) by A16,A46
.= f/.(p+(q-p)) by RLVECT_1:def 8
.= f/.(q-(p-p)) by RLVECT_1:29
.= f/.(q-0.S) by RLVECT_1:15
.= f/.q by RLVECT_1:13;
phi/.0 = f/.(p+( 0 qua Real ) * (q-p)) by A16,A46
.= f/.(p+0.S) by RLVECT_1:10
.= f/.p by RLVECT_1:4;
hence thesis by A45,A47,A48,A49;
end;
end;
theorem Th20:
for S,T be RealNormSpace, f be PartFunc of S,T,
p,q be Point of S, M be Real,
L be Point of R_NormSpace_of_BoundedLinearOperators(S,T)
st [.p,q.] c= dom f
& (for x be Point of S st x in [.p,q.] holds f is_continuous_in x)
& (for x be Point of S st x in ].p,q.[ holds f is_differentiable_in x)
& (for x be 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
let S,T be RealNormSpace,
f be PartFunc of S,T,
p,q be Point of S,
M be Real,
L be Point of R_NormSpace_of_BoundedLinearOperators(S,T);
assume that
A1: [.p,q.] c= dom f and
A2: (for x be Point of S st x in [.p,q.] holds f is_continuous_in x)
& (for x be Point of S st x in ].p,q.[ holds f is_differentiable_in x)
& (for x be Point of S st x in ].p,q.[ holds ||. diff(f,x) - L .|| <= M);
reconsider LP=L as Lipschitzian LinearOperator of S,T by LOPBAN_1:def 9;
deffunc LL(Point of S) = L.($1-p);
consider L0 be Function of the carrier of S,the carrier of T such that
A3: for t being Element of the carrier of S
holds L0.t = LL(t) from FUNCT_2:sch 4;
A4:dom L0 = the carrier of S by FUNCT_2:def 1;
now let x1,x2 be Point of S;
assume x1 in dom L0 & x2 in dom L0;
L0/.x1=L.(x1-p) & L0/.x2=L.(x2-p) by A3; then
||.L0/.x1-L0/.x2 .||
= ||.LP.(x1-p)+(-1)*LP.(x2-p) .|| by RLVECT_1:16
.= ||.LP.(x1-p)+LP.((-1)*(x2-p)) .|| by LOPBAN_1:def 5
.= ||.LP.((x1-p)+(-1)*(x2-p)) .|| by VECTSP_1:def 20
.= ||.LP.((x1-p)-(x2-p)) .|| by RLVECT_1:16
.= ||. LP.(x1-((x2-p)+p)) .|| by RLVECT_1:27
.= ||. LP.(x1-(x2-(p-p))) .|| by RLVECT_1:29
.= ||. LP.(x1-(x2-0.S)) .|| by RLVECT_1:15
.= ||. LP.(x1-x2) .|| by RLVECT_1:13; then
A5: ||.L0/.x1-L0/.x2 .|| <= ||.L.|| * ||.x1-x2.|| by LOPBAN_1:32;
(0 qua Real) + ||.L.|| < 1 + ||.L.|| by XREAL_1:8; then
||.L.|| * ||.x1-x2.|| <= (||.L.||+1) * ||.x1-x2.|| by XREAL_1:64;
hence
||.L0/.x1-L0/.x2 .|| <= (||.L.||+1) * ||.x1-x2.|| by A5,XXREAL_0:2;
end; then
A6:L0 is_continuous_on (dom L0) by NFCONT_1:45,def 9;
reconsider R = (the carrier of S) --> 0.T as PartFunc of S,T;
A7:dom R = the carrier of S;
now let h be (0.S)-convergent sequence of S;
assume h is non-zero;
A8: now let n be Nat;
A9: R/.(h.n) =R.(h.n) by A7,PARTFUN1:def 6
.=0.T;
A10: rng h c= dom R;
A11: n in NAT by ORDINAL1:def 12;
thus ((||.h.||")(#)(R/*h)).n = (||.h.||".n)*((R/*h).n)
by NDIFF_1:def 2
.=(||.h.||".n)*(R/.(h.n)) by A11,A10,FUNCT_2:109
.=0.T by A9,RLVECT_1:10;
end; then
A12: (||.h.||")(#)(R/*h) is constant by VALUED_0:def 18;
hence (||.h.||")(#)(R/*h) is convergent by NDIFF_1:18;
((||.h.||")(#)(R/*h)).0 = 0.T by A8;
hence lim ((||.h.||")(#)(R/*h)) = 0.T by A12,NDIFF_1:18;
end; then
reconsider R as RestFunc of S,T by NDIFF_1:def 5;
A13:
now let x0 be Point of S;
set N = the Neighbourhood of x0;
A14:for x be Point of S st x in N holds L0/.x-L0/.x0=L.(x-x0)+R/.(x-x0)
proof
let x be Point of S;
A15: R/.(x-x0) =R.(x-x0) by A7,PARTFUN1:def 6
.=0.T;
assume x in N;
thus L0/.x-L0/.x0 = L.(x-p)-L0/.x0 by A3
.= L.(x-p)-L.(x0-p) by A3
.= LP.(x-p)+(-1)*LP.(x0-p) by RLVECT_1:16
.= LP.(x-p)+LP.((-1)*(x0-p)) by LOPBAN_1:def 5
.= LP.((x-p)+(-1)*(x0-p)) by VECTSP_1:def 20
.= LP.((x-p)-(x0-p)) by RLVECT_1:16
.= LP.(x-((x0-p)+p)) by RLVECT_1:27
.= LP.(x-(x0-(p-p))) by RLVECT_1:29
.= LP.(x-(x0-0.S)) by RLVECT_1:15
.= LP.(x-x0) by RLVECT_1:13
.= L.(x-x0) + R/.(x-x0) by A15,RLVECT_1:4;
end;
hence L0 is_differentiable_in x0 by A4,NDIFF_1:def 6;
hence diff(L0,x0) = L by A4,A14,NDIFF_1:def 7;
end;
set g= f - L0;
A16:dom g = dom f /\ dom L0 by VFUNCT_1:def 2
.= dom f by A4,XBOOLE_1:28;
A17:for x be Point of S st x in dom g holds g/.x= f/.x - L.(x-p)
proof
let x be Point of S;
assume x in dom g;
hence g/.x= f/.x - L0/.x by VFUNCT_1:def 2
.=f/.x - L.(x-p) by A3;
end;
A18:for x be Point of S st x in [.p,q.] holds g is_continuous_in x
proof
let x be Point of S;
assume x in [.p,q.]; then
A19:f is_continuous_in x by A2;
L0 | (dom L0) is_continuous_in x by A4,A6,NFCONT_1:def 7;
hence thesis by A19,NFCONT_1:15;
end;
A20:for x be Point of S st x in ].p,q.[ holds g is_differentiable_in x
proof
let x be Point of S;
assume x in ].p,q.[; then
f is_differentiable_in x & L0 is_differentiable_in x by A2,A13;
hence g is_differentiable_in x by NDIFF_1:36;
end;
for x be Point of S st x in ].p,q.[ holds ||. diff(g,x) .|| <= M
proof
let x be Point of S;
assume A21: x in ].p,q.[; then
A22: f is_differentiable_in x by A2;
L0 is_differentiable_in x & diff(L0,x) = L by A13; then
diff(g,x) = diff(f,x) - L by A22,NDIFF_1:36;
hence ||. diff(g,x) .|| <= M by A2,A21;
end; then
A23:
||. g/.q - g/.p .|| <= M*||. q-p .|| by Th19,A1,A16,A18,A20;
p in [.p,q.] by RLTOPSP1:68; then
g/.p= f/.p - L.(p-p) by A1,A16,A17; then
A24:g/.p = f/.p - LP.(0.S) by RLVECT_1:15
.=f/.p - LP.( 0 *p ) by RLVECT_1:10
.=f/.p - 0 * LP.p by LOPBAN_1:def 5
.=f/.p - 0.T by RLVECT_1:10
.=f/.p by RLVECT_1:13;
q in [.p,q.] by RLTOPSP1:68; then
g/.q= f/.q - L.(q-p) by A1,A16,A17; then
f/.q - (L.(q-p) +f/.p ) = g/.q - g/.p by A24,RLVECT_1:27;
hence thesis by A23,RLVECT_1:27;
end;
begin :: Partial derivative of a function of several variables
definition
let G be RealNormSpace-Sequence;
let i be Element of dom G;
func proj i -> Function of product G,G.i means :Def3:
for x be Element of product carr G holds it.x = x.i;
existence
proof
deffunc F(Element of product carr G) = $1.i;
consider f being Function of product carr G,G.i such that
A1: for x being Element of product carr G holds f.x = F(x) from FUNCT_2:sch 4;
product G = NORMSTR(# product carr G,zeros G,[:addop G:]
,[:multop G:], productnorm G #) by PRVECT_2:6; then
reconsider f as Function of product G,G.i;
take f;
thus thesis by A1;
end;
uniqueness
proof
let f,g be Function of the carrier of (product G),the carrier of (G.i);
assume that
A2: for x being Element of product carr G holds f.x = x.i and
A3: for x being Element of product carr G holds g.x = x.i;
A4:product G = NORMSTR(# product carr G,zeros G,[:addop G:]
,[:multop G:], productnorm G #) by PRVECT_2:6;
now let x1 be Element of the carrier of product G;
reconsider x=x1 as Element of product carr G by A4;
f.x1 =x.i by A2;
hence f.x1 = g.x1 by A3;
end;
hence thesis;
end;
end;
definition
let G be RealNormSpace-Sequence;
let i be Element of dom G;
let x be Element of product G;
func reproj(i,x) -> Function of G.i,product G means :Def4:
for r be Element of G.i holds it.r = x +* (i,r);
existence
proof
reconsider x1 = x as Element of product carr G by Th10;
defpred P[Element of G.i,
Element of the carrier of product G] means
$2 = x1 +* (i,$1);
A1:for r being Element of G.i
ex y be Element of the carrier of product G st P[r,y]
proof
let r be Element of G.i;
x1 +* (i,r) is Element of the carrier of product G by Th11;
hence thesis;
end;
ex f being Function of the carrier of (G.i),the carrier of product G st
for r be Element of G.i
holds P[r,f.r] from FUNCT_2:sch 3(A1);
hence thesis;
end;
uniqueness
proof
let f,g be Function of the carrier of (G.i),the carrier of product G;
assume that
A2:for r be Element of G.i holds f.r = x +* (i,r) and
A3:for r be Element of G.i holds g.r = x +* (i,r);
let r be Element of G.i;
f.r = x +* (i,r) by A2;
hence f.r = g.r by A3;
end;
end;
definition
::$CD
let G be RealNormSpace-Sequence;
let F be RealNormSpace;
let i be set;
let f be PartFunc of product G,F;
let x being Element of product G;
pred f is_partial_differentiable_in x,i means
f*reproj(In(i,dom G),x) is_differentiable_in proj(In(i,dom G)).x;
end;
definition
let G be RealNormSpace-Sequence;
let F be 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.In(i,dom G),F)
equals
diff(f*reproj(In(i,dom G),x),proj(In(i,dom G)).x);
coherence;
end;
begin :: Linearity of Partial Differential Operator
reserve G for RealNormSpace-Sequence;
reserve F for RealNormSpace;
reserve i for Element of dom G;
reserve f,f1,f2 for PartFunc of product G, F;
reserve x for Point of product G;
reserve X for set;
definition
let G be RealNormSpace-Sequence;
let F be RealNormSpace;
let i be set;
let f be PartFunc of product G,F;
let X be set;
pred f is_partial_differentiable_on X,i means
X c= dom f & for x be Point of product G st x in X
holds f|X is_partial_differentiable_in x,i;
end;
theorem Th21:
for xi be Element of G.i
holds ||. reproj(i,0.(product G)).xi .|| = ||.xi.||
proof
let xi be Element of G.i;
set j = len G;
reconsider i0 = i as Element of NAT;
Seg len G = dom G by FINSEQ_1:def 3; then
A1:1 <= i0 & i0 <= j by FINSEQ_1:1;
set z = 0.(product G);
A3: the carrier of (product G) = product carr G by Th10;
then reconsider w = z +* (i0,xi) as Element of product carr G by Th11;
A4: ||. reproj(i,z).xi .|| = |. normsequence(G,w) .|
by Def4,PRVECT_2:7;
reconsider q = ||.xi.|| as Element of REAL;
set q1 = <*q*>;
set y = 0*j;
A5:len normsequence(G,w) = j by PRVECT_2:def 11;
A6:len y = j by CARD_1:def 7; then
A7:(y| (i0-'1))^<*q*>^(y /^ i0) = Replace(y,i0,q) by A1,FINSEQ_7:def 1; then
A8:len ((y| (i0-'1))^<*q*>^(y /^ i0)) = len y by FINSEQ_7:5;
A9:len y = len Replace(y,i0,q) by FINSEQ_7:5;
for k be Nat st 1 <= k & k <= len normsequence(G,w) holds
normsequence(G,w).k = ((y| (i0-'1))^<*q*>^(y /^ i0)).k
proof
let k be Nat;
assume A10: 1 <= k & k <= len normsequence(G,w); then
reconsider k1 = k as Element of dom G by A5,FINSEQ_3:25;
A11: k1 in dom G;
z in the carrier of product G; then
z in product carr G by Th10; then
consider g being Function such that
A12: z = g & dom g = dom carr G &
for y being object st y in dom carr G holds g.y in (carr G).y
by CARD_3:def 5;
A13: k in dom z by A11,A12,Lm1;
A14: (normsequence(G,w)).k
= (the normF of (G.k1)).(w.k1) by PRVECT_2:def 11;
per cases;
suppose A15: k = i0; then
A16: (normsequence(G,w)).k = ||. xi .|| by A14,A13,FUNCT_7:31;
Replace(y,i0,q)/.k = q by A15,A10,A5,A6,FINSEQ_7:8;
hence normsequence(G,w).k = ((y| (i0-'1))^<*q*>^(y /^ i0)).k
by A16,A7,A10,A5,A6,A9,FINSEQ_4:15;
end;
suppose A17: k <> i0; then
w.k1 = z.k1 by FUNCT_7:32; then
A18: (normsequence(G,w)).k = ||. 0.(G.k1) .|| by A14,Th14,A3;
Replace(y,i0,q)/.k = y/.k by A17,A10,A5,A6,FINSEQ_7:10; then
Replace(y,i0,q).k = y/.k by A10,A5,A6,A9,FINSEQ_4:15; then
Replace(y,i0,q).k = y.k by A10,A5,A6,FINSEQ_4:15;
hence normsequence(G,w).k = ((y| (i0-'1))^<*q*>^(y /^ i0)).k
by A18,A6,A1,FINSEQ_7:def 1;
end;
end; then
A19:normsequence(G,w) = (y| (i0-'1))^<*q*>^(y /^ i0)
by A6,A8,PRVECT_2:def 11;
sqrt Sum sqr(y| (i0-'1)) = |. 0*(i0-'1) .| by A1,PDIFF_7:2; then
sqrt Sum sqr(y| (i0-'1)) = 0 by EUCLID:7; then
A20:Sum sqr(y| (i0-'1)) = 0 by RVSUM_1:86,SQUARE_1:24;
sqrt Sum sqr(y/^i0) = |. 0*(j-'i0) .| by PDIFF_7:3; then
A21:sqrt Sum sqr(y/^i0) = 0 by EUCLID:7;
reconsider q2 = q^2 as Element of REAL by XREAL_0:def 1;
sqr((y| (i0-'1))^<*q*>^(y/^i0))
= sqr((y| (i0-'1))^<*q*>)^sqr(y/^i0) by RVSUM_1:144
.= sqr(y| (i0-'1))^sqr<*q*>^sqr(y/^i0) by RVSUM_1:144
.= sqr(y| (i0-'1))^<*q^2*>^sqr(y/^i0) by RVSUM_1:55; then
Sum sqr((y| (i0-'1))^<*q*>^(y/^i0))
= Sum(sqr(y| (i0-'1))^<*q2*>) + Sum sqr(y/^i0) by RVSUM_1:75
.= Sum sqr(y| (i0-'1)) + q^2 + Sum sqr(y/^i0) by RVSUM_1:74
.= q^2 by A20,A21,RVSUM_1:86,SQUARE_1:24; then
||. reproj(i,z).xi .|| = |. q .| by A19,A4,COMPLEX1:72;
hence thesis by COMPLEX1:43;
end;
theorem Th22:
for G be RealNormSpace-Sequence,
i be Element of dom G,
x be Point of product G,
r be Point of G.i holds
reproj(i,x).r - x = reproj(i,0.(product G)).(r - proj(i).x) &
x - reproj(i,x).r = reproj(i,0.(product G)).(proj(i).x - r)
proof
let G be RealNormSpace-Sequence,
i be Element of dom G,
x be Point of product G,
r be Point of G.i;
set m=len G;
reconsider xf=x as Element of product carr G by Th10;
A1:dom carr G = dom G by Lm1;
reconsider Zr = 0.(product G) as Element of product carr G by Th10;
reconsider ixr = reproj(i,x).r as Element of product carr G by Th10;
reconsider p = reproj(i,x).r - x as Element of product carr G by Th10;
reconsider q = reproj(i,0.(product G)).(r - proj(i).x)
as Element of product carr G by Th10;
A3:dom q = dom (carr G) by CARD_3:9;
reconsider s = x - reproj(i,x).r as Element of product carr G by Th10;
reconsider t = reproj(i,0.(product G)).(proj(i).x - r)
as Element of product carr G by Th10;
A5:dom t = dom carr G by CARD_3:9;
A6: reproj(i,x).r = x +* (i,r) by Def4;
reconsider xfi =xf.i as Point of G.i;
A7: reproj(i,0.(product G)).(r - proj(i).x)
= 0.(product G) +* (i,(r - proj(i).x)) by Def4;
then
A7a:
q = Zr +* (i,(r- xfi)) by Def3;
A8: reproj(i,0.(product G)).(proj(i).x -r)
= 0.(product G) +* (i,(proj(i).x - r)) by Def4;
then
A8a:
t = Zr +* (i,(xfi -r)) by Def3;
set ir= i .--> r;
set irx1= (i .--> (r- xfi));
set irx2= (i .--> (xfi - r));
x in the carrier of product G; then
A9: x in product carr G by Th10;
consider g1 be Function such that
A10: x = g1 & dom g1 = dom carr G
& for i be object st i in dom carr G holds g1.i in (carr G).i
by A9,CARD_3:def 5;
for k be object st k in dom p holds p.k = q.k
proof
let k be object;
assume A11: k in dom p; then
reconsider k0=k as Element of dom G by A1,CARD_3:9;
consider g be Function such that
A12: Zr = g & dom g = dom carr G
& for i be object st i in dom carr G holds g.i in (carr G).i
by CARD_3:def 5;
A13: k in dom Zr by A12,A11,CARD_3:9;
A14: k in dom x by A10,A11,CARD_3:9;
per cases;
suppose not k in {i}; then
A15: k <> i by TARSKI:def 1; then
A16: q.k0 = Zr.k0 by A7,FUNCT_7:32;
p.k = ixr.k0 -xf.k0 by Th15
.= xf.k0 -xf.k0 by A15,A6,FUNCT_7:32; then
p.k =0.(G.k0) by RLVECT_1:15;
hence p.k = q.k by A16,Th14;
end;
suppose k in {i}; then
A17: k=i by TARSKI:def 1; then
A18: q.k0 = r- xfi by A7a,A13,FUNCT_7:31;
p.k=ixr.k0 -xf.k0 by Th15;
hence p.k = q.k by A18,A6,A17,A14,FUNCT_7:31;
end;
end;
hence reproj(i,x).r - x = reproj(i,0.(product G)).(r - proj(i).x)
by A3,FUNCT_1:2,CARD_3:9;
for k be object st k in dom s holds s.k = t.k
proof
let k be object;
assume A19: k in dom s; then
reconsider k0=k as Element of dom G by A1,CARD_3:9;
consider g be Function such that
A20: Zr = g & dom g = dom carr G
& for i be object st i in dom carr G holds g.i in (carr G).i
by CARD_3:def 5;
A21: k in dom Zr by A20,A19,CARD_3:9;
A22: k in dom x by A10,A19,CARD_3:9;
per cases;
suppose not k in {i}; then
A23: k <> i by TARSKI:def 1; then
A24: t.k0 = Zr.k0 by A8,FUNCT_7:32;
s.k= xf.k0 - ixr.k0 by Th15
.=xf.k0 -xf.k0 by A6,A23,FUNCT_7:32; then
s.k =0.(G.k0) by RLVECT_1:15;
hence s.k = t.k by A24,Th14;
end;
suppose k in {i}; then
A25: k=i by TARSKI:def 1; then
A26: t.k0 = xfi-r by A8a,A21,FUNCT_7:31;
s.k=xf.k0 - ixr.k0 by Th15;
hence s.k = t.k by A26,A6,A25,A22,FUNCT_7:31;
end;
end;
hence thesis by A5,FUNCT_1:2,CARD_3:9;
end;
theorem Th23:
for G be RealNormSpace-Sequence,
i be Element of dom G,
x be Point of product G,
Z be Subset of product G
st Z is open & x in Z holds
ex N be Neighbourhood of proj(i).x st
for z be Point of G.i st z in N holds (reproj(i,x)).z in Z
proof
let G be RealNormSpace-Sequence,
i be Element of dom G,
x be Point of product G,
Z be Subset of product G;
assume Z is open & x in Z; then
consider r be Real such that
A1: 0 < r & {y where y is Point of product G : ||. y - x .|| < r} c= Z
by NDIFF_1:3;
set N = {y where y is Point of G.i : ||. y - proj(i).x .|| < r};
reconsider N as Neighbourhood of proj(i).x by A1,NFCONT_1:3;
take N;
thus for z be Point of G.i st z in N holds (reproj(i,x)).z in Z
proof
let z be Point of G.i;
assume z in N; then
A2: ex y be Point of G.i st y = z & ||. y - proj(i).x .|| < r;
||. (reproj(i,x)).z - x .||
= ||. reproj(i,0.(product G)).(z - proj(i).x) .|| by Th22
.= ||. z - proj(i).x .|| by Th21; then
(reproj(i,x)).z
in {y where y is Point of product G : ||. y - x .|| < r} by A2;
hence thesis by A1;
end;
end;
theorem Th24:
for G be RealNormSpace-Sequence,
T be RealNormSpace,
i be set,
f be PartFunc of product G, T,
Z be Subset of product G
st Z is open holds
f is_partial_differentiable_on Z,i
iff
Z c=dom f &
for x be Point of product G st x in Z holds
f is_partial_differentiable_in x,i
proof
let G be RealNormSpace-Sequence,
T be RealNormSpace,
i be set,
f be PartFunc of product G, T,
Z be Subset of product G;
assume
A1: Z is open;
set i0=In(i,dom G);
set S=G.i0;
set RNS= R_NormSpace_of_BoundedLinearOperators(S,T);
thus f is_partial_differentiable_on Z,i implies
Z c=dom f &
for x be Point of product G st x in Z holds
f is_partial_differentiable_in x,i
proof
assume A2: f is_partial_differentiable_on Z,i;
hence Z c=dom f;
let nx0 be Point of product G;
reconsider x0=proj(i0).nx0 as Point of S;
assume A4: nx0 in Z; then
f|Z is_partial_differentiable_in nx0,i by A2; then
consider N0 being Neighbourhood of x0 such that
A5: N0 c= dom((f|Z)*reproj(i0,nx0)) and
A6: ex L be Point of RNS,R be RestFunc of S,T st
for x be Point of S st x in N0 holds
((f|Z)*reproj(i0,nx0))/.x-((f|Z)*reproj(i0,nx0))/.x0
= L .( x-x0)+R/.(x-x0) by NDIFF_1:def 6;
consider L be Point of RNS,R be RestFunc of S,T such that
A7: for x be Point of S st x in N0 holds
((f|Z)*reproj(i0,nx0))/.x - ((f|Z)*reproj(i0,nx0))/.x0
= L.(x-x0) + R/.(x-x0) by A6;
consider N1 being Neighbourhood of x0 such that
A8: for x be Point of S st x in N1 holds
(reproj(i0,nx0)).x in Z by A1,A4,Th23;
A9:now let x be Point of S;
assume x in N1; then
(reproj(i0,nx0)).x in Z by A8; then
(reproj(i0,nx0)).x in (dom f) /\ Z by A2,XBOOLE_0:def 4;
hence (reproj(i0,nx0)).x in dom(f|Z) by RELAT_1:61;
end;
reconsider N = N0 /\ N1 as Neighbourhood of x0 by Th8;
(f|Z)*reproj(i0,nx0) c= f*reproj(i0,nx0) by RELAT_1:29,59; then
A10:dom((f|Z)*reproj(i0,nx0)) c= dom(f*reproj(i0,nx0)) by RELAT_1:11;
N c= N0 by XBOOLE_1:17; then
A11:N c= dom(f*reproj(i0,nx0)) by A5,A10;
now let x be Point of S;
assume A12: x in N; then
A13: x in N0 by XBOOLE_0:def 4;
A14: dom(reproj(i0,nx0)) = the carrier of G.i0 by FUNCT_2:def 1;
x in N1 by A12,XBOOLE_0:def 4; then
A15: (reproj(i0,nx0)).x in dom(f|Z) by A9; then
A16: (reproj(i0,nx0)).x in dom f &
(reproj(i0,nx0)).x in Z by RELAT_1:57;
A17: (reproj(i0,nx0)).x0 in dom(f|Z) by A9,NFCONT_1:4; then
A18: (reproj(i0,nx0)).x0 in dom f &
(reproj(i0,nx0)).x0 in Z by RELAT_1:57;
A19: ((f|Z)*reproj(i0,nx0))/.x
=(f|Z)/.(reproj(i0,nx0)/.x) by A15,A14,PARTFUN2:4
.= f/. (reproj(i0,nx0)/.x) by A16,PARTFUN2:17
.= (f*reproj(i0,nx0))/.x by A14,A16,PARTFUN2:4;
((f|Z)*reproj(i0,nx0))/.x0
=(f|Z)/. (reproj(i0,nx0)/.x0 ) by A14,A17,PARTFUN2:4
.= f/. (reproj(i0,nx0)/.x0) by A18,PARTFUN2:17
.= (f*reproj(i0,nx0))/.x0 by A14,A18,PARTFUN2:4;
hence (f*reproj(i0,nx0))/.x-(f*reproj(i0,nx0))/.x0 =L.(x-x0)+R/.(x-x0)
by A7,A13,A19;
end;
hence f is_partial_differentiable_in nx0,i by A11,NDIFF_1:def 6;
end;
assume that
A20:Z c=dom f and
A21:for nx be Point of product G st nx in Z holds
f is_partial_differentiable_in nx,i;
now let nx0 be Point of product G;
assume A22: nx0 in Z; then
A23:f is_partial_differentiable_in nx0,i by A21;
reconsider x0=proj(i0).nx0 as Point of S;
consider N0 being Neighbourhood of x0 such that
N0 c= dom (f*reproj(i0,nx0)) and
A24: ex L be Point of RNS,R be RestFunc of S,T st
for x be Point of S st x in N0 holds
(f*reproj(i0,nx0))/.x-(f*reproj(i0,nx0))/.x0
= L.(x-x0)+R /.(x-x0) by A23,NDIFF_1:def 6;
consider N1 being Neighbourhood of x0 such that
A25: for x be Point of S st x in N1 holds
(reproj(i0,nx0)).x in Z by A1,A22,Th23;
A26:now let x be Point of S;
assume x in N1; then
(reproj(i0,nx0)).x in Z by A25; then
(reproj(i0,nx0)).x in (dom f) /\ Z by A20,XBOOLE_0:def 4;
hence (reproj(i0,nx0)).x in dom(f|Z) by RELAT_1:61;
end;
A27:N1 c= dom((f|Z)*reproj(i0,nx0))
proof
let z be object;
assume A28:z in N1; then
A29: z in the carrier of S;
reconsider x=z as Point of S by A28;
A30: (reproj(i0,nx0)).x in dom(f|Z) by A28,A26;
z in dom (reproj(i0,nx0)) by A29,FUNCT_2:def 1;
hence z in dom((f|Z)*reproj(i0,nx0)) by A30,FUNCT_1:11;
end;
reconsider N=N0 /\ N1 as Neighbourhood of x0 by Th8;
N c= N1 by XBOOLE_1:17; then
A31:N c= dom((f|Z)*reproj(i0,nx0)) by A27;
consider L be Point of RNS,R be RestFunc of S,T such that
A32: for x be Point of S st x in N0 holds
(f*reproj(i0,nx0))/.x-(f*reproj(i0,nx0))/.x0=L.(x-x0)+R/.(x-x0) by A24;
now let x be Point of S;
assume A33: x in N; then
A34: x in N0 by XBOOLE_0:def 4;
A35: dom (reproj(i0,nx0)) = the carrier of G.i0 by FUNCT_2:def 1;
x in N1 by A33,XBOOLE_0:def 4; then
A36: (reproj(i0,nx0)).x in dom(f|Z) by A26; then
A37: (reproj(i0,nx0)).x in dom f /\ Z by RELAT_1:61; then
A38: (reproj(i0,nx0)).x in dom f by XBOOLE_0:def 4;
A39: (reproj(i0,nx0)).x0 in dom(f|Z) by A26,NFCONT_1:4; then
A40: (reproj(i0,nx0)).x0 in dom f /\ Z by RELAT_1:61; then
A41: (reproj(i0,nx0)).x0 in dom f by XBOOLE_0:def 4;
A42: ((f|Z)*reproj(i0,nx0))/.x
= (f|Z)/.(reproj(i0,nx0)/.x) by A36,A35,PARTFUN2:4
.= f/.(reproj(i0,nx0)/.x) by A37,PARTFUN2:16
.= (f*reproj(i0,nx0))/.x by A35,A38,PARTFUN2:4;
((f|Z)*reproj(i0,nx0))/.x0
= (f|Z)/. (reproj(i0,nx0)/.x0 ) by A35,A39,PARTFUN2:4
.= f/. (reproj(i0,nx0)/.x0) by A40,PARTFUN2:16
.= (f*reproj(i0,nx0))/.x0 by A35,A41,PARTFUN2:4;
hence ((f|Z)*reproj(i0,nx0))/.x -((f|Z)*reproj(i0,nx0))/.x0
= L.(x-x0)+R/.(x-x0) by A42,A34,A32;
end;
hence (f|Z) is_partial_differentiable_in nx0,i by A31,NDIFF_1:def 6;
end;
hence thesis by A20;
end;
theorem
for i be set st i in dom G & f is_partial_differentiable_on X,i
holds X is Subset of product G
by XBOOLE_1:1;
definition
let G be RealNormSpace-Sequence;
let S be RealNormSpace;
let i be set;
let f be PartFunc of product G, S;
let X be set;
assume A2: f is_partial_differentiable_on X,i;
func f `partial|(X,i) -> PartFunc of product G,
R_NormSpace_of_BoundedLinearOperators(G.In(i,dom G),S) means
:Def9:
dom it = X &
for x be Point of product G st x in X holds it/.x = partdiff(f,x,i);
existence
proof
deffunc F(Element of product G) = partdiff(f,$1,i);
defpred P[Element of product G] means $1 in X;
consider F being PartFunc of product G,
R_NormSpace_of_BoundedLinearOperators(G.In(i,dom G),S) such that
A3: (for x be Point of product G holds x in dom F iff P[x]) & for x be
Point of product G st x in dom F holds F.x = F(x) from SEQ_1:sch 3;
take F;
now
A4: X is Subset of product G by A2,XBOOLE_1:1;
let y be object;
assume y in X;
hence y in dom F by A3,A4;
end; then
A5:X c= dom F;
dom F c= X by A3;
hence dom F = X by A5,XBOOLE_0:def 10;
hereby let x be Point of product G;
assume A6: x in X; then
F.x = partdiff(f,x,i) by A3;
hence F/.x = partdiff(f,x,i) by A3,A6,PARTFUN1:def 6;
end;
end;
uniqueness
proof
let F,H be PartFunc of product G,
R_NormSpace_of_BoundedLinearOperators(G.In(i,dom G),S);
assume that
A7: dom F = X and
A8: for x be Point of product G st x in X holds F/.x = partdiff(f,x,i) and
A9: dom H = X and
A10: for x be Point of product G st x in X holds H/.x = partdiff(f,x,i);
now let x be Point of product G;
assume A11: x in dom F; then
F/.x = partdiff(f,x,i) by A7,A8;
hence F/.x=H/.x by A7,A10,A11;
end;
hence thesis by A7,A9,PARTFUN2:1;
end;
end;
theorem Th26:
for i be 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
let i0 be set;
assume i0 in dom G;
set i=In(i0,dom G);
A1:dom(reproj(i,x))=the carrier of G.i by FUNCT_2:def 1;
A2:dom(f1+f2) = dom f1 /\ dom f2 by VFUNCT_1:def 1;
A3b: for s be Element of G.i holds s in dom((f1+f2)*reproj(i,x))
iff s in dom(f1*reproj(i,x)+f2*reproj(i,x))
proof
let s be Element of G.i;
s in dom((f1+f2)*reproj(i,x)) iff reproj(i,x).s in dom f1 /\ dom f2
by A2,A1,FUNCT_1:11; then
s in dom((f1+f2)*reproj(i,x))
iff reproj(i,x).s in dom f1 & reproj(i,x).s in dom f2
by XBOOLE_0:def 4; then
s in dom((f1+f2)*reproj(i,x))
iff s in dom(f1*reproj(i,x)) & s in dom(f2*reproj(i,x))
by A1,FUNCT_1:11; then
s in dom((f1+f2)*reproj(i,x))
iff s in dom(f1*reproj(i,x)) /\ dom(f2*reproj(i,x)) by XBOOLE_0:def 4;
hence thesis by VFUNCT_1:def 1;
end; then
A3:for s be object holds s in dom((f1+f2)*reproj(i,x))
iff s in dom(f1*reproj(i,x) + f2*reproj(i,x));
then
A3a:dom((f1+f2)*reproj(i,x)) = dom(f1*reproj(i,x)+f2*reproj(i,x)) by TARSKI:2;
A4:for z being Element of G.i st z in dom((f1+f2)*reproj(i,x)) holds
((f1+f2)*reproj(i,x)).z = (f1*reproj(i,x)+f2*reproj(i,x)).z
proof
let z be Element of G.i;
assume A5: z in dom((f1+f2)*reproj(i,x)); then
A6: reproj(i,x).z in dom(f1+f2) by FUNCT_1:11;
z in dom(f1*reproj(i,x)) /\ dom(f2*reproj(i,x))
by A3a,A5,VFUNCT_1:def 1; then
A7: z in dom(f1*reproj(i,x)) & z in dom(f2*reproj(i,x)) by XBOOLE_0:def 4;
A8: reproj(i,x).z in dom f1 /\ dom f2 by A2,A5,FUNCT_1:11; then
reproj(i,x).z in dom f1 by XBOOLE_0:def 4; then
A9:f1/.(reproj(i,x).z) = f1.(reproj(i,x).z) by PARTFUN1:def 6
.=(f1*reproj(i,x)).z by A7,FUNCT_1:12
.=(f1*reproj(i,x))/.z by A7,PARTFUN1:def 6;
reproj(i,x).z in dom f2 by A8,XBOOLE_0:def 4; then
A10:f2/.(reproj(i,x).z) = f2.(reproj(i,x).z) by PARTFUN1:def 6
.=(f2*reproj(i,x)).z by A7,FUNCT_1:12
.=(f2*reproj(i,x))/.z by A7,PARTFUN1:def 6;
((f1+f2)*reproj(i,x)).z = (f1+f2).(reproj(i,x).z) by A5,FUNCT_1:12
.=(f1+f2)/.(reproj(i,x).z) by A6,PARTFUN1:def 6
.= f1/.(reproj(i,x).z) +f2/.(reproj(i,x).z) by A6,VFUNCT_1:def 1
.=(f1*reproj(i,x)+ f2*reproj(i,x))/.z
by A3b,A5,A9,A10,VFUNCT_1:def 1;
hence thesis by A3b,A5,PARTFUN1:def 6;
end;
A11:
dom(f1-f2) = dom f1 /\ dom f2 by VFUNCT_1:def 2;
A12b: for s be Element of G.i holds s in dom((f1-f2)*reproj(i,x))
iff s in dom(f1*reproj(i,x)-f2*reproj(i,x))
proof
let s be Element of G.i;
s in dom((f1-f2)*reproj(i,x)) iff reproj(i,x).s in dom f1 /\ dom f2
by A11,A1,FUNCT_1:11; then
s in dom((f1-f2)*reproj(i,x))
iff reproj(i,x).s in dom f1 & reproj(i,x).s in dom f2
by XBOOLE_0:def 4; then
s in dom((f1-f2)*reproj(i,x))
iff s in dom(f1*reproj(i,x)) & s in dom(f2*reproj(i,x))
by A1,FUNCT_1:11; then
s in dom((f1-f2)*reproj(i,x))
iff s in dom(f1*reproj(i,x)) /\ dom(f2*reproj(i,x)) by XBOOLE_0:def 4;
hence thesis by VFUNCT_1:def 2;
end; then
A12: for s be object holds s in dom((f1-f2)*reproj(i,x))
iff s in dom(f1*reproj(i,x) - f2*reproj(i,x));
then
A12a:
dom((f1-f2)*reproj(i,x)) = dom(f1*reproj(i,x)-f2*reproj(i,x)) by TARSKI:2;
for z being Element of G.i st z in dom((f1-f2)*reproj(i,x)) holds
((f1-f2)*reproj(i,x)).z = (f1*reproj(i,x)-f2*reproj(i,x)).z
proof
let z be Element of G.i;
assume A13: z in dom((f1-f2)*reproj(i,x)); then
A14:reproj(i,x).z in dom (f1-f2) by FUNCT_1:11;
z in dom(f1*reproj(i,x)) /\ dom(f2*reproj(i,x))
by A12a,A13,VFUNCT_1:def 2; then
A15:z in dom(f1*reproj(i,x)) & z in dom(f2*reproj(i,x)) by XBOOLE_0:def 4;
A16:reproj(i,x).z in dom f1 /\ dom f2 by A11,A13,FUNCT_1:11; then
reproj(i,x).z in dom f1 by XBOOLE_0:def 4; then
A17:f1/.(reproj(i,x).z) = f1.(reproj(i,x).z) by PARTFUN1:def 6
.=(f1*reproj(i,x)).z by A15,FUNCT_1:12
.=(f1*reproj(i,x))/.z by A15,PARTFUN1:def 6;
reproj(i,x).z in dom f2 by A16,XBOOLE_0:def 4; then
A18:f2/.(reproj(i,x).z) = f2.(reproj(i,x).z) by PARTFUN1:def 6
.=(f2*reproj(i,x)).z by A15,FUNCT_1:12
.=(f2*reproj(i,x))/.z by A15,PARTFUN1:def 6;
thus ((f1-f2)*reproj(i,x)).z =(f1-f2).(reproj(i,x).z) by A13,FUNCT_1:12
.=(f1-f2)/.(reproj(i,x).z) by A14,PARTFUN1:def 6
.= f1/.(reproj(i,x).z) - f2/.(reproj(i,x).z) by A14,VFUNCT_1:def 2
.=(f1*reproj(i,x)- f2*reproj(i,x))/.z
by A12b,A13,A17,A18,VFUNCT_1:def 2
.=(f1*reproj(i,x)- f2*reproj(i,x)).z
by A12b,A13,PARTFUN1:def 6;
end;
hence thesis by A3,A12,A4,TARSKI:2,PARTFUN1:5;
end;
theorem Th27:
for i be set st i in dom G holds
r(#)(f*reproj(In(i,dom G),x)) = (r(#)f)*reproj(In(i,dom G),x)
proof
let i0 be set;
assume i0 in dom G;
set i=In(i0,dom G);
A1:dom(r(#)f) = dom f by VFUNCT_1:def 4;
A2:dom(r(#)(f*reproj(i,x))) =dom(f*reproj(i,x)) by VFUNCT_1:def 4;
A3:dom(reproj(i,x))=the carrier of G.i by FUNCT_2:def 1;
A4b: for s be Element of G.i holds s in dom((r(#)f)*reproj(i,x))
iff s in dom(f*reproj(i,x))
proof
let s be Element of G.i;
s in dom((r(#)f)*reproj(i,x)) iff reproj(i,x).s in dom(r(#)f)
by A3,FUNCT_1:11;
hence thesis by A1,A3,FUNCT_1:11;
end; then
A4: for s be object holds s in dom(r(#)(f*reproj(i,x)))
iff s in dom((r(#)f)*reproj(i,x)) by A2;
then
A4a:dom(r(#)(f*reproj(i,x))) =dom((r(#)f)*reproj(i,x)) by TARSKI:2;
A5:for s be Element of G.i holds s in dom((r(#)f)*reproj(i,x))
iff reproj(i,x).s in dom(r(#)f)
proof
let s be Element of G.i;
dom(reproj(i,x))=the carrier of G.i by FUNCT_2:def 1;
hence thesis by FUNCT_1:11;
end;
for z being Element of G.i st z in dom(r(#)(f*reproj(i,x))) holds
(r(#)(f*reproj(i,x))).z = ((r(#)f)*reproj(i,x)).z
proof
let z be Element of G.i;
assume A6: z in dom(r(#)(f*reproj(i,x))); then
A7: z in dom(f*reproj(i,x)) by VFUNCT_1:def 4;
A9: f/.(reproj(i,x).z) = f.(reproj(i,x).z) by A1,A5,A4a,A6,PARTFUN1:def 6
.= (f*reproj(i,x)).z by A7,FUNCT_1:12
.= (f*reproj(i,x))/.z by A7,PARTFUN1:def 6;
A10:(r(#)(f*reproj(i,x))).z =(r(#)(f*reproj(i,x)))/.z by A6,PARTFUN1:def 6
.= r * f/.(reproj(i,x).z) by A6,A9,VFUNCT_1:def 4;
((r(#)f)*reproj(i,x)).z = (r(#)f).(reproj(i,x).z)
by A2,A4b,A6,FUNCT_1:12
.= (r(#)f)/.(reproj(i,x).z) by A5,A4a,A6,PARTFUN1:def 6
.= r * f/.(reproj(i,x).z) by A5,A4a,A6,VFUNCT_1:def 4;
hence thesis by A10;
end;
hence thesis by A4,TARSKI:2,PARTFUN1:5;
end;
theorem
for i be 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
let i0 be set;
set i=In(i0,dom G);
assume A1: i0 in dom G; then
A2:(f1+f2)*reproj(i,x) = f1*reproj(i,x)+f2*reproj(i,x) by Th26;
assume
A3: f1 is_partial_differentiable_in x,i0 &
f2 is_partial_differentiable_in x,i0;
hence f1+f2 is_partial_differentiable_in x,i0 by A2,NDIFF_1:35;
thus
partdiff(f1,x,i0)+partdiff(f2,x,i0)
= diff(f1*reproj(i,x)+f2*reproj(i,x),proj(i).x) by A3,NDIFF_1:35
.= partdiff((f1+f2),x,i0) by A1,Th26;
end;
theorem
for i be 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
let i0 be set;
assume A1: i0 in dom G;
set i=In(i0,dom G);
assume A2: f1 is_partial_differentiable_in x,i0
& f2 is_partial_differentiable_in x,i0;
(f1-f2)*reproj(i,x) = f1*reproj(i,x)-f2*reproj(i,x) by A1,Th26;
hence f1-f2 is_partial_differentiable_in x,i0 by A2,NDIFF_1:36;
thus partdiff(f1,x,i0)-partdiff(f2,x,i0)
= diff(f1*reproj(i,x)-f2*reproj(i,x),proj(i).x) by A2,NDIFF_1:36
.= partdiff((f1-f2),x,i0) by A1,Th26;
end;
theorem
for i be 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
let i0 be set;
assume A1: i0 in dom G;
set i=In(i0,dom G);
assume A2: f is_partial_differentiable_in x,i0;
r(#)(f*reproj(i,x)) = (r(#)f)*reproj(i,x) by A1,Th27;
hence r(#)f is_partial_differentiable_in x,i0 by A2,NDIFF_1:37;
thus partdiff(r(#)f,x,i0) = diff(r(#)(f*reproj(i,x)),proj(i).x) by A1,Th27
.= r*partdiff(f,x,i0) by A2,NDIFF_1:37;
end;
begin :: Continuously differentiable and Partial derivative
theorem Th31:
||. proj(i).x .|| <= ||.x.||
proof
reconsider y= x as Element of product carr G by Th10;
proj(i).x = y.i by Def3;
hence thesis by PRVECT_2:10;
end;
registration
let G be RealNormSpace-Sequence;
cluster -> (len G)-element for Point of product G;
coherence
proof
let x be Point of product G;
A1: the carrier of (product G) = product carr G by Th10;
A2: dom x = dom (carr G)
& for i be set st i in dom (carr G) holds x.i in carr G.i by A1,CARD_3:9;
len carr G = len G by PRVECT_1:def 11; then
dom x= Seg len G by A2,FINSEQ_1:def 3; then
len x = len G by FINSEQ_1:def 3;
hence thesis by CARD_1:def 7;
end;
end;
theorem Th32:
for G be RealNormSpace-Sequence,
T be RealNormSpace,
i be set,
Z be Subset of product G,
f be PartFunc of product G,T
st Z is open holds
f is_partial_differentiable_on Z,i
iff
Z c=dom f &
for x be Point of product G st x in Z holds
f is_partial_differentiable_in x,i
proof
let G be RealNormSpace-Sequence,
T be RealNormSpace,
i0 be set,
Z be Subset of product G,
f be PartFunc of product G,T;
assume
A1: Z is open;
set i = In(i0,dom G);
set S=G.i;
set RNS= R_NormSpace_of_BoundedLinearOperators(S,T);
hereby
assume A2: f is_partial_differentiable_on Z,i0;
hence Z c=dom f;
let nx0 be Point of product G;
reconsider x0=proj(i).nx0 as Point of S;
assume A4: nx0 in Z; then
f|Z is_partial_differentiable_in nx0,i0 by A2; then
consider N0 being Neighbourhood of x0 such that
A5: N0 c= dom((f|Z)*reproj(i,nx0)) and
A6: ex L be Point of RNS,R be RestFunc of S,T st
for x be Point of S st x in N0 holds
((f|Z)*reproj(i,nx0))/.x-((f|Z)*reproj(i,nx0))/.x0
= L .( x-x0)+R/.(x-x0) by NDIFF_1:def 6;
consider L be Point of RNS,R be RestFunc of S,T such that
A7: for x be Point of S st x in N0 holds
((f|Z)*reproj(i,nx0))/.x - ((f|Z)*reproj(i,nx0))/.x0
= L.(x-x0) + R/.(x-x0) by A6;
consider N1 being Neighbourhood of x0 such that
A8: for x be Point of S st x in N1 holds
(reproj(i,nx0)).x in Z by A1,A4,Th23;
A9:now let x be Point of S;
assume x in N1; then
(reproj(i,nx0)).x in Z by A8; then
(reproj(i,nx0)).x in (dom f) /\ Z by A2,XBOOLE_0:def 4;
hence (reproj(i,nx0)).x in dom(f|Z) by RELAT_1:61;
end;
reconsider N = N0 /\ N1 as Neighbourhood of x0 by Th8;
(f|Z)*reproj(i,nx0) c= f*reproj(i,nx0) by RELAT_1:29,59; then
A10:dom((f|Z)*reproj(i,nx0)) c= dom(f*reproj(i,nx0)) by RELAT_1:11;
N c= N0 by XBOOLE_1:17; then
A11:N c= dom(f*reproj(i,nx0)) by A5,A10;
A12:dom(reproj(i,nx0)) = the carrier of G.i by FUNCT_2:def 1;
now let x be Point of S;
assume x in N; then
A13: x in N0 & x in N1 by XBOOLE_0:def 4; then
A14: (reproj(i,nx0)).x in dom(f|Z) by A9; then
A15: (reproj(i,nx0)).x in dom f & (reproj(i,nx0)).x in Z by RELAT_1:57;
A16: (reproj(i,nx0)).x0 in dom(f|Z) by A9,NFCONT_1:4; then
A17: (reproj(i,nx0)).x0 in dom f & (reproj(i,nx0)).x0 in Z by RELAT_1:57;
A18: ((f|Z)*reproj(i,nx0))/.x
= (f|Z)/.(reproj(i,nx0)/.x) by A14,A12,PARTFUN2:4
.= f/.(reproj(i,nx0)/.x) by A15,PARTFUN2:17
.= (f*reproj(i,nx0))/.x by A12,A15,PARTFUN2:4;
((f|Z)*reproj(i,nx0))/.x0
= (f|Z)/.(reproj(i,nx0)/.x0) by A12,A16,PARTFUN2:4
.= f/.(reproj(i,nx0)/.x0) by A17,PARTFUN2:17
.= (f*reproj(i,nx0))/.x0 by A12,A17,PARTFUN2:4;
hence (f*reproj(i,nx0))/.x-(f*reproj(i,nx0))/.x0 =L.(x-x0)+R/.(x-x0)
by A7,A13,A18;
end;
hence f is_partial_differentiable_in nx0,i0 by A11,NDIFF_1:def 6;
end;
assume that
A19:Z c=dom f and
A20:for nx be Point of product G st nx in Z holds
f is_partial_differentiable_in nx,i0;
now let nx0 be Point of product G;
assume A21: nx0 in Z; then
A22:f is_partial_differentiable_in nx0,i0 by A20;
reconsider x0=proj(i).nx0 as Point of S;
consider N0 being Neighbourhood of x0 such that
N0 c= dom (f*reproj(i,nx0)) and
A23: ex L be Point of RNS,R be RestFunc of S,T st
for x be Point of S st x in N0 holds
(f*reproj(i,nx0))/.x-(f*reproj(i,nx0))/.x0
= L.(x-x0)+R /.(x-x0) by A22,NDIFF_1:def 6;
consider N1 being Neighbourhood of x0 such that
A24: for x be Point of S st x in N1 holds
(reproj(i,nx0)).x in Z by A1,A21,Th23;
A25:now let x be Point of S;
assume x in N1; then
(reproj(i,nx0)).x in Z by A24; then
(reproj(i,nx0)).x in (dom f) /\ Z by A19,XBOOLE_0:def 4;
hence (reproj(i,nx0)).x in dom(f|Z) by RELAT_1:61;
end;
A26:N1 c= dom((f|Z)*reproj(i,nx0))
proof
let z be object;
assume A27:z in N1; then
z in the carrier of S; then
A28: z in dom (reproj(i,nx0)) by FUNCT_2:def 1;
reconsider x=z as Point of S by A27;
(reproj(i,nx0)).x in dom(f|Z) by A27,A25;
hence z in dom((f|Z)*reproj(i,nx0)) by A28,FUNCT_1:11;
end;
reconsider N=N0 /\ N1 as Neighbourhood of x0 by Th8;
N c= N1 by XBOOLE_1:17; then
A29:N c= dom((f|Z)*reproj(i,nx0)) by A26;
consider L be Point of RNS,R be RestFunc of S,T such that
A30: for x be Point of S st x in N0 holds
(f*reproj(i,nx0))/.x-(f*reproj(i,nx0))/.x0=L.(x-x0)+R/.(x-x0) by A23;
now let x be Point of S;
assume A31: x in N; then
A32: x in N0 by XBOOLE_0:def 4;
A33: dom (reproj(i,nx0)) = the carrier of G.i by FUNCT_2:def 1;
x in N1 by A31,XBOOLE_0:def 4; then
A34: (reproj(i,nx0)).x in dom(f|Z) by A25; then
A35: (reproj(i,nx0)).x in dom f /\ Z by RELAT_1:61; then
A36: (reproj(i,nx0)).x in dom f by XBOOLE_0:def 4;
A37: (reproj(i,nx0)).x0 in dom(f|Z) by A25,NFCONT_1:4; then
A38: (reproj(i,nx0)).x0 in dom f /\ Z by RELAT_1:61; then
A39: (reproj(i,nx0)).x0 in dom f by XBOOLE_0:def 4;
A40: ((f|Z)*reproj(i,nx0))/.x
= (f|Z)/. (reproj(i,nx0)/.x ) by A34,A33,PARTFUN2:4
.= f/. (reproj(i,nx0)/.x) by A35,PARTFUN2:16
.= (f*reproj(i,nx0))/.x by A33,A36,PARTFUN2:4;
((f|Z)*reproj(i,nx0))/.x0
= (f|Z)/. (reproj(i,nx0)/.x0 ) by A33,A37,PARTFUN2:4
.= f/. (reproj(i,nx0)/.x0) by A38,PARTFUN2:16
.= (f*reproj(i,nx0))/.x0 by A33,A39,PARTFUN2:4;
hence ((f|Z)*reproj(i,nx0))/.x -((f|Z)*reproj(i,nx0))/.x0
= L.(x-x0)+R/.(x-x0) by A40,A32,A30;
end;
hence (f|Z) is_partial_differentiable_in nx0,i0 by A29,NDIFF_1:def 6;
end;
hence thesis by A19;
end;
theorem Th33:
for i,j be Element of dom G,
x be Point of G.i,
z be Element of product carr G
st z= reproj(i,0.(product G)).x
holds
(i = j implies z.j = x) & (i <> j implies z.j = 0.(G.j))
proof
let i,j be Element of dom G,
x be Point of G.i,
z be Element of product carr G;
assume A1: z= reproj(i,0.(product G)).x;
reconsider Zr = 0.(product G) as Element of product carr G by Th10;
reconsider ixr = (reproj(i,0.(product G))).x
as Element of product carr G by Th10;
A2:reproj(i,0.(product G)).x = 0.(product G) +* (i,x) by Def4;
set ix= i .--> x;
consider g be Function such that
A3: Zr = g & dom g = dom carr G
& for i be object st i in dom carr G holds g.i in (carr G).i
by CARD_3:def 5;
A4:dom Zr = dom G by A3,Lm1;
now assume i <> j; then
z.j = Zr.j by A1,A2,FUNCT_7:32;
hence z.j = 0.(G.j) by Th14;
end;
hence thesis by A1,A2,A4,FUNCT_7:31;
end;
theorem Th34:
for x,y be Point of G.i
holds reproj(i,0.(product G)).(x+y)
= reproj(i,0.(product G)).x + reproj(i,0.(product G)).y
proof
let x,y be Point of G.i;
reconsider v=reproj(i,0.(product G)).(x+y) as Element of product carr G
by Th10;
reconsider s=reproj(i,0.(product G)).x as Element of product carr G
by Th10;
reconsider t=reproj(i,0.(product G)).y as Element of product carr G
by Th10;
for j be Element of dom G holds v.j=s.j + t.j
proof
let j be Element of dom G;
per cases;
suppose A1: i= j; then
reconsider yy=y as Point of G.j;
v.j = x+y by Th33,A1; then
v.j =s.j + yy by Th33,A1;
hence v.j =s.j + t.j by Th33,A1;
end;
suppose A2: i <> j; then
v.j = 0.(G.j) by Th33; then
v.j = 0.(G.j) + 0.(G.j) by RLVECT_1:def 4; then
v.j =s.j + 0.(G.j) by Th33,A2;
hence v.j =s.j + t.j by Th33,A2;
end;
end;
hence thesis by Th12;
end;
theorem Th35:
for x,y be Point of product G
holds proj(i).(x+y) = proj(i).x + proj(i).y
proof
let x,y be Point of product G;
reconsider v=x+y as Element of product carr G by Th10;
reconsider s=x as Element of product carr G by Th10;
reconsider t=y as Element of product carr G by Th10;
proj(i).(x+y)= v.i & proj(i).x = s.i & proj(i).y = t.i by Def3;
hence thesis by Th12;
end;
theorem
for x,y be Point of G.i
holds reproj(i,0.(product G)).(x-y)
= reproj(i,0.(product G)).x - reproj(i,0.(product G)).y
proof
let x,y be Point of G.i;
reconsider v=reproj(i,0.(product G)).(x-y) as Element of product carr G
by Th10;
reconsider s=reproj(i,0.(product G)).x as Element of product carr G
by Th10;
reconsider t=reproj(i,0.(product G)).y as Element of product carr G
by Th10;
for j be Element of dom G holds v.j=s.j - t.j
proof
let j be Element of dom G;
per cases;
suppose A1: i= j; then
reconsider yy=y as Point of G.j;
v.j = x-y by Th33,A1; then
v.j =s.j - yy by Th33,A1;
hence v.j =s.j - t.j by Th33,A1;
end;
suppose A2: i <> j; then
v.j = 0.(G.j) by Th33; then
v.j = 0.(G.j) - 0.(G.j) by RLVECT_1:13; then
v.j =s.j - 0.(G.j) by Th33,A2;
hence v.j =s.j - t.j by Th33,A2;
end;
end;
hence thesis by Th15;
end;
theorem Th37:
for x,y be Point of product G
holds proj(i).(x-y) = proj(i).x - proj(i).y
proof
let x,y be Point of product G;
reconsider v=x-y as Element of product carr G by Th10;
reconsider s=x as Element of product carr G by Th10;
reconsider t=y as Element of product carr G by Th10;
proj(i).(x-y)= v.i & proj(i).x = s.i & proj(i).y = t.i by Def3;
hence thesis by Th15;
end;
theorem Th38:
for x be Point of G.i st x <> 0.(G.i)
holds reproj(i,0.(product G)).x <> 0.(product G)
proof
let x be Point of G.i;
assume A1: x <> 0.(G.i);
assume A2: reproj(i,0.(product G)).x = 0.(product G);
reconsider v=reproj(i,0.(product G)).x as Element of product carr G
by Th10;
x = v.i by Th33;
hence contradiction by A1,Th14,A2;
end;
theorem Th39:
for x be Point of G.i, a be Real
holds reproj(i,0.(product G)).(a*x)
= a*(reproj(i,0.(product G)).x)
proof
let x be Point of G.i,a be Real;
reconsider a as Real;
reconsider v=reproj(i,0.(product G)).(a*x) as Element of product carr G
by Th10;
reconsider s=reproj(i,0.(product G)).x as Element of product carr G
by Th10;
for j be Element of dom G holds v.j=a*(s.j)
proof
let j be Element of dom G;
per cases;
suppose A1: i= j; then
v.j = a*x by Th33;
hence v.j =a*(s.j) by Th33,A1;
end;
suppose A2: i <> j; then
v.j = 0.(G.j) by Th33; then
v.j = a*0.(G.j) by RLVECT_1:10;
hence v.j =a*(s.j) by Th33,A2;
end;
end;
hence thesis by Th13;
end;
theorem Th40:
for x be Point of product G,a be Real
holds proj(i).(a*x) = a*(proj(i).x)
proof
let x be Point of product G,a be Real;
reconsider a as Real;
reconsider v=a*x as Element of product carr G by Th10;
reconsider s=x as Element of product carr G by Th10;
proj(i).(a*x)= v.i & proj(i).x = s.i by Def3;
hence thesis by Th13;
end;
theorem Th41:
for G be RealNormSpace-Sequence,
S be RealNormSpace,
f be PartFunc of product G, S,
x be Point of product G,
i be 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))
proof
let G be RealNormSpace-Sequence,
S be RealNormSpace,
f be PartFunc of product G, S,
x be Point of product G,
i0 be set;
assume
A1: f is_differentiable_in x;
set i=In(i0,dom G);
consider N being Neighbourhood of x such that
A2: N c= dom f &
ex R be RestFunc of product G,S st
for y be 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 be RestFunc of product G,S such that
A3: for y be 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 be 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(i,x);
reconsider x0 = proj(i).x as Point of G.i;
set Z=0.(product G);
set Nx0 = {z where z is Point of G.i: ||. z-x0 .|| < r0 };
now let s be object;
assume s in Nx0; then
ex z be Point of G.i st s=z & ||. z-x0 .|| < r0;
hence s in the carrier of G.i;
end; then
Nx0 is Subset of G.i by TARSKI:def 3; then
reconsider Nx0 as Neighbourhood of x0 by A4,NFCONT_1:def 1;
A5:for xi be Element of G.i st xi in Nx0 holds reproj(i,x).xi in N
proof
let xi be Element of G.i;
assume xi in Nx0; then
A6: ex z be Point of G.i st xi=z & ||. z-x0 .|| < r0;
reproj(i,x).xi-x = reproj(i,Z).(xi-x0) by Th22; then
||. reproj(i,x).xi-x .|| < r0 by Th21,A6; then
reproj(i,x).xi in {z where z is Point of product G : ||. z-x .|| < r0 };
hence thesis by A4;
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(i,0.(product G)) as PartFunc of G.i,S;
A9:
dom(reproj(i,0.(product G))) = the carrier of G.i by FUNCT_2:def 1;
A10:
dom R1 = the carrier of G.i by A7,PARTFUN1:def 2;
for r be Real st r > 0
ex d be Real st d > 0 &
for z be Point of G.i st z <> 0.(G.i) & ||.z.|| < d
holds (||.z.||" * ||. R1/.z .||) < r
proof
let r be Real;
assume r > 0; then
consider d be Real such that
A11: d > 0 &
for z be Point of product G st z <> 0.(product G ) & ||.z.|| < d
holds (||.z.||" * ||. R/.z .||) < r by A7,NDIFF_1:23;
take d;
now let z be Point of G.i;
assume A12: z <> 0.(G.i) & ||.z.|| < d;
A13: ||. reproj(i,Z).z .|| = ||.z.|| by Th21;
R/.(reproj(i,Z).z) = R.(reproj(i,Z).z) by A8,PARTFUN1:def 6; then
R/.(reproj(i,Z).z) =R1.z by A9,FUNCT_1:13; then
R/.(reproj(i,Z).z) =R1/.z by A10,PARTFUN1:def 6;
hence ||.z.||" * ||. R1/.z .|| < r by A11,A13,A12,Th38;
end;
hence thesis by A11;
end; then
reconsider R1 as RestFunc of G.i,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(i,0.(product G )) as Function of G.i,S;
A14:
now let x,y be Element of G.i;
LD1.(x+y) = dfx.(reproj(i,Z).(x+y)) by FUNCT_2:15; then
LD1.(x+y) =dfx.(reproj(i,Z).x+reproj(i,Z).y) by Th34; then
LD1.(x+y) =dfx.(reproj(i,Z).x)+dfx.(reproj(i,Z).y)
by VECTSP_1:def 20; then
LD1.(x+y) =LD1.x+dfx.(reproj(i,Z).y) by FUNCT_2:15;
hence LD1.(x+y) =LD1.x+LD1.y by FUNCT_2:15;
end;
now let x be Element of G.i, a be Real;
LD1.(a*x) = dfx.(reproj(i,Z).(a*x)) by FUNCT_2:15; then
LD1.(a*x) = dfx.(a*(reproj(i,Z).x)) by Th39; then
LD1.(a*x) =a*dfx.(reproj(i,Z).x) by LOPBAN_1:def 5;
hence LD1.(a*x) =a*LD1.x by FUNCT_2:15;
end; then
reconsider LD1 as LinearOperator of G.i,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;
now let r being VECTOR of G.i;
||. dfx.(reproj(i,Z).r) .|| <= K0 * ||. reproj(i,Z).r .|| by A15; then
||. dfx.(reproj(i,Z).r ) .|| <= K0 * ||.r.|| by Th21;
hence ||. LD1.r .|| <= K0 * ||.r.|| by FUNCT_2:15;
end; then
LD1 is Lipschitzian by A15; then
reconsider LD1 as Point of
R_NormSpace_of_BoundedLinearOperators(G.i,S) by LOPBAN_1:def 9;
now let s be object;
assume s in (reproj(i,x)).:Nx0; then
ex t being Element of G.i st
t in Nx0 & s = (reproj(i,x)).t by FUNCT_2:65;
hence s in dom f by A2,A5;
end; then
A16:
(reproj(i,x)).:Nx0 c= dom f;
dom(reproj(i,x)) = the carrier of G.i by FUNCT_2:def 1; then
A17:
Nx0 c= dom u by A16,FUNCT_3:3;
A18:
for y be Point of G.i st y in Nx0 holds
u/.y-u/.x0 = LD1.(y-x0) + R1/.(y-x0)
proof
let y be Point of G.i;
assume A19: y in Nx0; then
A20:reproj(i,x).y in N by A5;
A21: reproj(i,x).x0 = x +* (i,x0) by Def4;
A22: the carrier of (product G) = product carr G by Th10;
x.i=x0 by Def3,A22; then
A23:x= x +* (i,x0) by FUNCT_7:35;
A24:reproj(i,x).x0 in N by A5,NFCONT_1:4;
u/.y = u.y by A19,A17,PARTFUN1:def 6; then
u/.y = f.(reproj(i,x).y) by FUNCT_2:15; then
A25:u/.y = f/.(reproj(i,x).y) by A20,A2,PARTFUN1:def 6;
R/.(reproj(i,Z).(y-x0)) = R.(reproj(i,Z).(y-x0))
by A8,PARTFUN1:def 6; then
R/.(reproj(i,Z).(y-x0)) = R1.(y-x0) by A9,FUNCT_1:13; then
A26:R/.(reproj(i,Z).(y-x0)) = R1/.(y-x0) by A10,PARTFUN1:def 6;
x0 in Nx0 by NFCONT_1:4; then
u/.x0 = u.x0 by A17,PARTFUN1:def 6; then
u/.x0 = f.(reproj(i,x).x0) by FUNCT_2:15; then
u/.y-u/.x0 = f/.(reproj(i,x).y) -f/.x
by A25,A23,A24,A2,A21,PARTFUN1:def 6; then
u/.y-u/.x0 = diff(f,x).(reproj(i,x).y-x) + R/.(reproj(i,x).y-x)
by A3,A19,A5; then
u/.y-u/.x0 = dfx.(reproj(i,Z).(y-x0)) + R/.(reproj(i,x).y-x) by Th22; then
u/.y-u/.x0 = dfx.(reproj(i,Z).(y-x0)) + R/.(reproj(i,Z).(y-x0)) by Th22;
hence u/.y-u/.x0 = LD1.(y-x0) + R1/.(y-x0) by A26,FUNCT_2:15;
end;
hence f is_partial_differentiable_in x,i0 by A17,NDIFF_1:def 6;
u is_differentiable_in x0 by A17,A18,NDIFF_1:def 6;
hence thesis by A17,A18,NDIFF_1:def 7;
end;
Lm5:
for G be RealNormSpace-Sequence,
S be RealNormSpace,
f be PartFunc of product G,S, x be Point of product G
ex L be Lipschitzian LinearOperator of product G,S
st
for h be Element of product G
ex w be FinSequence of S st
dom w = Seg len G
& (for i be 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
let G be RealNormSpace-Sequence,
S be RealNormSpace,
f be PartFunc of product G,S,
x be Point of product G;
set m=len G;
defpred LX[set,set] means
ex w be FinSequence of S st
dom w = Seg m
& (for i be Element of NAT st i in Seg m holds
w.i = partdiff(f,x,i).(proj(In(i,dom G)).$1) )
& $2=Sum w;
A1:for v being Element of product G holds
ex y be Element of S st LX[v,y]
proof
let v being Element of product G;
defpred YX[set,set] means
ex i be Element of NAT st i=$1 &
$2 = partdiff(f,x,i).(proj(In(i,dom G)).v);
A2: for i be Nat st i in Seg m holds ex r being Element of S st YX[i,r]
proof
let i be Nat;
assume i in Seg m;
reconsider i0=i as Element of NAT by ORDINAL1:def 12;
partdiff(f,x,i0).(proj(In(i0,dom G)).v) in the carrier of S;
hence thesis;
end;
consider w be FinSequence of S such that
A3: dom w = Seg m
& for i be Nat st i in Seg m holds YX[i,w.i] from FINSEQ_1:sch 5(A2);
A4: now let i be Element of NAT;
assume i in Seg m; then
YX[i,w.i] by A3;
hence w.i = partdiff(f,x,i).(proj(In(i,dom G)).v);
end;
reconsider w0 = Sum w as Element of S;
ex w be FinSequence of S st
dom w=Seg m
& (for i be Element of NAT st i in Seg m holds
w.i = partdiff(f,x,i).(proj(In(i,dom G)).v))
& w0 = Sum w by A4,A3;
hence ex y0 be Element of S st LX[v,y0];
end;
consider L being Function of product G,S such that
A5: for h being Element of product G holds LX[h,L.h] from FUNCT_2:sch 3(A1);
A6:for s,t being Element of product G holds L.(s+t) = L.s + L.t
proof
let s,t being Element of product G;
consider w be FinSequence of S such that
A7: dom w=Seg m
& (for i be Element of NAT st i in Seg m holds
w.i = partdiff(f,x,i).(proj(In(i,dom G)).s))
& L.s = Sum w by A5;
consider v be FinSequence of S such that
A8: dom v=Seg m
& (for i be Element of NAT st i in Seg m holds
v.i = partdiff(f,x,i).(proj(In(i,dom G)).t ))
& L.t = Sum v by A5;
consider u be FinSequence of S such that
A9: dom u=Seg m
& (for i be Element of NAT st i in Seg m holds
u.i = partdiff(f,x,i).(proj(In(i,dom G)).(s+t)))
& L.(s+t) = Sum u by A5;
A10: len w = m by A7,FINSEQ_1:def 3;
A11: len v = m by A8,FINSEQ_1:def 3;
A12: len u = m by A9,FINSEQ_1:def 3;
now let i be Nat;
assume A13: i in dom w; then
A14: 1 <= i & i <= m by A7,FINSEQ_1:1; then
w/.i = w.i by A10,FINSEQ_4:15; then
A15: w/.i = partdiff(f,x,i).(proj(In(i,dom G)).s) by A7,A13;
v/.i = v.i by A14,A11,FINSEQ_4:15; then
A16: v/.i = partdiff(f,x,i).(proj(In(i,dom G)).t) by A7,A8,A13;
A17: partdiff(f,x,i) is Lipschitzian LinearOperator of G.(In(i,dom G)),S
by LOPBAN_1:def 9;
u.i = partdiff(f,x,i).(proj(In(i,dom G)).(s+t)) by A7,A9,A13; then
u.i = partdiff(f,x,i).(proj(In(i,dom G)).s + proj(In(i,dom G)).t)
by Th35;
hence u.i = w/.i + v/.i by A15,A16,A17,VECTSP_1:def 20;
end;
hence L.(s+t) = L.s + L.t by A9,A7,A8,A10,A11,A12,RLVECT_2:2;
end;
for s being Element of product G, r being Real
holds L.(r*s) = r*(L.s)
proof
let s being Element of product G, r being Real;
consider w be FinSequence of S such that
A18: dom w = Seg m
& (for i be Element of NAT st i in Seg m holds
w.i = partdiff(f,x,i).(proj(In(i,dom G)).s))
& L.s = Sum w by A5;
consider u be FinSequence of S such that
A19: dom u = Seg m
& (for i be Element of NAT st i in Seg m holds
u.i = partdiff(f,x,i).(proj(In(i,dom G)).(r*s)) )
& L.(r*s) = Sum u by A5;
A20: len w = m & len u = m by A18,A19,FINSEQ_1:def 3;
now let i be Nat;
assume A21: i in dom w; then
1 <= i & i <= m by A18,FINSEQ_1:1; then
w/.i = w.i by A20,FINSEQ_4:15; then
A22: w/.i = partdiff(f,x,i).(proj(In(i,dom G)).s ) by A18,A21;
A23: partdiff(f,x,i) is Lipschitzian LinearOperator of G.(In(i,dom G)),S
by LOPBAN_1:def 9;
u.i = partdiff(f,x,i).(proj(In(i,dom G)).(r*s)) by A18,A19,A21; then
u.i = partdiff(f,x,i).(r*proj(In(i,dom G)).s) by Th40;
hence u.i = r*(w/.i) by A22,A23,LOPBAN_1:def 5;
end;
hence L.(r*s) = r * L.s by A18,A19,A20,RLVECT_2:3;
end; then
reconsider L as LinearOperator of product G,S
by A6,LOPBAN_1:def 5,VECTSP_1:def 20;
defpred YXL[set,set] means
ex i be Element of NAT st i=$1 & $2 = ||. partdiff(f,x,i) .||;
A24:
for i be Nat st i in Seg m holds ex r being Element of REAL st YXL[i,r]
proof
let i be Nat;
assume i in Seg m;
reconsider i0=i as Element of NAT by ORDINAL1:def 12;
reconsider r = ||. partdiff(f,x,i0) .|| as Element of REAL;
YXL[i,r];
hence thesis;
end;
consider Kw be FinSequence of REAL such that
A25: dom Kw=Seg m
& for i be Nat st i in Seg m holds YXL[i,Kw.i] from FINSEQ_1:sch 5(A24);
A26:now let i be Element of NAT;
assume i in Seg m; then
YXL[i,Kw.i] by A25;
hence Kw.i = ||. partdiff(f,x,i) .||;
end;
A27:
now let i be Nat;
assume i in dom Kw; then
Kw.i = ||. partdiff(f,x,i) .|| by A26,A25;
hence 0 <= Kw.i;
end;
set LK= Sum Kw;
for s being Element of product G holds ||. L.s .|| <= LK*||. s .||
proof
let s being Element of product G;
consider w be FinSequence of S such that
A29: dom w=Seg m
& (for i be Element of NAT st i in Seg m holds
w.i = partdiff(f,x,i).(proj(In(i,dom G)).s))
& L.s = Sum w by A5;
defpred YXD[set,set] means
ex i be Element of NAT st i=$1 & $2 = ||.partdiff(f,x,i).|| * ||.s.||;
A30:for i be Nat st i in Seg m holds ex r being Element of REAL st YXD[i,r]
proof
let i be Nat;
assume i in Seg m;
reconsider i0=i as Element of NAT by ORDINAL1:def 12;
reconsider r = ||.partdiff(f,x,i0).|| * ||.s.|| as Element of REAL
by XREAL_0:def 1;
YXD[i,r];
hence thesis;
end;
consider Dw be FinSequence of REAL such that
A31:dom Dw=Seg m
& for i be Nat st i in Seg m holds YXD[i,Dw.i] from FINSEQ_1:sch 5(A30);
A32:now let i be Element of NAT;
assume i in Seg m; then
YXD[i,Dw.i] by A31;
hence Dw.i = ||.partdiff(f,x,i).|| * ||.s.||;
end;
defpred YXH[set,set] means
ex i be Element of NAT st i=$1 & $2 = ||. w/.i .||;
A33:for i be Nat st i in Seg m holds ex r being Element of REAL st YXH[i,r]
proof
let i be Nat;
assume i in Seg m;
reconsider i0=i as Element of NAT by ORDINAL1:def 12;
reconsider r = ||. w/.i0 .|| as Element of REAL;
YXH[i,r];
hence thesis;
end;
consider yseq be FinSequence of REAL such that
A34: dom yseq=Seg m
& for i be Nat st i in Seg m holds YXH[i,yseq.i] from FINSEQ_1:sch 5(A33);
A35: now let i be Element of NAT;
assume i in Seg m; then
YXH[i,yseq.i] by A34;
hence yseq.i = ||. w/.i .||;
end;
len w = len yseq by A29,A34,FINSEQ_3:29; then
A36: ||.L.s.|| <= Sum yseq by A29,A35,Th7;
m = len yseq by A34,FINSEQ_1:def 3; then
A37: yseq is Element of m-tuples_on REAL by FINSEQ_2:92;
len Dw = m by A31,FINSEQ_1:def 3; then
A38:Dw is Element of m-tuples_on REAL by FINSEQ_2:92;
now let i be Nat;
assume A39: i in Seg m; then
A40: yseq.i = ||. w/.i .|| by A35;
w/.i = w.i by A39,A29,PARTFUN1:def 6; then
A41: ||. w/.i .|| = ||.partdiff(f,x,i).(proj(In(i,dom G)).s) .||
by A29,A39;
reconsider DF1=partdiff(f,x,i) as
Lipschitzian LinearOperator of G.(In(i,dom G)),S by LOPBAN_1:def 9;
A42: ||. DF1.(proj(In(i,dom G)).s) .||
<= ||.partdiff(f,x,i).|| * ||.(proj(In(i,dom G)).s) .||
by LOPBAN_1:32;
product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop
G:], productnorm G #) by PRVECT_2:6; then
reconsider ss= s as Element of product carr G;
reconsider xi = proj(In(i,dom G)).s as Point of G.(In(i,dom G));
xi = ss.(In(i,dom G)) by Def3; then
||.partdiff(f,x,i).|| * ||.(proj(In(i,dom G)).s) .||
<=||.partdiff(f,x,i).|| * ||.s.|| by PRVECT_2:10,XREAL_1:64; then
||. w/.i .|| <= ||.partdiff(f,x,i).|| * ||.s.|| by A41,A42,XXREAL_0:2;
hence yseq.i <= Dw.i by A32,A39,A40;
end; then
A43: Sum yseq <= Sum Dw by A37,A38,RVSUM_1:82;
len Kw = m by A25,FINSEQ_1:def 3; then
reconsider KKw= Kw as Element of m-tuples_on REAL by FINSEQ_2:92;
(||.s.|| * KKw) in m-tuples_on REAL; then
ex t be Element of REAL* st t= (||.s.|| * KKw) & len t = m; then
A44: dom Dw = dom (||.s.|| * Kw) by A31,FINSEQ_1:def 3;
now let k be Nat;
assume A45: k in dom Dw; then
Dw.k = ||.partdiff(f,x,k).|| * ||.s.|| by A32,A31; then
Dw.k = ||.s.|| * Kw.k by A26,A45,A31;
hence Dw.k = (||.s.|| * Kw).k by RVSUM_1:45;
end; then
Dw = ||.s.|| * Kw by A44,FINSEQ_1:13; then
Sum Dw = (Sum Kw)* ||.s.|| by RVSUM_1:87;
hence thesis by A36,A43,XXREAL_0:2;
end; then
reconsider L as Lipschitzian LinearOperator of product G,S
by A27,RVSUM_1:84,LOPBAN_1:def 8;
take L;
thus thesis by A5;
end;
theorem Th42:
for S be RealNormSpace, h,g be FinSequence of S
st len h = len g + 1 &
(for i be Nat st i in dom g holds g/.i = h /.i - h/.(i+1)) holds
h /.1 - h/.(len h) = Sum g
proof
let S be RealNormSpace, h,g be FinSequence of S;
assume that
A1: len h = len g + 1 and
A2: for i be Nat st i in dom g holds g/.i = h/.i - h/.(i+1);
consider F be sequence of the carrier of S such that
A3: Sum g = F.(len g) & F.0 = 0.S
& for j be Nat,v be Element of S
st j < len g & v = g.(j + 1) holds F.(j + 1) = F.j + v
by RLVECT_1:def 12;
per cases;
suppose len g = 0;
hence thesis by A3,A1,RLVECT_1:15;
end;
suppose A4:len g > 0;
defpred P[Nat] means $1 <= len g implies F.$1 = h/.1 - h/.($1+1);
A5: P[1]
proof
assume A6: 1 <= len g; then
1 in Seg len g; then
A7: 1 in dom g by FINSEQ_1:def 3;
reconsider zz0=0 as Element of NAT;
g/.1 = g.( zz0 + 1 ) by A7,PARTFUN1:def 6; then
F.(zz0 + 1) = F.0 + g/.1 by A3,A6
.= g/.1 by A3,RLVECT_1:4;
hence F.1 = h/.1 - h/.(1+1) by A7,A2;
end;
A8: for j be Nat st 1 <= j holds P[j] implies P[j+1]
proof
let j be Nat;
assume 1 <= j;
assume A9: P[j];
assume A10:j+1 <= len g; then
A12: j+1 in dom g by XREAL_1:38,FINSEQ_3:25; then
A13: g.(j+1)=g/.(j+1) by PARTFUN1:def 6;
F.(j+1) = F.j + g/.(j+1) by A13,A10,A3,NAT_1:13
.=F.j + (h/.(j+1) - h/.(j+1+1)) by A2,A12
.= h/.1 - h/.(j+1) + h/.(j+1) - h/.(j+1+1)
by A9,A10,NAT_1:13,RLVECT_1:28
.= h/.1 -(h/.(j+1) - h/.(j+1)) - h/.(j+1+1) by RLVECT_1:29
.= h/.1 -0.S - h/.(j+1+1) by RLVECT_1:15;
hence thesis by RLVECT_1:13;
end;
A14:1 <= len g by A4,NAT_1:14;
for i be Nat st 1 <= i holds P[i] from NAT_1:sch 8(A5,A8);
hence thesis by A3,A1,A14;
end;
end;
theorem
for G be RealNormSpace-Sequence,
x,y be Element of product carr G, Z be set
holds x +* (y|Z) is Element of product carr G by CARD_3:79;
theorem Th44:
for G be RealNormSpace-Sequence,
x,y be Point of product G,
Z,x0 be Element of product carr G,
X be set
st Z=0.(product G) & x0=x & y= Z +* (x0|X)
holds ||.y.|| <= ||.x.||
proof
let G be RealNormSpace-Sequence,
x,y be Point of product G,
Z,x0 be Element of product carr G,
X be set;
assume A1: Z=0.(product G) & x0=x & y= Z +* (x0|X);
reconsider y0 = y as Element of product carr G by Th10;
A2: ||.y.|| = (productnorm G).y by PRVECT_2:def 13
.= |. normsequence(G,y0) .| by PRVECT_2:def 12;
A3: ||.x.|| = (productnorm G).x by PRVECT_2:def 13
.= |. normsequence(G,x0) .| by A1,PRVECT_2:def 12;
reconsider Ny = normsequence(G,y0) as (len G)-element FinSequence of REAL;
reconsider Nx = normsequence(G,x0) as (len G)-element FinSequence of REAL;
A4:len Nx = len G & len Ny = len G by CARD_1:def 7;
for k be Element of NAT st k in Seg len Ny holds 0 <= Ny.k & Ny.k <= Nx.k
proof
let k be Element of NAT;
assume A5: k in Seg len Ny; then
reconsider k1 = k as Element of dom G by CARD_1:def 7,FINSEQ_1:def 3;
x0 is Element of the carrier of (product G) by Th10; then
reconsider xx = x0 as (len G)-element FinSequence;
dom xx = Seg len G by FINSEQ_1:89; then
A6: k in dom x0 by A5,CARD_1:def 7;
reconsider yk = y0.k1, xk = x0.k1 as Element of the carrier of (G.k1);
A7: Nx.k = (the normF of G.k1).(x0.k1) by PRVECT_2:def 11;
A8: Ny.k = ||. yk .|| by PRVECT_2:def 11;
hence 0 <= Ny.k;
A9: Nx.k = ||. xk .|| by PRVECT_2:def 11;
per cases;
suppose k1 in X; then
A10: k1 in dom(x0|X) by A6,RELAT_1:57; then
y0.k1 = (x0|X).k1 by A1,FUNCT_4:13; then
y0.k1 = x0.k1 by A10,FUNCT_1:47;
hence Ny.k <= Nx.k by A7,PRVECT_2:def 11;
end;
suppose not k1 in X; then
not k1 in dom(x0|X); then
y0.k1 = Z.k1 by A1,FUNCT_4:11; then
y0.k1 = 0.(G.k1) by A1,Th14;
hence Ny.k <= Nx.k by A8,A9;
end;
end;
hence ||.y.|| <= ||.x.|| by A2,A3,A4,PRVECT_2:2;
end;
theorem Th45:
for G be RealNormSpace-Sequence,
S be RealNormSpace,
f be PartFunc of product G, S,
x,y be Point of product G
ex h be FinSequence of product G, g be FinSequence of S,
Z,y0 be Element of product carr G st
y0=y & Z = 0.(product G)
& len h = len G + 1 & len g = len G &
(for i be Nat st i in dom h holds h/.i = Z +* (y0| Seg (len G + 1-'i))) &
(for i be Nat st i in dom g holds g/.i = f/.(x+h/.i) - f/.(x+h/.(i+1))) &
(for i be Nat, hi be Point of product G st
i in dom h & h/.i= hi holds ||. hi .|| <=||. y .||) &
f /.(x+y) - f/.x = Sum g
proof
let G be RealNormSpace-Sequence,
S be RealNormSpace,
f be PartFunc of product G,S,
x,y be Point of product G;
set m= len G;
A1:
the carrier of (product G) = product carr G by Th10;
reconsider Z0 = 0.(product G) as Element of product carr G by Th10;
reconsider y0 = y as Element of product carr G by Th10;
reconsider y1=y as (len G)-element FinSequence;
reconsider Z1=0.(product G) as (len G)-element FinSequence;
len y1 = m by CARD_1:def 7; then
A2:dom y1 = dom G by FINSEQ_3:29;
len Z1 = m by CARD_1:def 7; then
A3:dom Z1 = dom G by FINSEQ_3:29;
defpred H[Nat,set] means $2=Z0 +* (y0| Seg (len G + 1-'$1));
A4:for k be Nat st k in Seg(m+1) ex x being Element of product G st H[k,x]
proof
let k be Nat;
assume k in Seg(m+1);
Z0 +* (y0| Seg (len G + 1-'k)) is Element of product carr G by CARD_3:79;
hence thesis by A1;
end;
consider h be FinSequence of product G such that
A5: dom h = Seg(m+1) &
for j being Nat st j in Seg(m+1) holds H[j,h.j] from FINSEQ_1:sch 5(A4);
A6:now let j being Nat;
assume A7: j in dom h; then
h/.j = h.j by PARTFUN1:def 6;
hence h/.j = Z0 +* (y0| Seg (len G + 1-'j)) by A7,A5;
end;
deffunc Z(Nat)=f/.(x+h/.$1);
consider z be FinSequence of S such that
A8: len z = m+1 &
for j being Nat st j in dom z holds z.j = Z(j) from FINSEQ_2:sch 1;
A9:now let j being Nat;
assume A10: j in dom z; then
z/.j = z.j by PARTFUN1:def 6;
hence z/.j = f/.(x+h/.j) by A10,A8;
end;
deffunc G(Nat) = z/.$1 - z/.($1+1);
consider g be FinSequence of S such that
A11:len g = m &
for j being Nat st j in dom g holds g.j = G(j) from FINSEQ_2:sch 1;
A12:now let j being Nat;
assume A13: j in dom g; then
g/.j = g.j by PARTFUN1:def 6;
hence g/.j = z/.j - z /.(j+1) by A13,A11;
end;
A14:m+1-'1 = m+1-1 by NAT_1:11,XREAL_1:233;
reconsider zz0=0 as Element of NAT;
1 <= m+1 by NAT_1:11; then
A15:1 in dom h by A5; then
h/.1 = Z0 +* (y0| Seg (len G + 1-'1)) by A6
.= Z0 +* (y0| dom G) by A14,FINSEQ_1:def 3
.= Z0 +* y0 by A2; then
A16:h/.1 = y by A2,A3,FUNCT_4:19;
A17:m+1-'(len z) = m+1 - len z by A8,XREAL_1:233;
1 <= len z & len z <= m+1 by A8,NAT_1:14; then
A18:len z in dom h by A5; then
A19:h/.(len z) = Z0 +* (y0| Seg 0) by A6,A17,A8
.=0.(product G);
A20:dom h= dom z by A5,A8,FINSEQ_1:def 3; then
A21:z/.1 = f/.(x+y) by A9,A16,A15;
z/.(len z) = f/. (x+h/.(len z)) by A9,A20,A18; then
A22:z/.(len z) = f/.x by A19,RLVECT_1:def 4;
take h,g,Z0,y0;
A23:now let i be Nat;
assume A24: i in dom g; then
A25:i in Seg m by A11,FINSEQ_1:def 3; then
1 <= i & i <= m by FINSEQ_1:1; then
A26:i+1 <= m+1 by XREAL_1:6;
Seg m c= Seg (m+1) by NAT_1:11,FINSEQ_1:5; then
A27:z/.i =f/.(x+h/.i) by A9,A5,A25,A20;
1 <= i+1 by NAT_1:11; then
i+1 in Seg (m+1) by A26; then
i+1 in dom z by A8,FINSEQ_1:def 3; then
z/.(i+1) =f /. (x+h/.(i+1)) by A9;
hence g/.i = f /. (x+h/.i) - f /.(x+h/.(i+1)) by A12,A24,A27;
end;
now let i be Nat, hi be Element of product G;
assume A28: i in dom h & h/.i= hi; then
h/.i = Z0 +* (y0| Seg (len G + 1-'i)) by A6;
hence ||. hi .|| <=||. y .|| by Th44,A28;
end;
hence thesis by A6,A21,A22,A23,A8,A12,Th42,A5,A11,FINSEQ_1:def 3;
end;
theorem Th46:
for G be RealNormSpace-Sequence,
i be Element of dom G,
x,y be Point of product G,
xi be Point of G.i
st y = reproj(i,x).xi holds proj(i).y = xi
proof
let G be RealNormSpace-Sequence,
i be Element of dom G, x,y be Point of product G,
xi be Point of G.i;
assume A1: y = reproj(i,x).xi;
A2:y = x +* (i,xi) by A1,Def4;
x in the carrier of product G; then
x in product carr G by Th10; then
consider g being Function such that
A3:x = g & dom g = dom carr G &
for y be object st y in dom carr G holds g.y in (carr G).y
by CARD_3:def 5;
A4:i in dom G;
A5:i in dom x by Lm1,A4,A3;
y is Element of product carr G by Th10; then
proj(i).y = (x +* (i,xi)).i by A2,Def3;
hence proj(i).y = xi by A5,FUNCT_7:31;
end;
theorem Th47:
for G be RealNormSpace-Sequence, i be Element of dom G,
y be Point of product G, q be Point of G.i
st q = proj(i).y holds y = reproj(i,y).q
proof
let G be RealNormSpace-Sequence, i be Element of dom G,
y be Point of product G, q be Point of G.i;
assume A1: q = proj(i).y;
reconsider z1 = reproj(i,y).q as (len G)-element FinSequence;
reconsider z2 = y as (len G)-element FinSequence;
A2:dom z1 = Seg len G by FINSEQ_1:89 .= dom z2 by FINSEQ_1:89;
for k be Nat st k in dom z1 holds z1.k = z2.k
proof
let k be Nat;
assume k in dom z1;
product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop
G:], productnorm G #) by PRVECT_2:6; then
A3: q = y.i by A1,Def3;
per cases;
suppose A4: k = i; then
(y +*(i,q)).k = q by A3,FUNCT_7:35;
hence z1.k = z2.k by A4,A3,Def4;
end;
suppose k <> i; then
(y +*(i,q)).k = y.k by FUNCT_7:32;
hence z1.k = z2.k by Def4;
end;
end;
hence thesis by A2,FINSEQ_1:13;
end;
theorem Th48:
for G be RealNormSpace-Sequence,
i be Element of dom G, x,y be Point of product G,
xi be Point of G.i
st y = reproj(i,x).xi holds reproj(i,x)=reproj(i,y)
proof
let G be RealNormSpace-Sequence,
i be Element of dom G, x,y be Point of product G,
xi be Point of G.i;
assume A1: y = reproj(i,x).xi;
for v be Element of G.i holds reproj(i,x).v = reproj(i,y).v
proof
let v be Element of G.i;
A2: reproj(i,x).v = x +* (i,v) & reproj(i,y).v = y +* (i,v) by Def4;
reconsider xv = reproj(i,x).v, yv = reproj(i,y).v
as (len G)-element FinSequence;
A3: dom xv = Seg len G & dom yv = Seg len G by FINSEQ_1:89; then
A4: dom xv = dom G by FINSEQ_1:def 3;
for k be Nat st k in dom xv holds xv.k = yv.k
proof
let k be Nat;
assume A5: k in dom xv;
x in the carrier of product G & y in the carrier of product G; then
A6: x in product carr G & y in product carr G by Th10; then
consider g be Function such that
A7: x = g & dom g = dom carr G
& for i be object st i in dom carr G holds g.i in (carr G).i
by CARD_3:def 5;
consider g1 be Function such that
A8: y = g1 & dom g1 = dom carr G
& for i be object st i in dom carr G holds g1.i in (carr G).i
by A6,CARD_3:def 5;
A9: k in dom y & k in dom x by A7,A8,Lm1,A5,A4;
per cases;
suppose k = i; then
(y +*(i,v)).k = v & (x +*(i,v)).k = v by A9,FUNCT_7:31;
hence yv.k = xv.k by A2;
end;
suppose A10: k <> i;
A11: yv.k = y.k & xv.k = x.k by A2,A10,FUNCT_7:32;
y = x +* (i,xi) by A1,Def4;
hence yv.k = xv.k by A11,A10,FUNCT_7:32;
end;
end;
hence reproj(i,x).v = reproj(i,y).v by A3,FINSEQ_1:13;
end;
hence thesis;
end;
theorem Th49:
for G be RealNormSpace-Sequence,
i,j be Element of dom G, x,y be Point of product G,
xi be Point of G.i
st y = reproj(i,x).xi & i <> j holds proj(j).x = proj(j).y
proof
let G be RealNormSpace-Sequence,
i,j be Element of dom G, x,y be Point of product G,
xi be Point of G.i;
assume A1: y = reproj(i,x).xi & i <> j;
reconsider y1 = y as Element of product carr G by Th10;
A2:y = x +* (i,xi) by A1,Def4;
set ix = i .--> xi;
A3: the carrier of (product G) = product carr G by Th10;
y1.j = x.j by A2,A1,FUNCT_7:32; then
proj(j).y = x.j by Def3;
hence thesis by A3,Def3;
end;
theorem
for G be RealNormSpace-Sequence,
F be RealNormSpace,
i be Element of dom G,
x be Point of product G,
xi be Point of G.i,
f be PartFunc of product G,F,
g be PartFunc of G.i,F
st proj(i).x=xi & g=f*reproj(i,x)
holds
diff(g,xi) = partdiff(f,x,i)
proof
let G be RealNormSpace-Sequence,
F be RealNormSpace,
i be Element of dom G,
x be Point of product G,
xi be Point of G.i,
f be PartFunc of product G,F,
g be PartFunc of G.i,F;
i=In(i,dom G) by SUBSET_1:def 8;
hence thesis;
end;
theorem Th51:
for G be RealNormSpace-Sequence,
F be RealNormSpace,
f be PartFunc of product G,F,
x be Point of product G,
i be set,
M be Real,
L be Point of R_NormSpace_of_BoundedLinearOperators
(G.(In(i,dom G)),F),
p,q be Point of G.(In(i,dom G))
st i in dom G
& (for h be 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 be 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 be 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
let G be RealNormSpace-Sequence,
F be RealNormSpace,
f be PartFunc of product G,F,
x be Point of product G,
i be set,
M be Real,
L be Point of R_NormSpace_of_BoundedLinearOperators
(G.(In(i,dom G)),F),
p,q be Point of G.(In(i,dom G));
assume
A1: i in dom G
& (for h be 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 be 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 be 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 );
per cases ;
suppose B2: p=q ;
set S = G.(In(i,dom G)) ;
reconsider LL=L as
Lipschitzian LinearOperator of S,F by LOPBAN_1:def 9;
B3: L.(0.S) = LL.(0 * 0.S) by RLVECT_1:10
.= 0 * LL.(0.S) by LOPBAN_1:def 5
.= 0.F by RLVECT_1:10 ;
B4:
||.f/.(reproj(In(i,dom G),x).q) - f/.(reproj(In(i,dom G),x).p)
- L.(q-p) .||
= ||. 0.F - L.(q-p) .|| by B2,RLVECT_1:15
.= ||. 0.F - L.(0.S) .|| by B2,RLVECT_1:15
.= ||. 0.F .|| by B3,RLVECT_1:13
.= 0;
M*||. q-p .|| = M * ||. 0.S .|| by B2,RLVECT_1:15
.= 0 ;
hence thesis by B4;
end;
suppose ASM: p<>q ;
set m=len G;
set S=G.(In(i,dom G));
set g=f*reproj(In(i,dom G),x);
A2:now let h be object;
assume A3: h in [. p,q .]; then
reconsider h1=h as Point of S;
A4: dom reproj(In(i,dom G),x) = the carrier of S by FUNCT_2:def 1;
reproj(In(i,dom G),x).h1 in dom f by A1,A3;
hence h in dom g by A4,FUNCT_1:11;
end; then
A5:[. p,q .] c= dom g;
A6:now let x0 be Point of S;
assume A7: x0 in [. p,q .];
set y=reproj(In(i,dom G),x).x0;
A8: proj(In(i,dom G)).y = x0 by Th46;
f is_partial_differentiable_in y,i by A1,A7;
hence g is_differentiable_in x0 by A8,Th48;
end;
X1: ]. p,q .[
= { p+t*(q-p) where t is Real : 0 < t & t < 1}
by ASM,LMOPN;
now let z be object;
assume z in ].p,q.[; then
consider z1 be Real such that A9: z=p+z1*(q-p) & 0 < z1 & z1 < 1
by X1;
z = (1-z1)*p+z1*q by A9,Lm2; then
z in {(1-r1)*p + r1*q where r1 is Real :
0 <= r1 & r1 <= 1 } by A9;
hence z in [. p,q .] by RLTOPSP1:def 2;
end; then
A10:for x be Point of S st x in ].p,q.[ holds g is_differentiable_in x by A6;
A11:for x be Point of S st x in [.p,q.] holds g is_continuous_in x
by A6,NDIFF_1:44;
A12:now let h be Point of S;
set y=reproj(In(i,dom G),x).h;
assume h in ]. p,q .[; then
A13: ||. partdiff(f,y,i) - L .|| <= M by A1;
proj(In(i,dom G)).y = h by Th46;
hence ||. diff(g,h) - L .|| <= M by A13,Th48;
end;
A14:p in dom g & q in dom g by A2,RLTOPSP1:68;
f/.(reproj(In(i,dom G),x).p) = f/.(reproj(In(i,dom G),x)/.p) &
f/.(reproj(In(i,dom G),x).q) = f/.(reproj(In(i,dom G),x)/.q); then
f/.(reproj(In(i,dom G),x).p) = g/.p &
f/.(reproj(In(i,dom G),x).q) = g/.q by A14,PARTFUN2:3;
hence ||.f/.(reproj(In(i,dom G),x).q)
- f/.(reproj(In(i,dom G),x).p) - L.(q-p) .||
<= M * ||.q-p.|| by A12,Th20,A5,A10,A11;
end;
end;
theorem Th52:
for G be RealNormSpace-Sequence,
x,y,z,w be Point of product G,
i be Element of dom G,
d be Real,
p,q,r be 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
let G be RealNormSpace-Sequence,
x,y,z,w be Point of product G,
i be Element of dom G,
d be Real,
p,q,r be Point of G.i;
assume that
A1: ||. y-x .|| < d & ||. z-x .|| < d and
A2: p= proj(i).y & z=reproj(i,y).q and
A3: r in [. p,q .] and
A4: w= reproj(i,y).r;
set wx = w-x;
set yx = y-x;
set zx = z-x;
reconsider xi = proj(i).x as Point of G.i;
r in {(1-t)*p + t*q where t is Real: 0 <= t & t <= 1 }
by A3,RLTOPSP1:def 2; then
consider t be Real such that
A5: r = (1-t)*p + t*q & 0 <= t & t <= 1;
A6: r = p + t*(q-p) & 0 <= t & t <= 1 by A5,Lm2;
reconsider wx0 = wx, yx0 = yx, zx0 = zx
as Element of product carr G by Th10;
reconsider Nwx = normsequence(G,wx0) as (len G)-element FinSequence of REAL;
reconsider Nyx = normsequence(G,yx0) as (len G)-element FinSequence of REAL;
reconsider Nzx = normsequence(G,zx0) as (len G)-element FinSequence of REAL;
set tyz = (1-t)*yx + t*zx;
reconsider tyz0 = tyz as Element of product carr G by Th10;
reconsider Ntyz = normsequence(G,tyz0)
as (len G)-element FinSequence of REAL;
A7:1 = 1-t+t;
r = p + (t*q - t*p) by A6,RLVECT_1:34
.= (p + -t*p) + t*q by RLVECT_1:def 3
.= (1*p - t*p) + t*q by RLVECT_1:def 8
.= (1-t)*p + t*q by RLVECT_1:35; then
A8:r-xi = (1-t)*p + t*q - 1*xi by RLVECT_1:def 8
.= (1-t)*p + t*q - ((1-t)*xi + t*xi) by A7,RLVECT_1:def 6
.= (1-t)*p + t*q - t*xi - (1-t)*xi by RLVECT_1:27
.= (1-t)*p +(t*q - t*xi) - (1-t)*xi by RLVECT_1:28
.= (t*q - t*xi) + ((1-t)*p - (1-t)*xi) by RLVECT_1:def 3
.= t*(q-xi) + ((1-t)*p - (1-t)*xi) by RLVECT_1:34
.= t*(q-xi) + (1-t)*(p-xi) by RLVECT_1:34;
reconsider Swx = wx as (len G)-element FinSequence;
reconsider Syz = (1-t)*yx + t*zx as (len G)-element FinSequence;
A9:dom Swx = Seg len G & dom Syz = Seg len G by FINSEQ_1:89;
A10:for k be Nat st k in dom Swx holds Swx.k = Syz.k
proof
let k be Nat;
assume k in dom Swx; then
reconsider k0 = k as Element of dom G by A9,FINSEQ_1:def 3;
per cases;
suppose A11: k = i; then
Swx.k = proj(i).wx0 by Def3; then
A12: Swx.k = proj(i).w - proj(i).x by Th37;
A13: proj(i).z = q by A2,Th46;
Syz.k = proj(i).tyz0 by A11,Def3; then
Syz.k = proj(i).((1-t)*yx) + proj(i).(t*zx) by Th35; then
Syz.k = (1-t)*(proj(i).yx) + proj(i).(t*zx) by Th40; then
Syz.k = (1-t)*(proj(i).yx) + t*proj(i).zx by Th40; then
Syz.k = (1-t)*(proj(i).y - proj(i).x) + t*proj(i).zx by Th37; then
Syz.k = (1-t)*(p-xi) + t*(q-xi) by A2,A13,Th37;
hence Swx.k = Syz.k by A12,A8,A4,Th46;
end;
suppose k <> i; then
A14: proj(k0).y = proj(k0).w & proj(k0).z = proj(k0).y by A2,A4,Th49;
Swx.k = proj(k0).wx0 by Def3; then
A15: Swx.k = proj(k0).w - proj(k0).x by Th37;
Syz.k = proj(k0).tyz0 by Def3
.= proj(k0).((1-t)*yx) + proj(k0).(t*zx) by Th35
.= (1-t)*(proj(k0).yx) + proj(k0).(t*zx) by Th40
.= (1-t)*(proj(k0).yx) + t*proj(k0).zx by Th40; then
Syz.k = (1-t)*(proj(k0).y - proj(k0).x) + t*proj(k0).zx by Th37; then
Syz.k = (1-t)*(proj(k0).y - proj(k0).x) + t*(proj(k0).y - proj(k0).x)
by A14,Th37; then
Syz.k = (1-t)*proj(k0).y - (1-t)*proj(k0).x
+ t*(proj(k0).y - proj(k0).x) by RLVECT_1:34; then
Syz.k = (1-t)*proj(k0).y - (1-t)*proj(k0).x
+ (t*proj(k0).y - t*proj(k0).x) by RLVECT_1:34; then
Syz.k = (1-t)*proj(k0).y - (1-t)*proj(k0).x
+ t*proj(k0).y - t*proj(k0).x by RLVECT_1:def 3; then
Syz.k = (1-t)*proj(k0).y
- ((1-t)*proj(k0).x - t*proj(k0).y)
- t*proj(k0).x by RLVECT_1:29; then
Syz.k = (1-t)*proj(k0).y
+ (t*proj(k0).y + - (1-t)*proj(k0).x)
- t*proj(k0).x by RLVECT_1:33; then
Syz.k = (1-t)*proj(k0).y
+ t*proj(k0).y + - (1-t)*proj(k0).x
- t*proj(k0).x by RLVECT_1:def 3; then
Syz.k = ((1-t)+t)*proj(k0).y
+ - (1-t)*proj(k0).x
- t*proj(k0).x by RLVECT_1:def 6; then
Syz.k = proj(k0).y
+ - (1-t)*proj(k0).x
- t*proj(k0).x by RLVECT_1:def 8; then
Syz.k = proj(k0).y
+ (- (1-t)*proj(k0).x - t*proj(k0).x) by RLVECT_1:28; then
Syz.k = proj(k0).y
+ (- (t*proj(k0).x + (1-t)*proj(k0).x)) by RLVECT_1:30; then
Syz.k = proj(k0).y
+ (- (t+(1-t))*proj(k0).x) by RLVECT_1:def 6;
hence Swx.k = Syz.k by A15,A14,RLVECT_1:def 8;
end;
end;
A16:len Nwx = len G & len Ntyz = len G by CARD_1:def 7;
for k be Element of NAT st k in Seg len Nwx
holds 0 <= Nwx.k & Nwx.k <= Ntyz.k
proof
let k be Element of NAT;
assume A17: k in Seg len Nwx; then
reconsider k1 = k as Element of dom G by CARD_1:def 7,FINSEQ_1:def 3;
reconsider wxk = wx0.k1 as Element of (G.k1);
A18: Nwx.k = ||. wxk .|| by PRVECT_2:def 11;
wx0.k1 = Syz.k by A10,A17,A16,A9;
hence thesis by A18,PRVECT_2:def 11;
end; then
A19: |. Nwx .| <= |. Ntyz .| by A16,PRVECT_2:2;
A20: ||. w-x .|| = (productnorm G).wx by PRVECT_2:def 13;
||. (1-t)*yx + t*zx .|| = (productnorm G).tyz by PRVECT_2:def 13
.= |. normsequence(G,tyz0) .| by PRVECT_2:def 12; then
A21: ||. w-x .|| <= ||. (1-t)*yx + t*zx .|| by A19,A20,PRVECT_2:def 12;
A22: ||. (1-t)*yx + t*zx .|| <= |.1-t.|*||. y-x .|| + |.t.|*||. z-x .||
by NORMSP_1:5;
A23: |.1-t.| = 1-t & |.t.| = t by A5,ABSVALUE:def 1,XREAL_1:48;
|.1-t.|*||. y-x .|| + |.t.|*||. z-x .|| < d
proof
per cases;
suppose t=1 or t=0;
hence thesis by A1,A23;
end;
suppose t<>1 & t<>0; then
0 < t & t < 1 by A5,XXREAL_0:1; then
0 < t & 1-t > 0 by XREAL_1:50; then
|.1-t.|*||. y-x .|| < (1-t)*d & |.t.|*||. z-x .|| < t*d
by A1,A23,XREAL_1:68; then
|.1-t.|*||. y-x .|| + |.t.|*||. z-x .|| < (1-t)*d + t*d by XREAL_1:8;
hence thesis;
end;
end; then
||. (1-t)*yx + t*zx .|| < d by A22,XXREAL_0:2;
hence ||. w-x .|| < d by A21,XXREAL_0:2;
end;
theorem Th53:
for G be RealNormSpace-Sequence,
S be RealNormSpace,
f be PartFunc of product G,S,
X be Subset of product G,
x,y,z be Point of product G,
i be set,
p,q be Point of G.(In(i,dom G)),
d,r be Real
st i in dom G & X is open & x in X &
||. y-x .|| < d & ||. z-x .|| < d & X c= dom f &
(for x be Point of product G st x in X holds
f is_partial_differentiable_in x,i) &
(for z be Point of product G st ||. z-x .|| < d holds z in X) &
(for z be Point of product G 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
let G be RealNormSpace-Sequence,
S be RealNormSpace,
f be PartFunc of product G,S,
X be Subset of product G,
x,y,z be Point of product G,
i0 be set,
p,q be Point of G.(In(i0,dom G)),
d,r be Real;
assume
A1: i0 in dom G & X is open & x in X &
||. y-x .|| < d & ||. z-x .|| < d & X c= dom f &
(for x be Point of product G st x in X holds
f is_partial_differentiable_in x,i0) &
(for z be Point of product G st ||. z-x .|| < d holds z in X) &
(for z be Point of product G st ||. z-x .|| < d
holds ||. partdiff(f,z,i0) - partdiff(f,x,i0).|| <=r) &
z = reproj(In(i0,dom G),y).p & q = proj(In(i0,dom G)).y;
set i=In(i0,dom G);
A2:y = reproj(i,y).q by A1,Th47;
A3:now let h be Point of G.i;
assume h in [. q,p .]; then
||. reproj(i,y).h - x .|| < d by A1,Th52;
hence reproj(i,y).h in dom f by A1;
end;
A4:now let h be Point of G.i;
assume h in [. q,p .]; then
||. reproj(i,y).h - x .|| < d by A1,Th52;
hence f is_partial_differentiable_in (reproj(i,y).h),i0 by A1;
end;
for h be Point of G.i st h in ]. q,p .[ holds
||. partdiff(f,reproj(i,y).h,i0) - partdiff(f,x,i0) .|| <=r
proof
let h be Point of G.i;
assume A5: h in ]. q,p .[;
].q,p.[ c= [. q,p .] by XBOOLE_1:36; then
||. reproj(i,y).h - x .|| < d by A1,A5,Th52;
hence ||. partdiff(f,reproj(i,y).h,i0) - partdiff(f,x,i0).|| <=r by A1;
end;
hence thesis by A2,A1,Th51,A3,A4;
end;
theorem Th54:
for G be RealNormSpace-Sequence,
h be FinSequence of product G,
y,x be Point of product G,
y0,Z be Element of product carr G,
j be Element of NAT
st y=y0 & Z=0.(product G)
& len h = (len G)+1 & 1 <= j & j <= len G &
(for i be 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
let G be RealNormSpace-Sequence,
h be FinSequence of product G,
y,x be Point of product G,
y0,Z be Element of product carr G,
j be Element of NAT;
assume that
A1: y = y0 and
A2: Z = 0.(product G) and
A3: len h = len G + 1 and
A4: 1 <= j & j <= len G and
A5: for i be Nat st i in dom h holds h/.i = Z +* (y0| Seg(len G + 1-'i));
len G <= len h by A3,NAT_1:11; then
j <= len h by A4,XXREAL_0:2; then
j in Seg len h by A4; then
j in dom h by FINSEQ_1:def 3; then
A6:h/.j = Z +* (y0| Seg(len G + 1 -'j)) by A5;
1 <= j+1 & j+1 <= len h by A3,A4,NAT_1:12,XREAL_1:6; then
j+1 in Seg len h; then
j+1 in dom h by FINSEQ_1:def 3; then
A7:h/.(j+1) = Z +* (y0| Seg(len G + 1-'(j+1))) by A5;
j in Seg len G by A4; then
len G -'j + 1 in Seg len G by NAT_2:6; then
len G + 1 -' j in Seg len G by A4,NAT_D:38; then
len G + 1 -' j in dom G by FINSEQ_1:def 3; then
A8:In((len G)+1-'j,dom G) = len G + 1 -' j by SUBSET_1:def 8;
set xh = x+h/.(j+1);
reconsider x1 = x, y1 = y as Element of product carr G by Th10;
reconsider xy = x + y as Element of product carr G by Th10;
xh is Element of product carr G by Th10; then
consider g being Function such that
A9:xh = g & dom g = dom carr G &
for y be object st y in dom carr G holds g.y in (carr G).y
by CARD_3:def 5;
A10:dom xh = dom G by A9,Lm1;
proj(In((len G)+1-'j,dom G)).(x+y) = xy.(len G + 1 -' j) by A8,Def3; then
A11:reproj(In((len G)+1-'j,dom G),(x+h/.(j+1)))
.(proj(In((len G)+1-'j,dom G)).(x+y))
= xh +* (In((len G)+1-'j,dom G), xy.(len G + 1 -' j)) by Def4
.= xh +* (In((len G)+1-'j,dom G) .--> xy.(len G + 1 -' j))
by A10,FUNCT_7:def 3
.= xh +* ({len G + 1 -'j} --> xy.(len G + 1 -' j)) by A8,FUNCOP_1:def 9;
reconsider F1 = x + h/.j as (len G)-element FinSequence;
reconsider F2 = reproj(In((len G)+1-'j,dom G),(x+h/.(j+1)))
.(proj(In((len G)+1-'j,dom G)).(x+y))
as (len G)-element FinSequence;
reconsider h1 = h/.j as Element of product carr G by Th10;
reconsider xh1 = x + h/.j as Element of product carr G by Th10;
reconsider h2 = h/.(j+1) as Element of product carr G by Th10;
A12:len F1 = len G & len F2 = len G by CARD_1:def 7;
for k be Nat st 1 <= k & k <= len F1 holds F1.k = F2.k
proof
let k be Nat;
assume A13: 1 <= k & k <= len F1; then
A14: k in Seg len F1; then
reconsider k1 = k as Element of dom G by CARD_1:def 7,FINSEQ_1:def 3;
proj(k1).xh1 = proj(k1).x + proj(k1).(h/.j) by Th35; then
A15: F1.k = proj(k1).x + proj(k1).(h/.j) by Def3;
y0 is Element of the carrier of product G by Th10; then
A16: dom y0 = Seg len G by FINSEQ_1:89;
A17: proj(k1).(h/.j) = h1.k by Def3;
A18: dom(y0|Seg(len G + 1-'j)) = dom y0 /\ Seg (len G + 1 -' j) by RELAT_1:61;
A19: the carrier of (product G) = product carr G by Th10;
per cases;
suppose A20: not k in Seg(len G + 1 -' j); then
not k in dom(y0|Seg(len G +1 -'j)) by A18,XBOOLE_0:def 4; then
proj(k1).(h/.j) = Z.k by A17,A6,FUNCT_4:11; then
A21: proj(k1).(h/.j) = proj(k1).(0.(product G)) by A2,Def3;
not 1 <= k or not k <= len G + 1 -' j by A20; then
not k in dom ({len G + 1 -'j} --> xy.(len G + 1 -' j))
by A13,TARSKI:def 1; then
(xh +* ({len G + 1 -'j} --> xy.(len G + 1 -' j))).k1
= xh.k1 by FUNCT_4:11; then
A22: F2.k = proj(k1).(x+h/.(j+1)) by A19,A11,Def3;
A23: proj(k1).(h/.(j+1)) = h2.k by Def3;
len G + 1-'(j+1) <= len G +1-'j by NAT_1:11,NAT_D:41; then
Seg(len G +1-'(j+1)) c= Seg(len G +1-'j) by FINSEQ_1:5; then
not k in Seg(len G+1-'(j+1)) by A20; then
not k in dom y0 /\ Seg(len G +1-'(j+1)) by XBOOLE_0:def 4; then
not k in dom(y0|Seg(len G+1-'(j+1))) by RELAT_1:61; then
(Z +* (y0| Seg(len G + 1-'(j+1)))).k = Z.k by FUNCT_4:11; then
proj(k1).(h/.(j+1)) = proj(k1).(0.(product G)) by A2,A23,A7,Def3;
hence F1.k = F2.k by A21,A15,A22,Th35;
end;
suppose A24: k in Seg(len G + 1 -' j); then
A25: k in dom(y0|Seg(len G +1 -' j)) by A18,A14,A16,A12,XBOOLE_0:def 4; then
proj(k1).(h/.j) = (y0|Seg(len G +1-'j)).k by A17,A6,FUNCT_4:13; then
proj(k1).(h/.j) = y0.k by A25,FUNCT_1:47; then
A26: proj(k1).(h/.j) = proj(k1).y by A1,Def3; then
A27: F1.k = proj(k1).(x+y) by A15,Th35;
per cases;
suppose A28: k = len G + 1 -' j;
A29: k in {k} by TARSKI:def 1; then
k in dom({k} --> xy.k); then
( xh +* ({k} --> xy.k)).k1 = ({k} --> xy.k).k by FUNCT_4:13; then
F2.k = xy.k by A11,A29,A28,FUNCOP_1:7;
hence F1.k = F2.k by A27,Def3;
end;
suppose A30: k <> len G + 1 -' j; then
not k in dom({len G + 1 -'j} --> xy.(len G +1 -'j)) by TARSKI:def 1; then
F2.k = xh.k by A11,FUNCT_4:11; then
A31: F2.k = proj(k1).(x+h/.(j+1)) by A19,Def3;
k <= len G + 1 -' j by A24,FINSEQ_1:1; then
k < len G + 1 -' j by A30,XXREAL_0:1; then
k <= len G + 1 -' j -' 1 by NAT_D:49; then
k <= len G + 1 -' (j+1) by NAT_2:30; then
k in Seg (len G+1-'(j+1)) by A13; then
A32: k in dom(y0| Seg(len G + 1-'(j+1))) by A14,A16,A12,RELAT_1:57;
proj(k1).(h/.(j+1)) = h2.k by Def3; then
proj(k1).(h/.(j+1)) = (y0| Seg(len G + 1-'(j+1))).k1
by A7,A32,FUNCT_4:13; then
proj(k1).(h/.(j+1)) = y0.k by A32,FUNCT_1:47; then
proj(k1).(h/.(j+1)) = proj(k1).y by A1,Def3;
hence F1.k = F2.k by A26,A15,A31,Th35;
end;
end;
end;
hence thesis by A12;
end;
theorem Th55:
for G be RealNormSpace-Sequence,
h be FinSequence of product G,
y,x be Point of product G,
y0,Z be Element of product carr G,
j be Element of NAT
st y=y0 & Z=0.(product G)
& len h = (len G)+1 & 1 <= j & j <= len G &
(for i be 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
let G be RealNormSpace-Sequence,
h be FinSequence of product G,
y,x be Point of product G,
y0,Z be Element of product carr G,
j be Element of NAT;
assume that
A1: y = y0 and
A2: Z=0.(product G) and
A3: len h = (len G)+1 & 1 <= j & j <= len G and
A4: for i be Nat st i in dom h holds h/.i=Z +* (y0| Seg (len G + 1-'i));
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)) by A1,A2,A3,A4,Th54; then
proj(In((len G)+1-'j,dom G)).(x+h/.j)
= proj(In((len G)+1-'j,dom G)).(x+y) by Th46; then
A5: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)).(x + h/.j - (x+h/.(j+1))) by Th37;
x + h/.j - (x + h/.(j+1))
= h/.j + x - x - h/.(j+1) by RLVECT_1:27
.= h/.j + (x - x) - h/.(j+1) by RLVECT_1:28
.= h/.j + 0.(product G) - h/.(j+1) by RLVECT_1:15
.= h/.j - h/.(j+1) by RLVECT_1:4; then
A6: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)).(h/.j)
- proj(In((len G)+1-'j,dom G)).(h/.(j+1)) by A5,Th37;
y0 is Element of the carrier of product G by Th10; then
A7:dom y0 = Seg len G by FINSEQ_1:89;
j in Seg len G by A3; then
len G -'j + 1 in Seg len G by NAT_2:6; then
A8:len G + 1 -' j in Seg len G by A3,NAT_D:38;
A9:j < len G +1 by A3,NAT_1:13; then
len G+1-'j in Seg(len G+1-'j) by FINSEQ_1:3,NAT_D:36; then
A10:len G+1-'j in dom (y0|Seg(len G+1-'j)) by A7,A8,RELAT_1:57;
len G+1-'j = len G+1-'(j+1)+1 by A9,NAT_2:7; then
A11:len G+1-'(j+1) < len G+1-'j by NAT_1:13;
dom (y0|Seg(len G+1-'(j+1))) c= Seg(len G+1-'(j+1)) by RELAT_1:58; then
A12:not len G+1-'j in dom (y0|Seg(len G+1-'(j+1))) by A11,FINSEQ_1:1;
reconsider h1 = h/.j as Element of product carr G by Th10;
reconsider h2 = h/.(j+1) as Element of product carr G by Th10;
j in Seg len h by A3,A9; then
j in dom h by FINSEQ_1:def 3; then
A13:h/.j = Z +* (y0|Seg(len G+1-'j)) by A4;
len G + 1 -' j in dom G by A8,FINSEQ_1:def 3; then
A14:In((len G)+1-'j,dom G) = len G + 1 -' j by SUBSET_1:def 8; then
A15:proj(In((len G)+1-'j,dom G)).(h/.j)
= h1.(len G+1-'j) by Def3
.= (y0|Seg(len G+1-'j)).(len G+1-'j) by A10,A13,FUNCT_4:13
.= y0.(len G +1-'j) by A10,FUNCT_1:47
.= proj(In(len G+1-'j,dom G)).y by A1,A14,Def3;
1 <= j+1 & j+1 <= len h by A3,NAT_1:12,XREAL_1:6; then
j+1 in Seg len h; then
j+1 in dom h by FINSEQ_1:def 3; then
A16:h/.(j+1) = Z +* (y0|Seg(len G+1-'(j+1))) by A4;
proj(In((len G)+1-'j,dom G)).(h/.(j+1))
= h2.(len G+1-'j) by A14,Def3
.= Z.(len G+1-'j) by A16,A12,FUNCT_4:11
.= proj(In(len G+1-'j,dom G)).(0.(product G)) by A14,A2,Def3;
hence 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 - 0.(product G)) by A6,A15,Th37
.= proj(In(len G+1-'j,dom G)).y by RLVECT_1:13;
end;
theorem Th56:
for G be RealNormSpace-Sequence,
S be RealNormSpace,
f be PartFunc of product G, S,
X be Subset of product G,
x be Point of product G
st X is open & x in X &
(for i be 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 be Point of product G
ex w be FinSequence of S st
dom w = dom G &
(for i be 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
let G be RealNormSpace-Sequence,
S be RealNormSpace,
f be PartFunc of product G, S,
X be Subset of product G,
x be Point of product G;
assume
A1: X is open & x in X &
(for i be set st i in dom G holds
f is_partial_differentiable_on X,i &
f`partial|(X,i) is_continuous_on X);
set m = len G;
A2: dom G = Seg m by FINSEQ_1:def 3;
reconsider Z0 = 0.(product G) as Element of product carr G by Th10;
reconsider x0 = x as Element of product carr G by Th10;
reconsider x1 = x as (len G)-element FinSequence;
reconsider Z1=0.(product G) as (len G)-element FinSequence;
consider L be Lipschitzian LinearOperator of product G,S such that
A3: for h be Point of product G
ex w be FinSequence of S st
dom w = Seg m &
(for i be Element of NAT st i in Seg m holds
w.i = partdiff(f,x,i).(proj(In(i,dom G)).h))
& L.h = Sum w by Lm5;
A4:
for h be Point of product G
ex w be FinSequence of S st
dom w = dom G
& (for i be set st i in dom G holds
w.i = partdiff(f,x,i).(proj(In(i,dom G)).h))
& L.h = Sum w
proof
let h be Point of product G;
consider w be FinSequence of S such that
A5: dom w = Seg m &
(for i be Element of NAT st i in Seg m holds
w.i = partdiff(f,x,i).(proj(In(i,dom G)).h))
& L.h = Sum w by A3;
take w;
thus dom w = dom G by A5,FINSEQ_1:def 3;
thus thesis by A5,A2;
end;
consider d0 be Real such that
A6: d0 >0 and
A7: {y where y is Element of product G: ||. y-x .|| < d0} c= X by A1,NDIFF_1:3;
set N = {y where y is Element of product G: ||. y-x .|| < d0};
N c= the carrier of product G by A7,XBOOLE_1:1; then
A8:
N is Neighbourhood of x by A6,NFCONT_1:def 1;
A9:
1 <= m by NAT_1:14; then
m in dom G by A2; then
f is_partial_differentiable_on X,m by A1; then
X c= dom f; then
A10:N c= dom f by A7;
deffunc RF(Element of product G) = f/.(x+$1) - f/.x - L.$1;
consider R be Function of the carrier of product G,the carrier of S
such that
A11:for h be Element of the carrier of product G holds R.h = RF(h)
from FUNCT_2:sch 4;
now let r0 be Real;
assume A12: r0 > 0;
set r1=r0/2;
set r=r1/m;
defpred DSQ[Nat, Real] means
ex k be Element of NAT st $1=k & 0 < $2 &
for q be Element of product G st q in X & ||. q-x .|| < $2 holds
||. partdiff(f,q,k)- partdiff(f,x,k) .|| < r;
A13:for k0 be Nat st k0 in Seg m holds
ex d be Element of REAL st DSQ[k0,d]
proof
let k0 be Nat;
assume A14: k0 in Seg m;
reconsider k = k0 as Element of NAT by ORDINAL1:def 12;
f`partial|(X,k) is_continuous_on X by A2,A14,A1; then
consider d be Real such that
A15: 0 < d &
for q be Point of product G st q in X & ||. q- x .|| < d holds
||. (f`partial|(X,k))/.q - (f`partial|(X,k))/.x .|| < r
by A12,A1,NFCONT_1:19;
reconsider d as Element of REAL by XREAL_0:def 1;
take d;
for q be Point of product G st q in X & ||. q-x .|| < d holds
||. partdiff(f,q,k) - partdiff(f,x,k) .|| < r
proof
let q be Point of product G;
assume A16:q in X & ||. q- x .|| < d; then
A17: ||. (f`partial|(X,k))/.q - (f`partial|(X,k))/.x .|| < r by A15;
A18: f is_partial_differentiable_on X,k by A1,A14,A2; then
(f`partial|(X,k))/.q = partdiff(f,q,k) by A16,Def9;
hence ||. partdiff(f,q,k)- partdiff(f,x,k) .|| < r
by A17,A18,A1,Def9;
end;
hence ex k be Element of NAT st k0=k & 0 < d &
for q be Element of product G st q in X & ||. q-x .|| < d holds
||. partdiff(f,q,k) - partdiff(f,x,k) .|| < r by A15;
end;
consider Dseq be FinSequence of REAL such that
A19: dom Dseq = Seg m &
for i be Nat st i in Seg m holds DSQ[i,Dseq.i] from FINSEQ_1:sch 5(A13);
m in Seg m by A9; then
reconsider rDseq = rng Dseq as non empty ext-real-membered set
by A19,FUNCT_1:3;
reconsider rDseq as left_end right_end non empty ext-real-membered set;
A20:min rDseq in rng Dseq by XXREAL_2:def 7;
reconsider d1 = min rDseq as Real;
set d = min(d0,d1);
A21: d <= d0 & d <= d1 by XXREAL_0:17;
consider i1 be object such that
A22: i1 in dom Dseq & d1 = Dseq.i1 by A20,FUNCT_1:def 3;
reconsider i1 as Nat by A22;
A23:ex k be Element of NAT st i1=k & 0 < Dseq.i1 &
for q be Element of product G st q in X & ||. q-x .|| < Dseq.i1 holds
||. partdiff(f,q,k) - partdiff(f,x,k) .|| < r by A19,A22;
A24:now let q be Element of product G;
assume ||. q-x .|| < d; then
||. q-x .|| < d0 by A21,XXREAL_0:2; then
q in {y where y is Element of product G: ||. y-x .|| < d0};
hence q in X by A7;
end;
A25:now let q be Element of product G, i be Element of NAT;
assume A26: ||. q-x .|| < d & i in Seg m;
reconsider i0=i as Nat;
consider k be Element of NAT such that
A27: i0 = k & 0 < Dseq.i0 &
for q be Element of product G st q in X & ||. q-x .|| < Dseq.i0 holds
||. partdiff(f,q,k) - partdiff(f,x,k) .|| < r by A19,A26;
Dseq.i0 in rng Dseq by A19,A26,FUNCT_1:3; then
d1 <= Dseq.i0 by XXREAL_2:def 7; then
d <= Dseq.i0 by A21,XXREAL_0:2; then
||. q-x .|| < Dseq.i0 by A26,XXREAL_0:2;
hence ||. partdiff(f,q,i) - partdiff(f,x,i) .|| < r by A24,A26,A27;
end;
take d;
thus 0 < d by A6,A22,A23,XXREAL_0:21;
thus for y be Point of product G st
y <> 0.(product G) & ||.y.|| < d holds ||.y.||"* ||. R/.y .|| < r0
proof
let y be Point of product G;
assume A28: y <> 0.(product G) & ||. y .||< d;
set z= R/.y;
consider h be FinSequence of product G, g be FinSequence of S,
Z,y0 be Element of product carr G such that
A30: y0=y & Z = 0.(product G)
& len h = len G + 1 & len g = len G
& (for i be Nat st i in dom h holds h/.i = Z +* (y0| Seg (len G + 1-'i)))
& (for i be Nat st i in dom g holds g/.i = f/.(x+h/.i) - f/.(x+h/.(i+1)))
& (for i be Nat, hi be Point of product G st
i in dom h & h/.i= hi holds ||. hi .|| <=||. y .||)
& f /.(x+y) - f/.x = Sum g by Th45;
consider w be FinSequence of S such that
A31: dom w = Seg m
& (for i be Element of NAT st i in Seg m holds
w.i = partdiff(f,x,i).(proj(In(i,dom G)).y))
& L.y = Sum w by A3;
A32: dom idseq m = Seg m & rng idseq m = Seg m; then
A33: dom Rev idseq m = Seg m & rng Rev idseq m = Seg m by FINSEQ_5:57; then
reconsider Ri=Rev idseq m as Function of Seg m,Seg m by FUNCT_2:1;
Ri is one-to-one onto by A32,FINSEQ_5:57; then
reconsider Ri=Rev idseq m as Permutation of dom w by A31;
A34: len (idseq m) = m & len w = m by A31,A32,FINSEQ_1:def 3;
dom (w * Ri) = dom Ri by A33,RELAT_1:27; then
A35: dom (w * Ri) = dom Rev w by A33,A31,FINSEQ_5:57;
reconsider wRi=w * Ri as FinSequence of S by FINSEQ_2:47;
now let k be Nat;
assume A36: k in dom Rev w; then
A37: k in dom Rev idseq m by A33,A31,FINSEQ_5:57; then
A38: 1 <= k & k <= m by A33,FINSEQ_1:1; then
reconsider mk=m-k as Nat by NAT_1:21;
reconsider zr0=0 as Nat;
0 <= mk; then
A39: zr0 + 1 <= m - k + 1 by XREAL_1:6;
k-1 >= 1-1 by A38,XREAL_1:9; then
m-(k-1) <= m by XREAL_1:43; then
A40: mk+1 in Seg m by A39;
(Rev w).k = w.(len (idseq m) - k + 1) by A34,A36,FINSEQ_5:def 3
.= w.((idseq m).(len (idseq m) - k + 1)) by A40,A34,FINSEQ_2:49
.= w.((Rev idseq m).k) by A37,FINSEQ_5:def 3;
hence (Rev w).k = wRi.k by A36,A35,FUNCT_1:12;
end; then
A41: Sum Rev w = Sum w by A35,FINSEQ_1:13,RLVECT_2:7;
deffunc GW(Nat) = g/.$1 - (Rev w)/.$1;
consider gw be FinSequence of S such that
A42: len gw =m &
for j being Nat st j in dom gw holds gw.j = GW(j) from FINSEQ_2:sch 1;
A43: now let j be Nat;
assume j in dom g; then
j in Seg m by A30,FINSEQ_1:def 3; then
j in dom gw by A42,FINSEQ_1:def 3;
hence gw.j = g/.j - (Rev w)/.j by A42;
end;
len Rev w = len g by A30,A34,FINSEQ_5:def 3; then
Sum gw = Sum g - Sum(Rev w) by A30,A42,A43,RLVECT_2:5; then
A44: R/.y = Sum gw by A11,A30,A31,A41;
A45: for j be Element of NAT st j in dom gw holds ||. gw/.j .|| <= ||. y .||*r
proof
let j be Element of NAT;
assume A46: j in dom gw; then
A47: j in Seg m by A42,FINSEQ_1:def 3; then
A48: j in dom g by A30,FINSEQ_1:def 3; then
A49: g/.j = f/.(x+h/.j) - f/.(x+h/.(j+1)) by A30;
A50: 1 <= j & j <=m by A47,FINSEQ_1:1; then
m+1 <= m+j & j+1 <= m+1 by XREAL_1:6; then
m+1-j <= m & 1 <= m+1-j by XREAL_1:19,20; then
m+1-'j <= m & 1 <= m+1-'j by A50,NAT_D:37; then
A52: m+1-'j in Seg m; then
f is_partial_differentiable_on X,(m+1-'j) by A1,A2; then
A53: X c=dom f &
for x be Element of product G st x in X holds
f is_partial_differentiable_in x,(m+1-'j) by Th24,A1;
w/.(m+1-'j) = w.(m+1-'j) by A31,A52,PARTFUN1:def 6; then
A54: w/.(m+1-'j) = (partdiff(f,x,(m+1-'j))).(proj(In(m+1-'j,dom G)).y)
by A52,A31;
A55: now let j be Element of NAT;
reconsider hj = h/.j as Element of product G;
assume 1 <= j & j <= m + 1; then
A56: ||. hj .|| <= ||. y .|| by A30,FINSEQ_3:25;
(x+h/.j)-x = h/.j + (x-x) by RLVECT_1:28
.= h/.j + 0.(product G) by RLVECT_1:15; then
(x+h/.j)-x = h/.j by RLVECT_1:4;
hence ||. (x+h/.j)-x .|| < d by A56,A28,XXREAL_0:2;
end;
Seg m c= Seg(m+1) by FINSEQ_1:5,NAT_1:11; then
1 <= j & j <= m + 1 by A47,FINSEQ_1:1; then
A57: ||. (x+h/.j)-x .|| < d by A55;
1 <= j+1 by NAT_1:11; then
A58: ||. (x+h/.(j+1))-x .|| < d by A50,A55,XREAL_1:6;
A59: x + h/.j = reproj(In(m+1-'j,dom G),(x+h/.(j+1)) )
.(proj(In(m+1-'j,dom G)).(x+y)) by Th54,A30,A50;
A60: (proj(In(m+1-'j,dom G)).(x+y))
- proj(In(m+1-'j,dom G)).(x+h/.(j+1))
= (proj(In(m+1-'j,dom G)).y) by Th55,A30,A50;
for z be Point of product G st ||. z-x .|| < d holds
||. partdiff(f,z,(m+1-'j)) - partdiff(f,x,(m+1-'j)).||
<=r by A25,A52; then
A61: ||. f/.(x+h/.j) - f/.(x+h/.(j+1))
- (partdiff(f,x,(m+1-'j))).(proj(In(m+1-'j,dom G)).y).||
<= ||.(proj(In(m+1-'j,dom G)).y).|| *r
by A1,A53,A52,A2,A24,A57,A58,A59,A60,Th53;
A62: m+1-'j = m+1-j by A50,NAT_1:12,XREAL_1:233;
j in Seg len (Rev w) by A42,A46,A34,FINSEQ_1:def 3,FINSEQ_5:def 3; then
A63: j in dom Rev w by FINSEQ_1:def 3; then
A64: (Rev w)/.j = (Rev w).j by PARTFUN1:def 6
.= w.(m-j+1) by A34,A63,FINSEQ_5:def 3
.= w/.(m+1-'j) by A62,A52,A31,PARTFUN1:def 6;
A65: gw/.j = gw.j by A46,PARTFUN1:def 6
.= f/.(x+h/.j) - f/.(x+h/.(j+1))
- (partdiff(f,x,(m+1-'j))).(proj(In(m+1-'j,dom G)).y)
by A54,A49,A64,A48,A43;
||. (proj(In(m+1-'j,dom G)).y).||*r <= ||. y .||*r
by A12,Th31,XREAL_1:64;
hence ||. gw/.j .|| <= ||. y .||*r by A65,A61,XXREAL_0:2;
end;
defpred YSQ[set,set] means $2 = ||. gw/.$1 .||;
A66: for k be Nat st k in Seg m holds
ex x be Element of REAL st YSQ[k,x];
consider yseq be FinSequence of REAL such that
A67: dom yseq = Seg m &
for i be Nat st i in Seg m holds YSQ[i,yseq.i] from FINSEQ_1:sch 5(A66);
A68: len gw = len yseq by A42,A67,FINSEQ_1:def 3;
A69: now let i be Element of NAT;
assume i in dom gw; then
i in Seg m by A42,FINSEQ_1:def 3;
hence yseq.i = ||. gw/.i .|| by A67;
end;
reconsider yseq as Element of REAL m by A68,A42,FINSEQ_2:92;
A70: ||. Sum gw .|| <= Sum yseq by A69,A68,Th7;
reconsider yr = ||. y .||*r as Element of REAL by XREAL_0:def 1;
for j be Nat st j in Seg m holds yseq.j <= (m |-> yr).j
proof
let j be Nat;
assume A71: j in Seg m; then
j in dom gw by A42,FINSEQ_1:def 3; then
A72: ||. gw/.j .|| <= ||. y .||*r by A45;
yseq.j = ||. gw/.j .|| by A67,A71;
hence yseq.j <= (m |-> yr).j by A71,A72,FINSEQ_2:57;
end; then
Sum yseq <= Sum(m |-> yr) by RVSUM_1:82; then
Sum yseq <= m*(||. y .||*r) by RVSUM_1:80; then
||. z .|| <= m*(||. y .||*r) by A44,A70,XXREAL_0:2; then
||. z .||*||.y.||" <= (m*||. y .||*r)*||.y.||" by XREAL_1:64; then
||. z .||*||.y.||" <= m*((r*||. y .||)*||.y.||"); then
||.y.||"* ||. z .|| <= m*r by A28,NORMSP_0:def 5,XCMPLX_1:203; then
A73: ||.y.||"* ||. z .|| <= r1 by XCMPLX_1:87;
r1 < r0 by A12,XREAL_1:216;
hence (||.y.||"* ||. z .||) < r0 by A73,XXREAL_0:2;
end;
end;
then reconsider R as RestFunc of product G,S by NDIFF_1:23;
reconsider L as Point of
R_NormSpace_of_BoundedLinearOperators(product G,S) by LOPBAN_1:def 9;
A74:
for y being Point of product G st y in N
holds f/.y - f/.x = L.(y-x) + R/.(y-x)
proof
let y be Point of product G;
assume y in N;
y-x in the carrier of (product G); then
y-x in dom R by PARTFUN1:def 2; then
R/.(y-x) = R.(y-x) by PARTFUN1:def 6; then
R/.(y-x) = f/.(x+(y-x)) - f/.x - L.(y-x) by A11;
hence L.(y-x) + R/.(y-x)
= f/.(x+(y-x)) - f/.x - (L.(y-x) - L.(y-x)) by RLVECT_1:29
.= f/.(x+(y-x)) - f/.x - 0.S by RLVECT_1:5
.= f/.(x+(y-x)) - f/.x by RLVECT_1:13
.= f/.(y-(x-x)) - f/.x by RLVECT_1:29
.= f/.(y-0.(product G)) - f/.x by RLVECT_1:5
.= f/.y - f/.x by RLVECT_1:13;
end; then
f is_differentiable_in x by A10,A8,NDIFF_1:def 6; then
diff(f,x) = L by A8,A10,A74,NDIFF_1:def 7;
hence thesis by A4,A74,A10,A8,NDIFF_1:def 6;
end;
theorem
for G be RealNormSpace-Sequence,
F be RealNormSpace,
f be PartFunc of product G, F,
X be Subset of product G
st X is open holds
(for i be 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
let G be RealNormSpace-Sequence,
F be RealNormSpace,
f be PartFunc of product G, F,
X be Subset of product G;
assume A1: X is open;
set m=len G;
A2: dom G = Seg m by FINSEQ_1:def 3;
hereby assume
A3: for i be set st i in dom G holds
f is_partial_differentiable_on X,i & f`partial|(X,i) is_continuous_on X;
A4: now let i be Element of NAT;
assume 1 <=i & i <= m; then
i in Seg m; then
f`partial|(X,i) is_continuous_on X by A3,A2;
hence X c= dom (f`partial|(X,i))
& for y0 be Point of product G, r be Real st y0 in X & 0<r
ex s be Real st 0<s &
for y1 be 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;
end;
A5: 1 <= m by NAT_1:14; then
m in dom G by A2; then
A6: f is_partial_differentiable_on X,m by A3;
for x be 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; then
A8: dom (f`|X) = X by NDIFF_1:def 9;
for y0 be Point of product G, r be Real st y0 in X & 0<r
ex s be Real st 0<s &
for y1 be 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, r be Real;
assume A9: y0 in X & 0<r;
defpred P[Nat,Real] means
for i being Element of NAT st i=$1 holds
(0<$2 &
for y1 be Point of product G st y1 in X & ||. y1- y0 .|| < $2 holds
||. (f`partial|(X,i))/.y1-(f`partial|(X,i))/.y0 .||<r/(2*m));
A10: now let i be Nat;
reconsider j=i as Element of NAT by ORDINAL1:def 12;
assume i in Seg m; then
1 <=j & j <= m by FINSEQ_1:1; then
consider s be Real such that
A11: 0<s &
for y1 be Point of product G st y1 in X & ||. y1- y0 .|| < s holds
||. (f`partial|(X,j))/.y1-(f`partial|(X,j))/.y0 .||<r/(2*m) by A9,A4;
reconsider s as Element of REAL by XREAL_0:def 1;
take s;
thus P[i,s] by A11;
end;
consider S being FinSequence of REAL such that
A12: dom S = Seg m
& for i be Nat st i in Seg m holds P[i,S.i] from FINSEQ_1:sch 5(A10);
take s = min S;
A13: len S = m by A12,FINSEQ_1:def 3; then
min_p S in dom S by RFINSEQ2:def 2;
hence s > 0 by A12;
let y1 be Point of product G;
assume A14: y1 in X & ||. y1- y0 .|| < s;
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 let mt be Real;
assume mt in PreNorms(DD); then
consider t being VECTOR of product G such that
A16: mt=||.DD.t.|| & ||.t.|| <= 1;
consider w0 be FinSequence of F such that
A17: dom w0 = dom G &
(for i be 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 be FinSequence of F such that
A18: dom w1 = dom G &
(for i be 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 F(set) = w1/.$1 - w0/.$1;
consider w2 being FinSequence of F such that
A19: len w2 = m & for i being Nat st i in dom w2 holds
w2.i = F(i) from FINSEQ_2:sch 1;
A20: len w1 = m & len w0 = m by A2,A17,A18,FINSEQ_1:def 3;
now let i be Nat;
assume i in dom w1; then
i in dom w2 by A19,A2,A18,FINSEQ_1:def 3;
hence w2.i = F(i) by A19;
end; 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 F(Nat) = In(||. (w2/.$1) .||,REAL);
consider ys being FinSequence of REAL such that
A22: len ys = m & for j being Nat st j in dom ys holds ys.j = F(j)
from FINSEQ_2:sch 1;
A23: now let i be Element of NAT;
assume i in dom w2; then
i in Seg m by A19,FINSEQ_1:def 3; then
i in dom ys by A22,FINSEQ_1:def 3;
hence ys.i = F(i) by A22
.= ||.w2/.i.||;
end; then
A24: ||. Sum w2 .|| <= Sum ys by A19,A22,Th7;
reconsider rm=r/(2*m) as Element of REAL by XREAL_0:def 1;
deffunc F(Nat) = rm;
consider rs being FinSequence of REAL such that
A25: len rs = m & for j being Nat st j in dom rs holds rs.j = F(j)
from FINSEQ_2:sch 1;
A26: dom rs = Seg m by A25,FINSEQ_1:def 3;
now let a be object;
assume a in rng rs; then
consider b being object such that
A27: b in dom rs & a=rs.b by FUNCT_1:def 3;
reconsider b as Nat by A27;
rs.b=rm by A27,A25;
hence a in {rm} by A27,TARSKI:def 1;
end; then
A28: rng rs c= {rm};
now let a be object;
assume a in {rm}; then
A29: a = rm by TARSKI:def 1;
A30: 1 in dom rs by A5,A26; then
a = rs.1 by A29,A25;
hence a in rng rs by A30,FUNCT_1:3;
end; then
{rm} c= rng rs; then
rs = m |-> (r/(2*m)) by A26,A28,XBOOLE_0:def 10,FUNCOP_1:9; then
Sum rs = m*(r/(2*m)) by RVSUM_1:80
.= m*(r/2/m) by XCMPLX_1:78; then
A31: Sum rs = r/2 by XCMPLX_1:87;
now let i be Element of NAT;
assume i in dom ys; then
A32: i in Seg m 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*m)
by A12,A32,A14; then
||. partdiff(f,y1,i)-(f`partial|(X,i))/.y0 .||<r/(2*m)
by Def9,A14,A37; then
A38: ||. partdiff(f,y1,i)-partdiff(f,y0,i) .||<r/(2*m)
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)
& PreNorms(PP) is non empty bounded_above by LOPBAN_1:27; then
||. PP.pt .|| <= upper_bound PreNorms(PP) by SEQ_4:def 1; then
||. P1-P0 .|| <= r/(2*m) by A40,A38,A39,XXREAL_0:2;
hence ys.i <= rs.i by A34,A25,A35,A36;
end; then
Sum ys <= r/2 by A31,A25,A22,INTEGRA5:3;
hence mt <= r/2 by A21,A24,XXREAL_0:2;
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;
end;
hence f`|X is_continuous_on X by A8,NFCONT_1:19;
end;
assume
A41:f is_differentiable_on X & f`|X is_continuous_on X; then
A42:
X c= dom f & for x be Point of product G st x in X holds
f is_differentiable_in x by A1,NDIFF_1:31;
thus for i be set st i in dom G holds
f is_partial_differentiable_on X,i & f`partial|(X,i) is_continuous_on X
proof
let i be set;
assume i in dom G; then
reconsider i0=i as Element of NAT;
now let x be Point of product G;
assume x in X; 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;
end; then
for x be 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; then
A45:dom (f`partial|(X,i)) = X by Def9;
for y0 be Point of product G, r be Real st y0 in X & 0<r
ex s be Real st 0<s & for y1 be 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, r be Real;
assume A46: y0 in X & 0<r; then
consider s be Real such that
A47: 0<s & for y1 be 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;
thus 0<s by A47;
let y1 be Point of product G;
assume A48: y1 in X & ||. y1- y0 .|| < s; 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 let a be object;
assume a in PreNorms(PP); then
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;
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;
end;
hence f`partial|(X,i) is_continuous_on X by A45,NFCONT_1:19;
end;
end;