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.

Power Series and Real-Analytic Functions

1 · Prerequisites

2 · Summary

This page builds on uniform convergence and its differentiation and integration limit theorems, absolute convergence and Cauchy products, completeness through limit superior, finite binomial coefficients, Cesaro means, and the working fundamental theorem of calculus. These tools control power series on compact subintervals and justify every interchange of limits, sums, derivatives, and integrals.

The resulting theory includes Cauchy–Hadamard with explicit zero and infinite conventions, re-expansion, real analyticity, isolated zeros and the identity theorem, algebraic and compositional closure, and Abel and Cesaro summability. Abel's boundary theorem, Frobenius' implication, and Tauber's converse show exactly how ordinary convergence interacts with the two summability methods; accompanying false statements mark the missing hypotheses.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-07-31Open item page →

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

Definition

Let $(a_{n})_{n \in N}$ be a sequence of reals and let $c \in R$ . The real power series about the centre $c$ with coefficients $(a_{n})$ is the series

$\sum_{n = 0}^{\infty} a_{n} (x - c)^{n}$

at a real argument $x$ , where powers are those of Integer powers $a^{m}$ and convergence is that of Series, partial sums, convergence and the sum, divergence, and the tail series. Its value, when the series converges, is called its sum at $x$ . At $x = c$ the series always converges to $a_{0}$ : the term with $n = 0$ is $a_{0}$ because $0^{0} = 1$ , and every later term is $0$ .

For $r \geq 0$ let $P (r)$ mean that the series converges absolutely at every real $x$ with $∣ x - c ∣ < r$ . The set of such $r$ contains $0$ , since the condition $∣ x - c ∣ < 0$ has no solutions. The radius of convergence is

$R : = \sup_{\overline{R}} {r \in R : r \geq 0 and P (r)} \in [0, + \infty],$

where the supremum is taken in the extended real line of The extended real line $\overline{R} = R \cup {- \infty, + \infty}$ , its order, and the arithmetic that is left undefined. Thus $R$ may be a nonnegative real or $+ \infty$ , but never $- \infty$ .

The open interval determined by the radius is

$I_{R} : = {x \in R : ∣ x - c ∣ < R} .$

When $0 < R < + \infty$ this is $(c - R, c + R)$ , when $R = + \infty$ it is all of $R$ , and when $R = 0$ it is empty. The centre still carries the convergent value $a_{0}$ in the last case. No endpoint is included in $I_{R}$ ; convergence at $c - R$ or $c + R$ , when these are real, is a separate question.

Remarks

The radius is extended-valued, but no undefined arithmetic in $\overline{R}$ is used. Expressions such as $c \pm R$ are written only when $R$ is finite. The reciprocal conventions used in Cauchy-Hadamard are stated explicitly in Cauchy–Hadamard: the reciprocal radius is ${lim sup}_{k \to \infty} ∣ a_{k + 1} ∣^{1 / (k + 1)}$ , with the zero and infinite cases included.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31Open item page →

Cauchy–Hadamard: the reciprocal radius is ${lim sup}_{k \to \infty} ∣ a_{k + 1} ∣^{1 / (k + 1)}$ , with the zero and infinite cases included

Statement

Let $\sum_{n \geq 0} a_{n} (x - c)^{n}$ be a real power series with radius $R$ (A real power series about a centre, its interval of convergence, and its radius in $[0, + \infty]$ ), and put

$L : = {lim sup}_{k \to \infty} ∣ a_{k + 1} ∣^{1 / (k + 1)} \in [0, + \infty] .$

Then $R$ is the reciprocal of $L$ in the following explicit sense:

$R = {\begin{cases} + \infty, & L = 0, \\ 1 / L, & 0 < L < + \infty, \\ 0, & L = + \infty . \end{cases}$

Equivalently, with the conventions $1 / 0 : = + \infty$ and $1 / (+ \infty) : = 0$ , one has $R = 1 / L$ . The roots use $a_{k + 1}$ and the exponent $1 / (k + 1)$ because $N$ starts at $0$ and a zeroth root is undefined.

Facts & Assumptions

Given: A real power series $\sum a_{n} (x - c)^{n}$ , its radius $R$ , the nonnegative root sequence $q_{k} : = ∣ a_{k + 1} ∣^{1 / (k + 1)}$ , and $L : = {lim sup}_{k} q_{k}$ .

[L1]

The limit superior $L$ exists in $\overline{R}$ for every real sequence (Limit superior and limit inferior of a real sequence as $\inf_{n} \sup_{k \geq n} x_{k}$ and $\sup_{n} \inf_{k \geq n} x_{k}$ in $\overline{R}$ , The tail suprema of any real sequence are nonincreasing in $\overline{R}$ , so the limit superior exists for every sequence).

[L2]

If $L$ is real, then for every real $ε > 0$ , $q_{k} < L + ε$ eventually and $q_{k} > L - ε$ frequently (For finite $L$ : $L = lim sup x_{k}$ iff for every $ε > 0$ one has $x_{k} < L + ε$ eventually and $x_{k} > L - ε$ frequently).

[L3]

The root test says that a real series from index $1$ converges absolutely when the limit superior of its shifted roots is $< 1$ , and diverges when that limit superior is $> 1$ (Root test: $lim sup ∣ a_{k} ∣^{1 / k} < 1$ gives absolute convergence and hence convergence, $> 1$ gives divergence, and $= 1$ decides nothing).

[L4]

Absolute convergence means convergence of the series of absolute values (Absolutely convergent and conditionally convergent series, and the general starting index).

Proof

technique · direct

1.1

Fix $x \in R$ and put $d : = ∣ x - c ∣$ . The shifted roots of the terms $a_{n} (x - c)^{n}$ , $n \geq 1$ , are $∣ a_{k + 1} (x - c)^{k + 1} ∣^{1 / (k + 1)} = q_{k} d$ .

givenalgebra

2.1

If $L = 0$ , then for $d = 0$ every root in step 1.1 is $0$ , while for $d > 0$ and any $η > 0$ , [L2] applied with $ε = η / d$ makes $q_{k} d < η$ eventually. Thus ${lim sup}_{k} (q_{k} d) = 0 < 1$ for every $x$ .

step 1.1L2

2.2

Suppose $0 < L < + \infty$ . If $d < 1 / L$ , choose a real $t$ with $L < t < 1 / d$ (with the second inequality omitted when $d = 0$ ). By [L2], $q_{k} < t$ eventually, so ${lim sup}_{k} (q_{k} d) \leq t d < 1$ . If $d > 1 / L$ , choose $t$ with $1 / d < t < L$ ; [L2] gives $q_{k} > t$ frequently, so ${lim sup}_{k} (q_{k} d) \geq t d > 1$ .

step 1.1L2choose

2.3

If $L = + \infty$ and $d > 0$ , then for every real $M > 0$ and every index $N$ there is $k \geq N$ with $q_{k} > M$ : otherwise $M$ would bound a tail and its supremum, forcing the infimum of the tail suprema to be finite. Taking $M > 1 / d$ shows $q_{k} d > 1$ arbitrarily late, hence ${lim sup}_{k} (q_{k} d) > 1$ .

L1step 1.1choose

3.1

By [L3] and [L4], step 2.1 gives absolute convergence at every real $x$ when $L = 0$ ; step 2.2 gives absolute convergence for $d < 1 / L$ and divergence for $d > 1 / L$ when $0 < L < + \infty$ ; and step 2.3 gives divergence at every $x \neq c$ when $L = + \infty$ , while the series converges at $c$ to $a_{0}$ .

step 2.1step 2.2step 2.3L3L4

4.1

Reading these three alternatives through the definition of the radius yields $R = + \infty$ , $R = 1 / L$ , and $R = 0$ , respectively, which is the stated convention-complete formula.

step 3.1∎

CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31Open item page →

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

Statement

Let $\sum a_{n} (x - c)^{n}$ have radius $R$ . It converges absolutely at every $x$ with $∣ x - c ∣ < R$ and diverges at every $x$ with $∣ x - c ∣ > R$ . When $0 < R < + \infty$ , no common conclusion holds at either endpoint $c \pm R$ : power series of radius $R$ can converge there, even absolutely, or diverge there.

Facts & Assumptions

Given: A real power series $\sum a_{n} (x - c)^{n}$ with radius $R$ (A real power series about a centre, its interval of convergence, and its radius in $[0, + \infty]$ ).

[L1]

Cauchy-Hadamard identifies $R$ from the limit superior of the coefficient roots and the root test gives absolute convergence below the reciprocal threshold and divergence above it (Cauchy–Hadamard: the reciprocal radius is ${lim sup}_{k \to \infty} ∣ a_{k + 1} ∣^{1 / (k + 1)}$ , with the zero and infinite cases included).

[L2]

At root-test boundary value $1$ , the coefficient families $1 / (n + 1)$ and $1 / (n + 1)^{2}$ both have root limit superior $1$ , while the first series diverges and the second converges; changing the coefficient signs does not change their absolute values (Root test: $lim sup ∣ a_{k} ∣^{1 / k} < 1$ gives absolute convergence and hence convergence, $> 1$ gives divergence, and $= 1$ decides nothing, claim 3).

Proof

technique · direct

1.1

The assertions for $∣ x - c ∣ < R$ and $∣ x - c ∣ > R$ are exactly the two strict alternatives supplied by [L1], including the cases $R = 0$ and $R = + \infty$ .

1.2

For endpoint behaviour at radius $1$ , the series with coefficients $1 / (n + 1)^{2}$ converges absolutely at both $x = 1$ and $x = - 1$ . The series with coefficients $1 / (n + 1)$ diverges at $x = 1$ , while the series with coefficients $(- 1)^{n} / (n + 1)$ diverges at $x = - 1$ . All three have radius $1$ by [L2].

2.1

Replacing $x$ by $(x - c) / R$ and multiplying coefficients by the corresponding powers of $R^{- 1}$ transports the two radius-one examples to any finite $R > 0$ and centre $c$ . Thus either behaviour may occur at an endpoint, while no assertion has been made when the endpoints are not real.

step 1.2algebra∎

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31Open item page →

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

Statement

Let $\sum a_{n} (x - c)^{n}$ have radius $R$ , and let $[u, v]$ be a nonempty closed interval for which

$r : = \max {∣ u - c ∣, ∣ v - c ∣} < R .$

Then the function series converges absolutely at every point of $[u, v]$ and converges uniformly there.

Facts & Assumptions

Given: A power series of radius $R$ and a closed interval $[u, v]$ satisfying the strict interior condition above (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, A series of real-valued functions and its pointwise and uniform convergence through its partial sums).

[L1]

The power series converges absolutely at every point whose distance from $c$ is less than $R$ (A real power series converges absolutely inside its radius and diverges outside it, while either behaviour may occur at an endpoint).

[L2]

If $∣ f_{n} (x) ∣ \leq M_{n}$ for all $n, x$ and $\sum M_{n}$ converges, the Weierstrass M-test gives absolute pointwise and uniform convergence of $\sum f_{n}$ (The Weierstrass M-test gives absolute pointwise convergence and uniform convergence of a function series).

Proof

technique · direct

1.1

Choose a real $ρ$ with $r < ρ < R$ , or merely $ρ > r$ when $R = + \infty$ . Then the scalar series $\sum ∣ a_{n} ∣ ρ^{n}$ converges by [L1], applied at $x = c + ρ$ .

givenL1choose

1.2

For every $x \in [u, v]$ , order-convexity gives $∣ x - c ∣ \leq \max {∣ u - c ∣, ∣ v - c ∣} = r < ρ$ , and hence $∣ a_{n} (x - c)^{n} ∣ \leq ∣ a_{n} ∣ ρ^{n}$ for every $n$ .

givenalgebra

2.1

Apply [L2] to $f_{n} (x) = a_{n} (x - c)^{n}$ and $M_{n} = ∣ a_{n} ∣ ρ^{n}$ . The series is absolutely convergent at each $x \in [u, v]$ and uniformly convergent on the whole interval.

step 1.1step 1.2L2∎

CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31Open item page →

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

Statement

If $f (x) = \sum_{n \geq 0} a_{n} (x - c)^{n}$ for $∣ x - c ∣ < R$ , then $f$ is continuous at every $x_{0}$ satisfying $∣ x_{0} - c ∣ < R$ .

Facts & Assumptions

Given: A power-series sum $f$ and a point $x_{0}$ strictly inside its radius.

[L1]

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).

[L2]

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).

[L3]

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

technique · direct

1.1

Choose $δ > 0$ so small that $[x_{0} - δ, x_{0} + δ]$ lies strictly inside $∣ x - c ∣ < R$ .

givenchoose

1.2

The polynomial partial sums are continuous on this interval by [L2] and converge uniformly there to $f$ by [L1].

L1L2

2.1

By [L3], $f$ is continuous on that interval, and in particular at $x_{0}$ .

step 1.2L3∎

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-07-31Open item page →

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

Statement

For a power series $\sum_{n \geq 0} a_{n} (x - c)^{n}$ , define its formal derivative and its zero-constant-term formal antiderivative by

$\sum_{n \geq 0} ι (n + 1) a_{n + 1} (x - c)^{n}, \sum_{n \geq 0} \frac{a_{n}}{ι (n + 1)} (x - c)^{n + 1},$

where $ι (n + 1) > 0$ is the canonical natural in $R$ (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Canonical naturals are positive and strictly increasing). All three power series have the same radius of convergence.

Facts & Assumptions

Given: The three formal power series in the statement, centred at the same real $c$ .

[L1]

For $0 \leq q < 1$ , the geometric series $\sum q^{n}$ converges. Its terms are nonnegative, so $∣ q^{n} ∣ = q^{n}$ and the convergence is absolute (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges, Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ , Basic properties of the absolute value).

[L2]

The Cauchy product of two absolutely convergent series converges absolutely; applying this to two copies of $\sum q^{n}$ shows that $\sum_{n \geq 0} ι (n + 1) q^{n}$ converges (If $\sum a_{k}$ and $\sum b_{k}$ both converge absolutely then their Cauchy product converges absolutely, with sum $A B$ ).

[L3]

The terms of a convergent series tend to $0$ (If a series converges then its terms tend to $0$ ), a convergent sequence is bounded (Every convergent sequence is bounded), and direct comparison preserves convergence of nonnegative series (If $0 \leq a_{k} \leq b_{k}$ eventually, convergence of $\sum b_{k}$ gives convergence of $\sum a_{k}$ , and divergence of $\sum a_{k}$ gives divergence of $\sum b_{k}$ ).

[L4]

The canonical naturals $ι (n + 1)$ are positive and at least $1$ (Canonical naturals are positive and strictly increasing).

Proof

technique · direct

1.1

Fix distances $0 \leq r < s$ and put $q = r / s$ when $s > 0$ . By [L2], the series with nonnegative terms $ι (n + 1) q^{n}$ converges. Its terms tend to $0$ and hence form a bounded sequence by [L3], say with bound $M$ .

L1L2L3choose

1.2

Conversely, if the derivative series converges absolutely at a distance $s > 0$ , then $∣ a_{n + 1} ∣ s^{n + 1} \leq s ι (n + 1) ∣ a_{n + 1} ∣ s^{n}$ because $ι (n + 1) \geq 1$ . Comparison gives absolute convergence of the original series there, after adjoining its first term.

L3L4algebra

1.3

If the original series converges absolutely at distance $s > 0$ , then the antiderivative terms satisfy $∣ a_{n} ∣ s^{n + 1} / ι (n + 1) \leq s ∣ a_{n} ∣ s^{n}$ , so the antiderivative converges absolutely at $s$ .

L3L4algebra

2.1

Suppose the original series converges absolutely at distance $s > 0$ . Its shifted absolute terms $u_{n} : = ∣ a_{n + 1} ∣ s^{n + 1}$ form a convergent series. At distance $r < s$ , the derivative's absolute terms satisfy $ι (n + 1) ∣ a_{n + 1} ∣ r^{n} = s^{- 1} ι (n + 1) q^{n} u_{n} \leq (M / s) u_{n}$ , so the derivative series converges absolutely there by [L3].

step 1.1L3

2.2

Conversely, if the antiderivative converges absolutely at distance $s > 0$ , put $v_{n} : = ∣ a_{n} ∣ s^{n + 1} / ι (n + 1)$ . At every $r < s$ , $∣ a_{n} ∣ r^{n} = s^{- 1} ι (n + 1) q^{n} v_{n} \leq (M / s) v_{n}$ , so the original series converges absolutely at $r$ by [L3].

step 1.1L3

3.1

Write $R_{0}, R_{D}, R_{I}$ for the three radii. If $0 \leq r < R_{0}$ , the supremum definition supplies an admissible distance $s > r$ for the original series; choosing $u$ with $r < u < s$ , the original series is absolutely convergent at $u$ , and step 2.1 makes the derivative absolutely convergent at every distance below $r$ . Thus $r$ is admissible for the derivative and $R_{0} \leq R_{D}$ . Conversely, if $0 \leq r < R_{D}$ , choose an admissible derivative distance $s > r$ and then $u$ with $r < u < s$ . The derivative converges absolutely at $u$ , so step 1.2 and direct comparison make the original series absolutely convergent at every distance below $r$ ; hence $R_{D} \leq R_{0}$ . The same argument with steps 1.3 and 2.2 gives $R_{0} = R_{I}$ . Therefore all three extended radii are equal, including $0$ and $+ \infty$ .

givenstep 2.1step 1.2step 1.3step 2.2L3∎

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31Open item page →

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

Statement

Let

$f (x) = \sum_{n = 0}^{\infty} a_{n} (x - c)^{n}$

have radius $R$ . For every $x$ with $∣ x - c ∣ < R$ , the function $f$ is differentiable at $x$ (The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set) and

$f^{'} (x) = \sum_{n = 0}^{\infty} ι (n + 1) a_{n + 1} (x - c)^{n} .$

The differentiated series has the same radius $R$ .

Facts & Assumptions

Given: A real power series of radius $R$ with polynomial partial sums $p_{N} (x) : = \sum_{n < N} a_{n} (x - c)^{n}$ .

[L1]

The formal derivative series has radius $R$ (A power series, its formal derivative, and its zero-constant-term formal antiderivative have the same radius of convergence).

[L2]

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

[L3]

If continuously differentiable functions converge at one point of a closed interval and their derivatives converge uniformly, then the functions converge uniformly to a differentiable function whose derivative is the derivative limit (If continuously differentiable functions converge at one point and their derivatives converge uniformly on a closed interval, then the functions converge uniformly to a differentiable function whose derivative is the derivative limit).

[L4]

The derivative of $(x - c)^{n}$ is $0$ for $n = 0$ and $ι (n) (x - c)^{n - 1}$ for $n \geq 1$ (For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term and the algebra of derivatives cited there).

Proof

technique · direct

1.1

Fix $x_{0}$ with $∣ x_{0} - c ∣ < R$ and choose a closed interval $J$ containing both $c$ and $x_{0}$ strictly inside the radius.

givenchoose

1.2

Each $p_{N}$ is continuously differentiable on $J$ , and [L4] gives $p_{N}^{'} (x) = \sum_{n < N - 1} ι (n + 1) a_{n + 1} (x - c)^{n}$ . The derivative partial sums converge uniformly on $J$ by [L1] and [L2].

L1L2L4

2.1

The sequence $p_{N} (c)$ converges to $a_{0}$ , since it equals $a_{0}$ for every $N \geq 1$ . Thus [L3] applies and says that the uniform limit of $(p_{N})$ on $J$ is differentiable with derivative equal to the uniform limit of $(p_{N}^{'})$ .

step 1.2L3

3.1

The uniform limit of $(p_{N})$ is $f$ , and the limit of $(p_{N}^{'})$ is the displayed differentiated series. Hence the formula holds at $x_{0}$ ; since $x_{0}$ was arbitrary it holds throughout $∣ x - c ∣ < R$ , and [L1] supplies the equality of radii.

step 2.1L1∎

CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31Open item page →

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

Statement

Let $f (x) = \sum_{n \geq 0} a_{n} (x - c)^{n}$ have radius $R$ , and define

$G (x) : = \sum_{n = 0}^{\infty} \frac{a_{n}}{ι (n + 1)} (x - c)^{n + 1} .$

For every closed interval $[u, v]$ strictly inside $∣ x - c ∣ < R$ , the function $f$ is Riemann integrable and

$\int_{u}^{v} f (x) d x = G (v) - G (u) = \sum_{n = 0}^{\infty} \frac{a_{n}}{ι (n + 1)} ((v - c)^{n + 1} - (u - c)^{n + 1}) .$

Thus the power series may be integrated term by term, and the antiderivative series has radius $R$ .

Facts & Assumptions

Given: The power-series sum $f$ , its zero-constant-term formal antiderivative $G$ , and a closed interval $[u, v]$ strictly inside the radius.

[L1]

The antiderivative series has radius $R$ (A power series, its formal derivative, and its zero-constant-term formal antiderivative have the same radius of convergence).

[L2]

Both series converge uniformly on $[u, v]$ (A power series converges absolutely and uniformly on every closed interval strictly inside its interval of convergence), and a uniform limit of integrable functions is integrable with the integral equal to the limit of the integrals (A uniform limit of Riemann-integrable functions is Riemann integrable, and its integral is the limit of their integrals).

[L3]

Termwise differentiation applied to $G$ gives $G^{'} = f$ on the open radius interval (Inside its radius a real power series may be differentiated term by term, and the differentiated series has the same radius).

[L4]

If $H (x) = \int_{u}^{x} f$ , then $H^{'} = f$ on $(u, v)$ because $f$ is continuous on $[u, v]$ (The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive).

[L5]

Differentiable functions are continuous, and two continuous functions on an interval with the same derivative differ by a constant (A function differentiable at $c$ is continuous at $c$ , A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant).

Proof

technique · direct

1.1

By [L1] and [L2], $G$ and $f$ converge uniformly on $[u, v]$ ; in particular $f$ is integrable there, and [L3] gives $G^{'} = f$ .

L1L2L3

2.1

Define $H (x) : = \int_{u}^{x} f (t) d t$ . The sum $f$ is continuous as a differentiable function by [L3] and [L5], so [L4] gives $H^{'} = f$ on $(u, v)$ , while the integral construction makes $H$ continuous on $[u, v]$ .

step 1.1L3L4L5

3.1

The functions $H$ and $G$ are continuous and have the same derivative on the interval. By [L5], $H - G$ is constant; evaluating at $u$ gives $H (v) = G (v) - G (u)$ .

step 2.1L5

4.1

Subtracting the two convergent series for $G (v)$ and $G (u)$ term by term is licensed by their convergence, and gives the displayed series. This is also the limit of the integrals of the polynomial partial sums by [L2].

step 3.1L2algebra∎

CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31Open item page →

A power-series sum is infinitely differentiable inside its radius and satisfies $a_{n} = f^{(n)} (c) / ι (n!)$ at its centre

Statement

Let $f (x) = \sum_{n \geq 0} a_{n} (x - c)^{n}$ have positive or infinite radius $R$ . Define $f^{(0)} : = f$ and $f^{(m + 1)} : = (f^{(m)})^{'}$ . Then every derivative exists on $∣ x - c ∣ < R$ , and for each $m \in N$ ,

$f^{(m)} (x) = \sum_{j = 0}^{\infty} ι ⁣ ((m + j)^{\underline{m}}) a_{m + j} (x - c)^{j} .$

In particular,

$f^{(m)} (c) = ι (m!) a_{m}, a_{m} = \frac{f^{(m)} (c)}{ι (m!)} .$

Facts & Assumptions

Given: A power-series sum $f$ of radius $R > 0$ and the recursively defined derivatives $f^{(m)}$ .

[L1]

A power series may be differentiated term by term throughout its open radius, and its first derived series has the same radius (Inside its radius a real power series may be differentiated term by term, and the differentiated series has the same radius).

[L2]

Falling factorials satisfy $n^{\underline{0}} = 1$ and $n^{\underline{k + 1}} = n^{\underline{k}} (n - k)$ for all natural $n, k$ , with truncated difference $n - k$ , and $n^{\underline{n}} = n! \neq 0$ (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ); the canonical embedding into $R$ is multiplicative and injective (Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ ).

[L3]

The induction principle on $N$ (The principle of mathematical induction).

Proof

technique · induction

1.1

For $m = 0$ , the formula reads $f (x) = \sum_{j \geq 0} ι (j^{\underline{0}}) a_{j} (x - c)^{j} = \sum_{j \geq 0} a_{j} (x - c)^{j}$ , so the claim holds.

basegivenL2

1.2

Fix $m$ and assume the displayed formula for $f^{(m)}$ , with radius $R$ .

2.1

By [L1], differentiate the series in step 1.2 term by term. Reindexing $j + 1$ as $j$ gives $f^{(m + 1)} (x) = \sum_{j \geq 0} ι (j + 1) ι ((m + j + 1)^{\underline{m}}) a_{m + j + 1} (x - c)^{j}$ .

step 1.2L1

3.1

The falling-factorial recursion with $n = m + j + 1$ and $k = m$ gives $(m + j + 1)^{\underline{m + 1}} = (m + j + 1)^{\underline{m}} (j + 1)$ . Since $ι$ preserves products, step 2.1 is precisely the asserted formula with $m + 1$ in place of $m$ .

step 2.1L2algebra

4.1

By [L3], the derivative formula holds for every $m$ . At each induction step [L1] also preserves the radius $R$ , so every derived series has radius $R$ .

step 1.1step 3.1L1L3discharge-induction

5.1

At $x = c$ , every term with $j \geq 1$ vanishes and the $j = 0$ term is $ι (m^{\underline{m}}) a_{m} = ι (m!) a_{m}$ ; since $m! \neq 0$ , division gives the coefficient formula.

step 4.1L2discharge-induction∎

DefinitionDefinition: Literature-sourcedProof: Not applicableprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-14Open item page →

Taylor and Maclaurin series

Definition

Let $I \subseteq R$ be an open interval, let $f \in C^{\infty} (I)$ (Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ ), and let $a \in I$ . The Taylor series of $f$ at $a$ is the real power series

$\sum_{n = 0}^{\infty} \frac{f^{(n)} (a)}{n!} (x - a)^{n} .$

Its $n$ th partial sum is the Taylor polynomial $T_{n, a} f$ (Taylor polynomials and their remainders). When $a = 0$ , the series is called the Maclaurin series of $f$ . This definition names a power series (A real power series about a centre, its interval of convergence, and its radius in $[0, + \infty]$ ); by itself it asserts neither that the series converges nor that its sum equals $f$ .

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-07-31Open item page →

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

Statement

Let $\sum_{n \geq 0} a_{n} (x - c)^{n}$ have radius $R$ , let $d$ satisfy $∣ d - c ∣ < R$ , and let $h$ satisfy $∣ d - c ∣ + ∣ h ∣ < R$ . Then

$\sum_{n = 0}^{\infty} \sum_{k = 0}^{n} ι ⁣ (\binom{n}{k}) ∣ a_{n} ∣ ∣ d - c ∣^{n - k} ∣ h ∣^{k} < \infty .$

Consequently the binomial double series is absolutely convergent and may be regrouped by powers of $h$ :

$\sum_{n = 0}^{\infty} a_{n} (d + h - c)^{n} = \sum_{k = 0}^{\infty} (\sum_{n = k}^{\infty} ι ⁣ (\binom{n}{k}) a_{n} (d - c)^{n - k}) h^{k} .$

Facts & Assumptions

Given: The power series and points $c, d, d + h$ from the statement.

[L1]

A power series converges absolutely at every distance smaller than its radius (A real power series converges absolutely inside its radius and diverges outside it, while either behaviour may occur at an endpoint).

[L2]

The binomial theorem gives $\sum_{k = 0}^{n} ι ⁣ (\binom{n}{k}) u^{n - k} v^{k} = (u + v)^{n}$ for all real $u, v$ (The binomial theorem in $R$ : $(x + y)^{n} = \sum_{k < n + 1} ι ⁣ (\binom{n}{k}) x^{k} y^{n - k}$ ).

[L3]

An absolutely convergent double series may be summed and regrouped in either order (Fubini for double series: if $\sum_{i} \sum_{j} ∣ a_{i j} ∣$ converges then both iterated sums and the sum along every bijection $N \to N \times N$ converge to one and the same value, Absolutely convergent and conditionally convergent series, and the general starting index).

Proof

technique · direct

1.1

Put $ρ : = ∣ d - c ∣ + ∣ h ∣ < R$ . By [L2], the sum of the absolute values in row $n$ is $∣ a_{n} ∣ ρ^{n}$ .

givenL2algebra

2.1

The series $\sum_{n} ∣ a_{n} ∣ ρ^{n}$ converges by [L1], so the triangular double series is absolutely convergent.

step 1.1L1

3.1

Apply the binomial theorem before summing and [L3] to regroup the absolutely convergent double series by $k$ . This yields the displayed identity.

step 2.1L2L3∎

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31Open item page →

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

Statement

Suppose $f (x) = \sum_{n \geq 0} a_{n} (x - c)^{n}$ has radius $R$ , and let $d$ satisfy $∣ d - c ∣ < R$ . Then for every real $x$ with

$∣ d - c ∣ + ∣ x - d ∣ < R$

one has

$f (x) = \sum_{k = 0}^{\infty} \frac{f^{(k)} (d)}{ι (k!)} (x - d)^{k} .$

Thus the sum may be re-expanded about every interior point.

Facts & Assumptions

Given: The series for $f$ and the interior point $d$ .

[L1]

The binomial double series is absolutely convergent when $∣ d - c ∣ + ∣ x - d ∣ < R$ and may be regrouped by powers of $x - d$ (The binomial double series used to re-expand a power series at an interior point is absolutely convergent and may be regrouped).

[L2]

Repeated termwise differentiation gives $f^{(k)} (d) = \sum_{n \geq k} ι (n^{\underline{k}}) a_{n} (d - c)^{n - k}$ (A power-series sum is infinitely differentiable inside its radius and satisfies $a_{n} = f^{(n)} (c) / ι (n!)$ at its centre).

[L3]

$(\binom{n}{k}) k! = n^{\underline{k}}$ for $k \leq n$ ( $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ ).

Proof

technique · direct

1.1

Fix $x$ satisfying the stated inequality and set $h : = x - d$ . By [L1], $f (x) = \sum_{k \geq 0} b_{k} h^{k}$ , where $b_{k} : = \sum_{n \geq k} ι ⁣ (\binom{n}{k}) a_{n} (d - c)^{n - k}$ .

givenL1

2.1

By [L2] and [L3], $ι (k!) b_{k} = f^{(k)} (d)$ for every $k$ .

step 1.1L2L3algebra

3.1

Substituting the coefficient identity from step 2.1 into the series in step 1.1 proves the formula.

step 1.1step 2.1∎

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-07-31Open item page →

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

Definition

Let $U \subseteq R$ be open (Open subset of $R$ (every point has a neighbourhood inside it), closed subset (complement open), and clopen). A function $f : U \to R$ is real analytic on $U$ if, for every $c \in U$ , there are a real $r > 0$ and real coefficients $(a_{n})_{n \in N}$ such that $N_{r} (c) \subseteq U$ and

$f (x) = \sum_{n = 0}^{\infty} a_{n} (x - c)^{n} (x \in N_{r} (c)) .$

The representing series must converge throughout this neighbourhood (A real power series about a centre, its interval of convergence, and its radius in $[0, + \infty]$ , The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ ). The radius and coefficients may initially depend on $c$ .

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-14Open item page →

Taylor-series representation by vanishing remainders

Statement

Let $I$ be an open interval, let $f \in C^{\infty} (I)$ , and let $a \in I$ . For each $x \in I$ , $f (x)$ equals the sum of the Taylor series of $f$ at $a$ if and only if

$R_{n, a} f (x) ⟶ 0.$

Moreover, let $r > 0$ and suppose that $[a - r, a + r] \subset I$ . For every $n \geq 0$ , set

$M_{n + 1} : = \max_{∣ t - a ∣ \leq r} ∣ f^{(n + 1)} (t) ∣ .$

$\frac{M_{n + 1} r^{n + 1}}{(n + 1)!} ⟶ 0,$

then the Taylor polynomials $T_{n, a} f$ converge uniformly to $f$ on the compact interval $[a - r, a + r]$ .

Facts & Assumptions

Given: An open interval $I$ , a function $f \in C^{\infty} (I)$ , a point $a \in I$ , and the Taylor polynomials and remainders of $f$ at $a$ .

[A1]

For the uniform assertion, $r > 0$ , $[a - r, a + r] \subset I$ , and $M_{n + 1} r^{n + 1} / (n + 1)! \to 0$ , where $M_{n + 1} = \max_{∣ t - a ∣ \leq r} ∣ f^{(n + 1)} (t) ∣$ .

[L1]

The $n$ th partial sum of the Taylor series at $a$ is $T_{n, a} f$ , and $R_{n, a} f (x) = f (x) - T_{n, a} f (x)$ (Taylor and Maclaurin series, Taylor polynomials and their remainders).

[L2]

A continuous real-valued function on a nonempty compact set attains its maximum and minimum (Extreme value theorem: a continuous real function on a nonempty compact subset of $R$ attains a greatest and a least value).

[L3]

If $∣ f^{(n + 1)} (t) ∣ \leq M$ throughout the closed interval between $a$ and $x$ , then $∣ R_{n, a} f (x) ∣ \leq \frac{M ∣ x - a ∣^{n + 1}}{(n + 1)!}$ (A uniform derivative bound gives a uniform Taylor remainder bound).

[L4]

A sequence $(g_{n})$ converges uniformly to $g$ on a set $E$ exactly when, for every $ε > 0$ , there is $N$ such that $∣ g_{n} (x) - g (x) ∣ < ε$ for every $x \in E$ and every $n \geq N$ (Pointwise convergence, uniform convergence, and the uniformly Cauchy condition for sequences of real-valued functions).

[L5]

A function is of class $C^{k}$ on an interval when $f^{(j)}$ exists there for every $j \leq k$ and each such $f^{(j)}$ is continuous there, and it is smooth, or $C^{\infty}$ , when it is $C^{k}$ for every $k \in N$ (Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ ).

[L6]

If $g$ is continuous at a point of its domain, then so is $∣ g ∣$ , the function $x \mapsto ∣ g (x) ∣$ (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).

[L7]

For reals $u \leq v$ , the closed bounded interval $[u, v]$ is compact (Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact).

Proof

technique · direct

1.1

Fix $x \in I$ . If $T_{n, a} f (x) \to f (x)$ , then $R_{n, a} f (x) = f (x) - T_{n, a} f (x) \to 0$ .

L1assume-hypalgebra

1.2

Conversely, if $R_{n, a} f (x) \to 0$ , then $T_{n, a} f (x) = f (x) - R_{n, a} f (x) \to f (x)$ .

L1assume-hypalgebra

1.3

Let $n \geq 0$ . Since $f \in C^{\infty} (I)$ , the derivative $f^{(n + 1)}$ exists and is continuous on $I$ , so $∣ f^{(n + 1)} ∣$ is continuous on $I$ ; and $[a - r, a + r]$ is a closed bounded interval, hence compact, and it is a nonempty subset of $I$ because $r > 0$ and $a$ belongs to it. Applying the extreme value theorem to $∣ f^{(n + 1)} ∣$ on $[a - r, a + r]$ therefore produces the displayed maximum $M_{n + 1}$ .

A1L2L5L6L7

1.4

For every $y \in [a - r, a + r]$ and every $n \geq 0$ , $∣ f (y) - T_{n, a} f (y) ∣ = ∣ R_{n, a} f (y) ∣ \leq M_{n + 1} ∣ y - a ∣^{n + 1} / (n + 1)! \leq M_{n + 1} r^{n + 1} / (n + 1)!$ .

A1L1L3

1.5

Given $ε > 0$ , choose $N$ such that $M_{n + 1} r^{n + 1} / (n + 1)! < ε$ whenever $n \geq N$ .

A1choose

2.1

Thus, for this arbitrary $x$ , the Taylor series sums to $f (x)$ if and only if $R_{n, a} f (x) \to 0$ .

step 1.1step 1.2

2.2

For every $n \geq N$ and every $y \in [a - r, a + r]$ , $∣ f (y) - T_{n, a} f (y) ∣ < ε$ .

step 1.4step 1.5

3.1

Hence $T_{n, a} f \to f$ uniformly on $[a - r, a + r]$ .

L4step 2.2∎

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31Open item page →

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

Statement

If a real power series centred at $c$ has radius $R > 0$ , then its sum is real analytic on $(c - R, c + R)$ , interpreted as all of $R$ when $R = + \infty$ .

Facts & Assumptions

Given: A power-series sum $f$ on its open radius interval.

[L1]

At every point $d$ strictly inside the radius, $f$ has a convergent re-expansion in powers of $x - d$ on a positive neighbourhood (A power-series sum may be re-expanded about every interior point, with coefficients given by its derivatives there).

[L2]

Real analyticity means precisely the existence of such a local power-series representation at every point (A real-analytic function on an open subset of $R$ is locally represented by a convergent real power series).

Proof

technique · direct

1.1

Fix $d$ in the open radius interval. Then $R - ∣ d - c ∣ > 0$ , and [L1] represents $f$ by a power series about $d$ whenever $∣ x - d ∣ < R - ∣ d - c ∣$ .

givenL1

2.1

The neighbourhood in step 1.1 lies inside the open radius interval, so [L2] applies at every $d$ and proves that $f$ is real analytic there.

step 1.1L2∎

CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31Open item page →

Every real-analytic function is infinitely differentiable

Statement

Every real-analytic function on an open subset $U \subseteq R$ is infinitely differentiable at every point of $U$ .

Facts & Assumptions

Given: A real-analytic function $f : U \to R$ .

[L1]

Near every $c \in U$ , $f$ equals a convergent power series centred at $c$ (A real-analytic function on an open subset of $R$ is locally represented by a convergent real power series).

[L2]

A power-series sum is infinitely differentiable inside its radius (A power-series sum is infinitely differentiable inside its radius and satisfies $a_{n} = f^{(n)} (c) / ι (n!)$ at its centre).

Proof

technique · direct

1.1

Fix $c \in U$ and choose the local representing power series supplied by [L1].

givenL1choose

2.1

By [L2], that series, hence $f$ , has derivatives of every order on a neighbourhood of $c$ . Since $c$ was arbitrary, $f$ is smooth on $U$ .

step 1.1L2∎

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31Open item page →

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

Statement

Let $f$ be real analytic near $c$ and suppose $f (c) = 0$ . Exactly one of the following local alternatives holds:

every coefficient in a power-series expansion of $f$ about $c$ is zero, so $f$ vanishes on a neighbourhood of $c$ ;
there is a least $m \geq 1$ with $f^{(m)} (c) \neq 0$ , and $c$ is an isolated zero of $f$ .

Facts & Assumptions

Given: A real-analytic $f$ (A real-analytic function on an open subset of $R$ is locally represented by a convergent real power series) with $f (c) = 0$ and a local expansion $f (x) = \sum_{n \geq 0} a_{n} (x - c)^{n}$ .

[L1]

The coefficients are $a_{n} = f^{(n)} (c) / ι (n!)$ (A power-series sum is infinitely differentiable inside its radius and satisfies $a_{n} = f^{(n)} (c) / ι (n!)$ at its centre).

[L2]

Every nonempty subset of $N$ has a least member (The well-ordering principle).

[L3]

Power-series sums are continuous inside their radius. If a function has a nonzero limit at a limit point, it is nonzero on a sufficiently small punctured neighbourhood of that point (The sum of a real power series is continuous at every point strictly inside its interval of convergence, If $\lim_{x \to c} f (x) = L \neq 0$ then $∣ f ∣ > ∣ L ∣ / 2$ on a punctured neighbourhood of $c$ ; in particular if $L > 0$ then $f > L / 2 > 0$ there).

[L4]

A power series converges absolutely at every point strictly inside its radius (A real power series converges absolutely inside its radius and diverges outside it, while either behaviour may occur at an endpoint).

Proof

technique · cases

1.1

If every $a_{n} = 0$ , the local expansion gives $f = 0$ throughout its neighbourhood.

assume-case allzerogiven

1.2

Otherwise, [L2] gives a least $m$ with $a_{m} \neq 0$ . Since $a_{0} = f (c) = 0$ , one has $m \geq 1$ .

assume-case nonzerogivenL2choose

2.1

In the second case, write $f (x) = (x - c)^{m} g (x)$ , where $g (x) : = \sum_{j \geq 0} a_{m + j} (x - c)^{j}$ . At every nonzero point strictly inside the original local radius, the absolute series for $g$ is the corresponding absolute tail for $f$ multiplied by $∣ x - c ∣^{- m}$ ; it also converges at $c$ . Thus $g$ has positive local radius and $g (c) = a_{m} \neq 0$ .

step 1.2L4algebra

3.1

The alternatives in steps 1.1 and 1.2 are exhaustive. In the second, $g$ is continuous at $c$ and therefore has limit $g (c) = a_{m} \neq 0$ there; [L3] makes $g$ nonzero on a smaller punctured neighbourhood, while it is already nonzero at $c$ . Hence $f (x) = 0$ there only when $x = c$ , and the coefficient formula [L1] translates the least nonzero coefficient into the stated least nonzero derivative.

step 1.1step 1.2step 2.1L1L3cases-exhaustive∎

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31Open item page →

Two real-analytic functions on an open interval that agree on a set with an accumulation point in that interval agree throughout the interval

Statement

Let $I \subseteq R$ be an open interval and let $f, g : I \to R$ be real analytic. If the agreement set ${x \in I : f (x) = g (x)}$ has an accumulation point $c$ lying inside $I$ , then $f = g$ throughout $I$ .

Facts & Assumptions

Given: The interval, functions, agreement set, and interior accumulation point in the statement.

[L1]

Subtracting local power-series representations shows directly that $h : = f - g$ is real analytic (A real-analytic function on an open subset of $R$ is locally represented by a convergent real power series).

[L2]

At a zero of a real-analytic function, the zero is isolated unless the function vanishes on a neighbourhood (At a zero of a real-analytic function, either some first nonzero coefficient makes the zero isolated or every local coefficient vanishes).

[L3]

Every interval is connected: it has no decomposition into two nonempty separated sets, where each set must avoid the closure of the other (A subset of $R$ is connected if and only if it is order-convex, that is, an interval, Separated sets, disconnection, and connected subset of $R$ ).

[L4]

Local power-series sums are continuous (The sum of a real power series is continuous at every point strictly inside its interval of convergence).

Proof

technique · direct

1.1

Put $h : = f - g$ . By [L1], $h$ is real analytic. The accumulating zeros and [L4] give $h (c) = 0$ , and this zero is not isolated; hence [L2] makes $h$ identically zero on a neighbourhood of $c$ .

givenL1L2L4

2.1

Let $V$ be the set of points of $I$ having a neighbourhood in $I$ on which $h$ vanishes. Step 1.1 makes $V$ nonempty, and its definition makes it relatively open.

step 1.1

3.1

The complement $I ∖ V$ is also relatively open. Indeed, if $h (x) \neq 0$ , continuity gives a neighbourhood containing no zero and hence no point of $V$ ; if $h (x) = 0$ but $x \notin V$ , [L2] makes $x$ an isolated zero, and a sufficiently small neighbourhood again contains no point of $V$ .

step 2.1L2L4

4.1

Steps 2.1 and 3.1 make $V$ and $I ∖ V$ separated: every point of either set has a real neighbourhood disjoint from the other, so neither set meets the closure of the other. If $I ∖ V$ were nonempty, they would therefore disconnect the connected interval $I$ , contrary to [L3]. Thus $V = I$ and $h = 0$ throughout $I$ , so $f = g$ .

step 2.1step 3.1L3∎

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31Open item page →

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

Statement

Suppose $f (x) = \sum_{n \geq 0} a_{n} (x - c)^{n}$ and $g (x) = \sum_{n \geq 0} b_{n} (x - c)^{n}$ have radii $R_{f}, R_{g}$ . For $∣ x - c ∣ < \min (R_{f}, R_{g})$ ,

$f (x) g (x) = \sum_{n = 0}^{\infty} (\sum_{k = 0}^{n} a_{k} b_{n - k}) (x - c)^{n},$

and the displayed product series converges absolutely.

Facts & Assumptions

Given: The two power series in the statement and a point in their common open radius.

[L1]

Both numerical series converge absolutely there (A real power series converges absolutely inside its radius and diverges outside it, while either behaviour may occur at an endpoint).

[L2]

The Cauchy product of two absolutely convergent series converges absolutely to the product of their sums (The Cauchy product of two series: $c_{n} = \sum_{k = 0}^{n} a_{k} b_{n - k}$ , If $\sum a_{k}$ and $\sum b_{k}$ both converge absolutely then their Cauchy product converges absolutely, with sum $A B$ ).

Proof

technique · direct

1.1

Apply [L2] to the numerical series with terms $a_{k} (x - c)^{k}$ and $b_{j} (x - c)^{j}$ , whose absolute convergence is [L1].

L1L2

2.1

Its $n$ th Cauchy-product term is $\sum_{k = 0}^{n} a_{k} b_{n - k} (x - c)^{n}$ , which gives the formula and absolute convergence.

step 1.1algebra∎

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31Open item page →

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

Statement

Let $F (y) = \sum_{m \geq 0} b_{m} (y - e)^{m}$ have positive radius $S$ , and let $G (x) - e = \sum_{n \geq 1} c_{n} (x - d)^{n}$ converge near $d$ . If some $r > 0$ satisfies

$B_{r} : = \sum_{n \geq 1} ∣ c_{n} ∣ r^{n} < S,$

then $F \circ G$ is represented for $∣ x - d ∣ < r$ by a convergent power series about $d$ , obtained by expanding and regrouping $\sum_{m} b_{m} (G (x) - e)^{m}$ .

Facts & Assumptions

Given: The outer and inner series and $r$ from the statement.

[L1]

The Cauchy product of two absolutely convergent series converges absolutely, and its absolute sum is at most the product of the two absolute sums (If $\sum a_{k}$ and $\sum b_{k}$ both converge absolutely then their Cauchy product converges absolutely, with sum $A B$ ).

[L2]

The outer series converges absolutely at every distance below $S$ (A real power series converges absolutely inside its radius and diverges outside it, while either behaviour may occur at an endpoint).

[L3]

An absolutely convergent multiple series may be regrouped (Fubini for double series: if $\sum_{i} \sum_{j} ∣ a_{i j} ∣$ converges then both iterated sums and the sum along every bijection $N \to N \times N$ converge to one and the same value).

Proof

technique · constructive

1.1

For each $m$ , repeatedly use [L1] to expand $(G (x) - e)^{m}$ in powers of $x - d$ ; take the zeroth power to be $1$ . For $∣ x - d ∣ \leq r$ , the inner numerical series is absolutely convergent with absolute sum at most $B_{r}$ , so the expanded $m$ th power has absolute term sum at most $B_{r}^{m}$ .

givenconstructL1

2.1

Consequently, for $∣ x - d ∣ \leq r$ , the sum of absolute values of all expanded terms with outer degree $m$ is at most $∣ b_{m} ∣ B_{r}^{m}$ . The series of these bounds converges because $B_{r} < S$ and [L2] applies.

step 1.1L2algebra

3.1

By [L3], regroup the absolutely convergent expansion by total powers of $x - d$ . The resulting power series converges on $∣ x - d ∣ < r$ and sums to $\sum_{m} b_{m} (G (x) - e)^{m} = F (G (x))$ .

step 1.1step 2.1L3discharge-construct∎

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31Open item page →

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

Statement

Let $f (x) = \sum_{n \geq 0} a_{n} (x - c)^{n}$ have positive radius and $a_{0} \neq 0$ . Then on some neighbourhood of $c$ , $1 / f$ is represented by a convergent real power series about $c$ .

Facts & Assumptions

Given: The convergent power series $f$ with $f (c) = a_{0} \neq 0$ .

[L1]

For $∣ z ∣ < 1$ , $\sum_{m \geq 0} (- z)^{m} = 1 / (1 + z)$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges).

[L2]

A power series converges absolutely inside its radius, and its sum is continuous there (A real power series converges absolutely inside its radius and diverges outside it, while either behaviour may occur at an endpoint, The sum of a real power series is continuous at every point strictly inside its interval of convergence).

[L3]

Finite powers of a power series are represented by repeated Cauchy products (Inside the common radius the product of two power-series sums is represented by the Cauchy product of their coefficients).

[L4]

Absolutely convergent double series may be regrouped without changing their sum (Fubini for double series: if $\sum_{i} \sum_{j} ∣ a_{i j} ∣$ converges then both iterated sums and the sum along every bijection $N \to N \times N$ converge to one and the same value).

Proof

technique · constructive

1.1

Write $f = a_{0} + h$ , where $h (c) = 0$ . By absolute convergence, choose $r > 0$ inside the radius so small that $B_{r} : = \sum_{n \geq 1} ∣ a_{n} ∣ r^{n} < ∣ a_{0} ∣$ .

constructL2choose

2.1

By [L1], $1 / f (x) = a_{0}^{- 1} \sum_{m \geq 0} (- h (x) / a_{0})^{m}$ for $∣ x - c ∣ \leq r$ . Expand each power by [L3].

step 1.1L1L3

3.1

The total absolute sum of the expanded terms is bounded by $∣ a_{0} ∣^{- 1} \sum_{m} (B_{r} / ∣ a_{0} ∣)^{m} < \infty$ . By [L4], regrouping by powers of $x - c$ gives a convergent reciprocal power series on the neighbourhood.

step 1.1step 2.1L1L4discharge-construct∎

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31Open item page →

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

Statement

On open real domains, sums and products of real-analytic functions are real analytic. If $g$ is nonzero throughout the domain, then $f / g$ is real analytic. If $g : U \to V$ and $f : V \to R$ are real analytic, then $f \circ g$ is real analytic on $U$ .

Facts & Assumptions

Given: Real-analytic functions with compatible domains as in the statement.

[L1]

Each function has a convergent local power-series representation at every point (A real-analytic function on an open subset of $R$ is locally represented by a convergent real power series).

[L2]

Products are represented by Cauchy products, local reciprocals exist when the constant term is nonzero, and local compositions have convergent expansions (Inside the common radius the product of two power-series sums is represented by the Cauchy product of their coefficients, A convergent real power series with nonzero constant term has a convergent reciprocal power series on a smaller neighbourhood, 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).

Proof

technique · cases

1.1

For sums and products, fix a point and choose local series for the functions by [L1]. Termwise addition gives a convergent series for the sum, while [L2] gives one for the product.

assume-case algebraL1L2

1.2

For a quotient, the denominator is nonzero at the point, so its local series has nonzero constant term. By [L2] it has a local reciprocal series, whose Cauchy product with the numerator series represents the quotient.

assume-case quotientL1L2

1.3

For a composition, centre the outer series at the inner value. The inner series then has zero constant term, and absolute convergence lets one shrink the radius until the sum of the absolute values of its nonconstant terms is smaller than the outer radius. The composition lemma in [L2] then supplies a local series.

assume-case compositionL1L2

2.1

The cases in steps 1.1--1.3 are precisely the operations in the statement. Each construction works at every point of the relevant open domain, so the definition [L1] proves all assertions.

step 1.1step 1.2step 1.3L1cases-exhaustive∎

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-07-31Open item page →

Abel summability by $\lim_{x ↑ 1} \sum a_{n} x^{n}$ and Cesaro summability by the Cesaro means of the partial sums

Definition

For a real series $\sum_{n \geq 0} a_{n}$ , write its inclusive partial sums as

$S_{n} : = \sum_{k = 0}^{n} a_{k}$

and their Cesaro means as

$σ_{n} : = \frac{1}{ι (n + 1)} \sum_{k = 0}^{n} S_{k} .$

The series is Cesaro summable to $s$ if $σ_{n} \to s$ (The Cesaro means $σ_{n} = (x_{0} + \dots + x_{n}) / (n + 1)$ and $(C, 1)$ -summability).

It is Abel summable to $s$ if the power series

$A (x) : = \sum_{n = 0}^{\infty} a_{n} x^{n}$

converges for every $0 \leq x < 1$ and $\lim_{x ↑ 1} A (x) = s$ in the one-sided sense of The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ . These are summability methods for the zero-indexed series of Series, partial sums, convergence and the sum, divergence, and the tail series; they do not assert ordinary convergence.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-07-31Open item page →

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

Statement

If the real series $\sum_{n \geq 0} a_{n}$ converges ordinarily to $s$ , then it is Abel summable to $s$ :

$\lim_{x ↑ 1} \sum_{n = 0}^{\infty} a_{n} x^{n} = s .$

Facts & Assumptions

Given: Inclusive partial sums $S_{n} : = \sum_{k = 0}^{n} a_{k}$ with $S_{n} \to s$ .

[L1]

Finite Abel summation gives $\sum_{k = 0}^{N} a_{k} x^{k} = S_{N} x^{N} + (1 - x) \sum_{k = 0}^{N - 1} S_{k} x^{k}$ (Abel summation by parts: with $A_{n} = \sum_{k < n} a_{k}$ one has $\sum_{k < n} a_{k} b_{k} = A_{n} b_{n - 1} - \sum_{k < n - 1} A_{k + 1} (b_{k + 1} - b_{k})$ for every $n \geq 1$ ).

[L2]

A convergent sequence is bounded (Every convergent sequence is bounded).

[L3]

$\sum_{n \geq 0} x^{n} = 1 / (1 - x)$ for $0 \leq x < 1$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges).

[L4]

A nonnegative series dominated termwise by a convergent nonnegative series converges (If $0 \leq a_{k} \leq b_{k}$ eventually, convergence of $\sum b_{k}$ gives convergence of $\sum a_{k}$ , and divergence of $\sum a_{k}$ gives divergence of $\sum b_{k}$ ).

Proof

technique · direct

1.1

By [L2], choose $M$ with $∣ S_{n} ∣ \leq M$ for every $n$ . For fixed $0 \leq x < 1$ , one has $∣ S_{n} x^{n} ∣ \leq M x^{n}$ , so [L3] and [L4] give absolute convergence of $\sum_{n} S_{n} x^{n}$ ; the same bound gives $S_{N} x^{N} \to 0$ .

L2L3L4choose

2.1

Apply [L1] and let $N \to \infty$ . Step 1.1 gives convergence of the Abel series and $A (x) = (1 - x) \sum_{n \geq 0} S_{n} x^{n}$ . Subtracting $s = (1 - x) \sum_{n \geq 0} s x^{n}$ gives $A (x) - s = (1 - x) \sum_{n \geq 0} (S_{n} - s) x^{n}$ .

step 1.1L1L3

3.1

Given $ε > 0$ , choose $N$ so that $∣ S_{n} - s ∣ < ε$ for $n \geq N$ . The tail of step 2.1 has absolute value at most $ε (1 - x) \sum_{n \geq N} x^{n} \leq ε$ .

givenstep 2.1L3choose

4.1

The finite head $(1 - x) \sum_{n < N} (S_{n} - s) x^{n}$ tends to $0$ as $x ↑ 1$ . Thus $∣ A (x) - s ∣ < 2 ε$ for all sufficiently large $x < 1$ , proving the asserted one-sided limit and Abel summability.

step 2.1step 3.1∎

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-07-31Open item page →

For $0 < x < 1$ , the Abel transform of a series is $(1 - x)^{2} \sum_{n \geq 0} (n + 1) σ_{n} x^{n}$ , where $σ_{n}$ are the Cesaro means of its partial sums

Statement

Let $S_{n} : = \sum_{k = 0}^{n} a_{k}$ and $σ_{n} : = ι (n + 1)^{- 1} \sum_{k = 0}^{n} S_{k}$ . If $(σ_{n})$ is bounded, then for every $0 < x < 1$ the Abel series converges and

$\sum_{n = 0}^{\infty} a_{n} x^{n} = (1 - x)^{2} \sum_{n = 0}^{\infty} ι (n + 1) σ_{n} x^{n} .$

Facts & Assumptions

Given: The coefficients, partial sums, and Cesaro means in the statement.

[L1]

The canonical natural $ι (n + 1)$ is positive. Thus, putting $T_{n} : = \sum_{k = 0}^{n} S_{k}$ , the definition of $σ_{n}$ gives $T_{n} = ι (n + 1) σ_{n}$ . Also $S_{n} = T_{n} - T_{n - 1}$ with $T_{- 1} : = 0$ ; putting $S_{- 1} : = 0$ gives $a_{n} = S_{n} - S_{n - 1}$ for every $n \geq 0$ (Abel summability by $\lim_{x ↑ 1} \sum a_{n} x^{n}$ and Cesaro summability by the Cesaro means of the partial sums, Finite sums and finite products, by recursion, The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Canonical naturals are positive and strictly increasing).

[L2]

For $0 < x < 1$ , the geometric series is absolutely convergent because its terms are nonnegative. Its Cauchy product with itself has coefficient $\sum_{k = 0}^{n} x^{k} x^{n - k} = ι (n + 1) x^{n}$ and sum $1 / (1 - x)^{2}$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges, Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ , Basic properties of the absolute value, The Cauchy product of two series: $c_{n} = \sum_{k = 0}^{n} a_{k} b_{n - k}$ , If $\sum a_{k}$ and $\sum b_{k}$ both converge absolutely then their Cauchy product converges absolutely, with sum $A B$ , Finite sums and finite products, by recursion, The canonical natural $ι (n) = n \cdot 1_{F}$ of a field).

[L3]

Convergent real series may be added, subtracted and scaled term by term (Convergent series add and scale termwise).

[L4]

Proof

technique · direct

1.1

Choose $M \geq 0$ with $∣ σ_{n} ∣ \leq M$ for every $n$ . Then $∣ T_{n} x^{n} ∣ \leq M ι (n + 1) x^{n}$ ; [L2] and [L3] give convergence of the majorant series, so [L4] gives absolute convergence of $\sum_{n} T_{n} x^{n}$ .

L1L2L3L4choose

2.1

Since $S_{n} = T_{n} - T_{n - 1}$ , step 1.1 gives absolute convergence of $\sum_{n} S_{n} x^{n}$ . With $T_{- 1} = 0$ , the shifted series satisfies $\sum_{n \geq 0} T_{n - 1} x^{n} = x \sum_{n \geq 0} T_{n} x^{n}$ ; combining the two convergent series by [L3] gives $\sum_{n \geq 0} S_{n} x^{n} = (1 - x) \sum_{n \geq 0} T_{n} x^{n}$ .

step 1.1L1L3algebra

3.1

Since $a_{n} = S_{n} - S_{n - 1}$ with $S_{- 1} = 0$ , step 2.1 likewise gives absolute convergence and $\sum_{n} a_{n} x^{n} = (1 - x) \sum_{n} S_{n} x^{n}$ . Substitute step 2.1 and $T_{n} = ι (n + 1) σ_{n}$ to get the formula.

step 2.1L1L3∎

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31Open item page →

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

Statement

If a real series is Cesaro summable to $s$ , then it is Abel summable to $s$ .

Facts & Assumptions

Given: Cesaro means $σ_{n} \to s$ for the partial sums of $\sum a_{n}$ .

[L1]

If $(σ_{n})$ is bounded, the Abel series converges for $0 < x < 1$ and its transform is $A (x) = (1 - x)^{2} \sum_{n \geq 0} ι (n + 1) σ_{n} x^{n}$ (For $0 < x < 1$ , the Abel transform of a series is $(1 - x)^{2} \sum_{n \geq 0} (n + 1) σ_{n} x^{n}$ , where $σ_{n}$ are the Cesaro means of its partial sums).

[L2]

The nonnegative weights $w_{n} (x) : = (1 - x)^{2} ι (n + 1) x^{n}$ sum to $1$ for $0 < x < 1$ . Indeed, apply the transform in [L1] to the series with coefficients $1, 0, 0, \dots$ , whose partial sums and Cesaro means are all $1$ (For $0 < x < 1$ , the Abel transform of a series is $(1 - x)^{2} \sum_{n \geq 0} (n + 1) σ_{n} x^{n}$ , where $σ_{n}$ are the Cesaro means of its partial sums).

[L3]

Abel summability to $s$ means that the Abel series converges on $0 \leq x < 1$ and tends to $s$ as $x ↑ 1$ (Abel summability by $\lim_{x ↑ 1} \sum a_{n} x^{n}$ and Cesaro summability by the Cesaro means of the partial sums).

Proof

technique · direct

1.1

Since $(σ_{n})$ converges, it is bounded, so [L1] applies and $A (x) - s = \sum_{n \geq 0} w_{n} (x) (σ_{n} - s)$ .

givenL1L2

2.1

Given $ε > 0$ , choose $N$ with $∣ σ_{n} - s ∣ < ε$ for $n \geq N$ . The corresponding tail is at most $ε \sum_{n \geq N} w_{n} (x) \leq ε$ .

step 1.1L2choose

3.1

For each fixed $n$ , $w_{n} (x) \to 0$ as $x ↑ 1$ , so the finite head tends to $0$ . Together with step 2.1 this gives $A (x) \to s$ , which is Abel summability by definition.

step 1.1step 2.1L2L3∎

CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31Open item page →

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

Statement

If $\sum_{n \geq 0} a_{n}$ converges ordinarily to $s$ , then it is both Cesaro summable and Abel summable to $s$ .

Facts & Assumptions

Given: Partial sums $S_{n} \to s$ .

[L1]

The Cesaro means of a convergent sequence converge to the same limit (If $x_{k} \to L$ then $σ_{n} \to L$ : convergence implies $(C, 1)$ -summability to the same value).

[L2]

Abel's limit theorem sends an ordinarily convergent series to its ordinary sum (Abel's limit theorem: if a real series converges to $s$ , then its power series tends to $s$ as $x ↑ 1$ ).

Proof

technique · direct

1.1

Apply [L1] to $(S_{n})$ to obtain $σ_{n} \to s$ , which is Cesaro summability.

givenL1

2.1

Apply [L2] to the original series to obtain Abel summability to $s$ .

givenL2∎

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-07-31Open item page →

If $ι (n + 1) a_{n} \to 0$ , short multiplicative blocks of the coefficients have uniformly small sums

Statement

Suppose $ι (n + 1) a_{n} \to 0$ . For every $ε > 0$ there is $N_{0}$ such that, whenever $q \geq p \geq N_{0}$ ,

$\sum_{n = p}^{q} ∣ a_{n} ∣ \leq ε \frac{ι (q - p + 1)}{ι (p + 1)} .$

Moreover, for $N \geq N_{0}$ and $x_{N} : = 1 - 1 / ι (N + 1)$ ,

$\sum_{n = N_{0}}^{N} ∣ a_{n} ∣ (1 - x_{N}^{n}) \leq ε, \sum_{n > N} ∣ a_{n} ∣ x_{N}^{n} \leq ε .$

Facts & Assumptions

Given: The Tauber condition $ι (n + 1) a_{n} \to 0$ .

[L1]

The canonical naturals $ι (n + 1)$ are positive and strictly increasing, positive reciprocals reverse order, and $∣ u v ∣ = ∣ u ∣ ∣ v ∣$ (Canonical naturals are positive and strictly increasing, Inverses of positives are positive, and reciprocation reverses order, Basic properties of the absolute value).

[L2]

Real-sequence convergence is tested with positive rational tolerances, and below every positive real lies a positive rational (Limits and Cauchy sequences of reals, The rationals embed densely in the reals).

[L3]

For $0 \leq x \leq 1$ , multiplying out the finite sum gives $1 - x^{n} = (1 - x) \sum_{k = 0}^{n - 1} x^{k} \leq ι (n) (1 - x)$ .

[L4]

For $0 \leq x < 1$ , the geometric-series formula gives $\sum_{n > N} x^{n} = x^{N + 1} / (1 - x)$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges).

Proof

technique · direct

1.1

Choose a positive rational $δ < ε$ . By the limit hypothesis and [L2], choose $N_{0}$ so that $∣ ι (n + 1) a_{n} ∣ < δ$ for $n \geq N_{0}$ . Positivity and multiplicativity in [L1] give $∣ a_{n} ∣ < δ / ι (n + 1) < ε / ι (n + 1)$ there. Since $1 / ι (n + 1) \leq 1 / ι (p + 1)$ on $p \leq n \leq q$ , summing proves the block estimate.

L1L2choosealgebra

2.1

For $N_{0} \leq n \leq N$ , [L3] gives $∣ a_{n} ∣ (1 - x_{N}^{n}) \leq ε (1 - x_{N})$ . There are at most $N + 1$ terms and $ι (N + 1) (1 - x_{N}) = 1$ , proving the first weighted estimate.

step 1.1L3algebra

3.1

For $n > N$ , step 1.1 gives $∣ a_{n} ∣ \leq ε / ι (N + 2)$ . Summing the geometric tail yields $\sum_{n > N} ∣ a_{n} ∣ x_{N}^{n} \leq ε x_{N}^{N + 1} ι (N + 1) / ι (N + 2) \leq ε$ .

step 1.1L4algebra∎

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31Open item page →

Tauber's theorem: an Abel-summable series with $ι (n + 1) a_{n} \to 0$ converges ordinarily to its Abel sum

Statement

Let $\sum_{n \geq 0} a_{n}$ be Abel summable to $s$ . If

$ι (n + 1) a_{n} ⟶ 0,$

then its ordinary partial sums converge to $s$ .

Facts & Assumptions

Given: The Abel sum $A (x) : = \sum_{n \geq 0} a_{n} x^{n} \to s$ as $x ↑ 1$ and the stated Tauber condition.

[L1]

The block lemma supplies uniform bounds for the weighted middle and tail when $x_{N} : = 1 - 1 / ι (N + 1)$ (If $ι (n + 1) a_{n} \to 0$ , short multiplicative blocks of the coefficients have uniformly small sums).

[L2]

The Archimedean reciprocal property gives a reciprocal below every positive tolerance. Canonical naturals increase and reciprocation reverses positive order, so every later reciprocal remains below that tolerance; hence $1 / ι (N + 1) \to 0$ and $x_{N} ↑ 1$ . Abel summability then gives $A (x_{N}) \to s$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , Canonical naturals are positive and strictly increasing, Inverses of positives are positive, and reciprocation reverses order, Abel summability by $\lim_{x ↑ 1} \sum a_{n} x^{n}$ and Cesaro summability by the Cesaro means of the partial sums, Limits and Cauchy sequences of reals).

Proof

technique · direct

1.1

Write $S_{N} : = \sum_{n = 0}^{N} a_{n}$ . For $N \geq 1$ , one has $S_{N} - A (x_{N}) = \sum_{n = 0}^{N} a_{n} (1 - x_{N}^{n}) - \sum_{n > N} a_{n} x_{N}^{n}$ .

givenalgebra

2.1

Given $ε > 0$ , choose $N_{0}$ from [L1]. The part of the first sum with $n < N_{0}$ tends to $0$ because it is finite and $x_{N} \to 1$ ; the remaining part and the tail have absolute value at most $ε$ each by [L1].

step 1.1L1choose

3.1

Hence $S_{N} - A (x_{N}) \to 0$ . Since $A (x_{N}) \to s$ by [L2], it follows that $S_{N} \to s$ .

step 2.1L2∎

5 · Examples, counterexamples and false statements

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-07-31Open item page →

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

Statement

False claim: every real power series converges uniformly on its entire open interval of convergence.

Facts & Assumptions

Given: The geometric power series $\sum_{n \geq 0} x^{n}$ on $(- 1, 1)$ .

[L1]

It converges pointwise there to $1 / (1 - x)$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges).

[L2]

A sequence of real-valued functions converges uniformly if and only if it is uniformly Cauchy (A sequence of real-valued functions converges uniformly if and only if it is uniformly Cauchy).

Refutation

technique · direct

1.1

For every $N$ , the difference between the $(N + 1)$ st and $N$ th partial sums is $x^{N}$ . Its supremum over $x \in (- 1, 1)$ is $1$ .

givenalgebra

2.1

Thus the partial sums are not uniformly Cauchy and cannot converge uniformly by [L2], despite pointwise convergence on the entire open radius interval by [L1].

step 1.1L1L2∎

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-07-31Open item page →

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

Statement

False claim: if a power series converges at one point distinct from its centre, then it converges at every real point.

Facts & Assumptions

Given: The geometric power series $\sum_{n \geq 0} x^{n}$ centred at $0$ .

[L1]

The geometric series converges when $∣ x ∣ < 1$ and diverges when $∣ x ∣ \geq 1$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges).

Refutation

technique · direct

1.1

At $x = 1 / 2 \neq 0$ , the series converges by [L1]. At $x = 2$ , its terms do not tend to zero and it diverges.

2.1

This single power series satisfies the premise and fails the conclusion, refuting the claim.

step 1.1∎

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-07-31Open item page →

FALSE: Abel summability alone implies ordinary convergence of a series

Statement

False claim: every Abel-summable real series converges ordinarily.

Facts & Assumptions

Given: Grandi's series $\sum_{n \geq 0} (- 1)^{n}$ .

[L1]

For $0 \leq x < 1$ , the geometric series gives $\sum_{n \geq 0} (- 1)^{n} x^{n} = 1 / (1 + x)$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges).

[L2]

Ordinary convergence means convergence of the partial-sum sequence, whereas Abel summability uses the boundary limit of the power series (Series, partial sums, convergence and the sum, divergence, and the tail series, Abel summability by $\lim_{x ↑ 1} \sum a_{n} x^{n}$ and Cesaro summability by the Cesaro means of the partial sums).

Refutation

technique · direct

1.1

By [L1], the Abel transform tends to $1 / 2$ as $x ↑ 1$ , so the series is Abel summable to $1 / 2$ .

L1L2

2.1

Its inclusive partial sums alternate between $1$ and $0$ , so they do not converge. Hence Abel summability alone does not imply ordinary convergence.

givenL2∎

Power Series and Real-Analytic Functions

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

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

Definition

Remarks

Cauchy–Hadamard: the reciprocal radius is lim sup⁡k→∞∣ak+1∣1/(k+1)limsupk→∞​∣ak+1​∣1/(k+1), with the zero and infinite cases included

Statement

Facts & Assumptions

Proof

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

Statement

Facts & Assumptions

Proof

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

Statement

Facts & Assumptions

Proof

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

Statement

Facts & Assumptions

Proof

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

Statement

Facts & Assumptions

Proof

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

Statement

Facts & Assumptions

Proof

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

Statement

Facts & Assumptions

Proof

A power-series sum is infinitely differentiable inside its radius and satisfies an=f(n)(c)/ι(n!)an​=f(n)(c)/ι(n!) at its centre

Statement

Facts & Assumptions

Proof

Taylor and Maclaurin series

Definition

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

Statement

Facts & Assumptions

Proof

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

Statement

Facts & Assumptions

Proof

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

Definition

Taylor-series representation by vanishing remainders

Statement

Facts & Assumptions

Proof

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

Statement

Facts & Assumptions

Proof

Every real-analytic function is infinitely differentiable

Statement

Facts & Assumptions

Proof

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

Statement

Facts & Assumptions

Proof

Two real-analytic functions on an open interval that agree on a set with an accumulation point in that interval agree throughout the interval

Statement

Facts & Assumptions

Proof

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

Statement

Facts & Assumptions

Proof

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

Statement

Facts & Assumptions

Proof

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

Cauchy–Hadamard: the reciprocal radius is ${lim sup}_{k \to \infty} ∣ a_{k + 1} ∣^{1 / (k + 1)}$ , with the zero and infinite cases included

A power-series sum is infinitely differentiable inside its radius and satisfies $a_{n} = f^{(n)} (c) / ι (n!)$ at its centre

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

Abel summability by $\lim_{x ↑ 1} \sum a_{n} x^{n}$ and Cesaro summability by the Cesaro means of the partial sums

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

For $0 < x < 1$ , the Abel transform of a series is $(1 - x)^{2} \sum_{n \geq 0} (n + 1) σ_{n} x^{n}$ , where $σ_{n}$ are the Cesaro means of its partial sums

If $ι (n + 1) a_{n} \to 0$ , short multiplicative blocks of the coefficients have uniformly small sums

Tauber's theorem: an Abel-summable series with $ι (n + 1) a_{n} \to 0$ converges ordinarily to its Abel sum