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.
A real-analytic function on an open subset of is locally represented by a convergent real power series
Definition
Let be open (Open subset of (every point has a neighbourhood inside it), closed subset (complement open), and clopen). A function is real analytic on if, for every , there are a real and real coefficients such that and
The representing series must converge throughout this neighbourhood (A real power series about a centre, its interval of convergence, and its radius in , The -neighbourhood and the punctured -neighbourhood of a point of ). The radius and coefficients may initially depend on .
Depends on
- A real power series about a centre, its interval of convergence, and its radius in $[0,+\infty]$
- Open subset of $\mathbb{R}$ (every point has a neighbourhood inside it), closed subset (complement open), and clopen
- The $\varepsilon$-neighbourhood and the punctured $\varepsilon$-neighbourhood of a point of $\mathbb{R}$
Used by
- Every real-analytic function is infinitely differentiable Corollary
- At a zero of a real-analytic function, either some first nonzero coefficient makes the zero isolated or every local coefficient vanishes Lemma
- Real-analytic functions are closed under sums, products and compositions, and under quotients where the denominator is nonzero Theorem
- The sum of a real power series is real analytic throughout the open interval determined by its radius Theorem
- Two real-analytic functions on an open interval that agree on a set with an accumulation point in that interval agree throughout the interval Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 44 results over 11 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
- Analytic function, Encyclopedia of Mathematics (standard reference, not scraped)
- E. Randles, Supplementary Notes for Real Analysis (standard reference, not scraped)