:: Complex Function Differentiability :: by Chanapat Pacharapokin , Hiroshi Yamazaki , Yasunari Shidama and Yatsuka Nakamura :: :: Received November 4, 2008 :: Copyright (c) 2008-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, XCMPLX_0, COMSEQ_1, PARTFUN1, ORDINAL2, NAT_1, FDIFF_1, VALUED_0, SEQ_2, CARD_1, SEQ_1, FUNCT_1, COMPLEX1, RELAT_1, ARYTM_3, XXREAL_0, ARYTM_1, FUNCOP_1, VALUED_1, FUNCT_2, TARSKI, RCOMP_1, XBOOLE_0, FCONT_1, CFCONT_1, XXREAL_2, CFDIFF_1, FUNCT_7, ASYMPT_1; notations TARSKI, SUBSET_1, ORDINAL1, FUNCT_1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, PARTFUN1, FUNCT_2, FUNCOP_1, VALUED_0, VALUED_1, SEQ_1, RELSET_1, SEQ_2, CFUNCT_1, COMSEQ_1, COMSEQ_2, COMSEQ_3, CFCONT_1, XXREAL_0; constructors PARTFUN1, REAL_1, NAT_1, VALUED_0, VALUED_1, SEQ_2, FINSEQ_4, SEQM_3, PARTFUN2, SQUARE_1, COMSEQ_2, COMSEQ_3, CFCONT_1, XXREAL_0, CFUNCT_1, RELSET_1, SEQ_1; registrations FUNCT_1, RELSET_1, FUNCT_2, MEMBERED, NUMBERS, ORDINAL1, XREAL_0, XXREAL_0, COMSEQ_2, NAT_1, VALUED_0, VALUED_1, FUNCOP_1, XCMPLX_0, SEQ_2, CFUNCT_1, SEQ_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve k, k1, n, n1, m for Nat; reserve X, y for set; reserve p for Real; reserve r for Real; reserve a, a1, a2, b, b1, b2, x, x0, z, z0 for Complex; reserve s1, s3, seq, seq1 for Complex_Sequence; reserve Y for Subset of COMPLEX; reserve f, f1, f2 for PartFunc of COMPLEX,COMPLEX; reserve Nseq for increasing sequence of NAT; definition let x be Real; let IT be Complex_Sequence; attr IT is x-convergent means :: CFDIFF_1:def 1 IT is convergent & lim IT = x; end; theorem :: CFDIFF_1:1 for rs be Real_Sequence, cs be Complex_Sequence st rs = cs & rs is convergent holds cs is convergent; definition let r be Real; func InvShift(r) -> Complex_Sequence means :: CFDIFF_1:def 2 for n holds it.n = 1/(n+r); end; theorem :: CFDIFF_1:2 0 < r implies InvShift(r) is convergent; registration let r be positive Real; cluster InvShift(r) -> convergent; end; theorem :: CFDIFF_1:3 0 < r implies lim InvShift(r) = 0; registration let r be positive Real; cluster InvShift(r) -> non-zero 0-convergent; end; registration cluster 0-convergent non-zero for Complex_Sequence; end; registration cluster 0-convergent non-zero -> convergent for Complex_Sequence; end; registration cluster constant for Complex_Sequence; end; theorem :: CFDIFF_1:4 seq is constant iff for n,m holds seq.n = seq.m; theorem :: CFDIFF_1:5 for n holds (seq*Nseq).n = seq.(Nseq.n); reserve h for 0-convergent non-zero Complex_Sequence; reserve c for constant Complex_Sequence; definition let IT be PartFunc of COMPLEX,COMPLEX; attr IT is RestFunc-like means :: CFDIFF_1:def 3 for h holds (h")(#)(IT/*h) is convergent & lim ((h")(#)(IT/*h)) = 0; end; registration cluster total RestFunc-like for PartFunc of COMPLEX,COMPLEX; end; definition mode C_RestFunc is total RestFunc-like PartFunc of COMPLEX,COMPLEX; end; definition let IT be PartFunc of COMPLEX,COMPLEX; attr IT is linear means :: CFDIFF_1:def 4 ex a st for z holds IT/.z = a*z; end; registration cluster total linear for PartFunc of COMPLEX,COMPLEX; end; definition mode C_LinearFunc is total linear PartFunc of COMPLEX,COMPLEX; end; reserve R, R1, R2 for C_RestFunc; reserve L, L1, L2 for C_LinearFunc; registration let L1,L2; cluster L1+L2 -> total linear for PartFunc of COMPLEX,COMPLEX; cluster L1-L2 -> total linear for PartFunc of COMPLEX,COMPLEX; end; registration let a,L; cluster a(#)L -> total linear for PartFunc of COMPLEX,COMPLEX; end; registration let R1,R2; cluster R1+R2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX; cluster R1-R2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX; cluster R1(#)R2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX; end; registration let a,R; cluster a(#)R -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX; end; registration let L1,L2; cluster L1(#)L2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX; end; registration let R,L; cluster R(#)L -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX; cluster L(#)R -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX; end; definition let z0 be Complex; mode Neighbourhood of z0 -> Subset of COMPLEX means :: CFDIFF_1:def 5 ex g be Real st 0 < g & {y where y is Complex : |.y-z0.| < g} c= it; end; theorem :: CFDIFF_1:6 for g be Real st 0 < g holds {y where y is Complex : |.y-z0.| < g} is Neighbourhood of z0; theorem :: CFDIFF_1:7 for N being Neighbourhood of z0 holds z0 in N; definition let f; let z0 be Complex; pred f is_differentiable_in z0 means :: CFDIFF_1:def 6 ex N being Neighbourhood of z0 st N c= dom f & ex L,R st for z st z in N holds f/.z-f/.z0 = L/.(z-z0)+R/.(z-z0); end; definition let f; let z0 be Complex; assume f is_differentiable_in z0; func diff(f,z0) -> Element of COMPLEX means :: CFDIFF_1:def 7 ex N being Neighbourhood of z0 st N c= dom f & ex L,R st it = L/.1r & for z st z in N holds f/.z-f/.z0 = L/.(z-z0)+R/.(z-z0); end; definition let f; attr f is differentiable means :: CFDIFF_1:def 8 for x st x in dom f holds f is_differentiable_in x; end; definition let f,X; pred f is_differentiable_on X means :: CFDIFF_1:def 9 X c= dom f & f|X is differentiable; end; theorem :: CFDIFF_1:8 f is_differentiable_on X implies X is Subset of COMPLEX; definition :: complex-membered set let X be Subset of COMPLEX; attr X is closed means :: CFDIFF_1:def 10 for s1 be Complex_Sequence st rng s1 c= X & s1 is convergent holds lim s1 in X; end; definition let X be Subset of COMPLEX; attr X is open means :: CFDIFF_1:def 11 X` is closed; end; theorem :: CFDIFF_1:9 for X being Subset of COMPLEX st X is open for z0 be Complex st z0 in X ex N being Neighbourhood of z0 st N c= X; theorem :: CFDIFF_1:10 for X being Subset of COMPLEX st X is open for z0 be Complex st z0 in X holds ex g be Real st {y where y is Complex : |.y-z0.| < g} c= X; theorem :: CFDIFF_1:11 for X being Subset of COMPLEX holds ((for z0 be Complex st z0 in X holds ex N be Neighbourhood of z0 st N c= X) implies X is open); theorem :: CFDIFF_1:12 for X be Subset of COMPLEX holds X is open iff for x be Complex st x in X ex N be Neighbourhood of x st N c= X; theorem :: CFDIFF_1:13 for X be Subset of COMPLEX, z0 be Element of COMPLEX, r be Real st X = {y where y is Complex : |.y-z0.| < r} holds X is open; theorem :: CFDIFF_1:14 for X be Subset of COMPLEX, z0 be Element of COMPLEX, r be Real st X = {y where y is Complex : |.y-z0.| <= r} holds X is closed; registration cluster open for Subset of COMPLEX; end; reserve Z for open Subset of COMPLEX; theorem :: CFDIFF_1:15 f is_differentiable_on Z iff Z c= dom f & for x st x in Z holds f is_differentiable_in x; theorem :: CFDIFF_1:16 f is_differentiable_on Y implies Y is open; definition let f, X; assume f is_differentiable_on X; func f`|X -> PartFunc of COMPLEX,COMPLEX means :: CFDIFF_1:def 12 dom it = X & for x st x in X holds it/.x = diff(f,x); end; theorem :: CFDIFF_1:17 for f,Z st Z c= dom f & ex a1 st rng f = {a1} holds f is_differentiable_on Z & for x st x in Z holds (f`|Z)/.x = 0c; registration let seq be non-zero Complex_Sequence, k be Nat; cluster seq ^\k -> non-zero; end; registration let h,n; cluster h^\n -> 0-convergent for Complex_Sequence; end; theorem :: CFDIFF_1:18 (seq+seq1)^\k = (seq^\k)+(seq1^\k); theorem :: CFDIFF_1:19 (seq-seq1)^\k = (seq^\k)-(seq1^\k); theorem :: CFDIFF_1:20 (seq")^\k = (seq^\k)"; theorem :: CFDIFF_1:21 (seq(#)seq1)^\k = (seq^\k)(#)(seq1^\k); theorem :: CFDIFF_1:22 for x0 be Complex for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds for h,c st rng c = {x0} & rng (h+c) c= N holds h"(#)(f/*(h+c)-f/*c) is convergent & diff(f,x0) = lim (h"(#)(f/*(h+c )-f/*c)); theorem :: CFDIFF_1:23 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 :: CFDIFF_1:24 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 :: CFDIFF_1:25 for a,f,x0 st f is_differentiable_in x0 holds a(#)f is_differentiable_in x0 & diff((a(#)f),x0) = a*diff(f,x0); theorem :: CFDIFF_1:26 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 ) = (f2/.x0)*diff(f1,x0)+(f1/.x0)*diff(f2,x0); theorem :: CFDIFF_1:27 for f,Z st Z c= dom f & f|Z = id Z holds f is_differentiable_on Z & for x st x in Z holds (f`|Z)/.x = 1r; theorem :: CFDIFF_1:28 for f1,f2,Z 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 st x in Z holds ((f1+f2)`|Z)/.x = diff(f1,x)+diff(f2,x); theorem :: CFDIFF_1:29 for f1,f2,Z 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 st x in Z holds ((f1-f2)`|Z)/.x = diff(f1,x)-diff(f2,x); theorem :: CFDIFF_1:30 for a,f,Z st Z c= dom (a(#)f) & f is_differentiable_on Z holds a(#)f is_differentiable_on Z & for x st x in Z holds ((a(#)f)`|Z)/.x = a*diff(f,x); theorem :: CFDIFF_1:31 for f1,f2,Z 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 st x in Z holds ((f1(#)f2)`|Z)/.x = (f2/.x)*diff(f1,x)+(f1/.x)*diff(f2,x); theorem :: CFDIFF_1:32 Z c= dom f & f|Z is constant implies f is_differentiable_on Z & for x st x in Z holds (f`|Z)/.x = 0c; theorem :: CFDIFF_1:33 Z c= dom f & (for x st x in Z holds f/.x = a*x+b) implies f is_differentiable_on Z & for x st x in Z holds (f`|Z)/.x = a; theorem :: CFDIFF_1:34 for x0 be Complex holds f is_differentiable_in x0 implies f is_continuous_in x0; theorem :: CFDIFF_1:35 f is_differentiable_on X implies f is_continuous_on X; theorem :: CFDIFF_1:36 f is_differentiable_on X & Z c= X implies f is_differentiable_on Z; ::$CT theorem :: CFDIFF_1:38 f is_differentiable_in x0 implies ex R st R/.0c = 0c & R is_continuous_in 0c;