TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-01

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's Schlömilch–Roche remainder formula

Statement

Let $n\in\mathbb N$ , let $a<x$ , and suppose $f$ has derivatives through order $n+1$ on $[a,x]$ , with the usual endpoint continuity. For every natural $p$ with $1\le p\le n+1$ , some $\xi\in(a,x)$ satisfies $R_{n,a}f(x)=\frac{f^{(n+1)}(\xi)}{\iota(p)\,\iota(n!)}(x-\xi)^{n+1-p}(x-a)^p.$ The reflected formula holds when $x<a$ .

Facts & Assumptions

Given: $f,a,x,n,p$ as stated.

[L1]

The Taylor polynomial and remainder are those of Taylor polynomials and their remainders, with coefficient identities from Taylor polynomials match the prescribed derivatives at the centre.

[L2]

The Cauchy mean-value quotient form is Cauchy's mean-value theorem in quotient form when the denominator derivative is nonzero.

[L3]

Finite-sum differentiation is licensed by Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$ , $(\alpha f)'(c) = \alpha f'(c)$ , $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$ , and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$ , For a natural $n \ge 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $\iota(n)\,x^{\,n-1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \ge 1$ the function $x \mapsto x^{-n}$ is differentiable at every $x \ne 0$ with derivative $-\iota(n)\,x^{-n-1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, and Laws of finite sums and finite products.

[L4]

If $p\ge1$ , then the canonical real $\iota(p)$ is positive and nonzero (The canonical natural $\iota(n) = n \cdot 1_F$ of a field, Canonical naturals are positive and strictly increasing).

Proof

technique · direct

1.1

Define $\Phi(t):=f(x)-\sum_{j=0}^{n}f^{(j)}(t)(x-t)^j/\iota(j!)$ and $\Psi(t):=(x-t)^p$ . Telescoping after differentiating the sum gives $\Phi'(t)=-f^{(n+1)}(t)(x-t)^n/\iota(n!)$ , while $\Psi'(t)=-\iota(p)(x-t)^{p-1}$ .

L1L3algebra

1.2

We have $\Phi(a)=R_{n,a}f(x)$ , $\Phi(x)=0$ , $\Psi(a)=(x-a)^p$ , and $\Psi(x)=0$ . Also $\Psi'\ne0$ on $(a,x)$ , because $p\ge1$ , $\iota(p)>0$ , and $x-t>0$ .

givenL1L4algebra

2.1

Apply [L2] to $\Phi,\Psi$ . For some $\xi\in(a,x)$ , $\Phi(a)/\Psi(a)=\Phi'(\xi)/\Psi'(\xi)=f^{(n+1)}(\xi)(x-\xi)^{n+1-p}/(\iota(p)\iota(n!))$ .

step 1.1step 1.2L2

3.1

Multiply by $(x-a)^p$ . If $x<a$ , interchange the interval endpoints; the same algebraic identity results.

step 2.1algebra∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 100 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 OpenCourseWare 18.100B Real Analysis, Spring 2025 lecture notes (standard reference, not scraped)
MathWorld, Schlömilch's remainder (standard reference, not scraped)