LemmaStatement: AI-adaptedProof: 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.

On a convex open set the difference quotient is an average of the derivative along the segment

Statement

Let $V \subseteq C$ be open and convex (A convex subset of $R^{m}$ contains every line segment between two of its points) and let $f : V \to C$ be holomorphic. Then for all $z, w \in V$

$f (w) - f (z) = (w - z) \int_{0}^{1} f^{'} (z + t (w - z)) d t,$

the integral being the componentwise integral of a continuous $R^{2}$ -valued function of $t$ (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral). In particular, for $w \neq z$ ,

$\frac{f (w) - f (z)}{w - z} = \int_{0}^{1} f^{'} (z + t (w - z)) d t,$

while for $w = z$ the displayed integral equals $f^{'} (z)$ and both sides of the first identity are $0$ .

Facts & Assumptions

Given: An open convex $V \subseteq C$ , a holomorphic $f : V \to C$ and points $z, w \in V$ ; segments in the plane are those of Complex star-shaped and convex domains are the published Euclidean notions under the identification $C = R^{2}$ .

[L1]

If $F$ is a primitive of a continuous $f$ on an open set containing the trace of a rectifiable contour $γ : [a, b] \to C$ and $F^{'} = f$ is continuous, then $\int_{γ} f (z) d z = F (γ (b)) - F (γ (a))$ (The line integral of a continuous function admitting a primitive is that primitive's endpoint increment along every rectifiable path, A primitive of a complex function on an open set).

[L2]

For a piecewise- $C^{1}$ contour $γ$ and $f$ continuous on its trace, $\int_{γ} f (z) d z = \sum_{j} \int_{t_{j}}^{t_{j + 1}} f (γ (t)) γ_{j}^{'} (t) d t$ (For piecewise-C1 contours the Riemann–Stieltjes integral agrees with the parametric complex integral and the published real line integrals).

[L3]

A holomorphic $f = u + i v$ on an open subset of $C$ has $(u, v)$ of class $C^{k}$ for every natural $k$ , hence smooth (Holomorphic functions are real analytic and smooth in their two real coordinates), and every holomorphic function has complex derivatives of every natural order (All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle).

[L4]

A subset $U \subseteq R^{m}$ is convex when $(1 - t) x + t y \in U$ for all $x, y \in U$ and $t \in [0, 1]$ (A convex subset of $R^{m}$ contains every line segment between two of its points).

[L5]

Integrals of $R^{m}$ -valued functions are taken componentwise and are real-linear (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral); the real integral is linear in the integrand (Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ ).

[L6]

A function complex differentiable at a point is continuous there (Complex differentiability at a point implies continuity there).

[L7]

A continuous path differentiable with a continuous derivative on each piece of a partition is rectifiable (A continuous piecewise- $C^{1}$ path is rectifiable and its length is the sum of the speed integrals over its pieces).

Proof

technique · direct

1.1

By [L3] the derivative $f^{'}$ is again holomorphic on $V$ , hence continuous there by [L6], so $f$ is a primitive of the continuous $f^{'}$ with continuous $F^{'}$ in the sense of [L1].

givenL1L3L6

1.2

The map $ℓ (t) = z + t (w - z)$ on $[0, 1]$ has values in $V$ by [L4], since $V$ is convex, and is differentiable with the constant continuous derivative $w - z$ , so it is a piecewise- $C^{1}$ , hence rectifiable, contour with trace in $V$ ([L7]); its endpoints are $ℓ (0) = z$ and $ℓ (1) = w$ .

givenL4L7

2.1

By [L1] applied to $ℓ$ , $\int_{ℓ} f^{'} (ζ) d ζ = f (ℓ (1)) - f (ℓ (0)) = f (w) - f (z)$ .

step 1.1step 1.2L1

2.2

By [L2] applied to $ℓ$ , whose derivative is the constant $w - z$ , $\int_{ℓ} f^{'} (ζ) d ζ = \int_{0}^{1} f^{'} (z + t (w - z)) (w - z) d t$ , and pulling the complex constant $w - z$ out of the componentwise integral is real linearity, so this equals $(w - z) \int_{0}^{1} f^{'} (z + t (w - z)) d t$ .

step 1.1step 1.2L2L5algebra

3.1

Steps 2.1 and 2.2 give $f (w) - f (z) = (w - z) \int_{0}^{1} f^{'} (z + t (w - z)) d t$ ; dividing by $w - z$ when $w \neq z$ gives the difference-quotient form, and when $w = z$ the integrand is the constant $f^{'} (z)$ , whose integral over $[0, 1]$ is $f^{'} (z)$ by [L5], while both sides of the first identity are $0$ .

step 2.1step 2.2L5algebra∎

Depends on

Used by

Dependency tree · two levels

76 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

M. Weber, Complex Analysis (Indiana University), Ch. 4 §4.1 (standard reference, not scraped)