Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck 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]→C be a rectifiable contour with trace γ∗, let Ω⊆C be open, and let φ:γ∗×Ω→C be continuous, with z↦φ(w,z) holomorphic on Ω for every w∈γ∗. Then

F(z):=∫γφ(ζ,z) dζ

is defined for every z∈Ω and is holomorphic on Ω.

Here γ∗×Ω carries the Euclidean metric of R4 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]→C, an open Ω⊆C, and a continuous φ:γ∗×Ω→C with φ(w,⋅) holomorphic on Ω for each w∈γ∗; products of subsets of C are read in R4 through C=R[x]/(x2+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]→C with a<b, a continuous f on γ∗, a partition a=t0<⋯<tr=b and tags ξi∈[ti,ti+1], the difference between ∫γf dz and ∑i<rf(γ(ξi))(γ(ti+1)−γ(ti)) has modulus at most ωL(γ) whenever ω≥0 satisfies ∣f(u)−f(v)∣≤ω for all u,v∈γ∗ (Tagged sums approximate a contour integral within oscillation times length).

[L2]

If each fn:Ω→C is holomorphic on an open Ω and fn→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).

[L5]

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

[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]→C and f continuous on its trace, the complex line integral ∫γf dz exists (Continuous integrands have complex and absolute line integrals along every rectifiable path).

[L9]

For a<b and a natural N≥1 the uniform partition of [a,b] into N parts has points ti=a+i(b−a)/N and mesh (b−a)/N (Partition of [a,b] as a finite strictly increasing list a=t0<t1<⋯<tn=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≥1 with 1/n<ε (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε).

[L11]

B(x,r) is the set of points at distance below r from x and 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]→C, so L(γ) is a nonnegative real (Rectifiable complex contours, reversal, concatenation, closedness, and orientation).

Proof

technique · direct
1.1givenL4L6

The parameter interval [a,b] is compact by [L4] and γ is continuous, so the trace γ∗ is compact by [L6].

1.2givenL8

For each z∈Ω the map ζ↦φ(ζ,z) is continuous on γ∗, so F(z) exists by [L8].

1.3givenL7L9

Write PN for the uniform partition of [a,b] into N parts, with points tiN=a+i(b−a)/N, and set SN(z)=∑i<Nφ(γ(tiN),z)(γ(ti+1N)−γ(tiN)) for z∈Ω, assuming a<b. Each summand is a constant multiple of a function holomorphic on Ω, so SN is holomorphic on Ω by [L7].

2.1step 1.1L3L4L5L11

Fix z0∈Ω. By [L11] there is ρ>0 with Bˉ(z0,ρ)⊆Ω; put K=Bˉ(z0,ρ), which is closed and bounded, hence compact by [L4]. By [L5] and step 1.1 both γ∗ and K are closed and bounded, so γ∗×K is a closed bounded subset of R4 and is compact by [L4]; since φ is continuous there, [L3] makes it uniformly continuous on γ∗×K.

3.1step 2.1L3L4L10choose

Let ε>0. Step 2.1 gives η>0 such that ∣φ(u,z)−φ(v,z)∣≤ε whenever u,v∈γ∗ satisfy ∣u−v∣<η and z∈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≥1 with (b−a)/n<δ.

4.1step 1.2step 1.3step 3.1L1L12

Let N≥n and z∈K. Every two parameters in a subinterval of PN differ by at most (b−a)/N≤(b−a)/n<δ, so any two points of γ([tiN,ti+1N]) are within η of each other and step 3.1 bounds ∣φ(u,z)−φ(v,z)∣ by ε for such points. Applying [L1] to f=φ(⋅,z) on each subarc, with ω=ε on that subarc, and summing the subarc bounds gives ∣F(z)−SN(z)∣≤εL(γ).

5.1step 1.3step 4.1L2L7L11L12∎

Since ε>0 was arbitrary and L(γ) is a fixed nonnegative real by [L12], step 4.1 says SN→F uniformly on K, hence uniformly on the open neighbourhood B(z0,ρ) of z0; as z0∈Ω was arbitrary, SN→F locally uniformly on Ω, and [L2] with step 1.3 makes F holomorphic on Ω. If instead a=b then ∫γf dz=0 for every continuous f, so F is identically 0 and holomorphic by [L7].

Depends on

Used by

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