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

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.

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∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

54 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

W. F. Trench, Introduction to Real Analysis, §4.5, pp. 265–266 (standard reference, not scraped)
J. K. Hunter, An Introduction to Real Analysis, §10.7.1 (standard reference, not scraped)