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.
Cauchy's integral formula on a circle compactly contained in a disc of holomorphy
Statement
Let , let , and let be holomorphic on the disc
If , , and for , then
Facts & Assumptions
Given: A function holomorphic on , a radius , an interior point with , and the positively oriented circle of radius about .
The filled difference quotient is continuous on the disc and holomorphic away from its filled point (The filled difference quotient is continuous at its exceptional point and holomorphic away from it).
A continuous function holomorphic away from one point on a star-shaped open set has zero integral around every closed rectifiable contour there (A continuous function holomorphic away from one point on a star-shaped domain has a primitive and zero closed-contour integrals).
Complex line integrals are linear in the integrand (Complex line integrals are linear in the integrand).
On the positively oriented circle about , the integral of is for and zero for every other integer (On a positively oriented circle about a, the integral of (z-a)^m is zero for every integer m except -1, and is 2 pi i for m=-1).
Uniform convergence on a fixed rectifiable contour permits passage of the limit through the complex line integral (A uniformly convergent sequence of continuous integrands on a fixed contour permits passage of the limit through the complex line integral).
Proof
Define for and . By [L1], is continuous on and holomorphic away from .
If , [L4] gives . If , the finite identity holds on , and its remainder has modulus at most there.
The disc is star-shaped with respect to , since . The circle lies in the disc and is closed and rectifiable, so [L2] gives .
In the second case, [L6] makes the remainder tend uniformly to zero; [L5] and [L4] then give , because only the term has exponent . Thus the same kernel integral value holds also in the first case.
Since on , [L3] expands step 2.1 as .
Substitute step 2.2 into step 3.1 and divide by the nonzero number to obtain the formula.
Depends on
- A continuous function holomorphic away from one point on a star-shaped domain has a primitive and zero closed-contour integrals
- The filled difference quotient is continuous at its exceptional point and holomorphic away from it
- Complex line integrals are linear in the integrand
- On a positively oriented circle about a, the integral of (z-a)^m is zero for every integer m except -1, and is 2 pi i for m=-1
- A uniformly convergent sequence of continuous integrands on a fixed contour permits passage of the limit through the complex line integral
- For $|r| < 1$ the sequence $r^k$ is null, and for $|r| > 1$ the sequence $|r|^k$ diverges to $+\infty$
Used by
- A holomorphic function equals its average on every circle inside a larger concentric holomorphy disc Corollary
- Spectral projection of an isolated eigenvalue agrees with the riesz projection Example
- The circle integral of eᶻ/(z-1) over |z|=2 is 2π i e Example
- The iterated Cauchy formula computed for z₀z₁ on a bidisc Example
- A locally bounded punctured slice has a holomorphic parameter extension Lemma
- Hartogs figures give local extension across polydisc shells Lemma
- Locally bounded holomorphic families are locally equicontinuous Lemma
- Newman damped contour estimates Lemma
- A holomorphic function equals its Taylor series throughout the largest centred disc in its domain Theorem
- A holomorphic function on a Hartogs figure extends to the full bidisc Theorem
- All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle Theorem
- An isolated puncture is removable in complex dimension at least two Theorem
- Jensen's formula on a disc Theorem
- The iterated Cauchy integral formula on a polydisc Theorem
Dependency tree · two levels
43 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.2 (standard reference, not scraped)