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

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 jointly continuous finite-interval parameter integral of holomorphic functions is holomorphic

Statement

Let $a \leq b$ be real, let $Ω \subseteq C$ be open, and let $φ : [a, b] \times Ω \to C$ be jointly continuous. Suppose $φ (t, \cdot)$ is holomorphic on $Ω$ for every $t \in [a, b]$ . Then the componentwise Riemann integral

$F (z) : = \int_{a}^{b} φ (t, z) d t$

is holomorphic on $Ω$ .

If, in addition, $\partial_{z} φ (t, z)$ exists everywhere and is jointly continuous on $[a, b] \times Ω$ , then

$F^{'} (z) = \int_{a}^{b} \partial_{z} φ (t, z) d t .$

If $φ : [a, b] \times Ω \to C$ is jointly continuous and $φ (t, \cdot)$ is holomorphic for every $t$ , then $F (z) = \int_{a}^{b} φ (t, z) d t$ is holomorphic on $Ω$ .

Facts & Assumptions

Given: Real numbers $a \leq b$ , an open set $Ω \subseteq C$ , and a jointly continuous function $φ : [a, b] \times Ω \to C$ whose $z$ -slice is holomorphic for every parameter; the identification $C = R^{2}$ from $C$ is the real coordinate plane, with coordinate arithmetic.

[L1]

Complex-valued Riemann integration is the componentwise vector integral in $R^{2}$ , with zero integral when the limits agree and with linearity on every nondegenerate interval (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

[L2]

On a piecewise- $C^{1}$ contour, the complex contour integral equals the sum of the parameter integrals of $f (γ (s)) γ^{'} (s)$ over its smooth pieces (For piecewise-C1 contours the Riemann–Stieltjes integral agrees with the parametric complex integral and the published real line integrals).

[L3]

A Riemann-integrable real function on a product of nondegenerate closed rectangles has equal iterated integrals in either order when all sections are integrable (Riemann--Fubini on product rectangles, with lower and upper section integrals and content-zero exceptional sections).

[L4]

A holomorphic function has zero integral around every contained filled triangle (Goursat's triangle theorem: a holomorphic function integrates to zero around every triangle contained in its domain).

[L5]

A continuous function with zero integral around every contained filled triangle is holomorphic (Morera's theorem: vanishing triangle integrals characterize holomorphy among continuous functions).

[L6]

If $H$ is a primitive of a continuous function $h$ on a neighbourhood of a rectifiable contour $γ$ , then $\int_{γ} h = H (γ (b)) - H (γ (a))$ (The line integral of a continuous function admitting a primitive is that primitive's endpoint increment along every rectifiable path).

[L7]

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

[L8]

Closed bounded subsets of Euclidean space are 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).

[L9]

Every continuous real function on a closed nondegenerate rectangle is Riemann integrable (Every continuous function on a closed nondegenerate rectangle in $R^{m}$ is Riemann integrable).

[L10]

Let $a \leq b$ . If $a < b$ and $h : [a, b] \to R^{m}$ is integrable, then $t \mapsto ∥ h (t) ∥_{2}$ is integrable, and in all cases $∥ \int_{a}^{b} h ∥_{2} \leq \int_{a}^{b} ∥ h ∥_{2}$ (For $a \leq b$ and $f : [a, b] \to R^{m}$ integrable when $a < b$ , $∥ \int_{a}^{b} f ∥_{2} \leq \int_{a}^{b} ∥ f ∥_{2}$ ; for $a < b$ , $∥ f ∥_{2}$ is integrable).

[L11]

If $q$ is Riemann integrable and $0 \leq q (t) \leq B$ on $[a, b]$ with $a < b$ , then $\int_{a}^{b} q (t) d t \leq B (b - a)$ (If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ ).

Proof

technique · direct

1.1

If $a = b$ , [L1] makes $F = 0$ , so all conclusions are immediate. Suppose $a < b$ . For each $z$ , continuity of $t \mapsto φ (t, z)$ and [L9] make the componentwise integral exist; near any fixed $z_{0}$ , choose a compactly contained closed disc $K$ , so [L8] makes $[a, b] \times K$ compact, [L7] makes $φ$ uniformly continuous there, and [L10] with [L11] gives $∥ F (z) - F (z_{0}) ∥_{2} \leq (b - a) \sup_{t \in [a, b]} ∣ φ (t, z) - φ (t, z_{0}) ∣ \to 0$ , hence $F$ is continuous.

givenL1L7L8L9L10L11

1.2

For a filled triangle $Δ \subseteq Ω$ , parametrize each directed edge by its affine map on $[0, 1]$ ; [L2] rewrites the edge contribution to $\int_{\partial Δ} F (z) d z$ as an iterated parameter integral on $[a, b] \times [0, 1]$ .

givenL2

1.3

For the differentiation-under-the-integral conclusion, now assume $ψ : = \partial_{z} φ$ exists and is jointly continuous. Fix $z \in Ω$ and a closed disc about $z$ contained in $Ω$ ; for sufficiently small nonzero $h$ , [L6] and the parametrization in [L2] on the segment from $z$ to $z + h$ give $(φ (t, z + h) - φ (t, z)) / h = \int_{0}^{1} ψ (t, z + s h) d s$ , and [L7] on the compact parameter-disc product from [L8] makes this quotient converge to $ψ (t, z)$ uniformly in $t$ .

givenL2L6L7L8

2.1

For the basic holomorphy conclusion, each real and imaginary component of the edge integrand in step 1.2 is continuous, hence Riemann integrable by [L9]; [L3] interchanges its parameter and edge integrals, and [L4] makes the resulting inner contour integral $\int_{\partial Δ} φ (t, z) d z$ zero for every fixed $t$ , so $\int_{\partial Δ} F (z) d z = 0$ .

step 1.2L3L4L9

3.1

For the basic holomorphy conclusion, the continuity from step 1.1 and the vanishing triangle integrals from step 2.1 satisfy [L5], so $F$ is holomorphic on $Ω$ .

step 1.1step 2.1L5

4.1

For the differentiation-under-the-integral conclusion, by linearity in [L1], the difference quotient of $F$ minus $\int_{a}^{b} ψ (t, z) d t$ is the integral over $t$ of the error in step 1.3; [L10] and [L11] bound its modulus by $(b - a)$ times the uniform error, which tends to zero, so $F^{'} (z) = \int_{a}^{b} \partial_{z} φ (t, z) d t$ , including the already settled case $a = b$ .

step 1.3L1L10L11∎

Depends on

Used by

Morera proves holomorphy of z↦∫₀¹ tᶻ dt on Rez>1 Example

Dependency tree · two levels

116 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

E. Stein and R. Shakarchi, Complex Analysis, Ch. 2, Theorem 5.4 (standard reference, not scraped)