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.
The sum of a real power series is continuous at every point strictly inside its interval of convergence
Statement
If for , then is continuous at every satisfying .
Facts & Assumptions
Given: A power-series sum and a point strictly inside its radius.
The series converges uniformly on each closed interval strictly inside its radius (A power series converges absolutely and uniformly on every closed interval strictly inside its interval of convergence).
Every polynomial partial sum is continuous, since constants, the identity, powers, scalar multiples and finite sums are continuous (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function).
A uniform limit of continuous real-valued functions is continuous (The uniform limit of continuous real-valued functions on a metric space is continuous).
Proof
Choose so small that lies strictly inside .
The polynomial partial sums are continuous on this interval by [L2] and converge uniformly there to by [L1].
By [L3], is continuous on that interval, and in particular at .
Depends on
- A power series converges absolutely and uniformly on every closed interval strictly inside its interval of convergence
- The uniform limit of continuous real-valued functions on a metric space is continuous
- Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function
Used by
- The exponential is a continuous bijection from ℝ onto (0,∞) Corollary
- A convergent real power series with nonzero constant term has a convergent reciprocal power series on a smaller neighbourhood Lemma
- At a zero of a real-analytic function, either some first nonzero coefficient makes the zero isolated or every local coefficient vanishes Lemma
- Cosine has a smallest positive zero, lying strictly between zero and two Theorem
- The exponential function is strictly increasing 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: 67 results over 15 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
- MIT 18.100C, Lecture 11: Power Series (standard reference, not scraped)
- Power series, Encyclopedia of Mathematics (standard reference, not scraped)
- E. Randles, Supplementary Notes for Real Analysis (standard reference, not scraped)