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.
Analyticity of Holomorphic Functions; Liouville and Morera — Examples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Analyticity of Holomorphic Functions; Liouville and Morera
- Arc Length and Rectifiable Curves
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Variation and the Riemann–Stieltjes Integral
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Differentiability and the Cauchy–Riemann Equations
- Complex Power Series and Analytic Functions
- Connectedness
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Contour Integration
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Fubini and Change of Variables
- Function Space Topologies and the Exponential Law
- Fundamental Trigonometric Identities
- Goursat's Theorem and Cauchy's Theorem in a Convex Domain
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Line Integrals and the Gradient Theorem
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Metric Spaces
- Mixed Partials, Taylor Formulae, and Extrema
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Partitions of Unity and Paracompactness
- pi: the Equivalent Characterizations
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Properties of the Integral and the Working FTC
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Simple Field Extensions and the Construction of the Complex Numbers
- Sine, Cosine, and the Definition of Pi
- Subspaces, Products, and Quotients
- Suprema and Infima
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Complex Exponential and Euler's Formula
- The Derivative and the Mean Value Theorems
- The Exponential Function
- The Fundamental Theorems of Calculus
- The Logarithm and General Powers
- The Riemann Integral in Rᵐ and Jordan Content
- The Riemann Integral: Definition and Integrability
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
has a zero of order three at the origin
Example
The entire function has a zero of order at .
Facts & Assumptions
Given: The function .
The entire sine series is and has infinite radius of convergence (The exponential definitions of complex sine, cosine, hyperbolic sine, and hyperbolic cosine equal their entire power series).
The order is the least natural index of a nonzero Taylor coefficient, and is only when every coefficient is zero (The order of a zero of a holomorphic function).
Finite order is equivalent to a local factorization with holomorphic and (The order of a zero is the exponent in its local holomorphic factorization).
Complex sine and cosine are entire and satisfy and (Complex sine, cosine, hyperbolic sine, and hyperbolic cosine are entire with their standard derivatives).
The coefficients of a convergent complex power-series representation are uniquely the Taylor coefficients at its centre (The coefficients of a complex power series are its derivatives at the centre divided by the corresponding factorials).
Verification
Subtracting from [L1] gives .
By [L5], the convergent representation in step 1.1 is the Taylor series of at zero. Its coefficients in degrees , , and vanish, while the coefficient in degree is , so [L2] gives .
The factorization in [L3] therefore has with ; independently, [L4] and [L1] give and , confirming the same order and sign.
Morera proves holomorphy of on
Example
Let . For , use the principal power , and set for . Then
is holomorphic on .
Facts & Assumptions
Given: The half-plane and the endpoint convention in the example.
For a nonzero complex base and exponent , the principal power is ; for positive real , (Complex logarithms, the principal logarithm, and principal and multivalued complex powers, The natural logarithm as the inverse of the exponential function).
The complex exponential is entire and has derivative equal to itself (The complex exponential is entire and its complex derivative is itself).
For real , (, , and ).
The complex exponential agrees with the real exponential on the real axis (, and the complex exponential extends the real exponential).
The real exponential is strictly increasing (The exponential function is strictly increasing).
The natural logarithm is continuous and strictly increasing on the positive reals, with (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).
A complex differentiable function is continuous (Complex differentiability at a point implies continuity there).
The composite of complex differentiable functions is complex differentiable (The chain rule for complex derivatives).
Complex modulus is multiplicative and satisfies the triangle inequality (Conjugation is an involutive real-field automorphism, , and modulus is definite, multiplicative, and subadditive).
A jointly continuous finite-interval integral of holomorphic parameter slices is holomorphic (A jointly continuous finite-interval parameter integral of holomorphic functions is holomorphic).
Verification
For define by [L1], and define as stated in the example.
For fixed , the map is complex linear and [L2] with [L8] makes entire; for the slice is the constant zero function and is entire.
On , [L3] and [L4] give ; [L6] gives , so and [L5] yield . Thus uniformly for near any fixed point of as ; away from , continuity follows from [L6], [L7], and the multiplication estimate from [L9], so is jointly continuous on .
Steps 2.1 and 2.2 satisfy [L10] on the finite interval , so is holomorphic on .
Uniform convergence on the closed unit disc does not give a holomorphic extension to a larger disc
Statement refuted
Refuted claim: If a complex power series converges uniformly on a closed disc, its sum extends holomorphically to some larger centred disc.
The series
converges uniformly on , but its sum on has no holomorphic extension to any disc centred at with radius greater than .
Facts & Assumptions
Given: The complex power series defining , with its partial sums and convergence interpreted as in Complex series, absolute convergence, complex power series, and radius of convergence.
If and the real series converges, then the complex function series converges absolutely pointwise and uniformly (Weierstrass M-test for complex-valued function series).
The series converges, while the harmonic series diverges (For rational , converges iff ).
Inside the radius of convergence, a complex power series may be differentiated term by term: (Inside its disc of convergence a complex power series is holomorphic and may be differentiated term by term).
A continuous real-valued function on a nonempty compact metric space is bounded and attains a maximum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).
A complex differentiable function is continuous (Complex differentiability at a point implies continuity there).
Complex polynomials, including every monomial, are holomorphic (Complex polynomials are entire with the power-rule derivative, and rational functions are holomorphic wherever their denominator is nonzero).
Closed bounded subsets of Euclidean space, including the interval , are compact (Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).
Complex modulus is multiplicative and satisfies the triangle inequality, hence (Conjugation is an involutive real-field automorphism, , and modulus is definite, multiplicative, and subadditive).
Every holomorphic function has complex derivatives of every order locally (All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle).
Counterexample
On , one has , so [L1] and the convergent series in [L2] give absolute pointwise and uniform convergence of the displayed series.
For real , [L3] gives .
Suppose, for contradiction, that a function holomorphic on for some agrees with on . By [L9], is holomorphic near , hence continuous by [L5]; [L8] makes continuous, [L7] makes compact, and [L4] bounds there.
Given , divergence in [L2] supplies with ; by [L6] and [L5], the finitely many monomials are continuous at , so choose with for every , and step 1.2 then gives .
Step 2.1 makes exceed every proposed bound for points , contradicting step 1.3; no such extension exists, and the refuted claim is false.
tends locally uniformly to zero on the unit disc but not uniformly on the closed disc
Statement refuted
Refuted claim: Local uniform convergence on the open unit disc forces uniform convergence on the closed unit disc.
For , the sequence converges locally uniformly to on , but it does not converge to uniformly, or even pointwise, on .
Facts & Assumptions
Given: The functions and the local-uniform convention of Locally uniform convergence on an open subset of the complex plane is compact convergence.
A continuous real-valued function on a nonempty compact metric space is bounded and attains a maximum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).
If a real satisfies , then (For the sequence is null, and for the sequence diverges to ).
Uniform convergence to zero requires that for every , all sufficiently late functions have modulus below at every point of the domain (Uniform convergence and the uniformly Cauchy condition for complex-valued functions, with the componentwise dictionary).
Complex modulus satisfies , so is continuous (Conjugation is an involutive real-field automorphism, , and modulus is definite, multiplicative, and subadditive).
Counterexample
Let be compact. If , uniform convergence on is vacuous. Otherwise [L4] and [L1] give , and because the maximum is attained at a point of ; then by [L2], uniformly for .
At the boundary point , one has for every natural , including , so the sequence does not converge pointwise to zero there and fails the uniform condition [L3] on .
Step 1.1 proves local uniform convergence on the open disc, while step 1.2 proves failure on its closure, so the claimed implication is false.
Morera's theorem fails without continuity
Statement refuted
Refuted claim: A function on an open subset of whose integral around every contained triangle is zero must be holomorphic, even when continuity is not assumed.
In the edgewise Riemann sense, the function
has zero integral around every complex triangle, but is not holomorphic.
Facts & Assumptions
Given: The displayed function and an arbitrary ordered complex triangle.
If the velocity-weighted pullback of a function along each affine triangle edge is Riemann integrable, its edgewise triangle integral is the sum of those edge integrals (The edgewise Riemann integral around a complex triangle for an integrable pullback).
Changing a real Riemann-integrable function at finitely many points preserves integrability and its integral (Changing an integrable function at finitely many points changes neither its integrability nor its integral).
Every complex differentiable function is continuous at the point of differentiability (Complex differentiability at a point implies continuity there).
Morera's theorem assumes continuity in addition to zero integrals around every contained filled triangle (Morera's theorem: vanishing triangle integrals characterize holomorphy among continuous functions).
Counterexample
Fix an arbitrary triangle and read its boundary integral in the edgewise sense of [L1] for the point-supported function .
The function is discontinuous at , since every punctured neighbourhood contains points where its value is while ; by [L3], it is not complex differentiable, and hence not holomorphic, at .
On a nonconstant affine edge, the edge map is injective and therefore meets at most once, so each real component of its velocity-weighted pullback differs from zero at at most one parameter and [L2] makes its integral zero; on a constant edge the velocity is zero, so its pullback integral is also zero. Hence [L1] gives zero around every triangle, including repeated or collinear vertices.
Steps 2.1 and 1.2 exhibit vanishing edgewise triangle integrals without holomorphy, so removing the continuity hypothesis from [L4] makes the implication false.
FALSE: every smooth map between open subsets of the plane is real analytic
Statement
False claim: Every smooth map between open subsets of is real analytic.
Facts & Assumptions
Given: The function and planar map defined by
The real exponential is and every derivative of it is the exponential itself (The exponential function is smooth and ).
The derivative of a composite is given by the chain rule when the component derivatives exist (The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with ).
Sums, scalar multiples, products, and quotients with nonzero denominator obey the corresponding derivative rules (Sums, scalar multiples, products and quotients: , , , and when ).
For every natural and real , as (The exponential dominates every fixed nonnegative integer power at ).
A planar real function is when every coordinate-derivative word of length at most , including the word of length zero, exists and is continuous ( maps and multi-index derivative notation in Euclidean space).
A smooth map is real analytic when, near every point, both components equal their total-degree Taylor series (Real-analytic maps between open subsets of the coordinate plane).
The real exponential is positive everywhere and satisfies (The exponential is positive and satisfies ).
Refutation
For every natural , repeated use of [L1], [L2], and [L3] gives a real polynomial such that for : take , and differentiation replaces by the polynomial .
As , every expression and its quotient by tends to : with , polynomial growth is bounded by a natural power of , which for is bounded by a natural power of , and [L4] applied to makes that power times tend to zero.
Inductively set every derivative value : step 2.1 makes continuous at and makes its difference quotient there tend to , so the next derivative exists and has value . Thus is smooth, and [L5] makes smooth with every mixed derivative at equal to .
By step 3.1, the total-degree Taylor series of at is the zero map, but [L7] gives for every ; such points occur in every neighbourhood of the origin, so the equality required by [L6] fails there.
The map is smooth by step 3.1 and not real analytic by step 4.1, so it refutes the false claim.
FALSE: an entire function bounded on the real axis is constant
Statement
False claim: If an entire function is bounded on the real axis, then it is constant.
Facts & Assumptions
Given: The complex sine function.
The complex sine and cosine power series have infinite radius of convergence (The exponential definitions of complex sine, cosine, hyperbolic sine, and hyperbolic cosine equal their entire power series).
Complex sine restricts to the published real sine function on the real axis (The exponential formulas, real restrictions, and trigonometric-hyperbolic dictionary over ).
For every real , (Parity and the Pythagorean identity for sine and cosine).
Complex sine and cosine are entire and satisfy and (Complex sine, cosine, hyperbolic sine, and hyperbolic cosine are entire with their standard derivatives).
Refutation
By [L1] and [L4], complex sine is entire; by [L2] and [L3], its restriction to the real axis satisfies for every real .
By [L4], the derivative of sine is cosine, and the series in [L1] gives , so sine has a nonzero derivative and is not constant.
Steps 1.1 and 1.2 give an entire function bounded on the real axis but not constant, refuting the claim; this does not contradict Liouville's theorem: every bounded entire function is constant, whose hypothesis is boundedness on the whole complex plane.
FALSE: every entire function with an antiderivative is a polynomial
Statement
False claim: Every entire function that has an entire antiderivative is a polynomial.
Facts & Assumptions
Given: The complex exponential function.
The complex exponential is entire and satisfies on (The complex exponential is entire and its complex derivative is itself).
For all complex , , and the complex exponential agrees with the real exponential on the real axis (, and the complex exponential extends the real exponential).
Every nonconstant complex polynomial has a complex root (Fundamental theorem of algebra: every nonconstant complex polynomial has a complex root).
The normalized real exponential satisfies and has derivative at (Regular normalized multiplicative Cauchy equations characterize the exponential).
Refutation
By [L1], the complex exponential is entire and is its own entire antiderivative.
By [L2] and [L4], , so the exponential never vanishes; [L1] then makes its derivative nonzero everywhere, and it is nonconstant.
If the complex exponential were a nonconstant polynomial, [L3] would give it a complex zero, contradicting step 1.2.
It is not a constant polynomial because its derivative is nonzero by step 1.2, and step 2.1 excludes every nonconstant polynomial; together with step 1.1, the exponential is an entire nonpolynomial function with an entire antiderivative, refuting the claim.
Sources
- B. V. Shabat, Introduction to Complex Analysis, Example 2.32
- E. Stein and R. Shakarchi, Complex Analysis, Ch. 2, Theorem 5.4
- B. V. Shabat, Introduction to Complex Analysis, Remark 2.25
- Lars Ahlfors, Complex Analysis, 3rd ed., Ch. 5 §1.1
- E. Stein and R. Shakarchi, Complex Analysis, Ch. 2 §5.2
- Matthias Weber, Complex Analysis, §2.4
- B. V. Shabat, Introduction to Complex Analysis, Remark 2.22
- Michael Taylor, Introduction to Analysis in Several Variables, Ch. 2 §2.2, Exercise 4
- Lars Ahlfors, Complex Analysis, 3rd ed., Ch. 4 §2.3
- E. Stein and R. Shakarchi, Complex Analysis, Ch. 2 §4
- Steven G. Krantz, A Guide to Complex Variables, §3.1.4