:: Complex Function Differentiability
:: by Chanapat Pacharapokin , Hiroshi Yamazaki , Yasunari Shidama and Yatsuka Nakamura
::
:: Received November 4, 2008
:: Copyright (c) 2008-2016 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;