LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

The filled difference quotient of a holomorphic function is jointly continuous

Statement

Let $Ω \subseteq C$ be open and let $f : Ω \to C$ be holomorphic. Define the filled difference quotient $g : Ω \times Ω \to C$ by

$g (ζ, z) = {\begin{cases} \frac{f (ζ) - f (z)}{ζ - z}, & ζ \neq z, \\ f^{'} (z), & ζ = z . \end{cases}$

Then $g$ is continuous on $Ω \times Ω$ , the product carrying the Euclidean metric of $R^{4}$ under the coordinate identification of the plane. Moreover $g (ζ, z) = g (z, ζ)$ for all $ζ, z \in Ω$ .

Facts & Assumptions

Given: An open $Ω \subseteq C$ and a holomorphic $f : Ω \to C$ ; write $Φ (a + b i) = (a, b)$ and use $J (ζ, z) = (Φ (ζ), Φ (z))$ for product coordinates. The one-factor distance identity is The complex coordinate isometry transports topology and affine segments; summing its two squared identities gives $∥ J (ζ, z) - J (ζ_{0}, z_{0}) ∥_{2}^{2} = ∣ ζ - ζ_{0} ∣^{2} + ∣ z - z_{0} ∣^{2}$ , the product metric used here.

[L1]

For an open convex $V \subseteq C$ , a holomorphic $f$ on $V$ and $z, w \in V$ , $f (w) - f (z) = (w - z) \int_{0}^{1} f^{'} (z + t (w - z)) d t$ , and the displayed integral equals $f^{'} (z)$ when $w = z$ (On a convex open set the difference quotient is an average of the derivative along the segment).

[L2]

With $U$ open, $f$ holomorphic on $U$ and $z \in U$ fixed, the function equal to $(f (ζ) - f (z)) / (ζ - z)$ for $ζ \neq z$ and to $f^{'} (z)$ at $ζ = z$ is continuous on $U$ and holomorphic on $U ∖ {z}$ (The filled difference quotient is continuous at its exceptional point and holomorphic away from it).

[L3]

A holomorphic function is smooth in the real coordinates (Holomorphic functions are real analytic and smooth in their two real coordinates) and has complex derivatives of every natural order (All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle), and a complex differentiable function is continuous (Complex differentiability at a point implies continuity there).

[L4]

For an integrable $f : [a, b] \to R^{m}$ with $a \leq b$ , $∥ \int_{a}^{b} f ∥_{2} \leq \int_{a}^{b} ∥ f ∥_{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); integrals of vector-valued functions are componentwise and real-linear (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

[L5]

If $a < b$ , $h \leq H$ pointwise on $[a, b]$ , and both are integrable, then $\int_{a}^{b} h \leq \int_{a}^{b} H$ (If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ ).

[L6]

A map into $R^{m}$ from a subset of a metric space is continuous at $a$ exactly when the usual $ε$ – $δ$ condition holds with the Euclidean norm (Vector-valued functions $f : A \to R^{m}$ , their limits and continuity, with the dictionary to the metric notions).

[L7]

Sums, products and quotients with nonvanishing denominator of continuous real-valued maps on a topological space are continuous (Sums, products, absolute values, finite maxima and minima, and quotients of continuous real-valued maps on a topological space are continuous where defined).

[L8]

$B (x, ρ) = {y : d (x, y) < ρ}$ (Open ball, closed ball and sphere in a metric space), a set is open exactly when each of its points admits a ball inside it (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), and a set is convex when it contains the segment between any two of its points (A convex subset of $R^{m}$ contains every line segment between two of its points).

[L9]

$∣ z w ∣ = ∣ z ∣ ∣ w ∣$ and $∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive); for $z = a + b i$ with $a, b$ real, $Re z = a$ , $Im z = b$ and $∣ z ∣ = \sqrt{a^{2} + b^{2}}$ (Real and imaginary parts, complex conjugation, and modulus).

Proof

technique · direct

1.1givenalgebra

Interchanging $ζ$ and $z$ leaves the off-diagonal formula unchanged, both numerator and denominator changing sign, and leaves the diagonal value $f^{'} (z)$ unchanged; so $g$ is symmetric.

1.2givenL6L7L9

Each product projection is $1$ -Lipschitz by the squared distance identity in the given data, since each nonnegative summand is at most their sum; thus both projections are continuous. A complex-valued map on a metric subspace is continuous exactly when its real and imaginary parts are, by [L6] and [L9]: the norm bounds each coordinate difference, and two coordinate bounds below $ε / 2$ give a norm bound below $ε$ ; the real and imaginary parts of a sum, a product and a quotient with nonvanishing denominator of complex-valued maps are the corresponding real polynomial expressions in the parts, with denominator $∣ \cdot ∣^{2}$ , so [L7] makes such combinations of continuous complex-valued maps continuous.

1.3givenL3L6L8choose

Fix $a \in Ω$ and let $ε > 0$ . By [L8] choose $ρ > 0$ with $B (a, ρ) \subseteq Ω$ ; by [L3] the derivative $f^{'}$ is holomorphic, hence continuous, on $Ω$ , so by [L6] there is $ρ^{'}$ with $0 < ρ^{'} \leq ρ$ and $∣ f^{'} (ξ) - f^{'} (a) ∣ \leq ε$ for every $ξ \in B (a, ρ^{'})$ .

2.1givenstep 1.2L2L3L8

On the set $W = {(ζ, z) \in Ω \times Ω : ζ \neq z}$ , which is open by [L8], the maps $(ζ, z) \mapsto f (ζ) - f (z)$ and $(ζ, z) \mapsto ζ - z$ are continuous by [L3] and step 1.2, and [L2] already gives continuity of the filled difference quotient in each variable when the other is fixed; since the second map is nowhere zero on $W$ , step 1.2 makes $g$ continuous on $W$ .

2.2step 1.3L1L8L9

Let $ζ, z \in B (a, ρ^{'})$ . The ball $B (a, ρ^{'})$ is convex by [L8] and [L9] and $f$ is holomorphic on it, so [L1] gives $g (ζ, z) = \int_{0}^{1} f^{'} (z + t (ζ - z)) d t$ both off and on the diagonal, and every point $z + t (ζ - z)$ lies in $B (a, ρ^{'})$ by convexity.

3.1step 2.1step 1.3step 2.2L4L5L6L9∎

Subtracting the constant $g (a, a) = f^{'} (a)$ inside the integral of step 2.2 and applying [L4] and [L5] with the bound of step 1.3 gives $∣ g (ζ, z) - g (a, a) ∣ \leq \int_{0}^{1} ∣ f^{'} (z + t (ζ - z)) - f^{'} (a) ∣ d t \leq ε$ for all $ζ, z \in B (a, ρ^{'})$ ; by [L6] and [L9] this is continuity of $g$ at $(a, a)$ , and with step 2.1 it makes $g$ continuous on all of $Ω \times Ω$ .

Depends on

Dependency tree · 2 levels

Sources

J. Lebl, Complex Analysis, Ch. 4 §4.2