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
- Real analytic germs in several variables Definition
- A bounded function of two real variables whose every coordinate slice is real analytic is continuous False statement
- At a zero of a real-analytic function, either some first nonzero coefficient makes the zero isolated or every local coefficient vanishes Lemma
- Why local boundedness gives joint continuity here and nothing like it holds in the real case Remark
- 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 · two levels
17 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on 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)