Alphabeta Math

Power Series and Real-Analytic Functions

About this page
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.

✓ 29 results · all verified · 2 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 27 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.
1 · Prerequisites
Abstract Algebra
Combinatorics
Linear Algebra
Real Analysis
Set Theory
Topology
2 · Logical flowchart

3 · Items

Definition

A real power series about a centre, its interval of convergence, and its radius in [0,+∞]

Theorem

Cauchy–Hadamard: the reciprocal radius is limsup_k→∞|aₖ₊₁|^1/(k+1), with the zero and infinite cases included

Corollary

A real power series converges absolutely inside its radius and diverges outside it, while either behaviour may occur at an endpoint

Theorem

A power series converges absolutely and uniformly on every closed interval strictly inside its interval of convergence

Corollary

The sum of a real power series is continuous at every point strictly inside its interval of convergence

Lemma

A power series, its formal derivative, and its zero-constant-term formal antiderivative have the same radius of convergence

Theorem

Inside its radius a real power series may be differentiated term by term, and the differentiated series has the same radius

Corollary

Inside its radius a real power series may be integrated term by term on every closed subinterval

Corollary

A power-series sum is infinitely differentiable inside its radius and satisfies aₙ=f⁽ⁿ⁾(c)/ι(n!) at its centre

Definition

Taylor and Maclaurin series

Lemma

The binomial double series used to re-expand a power series at an interior point is absolutely convergent and may be regrouped

Theorem

A power-series sum may be re-expanded about every interior point, with coefficients given by its derivatives there

Definition

A real-analytic function on an open subset of ℝ is locally represented by a convergent real power series

Theorem

Taylor-series representation by vanishing remainders

Theorem

The sum of a real power series is real analytic throughout the open interval determined by its radius

Corollary

Every real-analytic function is infinitely differentiable

Lemma

At a zero of a real-analytic function, either some first nonzero coefficient makes the zero isolated or every local coefficient vanishes

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

Lemma

Inside the common radius the product of two power-series sums is represented by the Cauchy product of their coefficients

Lemma

A composition of convergent real power series has a convergent power-series expansion wherever the inner series maps a neighbourhood into the outer disk of convergence

Lemma

A convergent real power series with nonzero constant term has a convergent reciprocal power series on a smaller neighbourhood

Theorem

Real-analytic functions are closed under sums, products and compositions, and under quotients where the denominator is nonzero

Definition

Abel summability by lim_x↑1∑ aₙxⁿ and Cesaro summability by the Cesaro means of the partial sums

Theorem

Abel's limit theorem: if a real series converges to s, then its power series tends to s as x↑1

Lemma

For 0<x<1, the Abel transform of a series is (1-x)²∑_n≥0(n+1)σₙxⁿ, where σₙ are the Cesaro means of its partial sums

Theorem

Frobenius' theorem: Cesaro summability of a real series implies Abel summability to the same value

Corollary

Every convergent real series is Cesaro summable and Abel summable to its ordinary sum

Lemma

If ι(n+1)aₙ→0, short multiplicative blocks of the coefficients have uniformly small sums

Theorem

Tauber's theorem: an Abel-summable series with ι(n+1)aₙ→0 converges ordinarily to its Abel sum

False statement

FALSE: every power series converges uniformly on its entire open interval of convergence

False statement

FALSE: convergence of a power series at one point other than its centre forces convergence at every real point

False statement

FALSE: Abel summability alone implies ordinary convergence of a series

Sources