TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-17

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 $f$ be holomorphic on $D (a, R)$ , let $0 < r < R$ , and let $γ (t) = a + r \exp (i t)$ for $0 \leq t \leq 2 π$ . Define $f^{(0)} = f$ and, whenever it exists, $f^{(n + 1)} = (f^{(n)})^{'}$ . Then every $f^{(n)}$ exists on $D (a, r)$ and, for every $z \in D (a, r)$ and $n \in N$ ,

$f^{(n)} (z) = \frac{n!}{2 π i} \int_{γ} \frac{f (ζ)}{(ζ - z)^{n + 1}} d ζ .$

In particular, every holomorphic function has complex derivatives of all orders locally.

Facts & Assumptions

Given: A function $f$ holomorphic on $D (a, R)$ , a radius $0 < r < R$ , and the positively oriented circle $γ$ of radius $r$ about $a$ .

[L1]

Cauchy's circle formula gives the displayed identity when $n = 0$ (Cauchy's integral formula on a circle compactly contained in a disc of holomorphy).

[L2]

If $F_{m} (z) = (2 π i)^{- 1} \int_{γ} φ (ζ) / (ζ - z)^{m} d ζ$ for $m \geq 1$ off the trace, then $F_{m}^{'} = m F_{m + 1}$ (Cauchy-kernel contour integrals may be differentiated by a direct difference-quotient estimate).

[L3]

The factorial satisfies $0! = 1$ and $(n + 1)! = (n + 1) n!$ (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ).

[L4]

A base case and a successor implication prove a property for every natural number (The principle of mathematical induction).

[L5]

A holomorphic function is continuous (Complex differentiability at a point implies continuity there).

Proof

technique · induction

1.1

For $n = 0$ , [L1] and $0! = 1$ from [L3] give the formula and the existence of $f^{(0)} = f$ on $D (a, r)$ .

baseL1L3

1.2

Assume for a natural $n$ that $f^{(n)}$ exists on $D (a, r)$ and satisfies the displayed formula there.

2.1

By [L5], the boundary data $φ = f ∣_{γ}$ are continuous; the open disc $D (a, r)$ is disjoint from the radius- $r$ trace, so [L2] applies with $m = n + 1$ . Differentiating the induction formula gives $f^{(n + 1)} (z) = n! (n + 1) (2 π i)^{- 1} \int_{γ} f (ζ) / (ζ - z)^{n + 2} d ζ$ , which is the required formula because $n! (n + 1) = (n + 1)!$ by [L3].

step 1.2L2L3L5

3.1

Thus the property holds at $0$ and passes from $n$ to $n + 1$ ; [L4] proves existence and the formula for every $n \in N$ , including $n = 1$ and constant functions.

step 1.1step 2.1L4discharge-induction∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 141 results over 20 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Lars Ahlfors, Complex Analysis, third edition, Ch. 4, Section 2.3 (standard reference, not scraped)