:: The Differentiable Functions on Normed Linear Spaces :: by Hiroshi Imura , Morishige Kimura and Yasunari Shidama :: :: Received May 24, 2004 :: Copyright (c) 2004-2021 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, SUBSET_1, REAL_1, NORMSP_1, SEQ_1, NAT_1, PRE_TOPC, RCOMP_1, TARSKI, CARD_1, ARYTM_3, ARYTM_1, XXREAL_0, RELAT_1, FUNCT_1, SEQ_2, ORDINAL2, STRUCT_0, VALUED_0, SUPINF_2, RLVECT_1, VALUED_1, COMPLEX1, XXREAL_2, FDIFF_1, ZFMISC_1, PARTFUN1, FUNCOP_1, FUNCT_2, LOPBAN_1, XBOOLE_0, FCONT_1, RSSPACE, NFCONT_1, CFCONT_1, LOPBAN_2; notations TARSKI, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, PRE_TOPC, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, ORDINAL1, NUMBERS, REAL_1, NAT_1, RLVECT_1, STRUCT_0, FUNCOP_1, VALUED_0, VALUED_1, SEQ_1, SEQ_2, VFUNCT_1, NORMSP_0, NORMSP_1, RSSPACE, LOPBAN_1, LOPBAN_2, NFCONT_1, FDIFF_1, RECDEF_1; constructors REAL_1, SQUARE_1, COMPLEX1, SEQ_2, FDIFF_1, RSSPACE, VFUNCT_1, LOPBAN_3, NFCONT_1, RECDEF_1, RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2, NUMBERS; registrations FUNCT_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, FDIFF_1, STRUCT_0, LOPBAN_1, LOPBAN_2, VALUED_0, VALUED_1, FUNCT_2, FUNCOP_1, NAT_1; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; begin :: Differentiable Function on Normed Linear Spaces reserve n,k for Element of NAT; reserve x,y,X for set; reserve g,r,p for Real; reserve S for RealNormSpace; reserve rseq for Real_Sequence; reserve seq,seq1 for sequence of S; reserve x0 for Point of S; reserve Y for Subset of S; :: Normed Linear Spaces varsions of RCOMP_1:37 - :: RCOMP_1:37 --> NFCONT_1:4 theorem :: NDIFF_1:1 for x0 be Point of S for N1,N2 being Neighbourhood of x0 ex N being Neighbourhood of x0 st N c= N1 & N c= N2; theorem :: NDIFF_1:2 for X being Subset of S st X is open for r be Point of S st r in X ex N being Neighbourhood of r st N c= X; theorem :: NDIFF_1:3 for X being Subset of S st X is open for r be Point of S st r in X holds ex g st 00.S; theorem :: NDIFF_1:7 seq is non-zero iff for n being Nat holds seq.n<>0.S; definition let RNS be RealLinearSpace; let S be sequence of RNS; let a be Real_Sequence; func a (#) S -> sequence of RNS means :: NDIFF_1:def 2 for n being Nat holds it.n = a.n * S.n; end; definition let RNS be RealLinearSpace; let z be Point of RNS; let a be Real_Sequence; func a * z -> sequence of RNS means :: NDIFF_1:def 3 for n being Nat holds it.n = a.n * z; end; theorem :: NDIFF_1:8 for rseq1,rseq2 be Real_Sequence holds (rseq1+rseq2)(#)seq=rseq1(#)seq +rseq2(#)seq; theorem :: NDIFF_1:9 for rseq be Real_Sequence for seq1, seq2 be sequence of S holds rseq(#)(seq1+seq2)=rseq(#)seq1+rseq(#)seq2; theorem :: NDIFF_1:10 for rseq be Real_Sequence holds r*(rseq(#)seq) =rseq(#)(r*seq); theorem :: NDIFF_1:11 for rseq1,rseq2 be Real_Sequence holds (rseq1-rseq2)(#)seq=rseq1(#)seq -rseq2(#)seq; theorem :: NDIFF_1:12 for rseq be Real_Sequence for seq1, seq2 be sequence of S holds rseq(#)(seq1-seq2)=rseq(#)seq1-rseq(#)seq2; theorem :: NDIFF_1:13 rseq is convergent & seq is convergent implies rseq (#) seq is convergent; theorem :: NDIFF_1:14 rseq is convergent & seq is convergent implies lim (rseq (#) seq ) = (lim rseq) * (lim seq); theorem :: NDIFF_1:15 for k being Nat holds (seq+seq1) ^\k=(seq ^\k) +(seq1 ^\k); theorem :: NDIFF_1:16 (seq-seq1) ^\k=(seq ^\k) -(seq1 ^\k); theorem :: NDIFF_1:17 seq is non-zero implies seq ^\k is non-zero; definition let S; let x be Point of S; let IT be sequence of S; attr IT is x-convergent means :: NDIFF_1:def 4 IT is convergent & lim IT = x; end; theorem :: NDIFF_1:18 for X be RealNormSpace for seq be sequence of X holds seq is constant implies ( seq is convergent & for k be Element of NAT holds lim seq = seq.k ); theorem :: NDIFF_1:19 for r be Real st 0 0.S holds a*z is non-zero (0.S)-convergent; theorem :: NDIFF_1:22 (for r be Point of S holds r in Y iff r in the carrier of S) iff Y=the carrier of S; reserve S,T for RealNormSpace; reserve f,f1,f2 for PartFunc of S,T; reserve s1 for sequence of S; reserve x0 for Point of S; registration let S; cluster constant for sequence of S; end; :: Normed Linear Spaces versions of FDIFF_1 reserve h for (0.S)-convergent sequence of S; reserve c for constant sequence of S; definition let S,T; let IT be PartFunc of S,T; attr IT is RestFunc-like means :: NDIFF_1:def 5 IT is total & for h st h is non-zero holds (||.h.||")(#)(IT /*h) is convergent & lim ((||.h.||")(#)(IT/*h)) = 0.T; end; registration let S,T; cluster RestFunc-like for PartFunc of S,T; end; definition let S,T; mode RestFunc of S,T is RestFunc-like PartFunc of S,T; end; theorem :: NDIFF_1:23 for R be PartFunc of S,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 Point of S st z <> 0.S & ||.z.|| < d holds ( ||.z.||"* ||. R/.z .||) < r; theorem :: NDIFF_1:24 for R be RestFunc of S,T for s be (0.S)-convergent sequence of S st s is non-zero holds (R/*s) is convergent & lim (R/*s) = 0.T; reserve R,R1,R2 for RestFunc of S,T; reserve L,L1,L2 for Point of R_NormSpace_of_BoundedLinearOperators(S,T); theorem :: NDIFF_1:25 for h1,h2 be PartFunc of S,T for seq be sequence of S holds h1 is total & h2 is total implies (h1+h2)/*seq = h1/*seq + h2/*seq & (h1-h2)/*seq = h1/*seq - h2/*seq; theorem :: NDIFF_1:26 for h be PartFunc of S,T for seq be sequence of S for r be Real holds h is total implies (r(#)h)/*seq = r*(h/*seq); theorem :: NDIFF_1:27 f is_continuous_in x0 iff x0 in dom f & for s1 be sequence of S st rng s1 c= dom f & s1 is convergent & lim s1=x0 & (for n being Nat holds s1.n<>x0) holds f/*s1 is convergent & f/.x0=lim(f/*s1); theorem :: NDIFF_1:28 for R1,R2 holds R1+R2 is RestFunc of S,T & R1-R2 is RestFunc of S,T; theorem :: NDIFF_1:29 for r,R holds r(#)R is RestFunc of S,T; definition let S,T; let f be PartFunc of S,T; let x0 be Point of S; pred f is_differentiable_in x0 means :: NDIFF_1:def 6 ex N being Neighbourhood of x0 st N c= dom f & ex L,R st for x be Point of S st x in N holds f/.x - f/.x0 = L. (x-x0) + R/.(x-x0); end; definition let S,T; let f be PartFunc of S,T; let x0 be Point of S; assume f is_differentiable_in x0; func diff(f,x0) -> Point of R_NormSpace_of_BoundedLinearOperators(S,T) means :: NDIFF_1:def 7 ex N being Neighbourhood of x0 st N c= dom f & ex R st for x be Point of S st x in N holds f/.x-f/.x0 = it.(x-x0) + R/.(x-x0); end; definition let X; let S,T; let f be PartFunc of S,T; pred f is_differentiable_on X means :: NDIFF_1:def 8 X c=dom f & for x be Point of S st x in X holds f|X is_differentiable_in x; end; theorem :: NDIFF_1:30 for f be PartFunc of S,T holds (f is_differentiable_on X implies X is Subset of S); theorem :: NDIFF_1:31 for f be PartFunc of S,T for Z be Subset of S st Z is open holds ( f is_differentiable_on Z iff Z c=dom f & for x be Point of S st x in Z holds f is_differentiable_in x ); theorem :: NDIFF_1:32 for f be PartFunc of S,T for Y be Subset of S holds f is_differentiable_on Y implies Y is open; definition let S,T; let f be PartFunc of S,T; let X be set; assume f is_differentiable_on X; func f`|X -> PartFunc of S, R_NormSpace_of_BoundedLinearOperators(S,T) means :: NDIFF_1:def 9 dom it = X & for x be Point of S st x in X holds it/.x = diff(f,x); end; theorem :: NDIFF_1:33 for f be PartFunc of S,T for Z be Subset of S st Z is open & Z c= dom f & ex r be Point of T st rng f = {r} holds f is_differentiable_on Z & for x be Point of S st x in Z holds (f`|Z)/.x = 0.R_NormSpace_of_BoundedLinearOperators( S,T); registration let S; let h,n; cluster h^\n -> (0.S)-convergent for sequence of S; end; registration let S be non trivial RealNormSpace; let h be (0.S)-convergent non-zero sequence of S ; let n; cluster h^\n -> (0.S)-convergent non-zero for sequence of S; end; theorem :: NDIFF_1:34 for x0 be Point of S for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds for h be (0.S)-convergent sequence of S st h is non-zero holds for c st rng c = {x0} & rng (h+c) c= N holds (f/*(h+c) - f/*c) is convergent & lim (f/*(h+c) - f/*c) = 0.T; theorem :: NDIFF_1:35 for f1,f2,x0 st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds f1+f2 is_differentiable_in x0 & diff(f1+f2,x0)= diff(f1,x0)+diff(f2,x0); theorem :: NDIFF_1:36 for f1,f2,x0 st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds f1-f2 is_differentiable_in x0 & diff(f1-f2,x0)= diff(f1,x0)-diff(f2,x0); theorem :: NDIFF_1:37 for r,f,x0 st f is_differentiable_in x0 holds r(#)f is_differentiable_in x0 & diff((r(#)f),x0) = r*diff(f,x0); theorem :: NDIFF_1:38 for f be PartFunc of S,S for Z be Subset of S st Z is open & Z c= dom f & f|Z = id Z holds f is_differentiable_on Z & for x be Point of S st x in Z holds (f`|Z)/.x = id (the carrier of S); theorem :: NDIFF_1:39 for Z be Subset of S st Z is open for f1,f2 st Z c= dom (f1+f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds f1+f2 is_differentiable_on Z & for x be Point of S st x in Z holds ((f1+f2)`|Z)/.x = diff(f1,x) + diff(f2,x); theorem :: NDIFF_1:40 for Z be Subset of S st Z is open for f1,f2 st Z c= dom (f1-f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds f1-f2 is_differentiable_on Z & for x be Point of S st x in Z holds ((f1-f2)`|Z)/.x = diff(f1,x) - diff(f2,x); theorem :: NDIFF_1:41 for Z be Subset of S st Z is open for r,f st Z c= dom (r(#)f) & f is_differentiable_on Z holds r(#)f is_differentiable_on Z & for x be Point of S st x in Z holds ((r(#)f)`|Z)/.x =r*diff(f,x); theorem :: NDIFF_1:42 for Z be Subset of S st Z is open holds (Z c= dom f & f|Z is constant implies f is_differentiable_on Z & for x be Point of S st x in Z holds (f`|Z)/. x = 0.R_NormSpace_of_BoundedLinearOperators(S,T)); theorem :: NDIFF_1:43 for f be PartFunc of S,S for r be Real for p be Point of S for Z be Subset of S st Z is open holds ( Z c= dom f & (for x be Point of S st x in Z holds f/.x = r*x + p) implies f is_differentiable_on Z & for x be Point of S st x in Z holds (f`|Z)/.x = r * FuncUnit(S) ); theorem :: NDIFF_1:44 for x0 be Point of S holds f is_differentiable_in x0 implies f is_continuous_in x0; theorem :: NDIFF_1:45 f is_differentiable_on X implies f is_continuous_on X; theorem :: NDIFF_1:46 for Z be Subset of S st Z is open holds ( f is_differentiable_on X & Z c= X implies f is_differentiable_on Z ); theorem :: NDIFF_1:47 f is_differentiable_in x0 implies ex N being Neighbourhood of x0 st N c= dom f & ex R st R/.0.S=0.T & R is_continuous_in 0.S & for x be Point of S st x in N holds f/.x-f/.x0 = diff(f,x0).(x-x0) + R/.(x-x0); definition let S be non trivial RealNormSpace ,T; let IT be PartFunc of S,T; redefine attr IT is RestFunc-like means :: NDIFF_1:def 10 IT is total & for h be non-zero (0.S)-convergent sequence of S holds (||.h.||")(#)(IT /*h) is convergent & lim ((||.h.||")(#)(IT/*h)) = 0.T; end;