Alphabeta MathHow 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.
Complex analytic functions are closed under finite linear combinations, products, quotients with nonzero denominator, and composition
Statement
On their natural domains, finite complex linear combinations and products of analytic functions are analytic; is analytic where ; and is analytic wherever maps into the domain of .
Facts & Assumptions
Given: Analytic functions with the domain conditions in the Statement.
Analyticity supplies a convergent local power-series representation at every point (Complex analytic functions as locally representable by convergent power series).
Sums and scalar multiples are represented coefficientwise on a common disc (Sums and scalar multiples of convergent complex power series are represented coefficientwise on the common disc).
Products are represented by Cauchy-product coefficients on a common disc (Products of convergent complex power series are represented by their Cauchy-product coefficients on the common disc).
Local compositions and reciprocals have convergent local power-series expansions under their stated centre and nonzero-constant hypotheses (A composition of convergent complex power series has a convergent local power-series expansion when the inner sum maps the centre to the outer centre, A convergent complex power series with nonzero constant term has a convergent reciprocal power series locally).
Proof
Fix a point in the relevant natural domain and choose local series for all participating functions by [L1], shrinking to a common disc when necessary.
Apply [L2] to finite linear combinations and [L3] to products.
If is nonzero at the point, its local series has nonzero constant term, so [L4] gives a reciprocal series and [L3] gives ; for composition, recenter the outer series at the inner value and apply [L4].
Each construction supplies a convergent power-series representation near every point of its stated domain, so each result is analytic by [L1].
Depends on
- Complex analytic functions as locally representable by convergent power series
- Sums and scalar multiples of convergent complex power series are represented coefficientwise on the common disc
- Products of convergent complex power series are represented by their Cauchy-product coefficients on the common disc
- A composition of convergent complex power series has a convergent local power-series expansion when the inner sum maps the centre to the outer centre
- A convergent complex power series with nonzero constant term has a convergent reciprocal power series locally
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: 44 results over 12 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
- Power-series supplementary notes, Colby College (standard reference, not scraped)