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

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.

The higher-derivative form of the global Cauchy formula

Statement

Let $Ω \subseteq C$ be open, let $f : Ω \to C$ be holomorphic, and let $Γ$ be a complex chain which is a cycle, with trace in $Ω$ and null-homologous in $Ω$ . Then for every natural number $m$ and every $z \in Ω ∖ Γ^{*}$

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

with $f^{(0)} = f$ . The case $m = 0$ is the integral formula already proved.

Facts & Assumptions

Given: An open $Ω$ , a holomorphic $f : Ω \to C$ , and a cycle $Γ$ with $Γ^{*} \subseteq Ω$ which is null-homologous in $Ω$ .

[L1]

Under these hypotheses, $n (Γ, z) f (z) = (2 π i)^{- 1} \int_{Γ} f (ζ) (ζ - z)^{- 1} d ζ$ for every $z \in Ω ∖ Γ^{*}$ (Cauchy's integral formula for a null-homologous cycle).

[L2]

For a chain $Γ$ and $φ$ continuous on $Γ^{*}$ , the functions $F_{j} (z) = (2 π i)^{- 1} \int_{Γ} φ (ζ) (ζ - z)^{- j} d ζ$ are holomorphic on $C ∖ Γ^{*}$ for every natural $j \geq 1$ and satisfy $F_{j}^{'} = j F_{j + 1}$ (The Cauchy transform of a cycle is holomorphic off its trace, with the expected derivatives).

[L3]

For a cycle $Γ$ the trace is compact, the index is constant on every connected component of $C ∖ Γ^{*}$ , and each such component is open (The index of a cycle is locally constant off its trace and vanishes far from it).

[L4]

A holomorphic function is smooth in the real coordinates (Holomorphic functions are real analytic and smooth in their two real coordinates) and has complex derivatives of every natural order (All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle); a complex differentiable function is continuous (Complex differentiability at a point implies continuity there).

[L5]

If a property holds at $0$ and passes from $j$ to $j + 1$ , it holds for every natural number (The principle of mathematical induction).

[L6]

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

[L7]

A constant multiple of a function complex differentiable at a point is complex differentiable there with the corresponding derivative (Linearity, product, reciprocal, and quotient rules for complex derivatives).

[L8]

Negative integer powers are defined exactly for nonzero complex bases (Integer powers in the complex field).

[L9]

$n (Γ, z) = (2 π i)^{- 1} \int_{Γ} d ζ / (ζ - z)$ for $z \notin Γ^{*}$ (Integration over a complex chain and the index of a chain), and null-homology in $Ω$ means the index vanishes at every point outside $Ω$ (Null-homologous cycles and homologous cycles in an open set).

[L10]

The connected component of a point is the union of all connected subsets containing it (Connected components, quasicomponents, and totally disconnected spaces), and a set is closed exactly when its complement is open (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

Proof

technique · direct

1.1

The trace $Γ^{*}$ is compact by [L3], hence closed, so $C ∖ Γ^{*}$ is open by [L10] and $Ω ∖ Γ^{*}$ is open. The restriction of $f$ to $Γ^{*}$ is continuous by [L4], so the functions $F_{j} (z) = (2 π i)^{- 1} \int_{Γ} f (ζ) (ζ - z)^{- j} d ζ$ of [L2] are defined and holomorphic on $C ∖ Γ^{*}$ with $F_{j}^{'} = j F_{j + 1}$ , the powers being legitimate by [L8].

givenL2L3L4L8L10

1.2

By [L4] the function $f$ has complex derivatives $f^{(m)}$ of every natural order on $Ω$ .

givenL4

2.1

An induction on $j$ ([L5]) using $F_{1}^{'} = F_{2}$ , the relation $F_{j}^{'} = j F_{j + 1}$ of step 1.1, [L6] and [L7] gives $F_{1}^{(j)} = j! F_{j + 1}$ on $C ∖ Γ^{*}$ for every natural $j$ , the case $j = 0$ reading $F_{1} = 0! F_{1}$ .

step 1.1L5L6L7

2.2

Fix $z_{0} \in Ω ∖ Γ^{*}$ and let $C$ be the connected component of $z_{0}$ in $C ∖ Γ^{*}$ . By [L3] the set $C$ is open and $n (Γ, \cdot)$ is a constant $k$ on it, so $W = C \cap Ω$ is an open subset of $Ω ∖ Γ^{*}$ containing $z_{0}$ on which the index has the constant value $k$ .

step 1.1L3L9L10

3.1

By [L1] the identity $k f = F_{1}$ holds on $W$ ; both sides are holomorphic there by steps 1.1 and 1.2, and complex differentiation is a local operation, so differentiating $m$ times on $W$ and using [L7] gives $k f^{(m)} = F_{1}^{(m)}$ on $W$ .

step 1.2step 2.2L1L7

4.1

Combining step 3.1 with step 2.1 at the point $z_{0}$ gives $n (Γ, z_{0}) f^{(m)} (z_{0}) = k f^{(m)} (z_{0}) = m! F_{m + 1} (z_{0})$ , which is the displayed formula; since $z_{0} \in Ω ∖ Γ^{*}$ was arbitrary and $m$ was an arbitrary natural number, the formula holds throughout, and at $m = 0$ it is [L1] again by [L6].

step 2.1step 3.1L1L6∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

81 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

J. Lebl, Complex Analysis, Ch. 4 §4.2 (standard reference, not scraped)