LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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$ ; 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.

[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.1

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.

givenalgebra

1.2

A complex-valued map on a topological space is continuous exactly when its real and imaginary parts are, by [L6] and [L9]; 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.

L6L7L9

1.3

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, ρ^{'})$ .

givenL3L6L8choose

2.1

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$ .

givenstep 1.2L2L3L8

2.2

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.

step 1.3L1L8L9

3.1

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 Ω$ .

step 2.1step 1.3step 2.2L4L5L6L9∎

Depends on

Used by

Dependency tree · two levels

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