How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle
Statement
Let be holomorphic on , let , and let for . Define and, whenever it exists, . Then every exists on and, for every and ,
In particular, every holomorphic function has complex derivatives of all orders locally.
Facts & Assumptions
Given: A function holomorphic on , a radius , and the positively oriented circle of radius about .
Cauchy's circle formula gives the displayed identity when (Cauchy's integral formula on a circle compactly contained in a disc of holomorphy).
If for off the trace, then (Cauchy-kernel contour integrals may be differentiated by a direct difference-quotient estimate).
The factorial satisfies and (The factorial and the falling factorial , defined by recursion in ).
A base case and a successor implication prove a property for every natural number (The principle of mathematical induction).
A holomorphic function is continuous (Complex differentiability at a point implies continuity there).
Proof
For , [L1] and from [L3] give the formula and the existence of on .
Assume for a natural that exists on and satisfies the displayed formula there.
By [L5], the boundary data are continuous; the open disc is disjoint from the radius- trace, so [L2] applies with . Differentiating the induction formula gives , which is the required formula because by [L3].
Thus the property holds at and passes from to ; [L4] proves existence and the formula for every , including and constant functions.
Depends on
- Cauchy's integral formula on a circle compactly contained in a disc of holomorphy
- Cauchy-kernel contour integrals may be differentiated by a direct difference-quotient estimate
- The factorial $n!$ and the falling factorial $n^{\underline{k}}$, defined by recursion in $\mathbb{N}$
- The principle of mathematical induction
- Complex differentiability at a point implies continuity there
Used by
- Cauchy's inequalities bound every derivative by a boundary bound on a compactly contained circle Corollary
- Holomorphic functions are real analytic and smooth in their two real coordinates Corollary
- The higher-derivative form of the global Cauchy formula Corollary
- Uniform convergence on the closed unit disc does not give a holomorphic extension to a larger disc Counterexample
- The Taylor series of a holomorphic function at a point Definition
- The circle integral of cos z/(z-1)³ over |z|=2 is -π i cos 1 Example
- A bounded separately holomorphic function on a polydisc is Lipschitz on every smaller polydisc Lemma
- A nonvanishing holomorphic function on a disc has a holomorphic logarithm Lemma
- Cauchy estimates on a smaller concentric disc Lemma
- On a convex open set the difference quotient is an average of the derivative along the segment Lemma
- The filled difference quotient of a holomorphic function is jointly continuous Lemma
- Zeta logarithmic derivative zero bound Lemma
- Agreement of the power-series and Cauchy-integral formulas for Taylor coefficients Remark
- A holomorphic function equals its Taylor series throughout the largest centred disc in its domain Theorem
- A nonvanishing holomorphic function on a homologically simply connected domain has a holomorphic logarithm Theorem
- Equivalent characterisations of a homologically simply connected domain Theorem
- Morera's theorem: vanishing triangle integrals characterize holomorphy among continuous functions Theorem
- Spectral radius formula Theorem
Dependency tree · two levels
38 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Lars Ahlfors, Complex Analysis, third edition, Ch. 4, Section 2.3 (standard reference, not scraped)