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.
FALSE: existence of partial derivatives satisfying Cauchy–Riemann everywhere on an open set implies holomorphy
Statement
False claim: if all four first coordinate partial derivatives of exist at every point of an open set and satisfy the Cauchy–Riemann equations there, then is holomorphic on that set.
Facts & Assumptions
Given: The function on
The complex exponential is entire with derivative itself (The complex exponential is entire and its complex derivative is itself).
Complex differentiation is linear and satisfies the product rule; where the reciprocal is complex differentiable at with (Linearity, product, reciprocal, and quotient rules for complex derivatives); and a composite of complex differentiable maps is complex differentiable (The chain rule for complex derivatives). Iterating the product rule makes complex differentiable, so the reciprocal rule makes complex differentiable wherever . No general complex-exponent power rule is used.
For every natural and real , as (The exponential dominates every fixed nonnegative integer power at ).
Complex differentiability implies the Cauchy–Riemann equations, and it also implies continuity at the point (Complex differentiability is equivalent to real total differentiability together with a complex-linear derivative, with , or with the Cauchy–Riemann equations, Complex differentiability at a point implies continuity there).
Refutation
On , the power, reciprocal, exponential, and chain rules show that is holomorphic. Consequently all four partials exist and satisfy the Cauchy–Riemann equations there by [L1], [L2], and [L4].
For nonzero real , both and equal , so
Put . As , ; for , , and [L3] with , makes the last expression tend to . Hence .
Along with nonzero real , one has , and therefore So is unbounded in every neighbourhood of and is not continuous there.
Steps 1.2–1.3 give . Thus all four partials exist at and satisfy both Cauchy–Riemann equations there. Together with step 1.1, the false claim's hypotheses hold throughout the open set .
By [L4], the discontinuity in step 1.4 rules out complex differentiability at . Hence satisfies Cauchy–Riemann everywhere but is not holomorphic on , refuting the claim.
There is also a Wirtinger warning. Off , is holomorphic, so conjugating its Cauchy–Riemann equations gives ; at , step 2.1 gives the same value. Thus is identically zero and continuous. Nevertheless, off the chain rule gives , whose modulus along tends to infinity, so the coordinate partials of and are not continuous at .
Depends on
- The complex exponential is entire and its complex derivative is itself
- Linearity, product, reciprocal, and quotient rules for complex derivatives
- The chain rule for complex derivatives
- The exponential dominates every fixed nonnegative integer power at $+\infty$
- Complex differentiability is equivalent to real total differentiability together with a complex-linear derivative, with $\partial_{\bar z}f=0$, or with the Cauchy–Riemann equations
- Complex differentiability at a point implies continuity there
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: 108 results over 18 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.4 (standard reference, not scraped)