TheoremStatement: Literature-sourcedProof: AI-generatedSession-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.

A contour integral of a jointly continuous, parameter-holomorphic integrand is holomorphic

Statement

Let $γ : [a, b] \to C$ be a rectifiable contour with trace $γ^{*}$ , let $Ω \subseteq C$ be open, and let $φ : γ^{*} \times Ω \to C$ be continuous, with $z \mapsto φ (w, z)$ holomorphic on $Ω$ for every $w \in γ^{*}$ . Then

$F (z) : = \int_{γ} φ (ζ, z) d ζ$

is defined for every $z \in Ω$ and is holomorphic on $Ω$ .

Here $γ^{*} \times Ω$ carries the Euclidean metric of $R^{4}$ under the coordinate identification of the plane, so continuity of $φ$ is joint continuity in the two variables together.

Facts & Assumptions

Given: A rectifiable contour $γ : [a, b] \to C$ , an open $Ω \subseteq C$ , and a continuous $φ : γ^{*} \times Ω \to C$ with $φ (w, \cdot)$ holomorphic on $Ω$ for each $w \in γ^{*}$ ; products of subsets of $C$ are read in $R^{4}$ through $C = R [x] / (x^{2} + 1)$ as the Euclidean plane and as a normed real algebra: what the identification preserves, and locally uniform convergence is that of Locally uniform convergence on an open subset of the complex plane is compact convergence.

[L1]

For a rectifiable contour $γ : [a, b] \to C$ with $a < b$ , a continuous $f$ on $γ^{*}$ , a partition $a = t_{0} < \dots < t_{r} = b$ and tags $ξ_{i} \in [t_{i}, t_{i + 1}]$ , the difference between $\int_{γ} f d z$ and $\sum_{i < r} f (γ (ξ_{i})) (γ (t_{i + 1}) - γ (t_{i}))$ has modulus at most $ω L (γ)$ whenever $ω \geq 0$ satisfies $∣ f (u) - f (v) ∣ \leq ω$ for all $u, v \in γ^{*}$ (Tagged sums approximate a contour integral within oscillation times length).

[L2]

If each $f_{n} : Ω \to C$ is holomorphic on an open $Ω$ and $f_{n} \to f$ locally uniformly on $Ω$ , then $f$ is holomorphic (Locally uniform limits of holomorphic functions are holomorphic and their derivatives converge locally uniformly).

[L3]

A continuous map from a compact metric space to a metric space is uniformly continuous (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous).

[L4]

A subset of $R^{n}$ is compact exactly when it is closed and bounded, and every closed box is compact (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

[L5]

A compact subset of a metric space is closed and bounded (A compact subset of a metric space is closed and bounded).

[L6]

The continuous image of a compact subset is a compact subset (The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset).

[L7]

A linear combination $α f + β g$ of functions complex differentiable at a point is complex differentiable there, with $(α f + β g)^{'} = α f^{'} + β g^{'}$ , and every constant function has derivative $0$ (Linearity, product, reciprocal, and quotient rules for complex derivatives).

[L8]

For a rectifiable $γ : [a, b] \to C$ and $f$ continuous on its trace, the complex line integral $\int_{γ} f d z$ exists (Continuous integrands have complex and absolute line integrals along every rectifiable path).

[L9]

For $a < b$ and a natural $N \geq 1$ the uniform partition of $[a, b]$ into $N$ parts has points $t_{i} = a + i (b - a) / N$ and mesh $(b - a) / N$ (Partition of $[a, b]$ as a finite strictly increasing list $a = t_{0} < t_{1} < \dots < t_{n} = b$ , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions).

[L10]

For every real $ε > 0$ there is a natural $n \geq 1$ with $1 / n < ε$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

[L11]

$B (x, r)$ is the set of points at distance below $r$ from $x$ and $\overset{ˉ}{B} (x, r)$ the set at distance at most $r$ ; a set is open exactly when each of its points has some ball around it inside the set (Open ball, closed ball and sphere in a metric space, 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).

[L12]

A complex contour is a rectifiable path $γ : [a, b] \to C$ , so $L (γ)$ is a nonnegative real (Rectifiable complex contours, reversal, concatenation, closedness, and orientation).

Proof

technique · direct

1.1

The parameter interval $[a, b]$ is compact by [L4] and $γ$ is continuous, so the trace $γ^{*}$ is compact by [L6].

givenL4L6

1.2

For each $z \in Ω$ the map $ζ \mapsto φ (ζ, z)$ is continuous on $γ^{*}$ , so $F (z)$ exists by [L8].

givenL8

1.3

Write $P_{N}$ for the uniform partition of $[a, b]$ into $N$ parts, with points $t_{i}^{N} = a + i (b - a) / N$ , and set $S_{N} (z) = \sum_{i < N} φ (γ (t_{i}^{N}), z) (γ (t_{i + 1}^{N}) - γ (t_{i}^{N}))$ for $z \in Ω$ , assuming $a < b$ . Each summand is a constant multiple of a function holomorphic on $Ω$ , so $S_{N}$ is holomorphic on $Ω$ by [L7].

givenL7L9

2.1

Fix $z_{0} \in Ω$ . By [L11] there is $ρ > 0$ with $\overset{ˉ}{B} (z_{0}, ρ) \subseteq Ω$ ; put $K = \overset{ˉ}{B} (z_{0}, ρ)$ , which is closed and bounded, hence compact by [L4]. By [L5] and step 1.1 both $γ^{*}$ and $K$ are closed and bounded, so $γ^{*} \times K$ is a closed bounded subset of $R^{4}$ and is compact by [L4]; since $φ$ is continuous there, [L3] makes it uniformly continuous on $γ^{*} \times K$ .

step 1.1L3L4L5L11

3.1

Let $ε > 0$ . Step 2.1 gives $η > 0$ such that $∣ φ (u, z) - φ (v, z) ∣ \leq ε$ whenever $u, v \in γ^{*}$ satisfy $∣ u - v ∣ < η$ and $z \in K$ . The interval $[a, b]$ is compact by [L4], so $γ$ is uniformly continuous on it by [L3]: there is $δ > 0$ with $∣ γ (t) - γ (s) ∣ < η$ whenever $∣ t - s ∣ < δ$ . By [L10] applied to $δ / (b - a)$ there is a natural $n \geq 1$ with $(b - a) / n < δ$ .

step 2.1L3L4L10choose

4.1

Let $N \geq n$ and $z \in K$ . Every two parameters in a subinterval of $P_{N}$ differ by at most $(b - a) / N \leq (b - a) / n < δ$ , so any two points of $γ ([t_{i}^{N}, t_{i + 1}^{N}])$ are within $η$ of each other and step 3.1 bounds $∣ φ (u, z) - φ (v, z) ∣$ by $ε$ for such points. Applying [L1] to $f = φ (\cdot, z)$ on each subarc, with $ω = ε$ on that subarc, and summing the subarc bounds gives $∣ F (z) - S_{N} (z) ∣ \leq ε L (γ)$ .

step 1.2step 1.3step 3.1L1L12

5.1

Since $ε > 0$ was arbitrary and $L (γ)$ is a fixed nonnegative real by [L12], step 4.1 says $S_{N} \to F$ uniformly on $K$ , hence uniformly on the open neighbourhood $B (z_{0}, ρ)$ of $z_{0}$ ; as $z_{0} \in Ω$ was arbitrary, $S_{N} \to F$ locally uniformly on $Ω$ , and [L2] with step 1.3 makes $F$ holomorphic on $Ω$ . If instead $a = b$ then $\int_{γ} f d z = 0$ for every continuous $f$ , so $F$ is identically $0$ and holomorphic by [L7].

step 1.3step 4.1L2L7L11L12∎

Depends on

Used by

Dixon's glued function is entire and vanishes at infinity Lemma

Dependency tree · two levels

85 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)