TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13

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 conjugate difference quotient characterizes antiholomorphic maps

Statement

Let $U \subseteq C$ be open, let $a \in U$ , and let $f : U \to C$ . The limit

$G = \lim_{\begin{array}{c} h \to 0 \\ h \neq 0 \end{array}} \frac{f (a + h) - f (a)}{\overset{ˉ}{h}}$

exists if and only if $f$ is real totally differentiable at $a$ and $f_{z} (a) = 0$ . In that case $f_{\overset{ˉ}{z}} (a) = G$ . Consequently, the conjugate quotient exists at every point of $U$ exactly for real-differentiable antiholomorphic maps, and its value is $f_{\overset{ˉ}{z}}$ .

Facts & Assumptions

Given: An open set $U \subseteq C$ , a point $a \in U$ , and a map $f : U \to C$ .

[F1]

Total differentiability at $a$ means $f (a + h) = f (a) + D f (a) h + r (h)$ with $∣ r (h) ∣ / ∣ h ∣ \to 0$ (The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder).

[F2]

For a real-differentiable map, $D f (a) h = f_{z} (a) h + f_{\overset{ˉ}{z}} (a) \overset{ˉ}{h}$ (The Wirtinger derivatives $\partial_{z} f$ and $\partial_{\overset{ˉ}{z}} f$ , and antiholomorphic functions).

[L1]

Every real-linear map between Euclidean spaces has a matrix and is bounded by a constant times the Euclidean norm (Every Euclidean linear map has a unique matrix and satisfies $∥ L h ∥_{2} \leq K ∥ h ∥_{2}$ for some $K \geq 0$ ).

[L2]

Conjugation is a real-field automorphism with $\overline{\overline{z}} = z$ , the modulus is multiplicative, and $z \overline{z} = ∣ z ∣^{2}$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive). Since $\overline{\overline{z}} = z$ and $z \overline{z} = ∣ z ∣^{2}$ , one has $∣ \overline{z} ∣^{2} = \overline{z} \overline{\overline{z}} = \overline{z} z = ∣ z ∣^{2}$ , and both moduli are nonnegative, so $∣ \overline{z} ∣ = ∣ z ∣$ , so in particular $∣ \overset{ˉ}{h} ∣ = ∣ h ∣$ .

Proof

technique · direct

1.1

Suppose the conjugate quotient tends to $G$ , and put $r (h) = f (a + h) - f (a) - G \overset{ˉ}{h}$ . Then $∣ r (h) ∣ / ∣ h ∣ = ∣ (f (a + h) - f (a)) / \overset{ˉ}{h} - G ∣ \to 0$ .

givenL2algebra

1.2

Conversely, suppose $f$ is real totally differentiable and $f_{z} (a) = 0$ . By [F1] and [F2], $f (a + h) - f (a) = f_{\overset{ˉ}{z}} (a) \overset{ˉ}{h} + r (h)$ with $∣ r (h) ∣ / ∣ h ∣ \to 0$ .

givenF1F2

1.3

For the identity map, [F2] gives $f_{z} = 1$ and $f_{\overset{ˉ}{z}} = 0$ , while its conjugate quotient is $h / \overset{ˉ}{h}$ and has incompatible values $1$ and $- 1$ on real and imaginary increments. For conjugation, [F2] gives $f_{z} = 0$ and $f_{\overset{ˉ}{z}} = 1$ , and its conjugate quotient is identically $1$ . These two tests confirm the placement of the conjugates and the barred coefficient.

F2L2algebra

2.1

The map $h \mapsto G \overset{ˉ}{h}$ is real-linear and bounded by $∣ G ∣ ∣ h ∣$ , so [F1] and step 1.1 show that $f$ is real totally differentiable with $D f (a) h = G \overset{ˉ}{h}$ .

step 1.1F1L1L2

3.1

Comparing this differential with [F2] gives $f_{z} (a) = 0$ and $f_{\overset{ˉ}{z}} (a) = G$ .

step 2.1F2algebra

4.1

Dividing by $\overset{ˉ}{h}$ and using $∣ \overset{ˉ}{h} ∣ = ∣ h ∣$ gives $(f (a + h) - f (a)) / \overset{ˉ}{h} = f_{\overset{ˉ}{z}} (a) + r (h) / \overset{ˉ}{h} \to f_{\overset{ˉ}{z}} (a)$ . This proves the reverse implication and the value of the limit.

step 1.2L2algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 90 results over 19 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. Lebl, Guide to Cultivating Complex Analysis, Exercise 2.2.11 (standard reference, not scraped)