CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-07-31

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.

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

Statement

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

$G(x):=\sum_{n=0}^{\infty}\frac{a_n}{\iota(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)\,dx=G(v)-G(u)=\sum_{n=0}^{\infty}\frac{a_n}{\iota(n+1)}\bigl((v-c)^{n+1}-(u-c)^{n+1}\bigr).$

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)\,dt$ . 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∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 121 results over 23 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)