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.
Locally uniform limits of holomorphic functions are holomorphic, with locally uniform convergence of all derivatives
Statement
Let , let be open, let each be holomorphic, and suppose locally uniformly on : every point of has a neighbourhood on which the convergence is uniform. Then is holomorphic on , and for every multi-index
locally uniformly on .
Facts & Assumptions
Given: An open , holomorphic and with locally uniformly in the sense of Locally uniform convergence on an open subset of the complex plane is compact convergence and Uniform convergence and the uniformly Cauchy condition for complex-valued functions, with the componentwise dictionary; is read through Complex -space and its real coordinate dictionary.
A continuous separately holomorphic function on an open subset of is holomorphic (Osgood's lemma: continuous and separately holomorphic implies holomorphic).
For holomorphic on and a polyradius with , (Cauchy estimates for mixed derivatives on a polydisc).
If holomorphic functions of one variable converge locally uniformly on an open subset of , the limit is holomorphic (Locally uniform limits of holomorphic functions are holomorphic and their derivatives converge locally uniformly).
A uniform limit of continuous complex-valued functions on a metric space is continuous (A uniform limit of continuous complex-valued functions is continuous).
Separate holomorphy is holomorphy of each slice on its open slice domain (Separately holomorphic functions).
A holomorphic function of several variables is continuous and separately holomorphic (A holomorphic function of several variables is continuous and separately holomorphic); every iterated complex partial derivative of a holomorphic function is holomorphic (Holomorphic functions of several variables are smooth and their complex derivatives are holomorphic); differences of holomorphic functions are holomorphic (Sums, products and nonvanishing quotients of holomorphic functions are holomorphic).
, and are defined coordinatewise (Balls, polydiscs and the distinguished boundary in ); multi-index notation is that of maps and multi-index derivative notation in Euclidean 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, Open ball, closed ball and sphere in a metric space).
Proof
Each is continuous by [L6], and locally uniform convergence makes continuous at every point by [L4] applied on a neighbourhood where the convergence is uniform.
Fix and , and let be the th slice domain of through , an open subset of by [L5]. The slices of the are holomorphic on by [L6], and they converge to the slice of locally uniformly on , since a neighbourhood in of a point of the slice meets the slice in a neighbourhood there. So [L3] makes the slice of holomorphic on , and is separately holomorphic by [L5].
By steps 1.1 and 1.2 the limit is continuous and separately holomorphic on , so [L1] makes it holomorphic.
Fix and a multi-index . By [L8] choose with the ball and put , so by [L7] and [L9], and put . Shrinking if necessary, the convergence is uniform on .
Fix and put for each . Then because , and if then , so by [L7] and [L9]. Also because and . The difference is holomorphic on by [L6] and step 2.1, so [L2] applied on with inner polyradius gives .
The right-hand side of step 4.1 does not depend on and tends to by the uniform convergence of step 3.1, so uniformly on the neighbourhood of . Since and were arbitrary, the convergence is locally uniform for every multi-index.
Depends on
Osgood's lemma: continuous and separately holomorphic implies holomorphic
Cauchy estimates for mixed derivatives on a polydisc
Locally uniform limits of holomorphic functions are holomorphic and their derivatives converge locally uniformly
A uniform limit of continuous complex-valued functions is continuous
Locally uniform convergence on an open subset of the complex plane is compact convergence
Separately holomorphic functions
Uniform convergence and the uniformly Cauchy condition for complex-valued functions, with the componentwise dictionary
Holomorphic functions of several variables are smooth and their complex derivatives are holomorphic
Balls, polydiscs and the distinguished boundary in
A holomorphic function of several variables is continuous and separately holomorphic
Sums, products and nonvanishing quotients of holomorphic functions are holomorphic
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
Open ball, closed ball and sphere in a metric space
Complex -space and its real coordinate dictionary
Conjugation is an involutive real-field automorphism, , and modulus is definite, multiplicative, and subadditive
maps and multi-index derivative notation in Euclidean space