:: Differentiable Functions on Normed Linear Spaces :: by Yasunari Shidama :: :: Received June 2, 2011 :: Copyright (c) 2011-2018 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, PARTFUN1, CARD_1, MONOID_0, FUNCT_4, SQUARE_1; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; 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 :: NDIFF_5:1 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; theorem :: NDIFF_5:2 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.|; theorem :: NDIFF_5:3 for R be RestFunc of S for L be Lipschitzian LinearOperator of S,T holds L*R is RestFunc of T; theorem :: NDIFF_5:4 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; theorem :: NDIFF_5:5 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; theorem :: NDIFF_5:6 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); theorem :: NDIFF_5:7 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; theorem :: NDIFF_5:8 for S be RealNormSpace, x be Point of S, N1,N2 be Neighbourhood of x holds N1/\ N2 is Neighbourhood of x; theorem :: NDIFF_5:9 for X be non-empty FinSequence, x be set st x in product X holds x is FinSequence; registration let G be RealNormSpace-Sequence; cluster product G -> constituted-FinSeqs; 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; end; theorem :: NDIFF_5:10 the carrier of product G = product carr G; theorem :: NDIFF_5:11 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; definition let G be RealNormSpace-Sequence; attr G is non-trivial means :: NDIFF_5:def 1 for j be Element of dom G holds G.j is non trivial; end; registration cluster non-trivial for RealNormSpace-Sequence; end; registration let G be non-trivial RealNormSpace-Sequence; let i be Element of dom G; cluster G.i -> non trivial for RealNormSpace; end; registration let G be non-trivial RealNormSpace-Sequence; cluster product G -> non trivial; end; theorem :: NDIFF_5:12 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; theorem :: NDIFF_5:13 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); theorem :: NDIFF_5:14 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); theorem :: NDIFF_5:15 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; begin notation let S be RealLinearSpace; let p,q be Point of S; synonym [.p,q.] for LSeg(p,q); end; definition let S be RealLinearSpace; let p,q be Point of S; func ]. p,q .[ -> Subset of S equals :: NDIFF_5:def 2 [.p,q.] \ {p,q}; end; theorem :: NDIFF_5:16 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}; theorem :: NDIFF_5:17 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; theorem :: NDIFF_5:18 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; theorem :: NDIFF_5:19 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 .||; theorem :: NDIFF_5:20 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 .||; 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 :: NDIFF_5:def 3 for x be Element of product carr G holds it.x = x.i; 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 :: NDIFF_5:def 4 for r be Element of G.i holds it.r = x +* (i,r); 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 :: NDIFF_5:def 6 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 :: NDIFF_5:def 7 diff(f*reproj(In(i,dom G),x),proj(In(i,dom G)).x); 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 :: NDIFF_5:def 8 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 :: NDIFF_5:21 for xi be Element of G.i holds ||. reproj(i,0.(product G)).xi .|| = ||.xi.||; theorem :: NDIFF_5:22 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); theorem :: NDIFF_5:23 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; theorem :: NDIFF_5:24 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; theorem :: NDIFF_5:25 for i be set st i in dom G & f is_partial_differentiable_on X,i holds X is Subset of product G; 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 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 :: NDIFF_5:def 9 dom it = X & for x be Point of product G st x in X holds it/.x = partdiff(f,x,i); end; theorem :: NDIFF_5:26 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); theorem :: NDIFF_5:27 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); theorem :: NDIFF_5:28 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); theorem :: NDIFF_5:29 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); theorem :: NDIFF_5:30 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); begin :: Continuously differentiable and Partial derivative theorem :: NDIFF_5:31 ||. proj(i).x .|| <= ||.x.||; registration let G be RealNormSpace-Sequence; cluster -> (len G)-element for Point of product G; end; theorem :: NDIFF_5:32 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; theorem :: NDIFF_5:33 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)); theorem :: NDIFF_5:34 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; theorem :: NDIFF_5:35 for x,y be Point of product G holds proj(i).(x+y) = proj(i).x + proj(i).y; theorem :: NDIFF_5:36 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; theorem :: NDIFF_5:37 for x,y be Point of product G holds proj(i).(x-y) = proj(i).x - proj(i).y; theorem :: NDIFF_5:38 for x be Point of G.i st x <> 0.(G.i) holds reproj(i,0.(product G)).x <> 0.(product G); theorem :: NDIFF_5:39 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); theorem :: NDIFF_5:40 for x be Point of product G,a be Real holds proj(i).(a*x) = a*(proj(i).x); theorem :: NDIFF_5:41 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)); theorem :: NDIFF_5:42 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; theorem :: NDIFF_5:43 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; theorem :: NDIFF_5:44 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.||; theorem :: NDIFF_5:45 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; theorem :: NDIFF_5:46 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; theorem :: NDIFF_5:47 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; theorem :: NDIFF_5:48 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); theorem :: NDIFF_5:49 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; theorem :: NDIFF_5:50 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); theorem :: NDIFF_5:51 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.||; theorem :: NDIFF_5:52 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; theorem :: NDIFF_5:53 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; theorem :: NDIFF_5:54 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)); theorem :: NDIFF_5:55 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); theorem :: NDIFF_5:56 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; theorem :: NDIFF_5:57 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;