Cauchy Integral Formula

Statement

Let $f$ be holomorphic on a closed disk $\overline{B}(c, R)$ and let $w \in B(c, R)$ be any interior point. Then:

Equivalently, the smeared form:

holds whenever $f$ is holomorphic on the open disk and continuous on the closure.

Visualization

Take $f(z) = 1$ (constant), $c = 0$, $R = 1$, $w = 0$. The formula predicts:

Parameterize: $z = e^{i\theta}$, $dz = ie^{i\theta}d\theta$.

theta:    0       pi/2     pi      3pi/2    2pi
z:        1        i      -1       -i        1
1/z:      1       -i      -1        i        1

Dividing by $2\pi i$ gives $f(0) = 1$. Confirmed.

For $f(z) = z^n$ with $n \ge 1$ and $w = 0$: the integrand $z^n/z = z^{n-1}$ has no residue at $0$ when $n \ge 1$, so the integral is $0 = f(0)$ only when $f(0) = 0$. For $w \ne 0$ inside the disk, the formula reconstructs $w^n$ from boundary values.

Proof Sketch

1. For $w$ outside the contour, $z \mapsto f(z)/(z-w)$ is holomorphic everywhere inside, so the integral vanishes by Cauchy's theorem.
2. For $w$ inside, write $\frac{f(z)}{z-w} = \frac{f(z) - f(w)}{z-w} + \frac{f(w)}{z-w}$.
3. The first term extends continuously to $w$ (holomorphicity of $f$ at $w$), so its integral over a small circle around $w$ tends to $0$.
4. The second term contributes $f(w) \cdot \oint \frac{dz}{z-w} = f(w) \cdot 2\pi i$.
5. Deformation of contour (the integral is unchanged when deforming through regions where $f$ is holomorphic) finishes the proof.

Connections

The formula is the engine behind Liouville's TheoremLiouville's Theorem$$f : \mathbb{C} \to \mathbb{C} \text{ entire},\; |f| \leq C \implies f \equiv \text{const}$$A bounded entire function on ℂ must be constant — complex differentiability is far more rigid than real differentiabilityRead more → (bounded entire functions are constant) and the Fundamental Theorem of AlgebraFundamental Theorem of Algebra$$\deg p \geq 1,\; p \in \mathbb{C}[z] \implies \exists z_0 \in \mathbb{C}: p(z_0) = 0$$Every non-constant polynomial with complex coefficients has at least one root in ℂRead more → (non-constant polynomials have roots). It also drives Taylor's TheoremTaylor's Theorem$$f(x) = \sum_{k=0}^{n} \frac{f^{(k)}(x_0)}{k!}(x-x_0)^k + R_n(x)$$Approximate smooth functions by polynomials with explicit error boundsRead more → for complex functions: differentiating under the integral sign yields power series coefficients.

import Mathlib.Analysis.Complex.CauchyIntegral

open Complex MeasureTheory

/-- **Cauchy Integral Formula**: for `f` holomorphic on a closed disk,
    the value at any interior point `w` is recovered from the circle integral.
    Uses `DiffContOnCl.circleIntegral_sub_inv_smul` from Mathlib. -/
theorem cauchy_integral_formula {R : ℝ} {c w : ℂ} {f : ℂ → ℂ}
    (hf : DiffContOnCl ℂ f (Metric.ball c R))
    (hw : w ∈ Metric.ball c R) :
    ((2 * Real.pi * Complex.I)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z) = f w :=
  hf.two_pi_i_inv_smul_circleIntegral_sub_inv_smul hw