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.
A power series converges absolutely and uniformly on every closed interval strictly inside its interval of convergence
Statement
Let have radius , and let be a nonempty closed interval for which
Then the function series converges absolutely at every point of and converges uniformly there.
Facts & Assumptions
Given: A power series of radius and a closed interval satisfying the strict interior condition above (Intervals of : the nine order-convex forms, nondegeneracy, and length, A series of real-valued functions and its pointwise and uniform convergence through its partial sums).
The power series converges absolutely at every point whose distance from is less than (A real power series converges absolutely inside its radius and diverges outside it, while either behaviour may occur at an endpoint).
If for all and converges, the Weierstrass M-test gives absolute pointwise and uniform convergence of (The Weierstrass M-test gives absolute pointwise convergence and uniform convergence of a function series).
Proof
Choose a real with , or merely when . Then the scalar series converges by [L1], applied at .
For every , order-convexity gives , and hence for every .
Apply [L2] to and . The series is absolutely convergent at each and uniformly convergent on the whole interval.
Depends on
- A real power series converges absolutely inside its radius and diverges outside it, while either behaviour may occur at an endpoint
- The Weierstrass M-test gives absolute pointwise convergence and uniform convergence of a function series
- A series of real-valued functions and its pointwise and uniform convergence through its partial sums
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
Used by
- Inside its radius a real power series may be integrated term by term on every closed subinterval Corollary
- The sum of a real power series is continuous at every point strictly inside its interval of convergence Corollary
- Inside its radius a real power series may be differentiated term by term, and the differentiated series has the same radius Theorem
- Picard iteration from 1 produces the exponential partial sums Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 68 results over 14 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)